diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp
index e7ca7e3781..bc863a3b89 100644
--- a/CASC/PortfolioMode.cpp
+++ b/CASC/PortfolioMode.cpp
@@ -394,6 +394,9 @@ void PortfolioMode::getSchedules(Property& prop, Schedule& quick, Schedule& fall
   case Options::Schedule::LTB_DEFAULT_2017:
     Schedules::getLtb2017DefaultSchedule(prop,quick);
     break;
+  case Options::Schedule::RAPID:
+    Schedules::getRapidSchedule(prop,quick);
+    break;
   default:
     INVALID_OPERATION("Unknown schedule");
   }
diff --git a/CASC/Schedules.cpp b/CASC/Schedules.cpp
index a466411d7a..3fb3edc5b7 100644
--- a/CASC/Schedules.cpp
+++ b/CASC/Schedules.cpp
@@ -14755,3 +14755,69 @@ void Schedules::getLtb2017DefaultSchedule(const Property& property, Schedule& sc
   sched.push("lrs+11_3:1_bsr=unit_only:br=off:cond=on:ep=RST:fsr=off:gs=on:gsaa=from_current:gsem=off:nwc=3:stl=300:sd=2:ss=axioms:st=2.0:sac=on:add=large:afr=on:afp=100000:afq=1.4:amm=sco:anc=none:sp=reverse_arity:urr=on_60"); // MZR 30 (3)
   sched.push("lrs+1003_4_bsr=unit_only:cond=fast:fsr=off:gsp=input_only:gs=on:gsaa=from_current:nm=0:nwc=1:stl=300:sos=on:sac=on:add=large:afp=10000:afq=1.1:anc=none:urr=ec_only:uhcvi=on_60"); // HLL 50 (1)
 }
+
+void Schedules::getRapidSchedule(const Shell::Property& property, Schedule& sched) {
+  property.getSMTLIBLogic();
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=off_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=off_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_10");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_10");
+
+
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=off:plsq=off_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8:thsqr=20,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=30,1:plsq=off_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=off:plsq=off_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=5,5,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=10,10,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=20,20,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=on:plsqc=1,2:plsqr=1,1,1_300");
+  sched.push("lrs+1010_1_nwc=2:newcnf=on:thsq=on:bs=on:bsr=on:av=off:urr=on:lls=on:fsd=on:bsd=on:tha=on:thsqc=0,8,16,24:thsqr=20,10,10,10,1:slsq=on:slsqc=0:slsqr=1,1:plsq=off_300");
+}
diff --git a/CASC/Schedules.hpp b/CASC/Schedules.hpp
index 2b437627ab..24e5757d9a 100644
--- a/CASC/Schedules.hpp
+++ b/CASC/Schedules.hpp
@@ -75,6 +75,8 @@ class Schedules
   static void getLtb2014Schedule(const Shell::Property& property, Schedule& sched);
   static void getLtb2014MzrSchedule(const Shell::Property& property, Schedule& quick, Schedule& fallback);
   static void getLtb2017DefaultSchedule(const Shell::Property& property, Schedule& sched);
+
+  static void getRapidSchedule(const Shell::Property& property, Schedule& quick);
 };
 
 
diff --git a/Inferences/TermAlgebraReasoning.cpp b/Inferences/TermAlgebraReasoning.cpp
index 7dc3ced6bc..fa514f5c0a 100644
--- a/Inferences/TermAlgebraReasoning.cpp
+++ b/Inferences/TermAlgebraReasoning.cpp
@@ -26,6 +26,7 @@
 #include "Kernel/SortHelper.hpp"
 #include "Kernel/SubstHelper.hpp"
 #include "Kernel/Substitution.hpp"
+#include "Kernel/TermIterators.hpp"
 
 #include "Lib/Environment.hpp"
 #include "Lib/Metaiterators.hpp"
@@ -575,5 +576,41 @@ namespace Inferences {
     auto it3 = getFlattenedIterator(it2);
     return pvi(it3);
   }
+
+  Clause* TwoSuccessorsISE::simplify(Clause* c)
+  {
+    CALL("TwoSuccessorsISE::simplify");
+
+    auto natTA = env.signature->getNat();
+    auto zero = natTA->getZeroConstructor()->functor();
+    auto succ = natTA->getSuccConstructor()->functor();
+
+    int length = c->length();
+    for (int i = 0; i < length; i++)
+    {
+      Literal *lit = (*c)[i];
+      NonVariableIterator nvi(lit);
+      while (nvi.hasNext()) {
+        TermList tl = nvi.next();
+        ASS(tl.isTerm());
+        auto t1 = tl.term();
+        if (t1->functor() == succ && t1->nthArgument(0)->isTerm())
+        {
+          auto t2 = t1->nthArgument(0)->term();
+          if (t2->functor() == succ) {
+            // found an occurence s(s(...)), so remove clause
+            return 0;
+          }
+          else if (t2->functor() == zero) {
+            // found an occurence s(0), so remove clause
+            return 0;
+          }
+        }
+      }
+    }
+
+    // no occurences s(s(...)) found, so keep clause
+    return c;
+  }
  
 }
