diff --git a/CASC/PortfolioMode.cpp b/CASC/PortfolioMode.cpp
index e7ca7e378..bc863a3b8 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 a466411d7..3fb3edc5b 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 2b437627a..24e5757d9 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 7dc3ced6b..fa514f5c0 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 5ca267481..023590de3 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 827786fba..20d4818ee 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 f421f0922..ea5a4d48d 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 b2faace3b..8d23e07d7 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 3a2480610..6a90defcb 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 88d6b252c..9b65eda60 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 7c2bbbffa..c38fdc596 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 b8f388cdb..0e46cda43 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 eb76bd100..5713c8cff 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 34dcea71a..0e3baa175 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 aa3ac6dde..5d987b5af 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 85a04bfda..d2229a24d 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 1ad16e78c..549e07fd6 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 332046732..961f6db45 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 5eee1f12d..708269984 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 89d655ae7..89c3f357d 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 3b4f0fad6..ac40b50dc 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 36bc2458f..9960be874 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 591e3dda2..e8681d534 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);
 };