diff --git a/Inferences/TermAlgebraReasoning.hpp b/Inferences/TermAlgebraReasoning.hpp
index 5ca2674814..023590de3f 100644
--- a/Inferences/TermAlgebraReasoning.hpp
+++ b/Inferences/TermAlgebraReasoning.hpp
@@ -150,7 +150,20 @@ class AcyclicityGIE1
   struct LiteralIterator;
   struct SubtermDisequalityIterator;
 };
+
+// hack: deletion rule which removes each clause containing at least one term of either the form s(s(...)) or the form s(0).
+class TwoSuccessorsISE
+  : public ImmediateSimplificationEngine
+{
+
+public:
+  CLASS_NAME(TwoSuccessorsISE);
+  USE_ALLOCATOR(TwoSuccessorsISE);
   
+  Kernel::Clause* simplify(Kernel::Clause* c);
+};
+
+
 };
 
 #endif
diff --git a/Kernel/BestLiteralSelector.hpp b/Kernel/BestLiteralSelector.hpp
index 827786fbac..20d4818eed 100644
--- a/Kernel/BestLiteralSelector.hpp
+++ b/Kernel/BestLiteralSelector.hpp
@@ -96,6 +96,8 @@ class BestLiteralSelector
     ensureSomeColoredSelected(c, eligible);
     ASS_EQ(c->numSelected(), 1); //if there is colored, it should be selected by the QComparator
 #endif
+
+    ensureNonLemmaPredicateSelected(c, eligible);
   }
 
       private:
@@ -237,6 +239,7 @@ class CompleteBestLiteralSelector
     LiteralList::destroy(maximals);
 
     ensureSomeColoredSelected(c, eligible);
+    ensureNonLemmaPredicateSelected(c, eligible);
   }
 
 private:
diff --git a/Kernel/ELiteralSelector.cpp b/Kernel/ELiteralSelector.cpp
index f421f09220..ea5a4d48d5 100644
--- a/Kernel/ELiteralSelector.cpp
+++ b/Kernel/ELiteralSelector.cpp
@@ -186,4 +186,5 @@ void ELiteralSelector::doSelection(Clause* c, unsigned eligible)
   c->setSelected(selCnt);
 
   ensureSomeColoredSelected(c, eligible);
+  ensureNonLemmaPredicateSelected(c, eligible);
 }
diff --git a/Kernel/LiteralSelector.cpp b/Kernel/LiteralSelector.cpp
index b2faace3be..8d23e07d77 100644
--- a/Kernel/LiteralSelector.cpp
+++ b/Kernel/LiteralSelector.cpp
@@ -207,6 +207,39 @@ void LiteralSelector::ensureSomeColoredSelected(Clause* c, unsigned eligible)
       c->splits());             // .. unless the color comes from the propositional part
 }
 
+// hack: make sure that at least one non-lemma-predicate is selected
+void LiteralSelector::ensureNonLemmaPredicateSelected(Clause* c, unsigned eligible)
+{
+  CALL("LiteralSelector::ensureNonLemmaPredicateSelected");
+
+  if (!env.options->useLemmaPredicateLiteralSelection())
+  {
+    return;
+  }
+
+  unsigned selCnt=c->numSelected();
+
+  for(unsigned i=0;i<selCnt;i++) {
+    Signature::Symbol* psym=env.signature->getPredicate(((*c)[i]->functor()));
+    if(!psym->isLemmaPredicate)
+    {
+      // the literal selection already contains a non-lemma-literal
+      return;
+    }
+  }
+
+  // we know that no non-lemma-literal is selected, so select some non-lemma-literal if there is one
+  for(unsigned i=selCnt;i<eligible;i++) {
+    Signature::Symbol* psym=env.signature->getPredicate(((*c)[i]->functor()));
+    if(!psym->isLemmaPredicate)
+    {
+      swap((*c)[selCnt], (*c)[i]);
+      c->setSelected(selCnt+1);
+      return;
+    }
+  }
+}
+
 /**
  * Perform literal selection on clause @b c
  *
@@ -260,6 +293,21 @@ void LiteralSelector::select(Clause* c, unsigned eligibleInp)
   }
 
   ASS_G(eligible,1);
+
+  // hack: if there is a negative lemma-literal, select this literal (and no other literal).
+  if (_opt.useLemmaPredicateLiteralSelection())
+  {
+    for(unsigned i=0;i<eligible;i++) {
+      Signature::Symbol* psym=env.signature->getPredicate(((*c)[i]->functor()));
+      if(psym->isLemmaPredicate && isNegativeForSelection((*c)[i]))
+      {
+        swap((*c)[i], (*c)[0]);
+        c->setSelected(1);
+        return;
+      }
+    }
+  }
+
   doSelection(c, eligible);
 }
 
diff --git a/Kernel/LiteralSelector.hpp b/Kernel/LiteralSelector.hpp
index 3a24806105..6a90defcbc 100644
--- a/Kernel/LiteralSelector.hpp
+++ b/Kernel/LiteralSelector.hpp
@@ -61,6 +61,7 @@ class LiteralSelector
   static LiteralSelector* getSelector(const Ordering& ordering, const Options& options, int selectorNumber);
 
   static void ensureSomeColoredSelected(Clause* c, unsigned eligible);
+  static void ensureNonLemmaPredicateSelected(Clause* c, unsigned eligible);
 
   /**
    * Return true if literal @b l is positive for the purpose of
diff --git a/Kernel/LookaheadLiteralSelector.cpp b/Kernel/LookaheadLiteralSelector.cpp
index 88d6b252c0..9b65eda603 100644
--- a/Kernel/LookaheadLiteralSelector.cpp
+++ b/Kernel/LookaheadLiteralSelector.cpp
@@ -352,6 +352,7 @@ void LookaheadLiteralSelector::doSelection(Clause* c, unsigned eligible)
   c->setSelected(selCnt);
 
   ensureSomeColoredSelected(c, eligible);
+  ensureNonLemmaPredicateSelected(c, eligible);
 }
 
 }
diff --git a/Kernel/MaximalLiteralSelector.cpp b/Kernel/MaximalLiteralSelector.cpp
index 7c2bbbffa7..c38fdc5964 100644
--- a/Kernel/MaximalLiteralSelector.cpp
+++ b/Kernel/MaximalLiteralSelector.cpp
@@ -91,4 +91,5 @@ void MaximalLiteralSelector::doSelection(Clause* c, unsigned eligible)
   c->setSelected(selCnt);
 
   ensureSomeColoredSelected(c, eligible);
+  ensureNonLemmaPredicateSelected(c, eligible);
 }
diff --git a/Kernel/Signature.cpp b/Kernel/Signature.cpp
index b8f388cdb5..0e46cda43c 100644
--- a/Kernel/Signature.cpp
+++ b/Kernel/Signature.cpp
@@ -47,6 +47,7 @@ Signature::Symbol::Symbol(const vstring& nm,unsigned arity, bool interpreted, bo
     _protected(0),
     _skip(0),
     _label(0),
+    isLemmaPredicate(0),
     _equalityProxy(0),
     _color(COLOR_TRANSPARENT),
     _stringConstant(stringConstant ? 1: 0),
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index eb76bd100e..5713c8cff9 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -75,6 +75,10 @@ class Signature
     /** marks propositional predicate symbols that are labels to 
         be used as names during consequence finding or function relationship finding */
     unsigned _label : 1;
+  public:
+    /** marks predicate symbols which are annotated by the user as lemma predicates*/
+    unsigned isLemmaPredicate : 1;
+  protected:
     /** marks predicates that are equality proxy */
     unsigned _equalityProxy : 1;
     /** used in coloured proofs and interpolation */
@@ -514,6 +518,10 @@ class Signature
   VirtualIterator<Shell::TermAlgebra*> termAlgebrasIterator() const { return _termAlgebras.range(); }
   Shell::TermAlgebraConstructor* getTermAlgebraConstructor(unsigned functor);
 
+  /** Returns nullptr if nat is not used */
+  Shell::NatTermAlgebra* getNat() { return _natTermAlgebra; }
+  void setNat(Shell::NatTermAlgebra* nta) { ASS(!_natTermAlgebra); _natTermAlgebra = nta; }
+
   void recordDividesNvalue(TermList n){
     _dividesNvalues.push(n);
   }
@@ -585,6 +593,8 @@ class Signature
    */ 
   DHMap<unsigned, Shell::TermAlgebra*> _termAlgebras;
 
+  Shell::NatTermAlgebra* _natTermAlgebra = nullptr;
+
   void defineOptionTermAlgebra(unsigned optionSort);
   void defineEitherTermAlgebra(unsigned eitherSort);
 }; // class Signature
diff --git a/Kernel/SpassLiteralSelector.cpp b/Kernel/SpassLiteralSelector.cpp
index 34dcea71ac..0e3baa175b 100644
--- a/Kernel/SpassLiteralSelector.cpp
+++ b/Kernel/SpassLiteralSelector.cpp
@@ -106,4 +106,5 @@ void SpassLiteralSelector::doSelection(Clause* c, unsigned eligible)
   c->setSelected(selCnt);
 
   ensureSomeColoredSelected(c, eligible);
+  ensureNonLemmaPredicateSelected(c, eligible);
 }
diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
index aa3ac6ddea..5d987b5af0 100644
--- a/Parse/SMTLIB2.cpp
+++ b/Parse/SMTLIB2.cpp
@@ -157,6 +157,19 @@ void SMTLIB2::readBenchmark(LExprList* bench)
       continue;
     }
 
+    // custom hack to mark lemma-predicates
+    if (ibRdr.tryAcceptAtom("declare-lemma-predicate")) {
+      vstring name = ibRdr.readAtom();
+      LExprList* iSorts = ibRdr.readList();
+      LExpr* oSort = ibRdr.readNext();
+
+      readDeclareFun(name,iSorts,oSort, true);
+
+      ibRdr.acceptEOL();
+
+      continue;
+    }
+
     if (ibRdr.tryAcceptAtom("declare-fun")) {
       vstring name = ibRdr.readAtom();
       LExprList* iSorts = ibRdr.readList();
@@ -180,6 +193,21 @@ void SMTLIB2::readBenchmark(LExprList* bench)
       continue;
     }
 
+    if (ibRdr.tryAcceptAtom("declare-nat"))
+    {
+      vstring nat = ibRdr.readAtom();
+      vstring zero = ibRdr.readAtom();
+      vstring succ = ibRdr.readAtom();
+      vstring pred = ibRdr.readAtom();
+      vstring less = ibRdr.readAtom();
+
+      readDeclareNat(nat, zero, succ, pred, less);
+
+      ibRdr.acceptEOL();
+
+      continue;
+    }
+
     if (ibRdr.tryAcceptAtom("declare-codatatypes")) {
       LExprList* sorts = ibRdr.readList();
       LExprList* datatypes = ibRdr.readList();
@@ -777,7 +805,7 @@ bool SMTLIB2::isAlreadyKnownFunctionSymbol(const vstring& name)
   return false;
 }
 
-void SMTLIB2::readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort)
+void SMTLIB2::readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort, bool isLemmaPredicate)
 {
   CALL("SMTLIB2::readDeclareFun");
 
@@ -796,10 +824,10 @@ void SMTLIB2::readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSor
     argSorts.push(declareSort(isRdr.next()));
   }
 
-  declareFunctionOrPredicate(name,rangeSort,argSorts);
+  declareFunctionOrPredicate(name,rangeSort,argSorts, isLemmaPredicate);
 }
 
-SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack<unsigned>& argSorts)
+SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack<unsigned>& argSorts, bool isLemmaPredicate)
 {
   CALL("SMTLIB2::declareFunctionOrPredicate");
 
@@ -808,11 +836,18 @@ SMTLIB2::DeclaredFunction SMTLIB2::declareFunctionOrPredicate(const vstring& nam
   Signature::Symbol* sym;
   OperatorType* type;
 
+  ASS(!isLemmaPredicate || rangeSort == Sorts::SRT_BOOL);
   if (rangeSort == Sorts::SRT_BOOL) { // predicate
     symNum = env.signature->addPredicate(name, argSorts.size(), added);
 
     sym = env.signature->getPredicate(symNum);
 
+    ASS(added);
+    if (isLemmaPredicate)
+    {
+      sym->isLemmaPredicate = 1;
+    }
+
     type = OperatorType::getPredicateType(argSorts.size(),argSorts.begin());
 
     LOG1("declareFunctionOrPredicate-Predicate");
@@ -1004,6 +1039,39 @@ void SMTLIB2::readDeclareDatatypes(LExprList* sorts, LExprList* datatypes, bool
   }
 }
 
+void SMTLIB2::readDeclareNat(const vstring& nat, const vstring& zero, const vstring& succ, const vstring& pred, const vstring& less)
+{
+  _declaredSorts.insert(nat, 0);
+  bool added;
+  unsigned natSort = env.sorts->addSort(nat + "()",  added, false); // TODO: why false? shouldn't it be interpreted?
+
+  ASS(added);
+
+  Stack<TermAlgebraConstructor*> constructors;
+
+  Stack<vstring> destructorNamesZero;
+  Stack<unsigned> destructorArgSortsZero;
+  auto zeroConstructor = buildTermAlgebraConstructor(zero, natSort, destructorNamesZero, destructorArgSortsZero);
+  constructors.push(zeroConstructor);
+
+  Stack<vstring> destructorNamesSucc;
+  destructorNamesSucc.push(pred);
+  Stack<unsigned> destructorArgSortsSucc;
+  destructorArgSortsSucc.push(natSort);
+  auto succConstructor = buildTermAlgebraConstructor(succ, natSort, destructorNamesSucc, destructorArgSortsSucc);
+  constructors.push(succConstructor);
+
+  TermAlgebra* ta = new TermAlgebra(natSort, constructors.size(), constructors.begin(), false);
+  env.signature->addTermAlgebra(ta);
+
+  Stack<unsigned> argSorts;
+  argSorts.push(natSort);
+  argSorts.push(natSort);
+  auto pair = declareFunctionOrPredicate(less, Sorts::SRT_BOOL, argSorts);
+  NatTermAlgebra* nta = new NatTermAlgebra(ta, pair.first);
+  env.signature->setNat(nta);
+}
+
 TermAlgebraConstructor* SMTLIB2::buildTermAlgebraConstructor(vstring constrName, unsigned taSort,
                                                              Stack<vstring> destructorNames, Stack<unsigned> argSorts) {
   CALL("SMTLIB2::buildTermAlgebraConstructor");
diff --git a/Parse/SMTLIB2.hpp b/Parse/SMTLIB2.hpp
index 85a04bfda5..d2229a24d8 100644
--- a/Parse/SMTLIB2.hpp
+++ b/Parse/SMTLIB2.hpp
@@ -257,14 +257,14 @@ class SMTLIB2 {
    * store the ensuing DeclaredFunction in _declaredFunctions
    * and return it.
    */
-  DeclaredFunction declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack<unsigned>& argSorts);
+  DeclaredFunction declareFunctionOrPredicate(const vstring& name, signed rangeSort, const Stack<unsigned>& argSorts, bool isLemmaPredicate = false);
 
   /**
    * Handle "declare-fun" entry.
    *
    * Declaring a function just extends the signature.
    */
-  void readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort);
+  void readDeclareFun(const vstring& name, LExprList* iSorts, LExpr* oSort, bool isLemmaPredicate = false);
 
   /**
    * Handle "define-fun" entry.
@@ -275,6 +275,7 @@ class SMTLIB2 {
 
   void readDeclareDatatypes(LExprList* sorts, LExprList* datatypes, bool codatatype = false);
 
+  void readDeclareNat(const vstring& nat, const vstring& zero, const vstring& succ, const vstring& pred, const vstring& less);
   TermAlgebraConstructor* buildTermAlgebraConstructor(vstring constrName, unsigned taSort,
                                                       Stack<vstring> destructorNames, Stack<unsigned> argSorts);
 
diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp
index 1ad16e78c0..549e07fd61 100644
--- a/Saturation/SaturationAlgorithm.cpp
+++ b/Saturation/SaturationAlgorithm.cpp
@@ -1636,6 +1636,10 @@ ImmediateSimplificationEngine* SaturationAlgorithm::createISE(Problem& prb, cons
   res->addFront(new TautologyDeletionISE());
   res->addFront(new DuplicateLiteralRemovalISE());
 
+  if(prb.hasEquality() && env.signature->getNat() != nullptr && env.options->useSuccessorDeletionRule()) {
+    res->addFront(new TwoSuccessorsISE());
+  }
+
   return res;
 }
 
diff --git a/Shell/Options.cpp b/Shell/Options.cpp
index 332046732c..961f6db45a 100644
--- a/Shell/Options.cpp
+++ b/Shell/Options.cpp
@@ -176,7 +176,8 @@ void Options::Options::init()
          "smtcomp",
          "smtcomp_2016",
          "smtcomp_2017",
-         "smtcomp_2018"});
+         "smtcomp_2018",
+         "rapid"});
     _schedule.description = "Schedule to be run by the portfolio mode. casc and smtcomp usually point to the most recent schedule in that category. Note that some old schedules may contain option values that are no longer supported - see ignore_missing.";
     _lookup.insert(&_schedule);
     _schedule.reliesOnHard(Or(_mode.is(equal(Mode::CASC)),_mode.is(equal(Mode::CASC_SAT)),_mode.is(equal(Mode::SMTCOMP)),_mode.is(equal(Mode::PORTFOLIO))));
@@ -902,6 +903,16 @@ void Options::Options::init()
     _lookup.insert(&_ageWeightRatioShapeFrequency);
     _ageWeightRatioShapeFrequency.tag(OptionTag::SATURATION);
 
+    _useLemmaPredicateLiteralSelection = BoolOptionValue("lemma_literal_selection","lls",false);
+    _useLemmaPredicateLiteralSelection.description = "Turn on clause selection using multiple queues containing different clauses (split by amount of theory reasoning)";
+    _lookup.insert(&_useLemmaPredicateLiteralSelection);
+    _useLemmaPredicateLiteralSelection.tag(OptionTag::SATURATION);
+
+    _useSuccessorDeletionRule = BoolOptionValue("custom_successor_deletion","csd",false);
+    _useSuccessorDeletionRule.description = "Turn on custom deletion rule for the trace logic domain, which deletes all clauses containing terms of the form s(0) and terms of the form s(s(t)), for arbitrary subterms t";
+    _lookup.insert(&_useSuccessorDeletionRule);
+    _useSuccessorDeletionRule.tag(OptionTag::INFERENCES);
+
     _useTheorySplitQueues = BoolOptionValue("theory_split_queue","thsq",false);
     _useTheorySplitQueues.description = "Turn on clause selection using multiple queues containing different clauses (split by amount of theory reasoning)";
     _lookup.insert(&_useTheorySplitQueues);
diff --git a/Shell/Options.hpp b/Shell/Options.hpp
index 5eee1f12d5..708269984f 100644
--- a/Shell/Options.hpp
+++ b/Shell/Options.hpp
@@ -472,7 +472,9 @@ class Options
     SMTCOMP,
     SMTCOMP_2016,
     SMTCOMP_2017,
-    SMTCOMP_2018
+    SMTCOMP_2018, 
+
+    RAPID
 };
 
 
@@ -2067,6 +2069,8 @@ bool _hard;
   int ageRatio() const { return _ageWeightRatio.actualValue; }
   void setAgeRatio(int v){ _ageWeightRatio.actualValue = v; }
   int weightRatio() const { return _ageWeightRatio.otherValue; }
+  bool useLemmaPredicateLiteralSelection() const { return _useLemmaPredicateLiteralSelection.actualValue; }
+  bool useSuccessorDeletionRule() const { return _useSuccessorDeletionRule.actualValue; }
   bool useTheorySplitQueues() const { return _useTheorySplitQueues.actualValue; }
   Lib::vvector<int> theorySplitQueueRatios() const;
   Lib::vvector<float> theorySplitQueueCutoffs() const;
@@ -2345,6 +2349,8 @@ bool _hard;
   RatioOptionValue _ageWeightRatio;
 	ChoiceOptionValue<AgeWeightRatioShape> _ageWeightRatioShape;
 	UnsignedOptionValue _ageWeightRatioShapeFrequency;
+  BoolOptionValue _useLemmaPredicateLiteralSelection;
+  BoolOptionValue _useSuccessorDeletionRule;
   BoolOptionValue _useTheorySplitQueues;
   StringOptionValue _theorySplitQueueRatios;
   StringOptionValue _theorySplitQueueCutoffs;
diff --git a/Shell/TermAlgebra.cpp b/Shell/TermAlgebra.cpp
index 89d655ae70..89c3f357d5 100644
--- a/Shell/TermAlgebra.cpp
+++ b/Shell/TermAlgebra.cpp
@@ -147,4 +147,25 @@ unsigned TermAlgebra::getSubtermPredicate() {
   return s;
 }
 
+NatTermAlgebra::NatTermAlgebra(TermAlgebra* ta, unsigned lessPredicate)
+  : _ta(ta), _lessPredicate(lessPredicate)
+{
+  if (ta->nConstructors() != 2) {
+    throw BadNatTermAlgebra("nat must have two constructors");
+  }
+  if (ta->allowsCyclicTerms()) {
+    throw BadNatTermAlgebra("nat must not allow cyclic terms (use datatype instead of codatatype)");
+  }
+
+  _zero = ta->constructor(0);
+  _succ = ta->constructor(1);
+  if (_zero->arity() != 0) {
+    std::swap(_zero, _succ);
+  }
+  if (_zero->arity() != 0 || _succ->arity() != 1) {
+    throw BadNatTermAlgebra("nat constructors must have arity 0 and 1");
+  }
+}
+
+
 }
diff --git a/Shell/TermAlgebra.hpp b/Shell/TermAlgebra.hpp
index 3b4f0fad6d..ac40b50dcc 100644
--- a/Shell/TermAlgebra.hpp
+++ b/Shell/TermAlgebra.hpp
@@ -26,6 +26,7 @@
 #include "Lib/Array.hpp"
 #include "Lib/VString.hpp"
 #include "Kernel/Sorts.hpp"
+#include "Kernel/Term.hpp"
 
 namespace Shell {
   class TermAlgebraConstructor {
@@ -114,6 +115,51 @@ namespace Shell {
     bool _allowsCyclicTerms;
     ConstructorArray _constrs;
   };
+
+  class BadNatTermAlgebra : public Lib::Exception {
+    public:
+      explicit BadNatTermAlgebra(char const* msg)
+        : Lib::Exception(msg)
+      { }
+  };
+
+  class NatTermAlgebra {
+    public:
+      CLASS_NAME(NatTermAlgebra);
+      USE_ALLOCATOR(NatTermAlgebra);
+
+      /** May throw BadNatTermAlgebra */
+      NatTermAlgebra(TermAlgebra* ta, unsigned lessPredicate);
+
+      TermAlgebra* termAlgebra() { return _ta; }
+      TermAlgebraConstructor* getZeroConstructor() { return _zero; }
+      TermAlgebraConstructor* getSuccConstructor() { return _succ; }
+      /** $less for nat */
+      unsigned getLessPredicate() { return _lessPredicate; }
+
+      /*
+       * Convenience methods for generating interpreted terms and predicates
+       */
+      Kernel::TermList createZero()
+      {
+        return Kernel::TermList(Kernel::Term::create(_zero->functor(), 0, 0));
+      }
+      Kernel::TermList createSucc(Kernel::TermList arg)
+      {
+        return Kernel::TermList(Kernel::Term::create1(_succ->functor(), arg));
+      }
+      Kernel::Literal* createLess(bool polarity, Kernel::TermList lhs, Kernel::TermList rhs)
+      {
+        return Kernel::Literal::create2(_lessPredicate, polarity, lhs, rhs);
+      }
+
+    private:
+      TermAlgebra* _ta;
+      TermAlgebraConstructor* _zero;
+      TermAlgebraConstructor* _succ;
+      unsigned _lessPredicate;
+  };
+
 }
 
 #endif
diff --git a/Shell/TheoryAxioms.cpp b/Shell/TheoryAxioms.cpp
index 36bc2458f4..9960be8745 100644
--- a/Shell/TheoryAxioms.cpp
+++ b/Shell/TheoryAxioms.cpp
@@ -647,8 +647,12 @@ void TheoryAxioms::addExtraIntegerOrderingAxiom(Interpretation plus, TermList on
   Literal* nyLxPOne = Literal::create2(lessPred, false, y,xPOne);
 
   addTheoryClauseFromLits({nxLy,nyLxPOne}, InferenceRule::THA_EXTRA_INTEGER_ORDERING, EXPENSIVE);
+
+  // hack: add additional axiom x!=x+1 to enable simplification using subsumption-resolution
+  Literal* notXIsXPlusOne = Literal::createEquality(false, x, xPOne, theory->getOperationSort(plus));
+  addTheoryClauseFromLits({notXIsXPlusOne}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
 }
-    
+
 /**
  * Add axioms defining floor function
  * @author Giles
@@ -1137,6 +1141,16 @@ void TheoryAxioms::apply()
     modified = true;
   }
 
+  auto nat = env.signature->getNat();
+  if (nat != nullptr) {
+    addZeroSmallestElementAxiom(nat);
+    addDefineSubEqAxiom(nat);
+    addMonotonicityAxiom(nat);
+    addTransitivityAxioms(nat);
+    addTotalityAxiom(nat);
+    addDisjointnessAxioms(nat);
+  }
+
   if(modified) {
     _prb.reportEqualityAdded(false);
   }
@@ -1376,3 +1390,131 @@ bool TheoryAxioms::addSubtermDefinitions(unsigned subtermPredicate, TermAlgebraC
   }
   return added;
 }
+
+void TheoryAxioms::addZeroSmallestElementAxiom(NatTermAlgebra* nat)
+{
+  TermList x(0, false);
+  auto zero = nat->createZero();
+  auto sx = nat->createSucc(x);
+
+  // forall x. 0 < s(x)
+  auto lit = nat->createLess(true, zero, sx);
+
+  addTheoryClauseFromLits({lit}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+}
+
+void TheoryAxioms::addDefineSubEqAxiom(NatTermAlgebra* nat)
+{
+  // forall x,y. x<s(y) <=> (x=y or x<y)
+
+  TermList x(0, false);
+  TermList y(1, false);
+  auto sx = nat->createSucc(x);
+  auto sy = nat->createSucc(y);
+  auto natSort = nat->termAlgebra()->sort();
+
+  // clause 1: x!<s(y) or x=y or x<y
+  auto clause1Lit1 = nat->createLess(false, x, sy);
+  auto clause1Lit2 = Literal::createEquality(true, x, y, natSort);
+  auto clause1Lit3 = nat->createLess(true, x,y);
+
+  addTheoryClauseFromLits({clause1Lit1, clause1Lit2, clause1Lit3}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+
+  // clause 2: x!=y or x<s(y), simplified to x<s(x)
+  auto clause2Lit1 = nat->createLess(true, x, sx);
+
+  addTheoryClauseFromLits({clause2Lit1}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+
+  // clause 3: x!<y or x<s(y)
+  auto clause3Lit1 = nat->createLess(false, x, y);
+  auto clause3Lit2 = nat->createLess(true, x, sy);
+
+  addTheoryClauseFromLits({clause3Lit1, clause3Lit2}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+}
+
+void TheoryAxioms::addMonotonicityAxiom(NatTermAlgebra* nat)
+{
+  // forall x,y. x<y <=> s(x)<s(y)
+
+  TermList x(0, false);
+  TermList y(1, false);
+  auto sx = nat->createSucc(x);
+  auto sy = nat->createSucc(y);
+
+  // clause 1: x!<y or s(x)<s(y)
+  auto clause1Lit1 = nat->createLess(false, x, y);
+  auto clause1Lit2 = nat->createLess(true, sx, sy);
+
+  addTheoryClauseFromLits({clause1Lit1, clause1Lit2}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+
+  // clause 2: s(x)!<s(y) or x<y
+  auto clause2Lit1 = nat->createLess(false, sx, sy);
+  auto clause2Lit2 = nat->createLess(true, x, y);
+
+  addTheoryClauseFromLits({clause2Lit1, clause2Lit2}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+}
+
+void TheoryAxioms::addTransitivityAxioms(NatTermAlgebra* nat)
+{
+  TermList x(0, false);
+  TermList y(1, false);
+  TermList z(2, false);
+  auto sy = nat->createSucc(y);
+  auto sz = nat->createSucc(z);
+
+  auto strict1 = nat->createLess(false, x, y);
+  auto strict2 = nat->createLess(false, y, z);
+  auto strict3 = nat->createLess(true, x, z);
+  auto nonStrict1 = nat->createLess(false, x, sy);
+  auto nonStrict2 = nat->createLess(false, y, sz);
+  auto nonStrict3 = nat->createLess(true, x, sz);
+
+  // variant 1: forall x,y,z. x!<y or y!<z or x<z
+  addTheoryClauseFromLits({strict1, strict2, strict3}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+  // variant 2: forall x,y,z. x!<s(y) or y!<z or x<z
+  addTheoryClauseFromLits({nonStrict1, strict2, strict3}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+  // variant 3: forall x,y,z. x!<y or y!<s(z) or x<z
+  addTheoryClauseFromLits({strict1, nonStrict2, strict3}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+  // variant 4: forall x,y,z. x!<s(y) or y!<s(z) or x<s(z)
+  addTheoryClauseFromLits({nonStrict1, nonStrict2, nonStrict3}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+}
+
+void TheoryAxioms::addTotalityAxiom(NatTermAlgebra* nat)
+{
+  TermList x(0, false);
+  TermList y(1, false);
+  auto natSort = nat->termAlgebra()->sort();
+
+  // forall x,y. x<y or x=y or x>y
+  auto lit1 = nat->createLess(true, x, y);
+  auto lit2 = Literal::createEquality(true, x, y, natSort);
+  auto lit3 = nat->createLess(true, y, x);
+
+  addTheoryClauseFromLits({lit1, lit2, lit3}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+}
+
+void TheoryAxioms::addDisjointnessAxioms(NatTermAlgebra* nat)
+{
+  TermList x(0, false);
+  TermList y(1, false);
+  auto natSort = nat->termAlgebra()->sort();
+
+  // Clause 1: x!<y or x!=y, simplified to x!<x
+  auto clause1Lit1 = nat->createLess(false, x, x);
+
+  addTheoryClauseFromLits({clause1Lit1}, InferenceRule::GENERIC_THEORY_AXIOM, CHEAP);
+
+  // Clause 2: x!<y or y!<x
+  // already subsumed by other theory axioms, therefore omitted:
+  //    The standard transitivity axiom is
+  //       x<y and y<z => x<z
+  //    substituting z->x gives
+  //       x<y and y<x => x<x
+  //    resolving with disjointness-clause1 gives
+  //       x<y and y<x => false
+  //    which is equivalent (using modus tollens) to
+  //       x<y => y!<x
+
+  // Clause 3: x!=y or x!<y, simplified to x!<x.
+  // Already exists as clause 1 of disjointness axiom, therefore omitted.
+}
\ No newline at end of file
diff --git a/Shell/TheoryAxioms.hpp b/Shell/TheoryAxioms.hpp
index 591e3dda20..e8681d5346 100644
--- a/Shell/TheoryAxioms.hpp
+++ b/Shell/TheoryAxioms.hpp
@@ -28,6 +28,7 @@
 
 #include "Kernel/Theory.hpp"
 #include "Options.hpp"
+#include "Shell/TermAlgebra.hpp"
 
 #include <initializer_list>
 
@@ -117,6 +118,14 @@ static unsigned const EXPENSIVE = 1;
      recursive) */
   bool addSubtermDefinitions(unsigned subtermPredicate, TermAlgebraConstructor* c);
 
+  // nat axioms
+  void addZeroSmallestElementAxiom(NatTermAlgebra* nat);
+  void addDefineSubEqAxiom(NatTermAlgebra* nat);
+  void addMonotonicityAxiom(NatTermAlgebra* nat);
+  void addTransitivityAxioms(NatTermAlgebra* nat);
+  void addTotalityAxiom(NatTermAlgebra* nat);
+  void addDisjointnessAxioms(NatTermAlgebra* nat);
+  
   void addTheoryClauseFromLits(std::initializer_list<Literal*> lits, InferenceRule rule, unsigned level);
   void addAndOutputTheoryUnit(Unit* unit, unsigned level);
 };