%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX042+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:13:35 PM UTC 2026
% Result : Theorem 154.49s 20.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX042+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n020.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 10:24:34 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 154.49/20.10 % Refutation found
% 154.49/20.10 % SZS status Theorem for theBenchmark: Theorem is valid
% 154.49/20.10 % SZS output start CNFRefutation for theBenchmark
% 154.49/20.10 fof(f1,axiom,(
% 154.49/20.10 (! [Xx3] : '0' != s(Xx3) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f24,axiom,(
% 154.49/20.10 (! [Xx1,Xx2] :( '@<_succeeds'(Xx1,Xx2)<=> ( (? [Xx3,Xx4] :( Xx1 = s(Xx3)& Xx2 = s(Xx4)& '@<_succeeds'(Xx3,Xx4) ))| (? [Xx5] :( Xx1 = '0'& Xx2 = s(Xx5) ) )) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f45,axiom,(
% 154.49/20.10 (! [Xy] : '@+'('0',Xy) = Xy )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f46,axiom,(
% 154.49/20.10 (! [Xx,Xy] :( nat_succeeds(Xx)=> '@+'(s(Xx),Xy) = s('@+'(Xx,Xy)) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f49,axiom,(
% 154.49/20.10 (! [Xx] :( nat_succeeds(Xx)=> '@+'(Xx,'0') = Xx ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f51,axiom,(
% 154.49/20.10 (! [Xx,Xy] :( ( nat_succeeds(Xx)& nat_succeeds(Xy) )=> '@+'(Xx,Xy) = '@+'(Xy,Xx) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f71,axiom,(
% 154.49/20.10 (! [Xx,Xy] :( nat_succeeds(Xx)=> '@<_terminates'(Xx,Xy) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f72,axiom,(
% 154.49/20.10 (! [Xx,Xy] :( nat_succeeds(Xy)=> '@<_terminates'(Xx,Xy) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f73,axiom,(
% 154.49/20.10 (! [Xx,Xy] :( '@<_succeeds'(Xx,Xy)=> nat_succeeds(Xx) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f79,axiom,(
% 154.49/20.10 (! [Xx] :( nat_succeeds(Xx)=> ~ '@<_succeeds'(Xx,Xx) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f84,axiom,(
% 154.49/20.10 (! [Xx,Xy] :( nat_succeeds(Xx)=> '@=<_terminates'(Xx,Xy) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f85,axiom,(
% 154.49/20.10 (! [Xx,Xy] :( nat_succeeds(Xy)=> '@=<_terminates'(Xx,Xy) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f103,axiom,(
% 154.49/20.10 ( (! [Xx] :( ( (? [Xx2] :( Xx = s(Xx2)& nat_succeeds(Xx2)& (! [Xy,Xz] :( '@<_succeeds'(Xy,Xz)=> '@<_succeeds'('@+'(Xx2,Xy),'@+'(Xx2,Xz)) ) )))| Xx = '0' )=> (! [Xy,Xz] :( '@<_succeeds'(Xy,Xz)=> '@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) )))=> (! [Xx] :( nat_succeeds(Xx)=> (! [Xy,Xz] :( '@<_succeeds'(Xy,Xz)=> '@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) )) )) ),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f104,conjecture,(
% 154.49/20.10 (! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& '@<_succeeds'(Xy,Xz) )=> '@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) )),
% 154.49/20.10 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 154.49/20.10 fof(f105,negated_conjecture,(
% 154.49/20.10 ~((! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& '@<_succeeds'(Xy,Xz) )=> '@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) ))),
% 154.49/20.10 inference(negated_conjecture,[status(cth)],[f104])).
% 154.49/20.10 fof(f106,plain,(
% 154.49/20.10 ![X0]: (~'0'=s(X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f1])).
% 154.49/20.10 fof(f211,definition,(
% 154.49/20.10 ![Xx1,Xx2,Xx3,Xx4]: (sP4_prd(Xx4,Xx3,Xx2,Xx1)<=>((Xx1=s(Xx3)&Xx2=s(Xx4))&'@<_succeeds'(Xx3,Xx4)))),
% 154.49/20.10 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 154.49/20.10 fof(f212,plain,(
% 154.49/20.10 ![Xx1,Xx2]: ('@<_succeeds'(Xx1,Xx2)<=>((?[Xx3,Xx4]: sP4_prd(Xx4,Xx3,Xx2,Xx1))|(?[Xx5]: (Xx1='0'&Xx2=s(Xx5)))))),
% 154.49/20.10 inference(formula_renaming,[status(thm)],[f24,f211])).
% 154.49/20.10 fof(f213,plain,(
% 154.49/20.10 ![Xx1,Xx2]: ((~'@<_succeeds'(Xx1,Xx2)|((?[Xx3,Xx4]: sP4_prd(Xx4,Xx3,Xx2,Xx1))|(?[Xx5]: (Xx1='0'&Xx2=s(Xx5)))))&('@<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ~sP4_prd(Xx4,Xx3,Xx2,Xx1))&(![Xx5]: (~Xx1='0'|~Xx2=s(Xx5))))))),
% 154.49/20.10 inference(NNF_transformation,[status(thm)],[f212])).
% 154.49/20.10 fof(f214,plain,(
% 154.49/20.10 (![Xx1,Xx2]: (~'@<_succeeds'(Xx1,Xx2)|((?[Xx3,Xx4]: sP4_prd(Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&(?[Xx5]: Xx2=s(Xx5))))))&(![Xx1,Xx2]: ('@<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ~sP4_prd(Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|(![Xx5]: ~Xx2=s(Xx5))))))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f213])).
% 154.49/20.10 fof(f215,plain,(
% 154.49/20.10 (![Xx1,Xx2]: (~'@<_succeeds'(Xx1,Xx2)|(sP4_prd(sK20_skl(Xx2,Xx1),sK19_skl(Xx2,Xx1),Xx2,Xx1)|(Xx1='0'&Xx2=s(sK21_skl(Xx2,Xx1))))))&(![Xx1,Xx2]: ('@<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ~sP4_prd(Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|(![Xx5]: ~Xx2=s(Xx5))))))),
% 154.49/20.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(Xx3,sK19_skl(Xx2,Xx1)),skolemize(Xx4,sK20_skl(Xx2,Xx1)),skolemize(Xx5,sK21_skl(Xx2,Xx1))],[f214])).
% 154.49/20.10 fof(f218,plain,(
% 154.49/20.10 ![X0,X1,X2,X3]: ('@<_succeeds'(X0,X1)|~sP4_prd(X2,X3,X1,X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f215])).
% 154.49/20.10 fof(f305,plain,(
% 154.49/20.10 ![X0]: ('@+'('0',X0)=X0)),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f45])).
% 154.49/20.10 fof(f306,plain,(
% 154.49/20.10 ![Xx,Xy]: (~nat_succeeds(Xx)|'@+'(s(Xx),Xy)=s('@+'(Xx,Xy)))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 154.49/20.10 fof(f307,plain,(
% 154.49/20.10 ![Xx]: (~nat_succeeds(Xx)|(![Xy]: '@+'(s(Xx),Xy)=s('@+'(Xx,Xy))))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f306])).
% 154.49/20.10 fof(f308,plain,(
% 154.49/20.10 ![X0,X1]: (~nat_succeeds(X0)|'@+'(s(X0),X1)=s('@+'(X0,X1)))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f307])).
% 154.49/20.10 fof(f313,plain,(
% 154.49/20.10 ![Xx]: (~nat_succeeds(Xx)|'@+'(Xx,'0')=Xx)),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 154.49/20.10 fof(f314,plain,(
% 154.49/20.10 ![X0]: (~nat_succeeds(X0)|'@+'(X0,'0')=X0)),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f313])).
% 154.49/20.10 fof(f317,plain,(
% 154.49/20.10 ![Xx,Xy]: ((~nat_succeeds(Xx)|~nat_succeeds(Xy))|'@+'(Xx,Xy)='@+'(Xy,Xx))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 154.49/20.10 fof(f318,plain,(
% 154.49/20.10 ![X0,X1]: (~nat_succeeds(X0)|~nat_succeeds(X1)|'@+'(X0,X1)='@+'(X1,X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f317])).
% 154.49/20.10 fof(f365,plain,(
% 154.49/20.10 ![Xx,Xy]: (~nat_succeeds(Xx)|'@<_terminates'(Xx,Xy))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 154.49/20.10 fof(f366,plain,(
% 154.49/20.10 ![Xx]: (~nat_succeeds(Xx)|(![Xy]: '@<_terminates'(Xx,Xy)))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f365])).
% 154.49/20.10 fof(f367,plain,(
% 154.49/20.10 ![X0,X1]: (~nat_succeeds(X0)|'@<_terminates'(X0,X1))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f366])).
% 154.49/20.10 fof(f368,plain,(
% 154.49/20.10 ![Xx,Xy]: (~nat_succeeds(Xy)|'@<_terminates'(Xx,Xy))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f72])).
% 154.49/20.10 fof(f369,plain,(
% 154.49/20.10 ![Xy]: (~nat_succeeds(Xy)|(![Xx]: '@<_terminates'(Xx,Xy)))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f368])).
% 154.49/20.10 fof(f370,plain,(
% 154.49/20.10 ![X0,X1]: (~nat_succeeds(X0)|'@<_terminates'(X1,X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f369])).
% 154.49/20.10 fof(f371,plain,(
% 154.49/20.10 ![Xx,Xy]: (~'@<_succeeds'(Xx,Xy)|nat_succeeds(Xx))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 154.49/20.10 fof(f372,plain,(
% 154.49/20.10 ![Xx]: ((![Xy]: ~'@<_succeeds'(Xx,Xy))|nat_succeeds(Xx))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f371])).
% 154.49/20.10 fof(f373,plain,(
% 154.49/20.10 ![X0,X1]: (~'@<_succeeds'(X0,X1)|nat_succeeds(X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f372])).
% 154.49/20.10 fof(f388,plain,(
% 154.49/20.10 ![Xx]: (~nat_succeeds(Xx)|~'@<_succeeds'(Xx,Xx))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 154.49/20.10 fof(f389,plain,(
% 154.49/20.10 ![X0]: (~nat_succeeds(X0)|~'@<_succeeds'(X0,X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f388])).
% 154.49/20.10 fof(f398,plain,(
% 154.49/20.10 ![Xx,Xy]: (~nat_succeeds(Xx)|'@=<_terminates'(Xx,Xy))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 154.49/20.10 fof(f399,plain,(
% 154.49/20.10 ![Xx]: (~nat_succeeds(Xx)|(![Xy]: '@=<_terminates'(Xx,Xy)))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f398])).
% 154.49/20.10 fof(f400,plain,(
% 154.49/20.10 ![X0,X1]: (~nat_succeeds(X0)|'@=<_terminates'(X0,X1))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f399])).
% 154.49/20.10 fof(f401,plain,(
% 154.49/20.10 ![Xx,Xy]: (~nat_succeeds(Xy)|'@=<_terminates'(Xx,Xy))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 154.49/20.10 fof(f402,plain,(
% 154.49/20.10 ![Xy]: (~nat_succeeds(Xy)|(![Xx]: '@=<_terminates'(Xx,Xy)))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f401])).
% 154.49/20.10 fof(f403,plain,(
% 154.49/20.10 ![X0,X1]: (~nat_succeeds(X0)|'@=<_terminates'(X1,X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f402])).
% 154.49/20.10 fof(f446,plain,(
% 154.49/20.10 (?[Xx]: (((?[Xx2]: ((Xx=s(Xx2)&nat_succeeds(Xx2))&(![Xy,Xz]: (~'@<_succeeds'(Xy,Xz)|'@<_succeeds'('@+'(Xx2,Xy),'@+'(Xx2,Xz))))))|Xx='0')&(?[Xy,Xz]: ('@<_succeeds'(Xy,Xz)&~'@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))))|(![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: (~'@<_succeeds'(Xy,Xz)|'@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 154.49/20.10 fof(f447,plain,(
% 154.49/20.10 ((((sK37_skl=s(sK38_skl)&nat_succeeds(sK38_skl))&(![Xy,Xz]: (~'@<_succeeds'(Xy,Xz)|'@<_succeeds'('@+'(sK38_skl,Xy),'@+'(sK38_skl,Xz)))))|sK37_skl='0')&('@<_succeeds'(sK39_skl,sK40_skl)&~'@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))))|(![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: (~'@<_succeeds'(Xy,Xz)|'@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))))),
% 154.49/20.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl,sK38_skl,sK39_skl,sK40_skl]),skolemize(Xx,sK37_skl),skolemize(Xx2,sK38_skl),skolemize(Xy,sK39_skl),skolemize(Xz,sK40_skl)],[f446])).
% 154.49/20.10 fof(f448,plain,(
% 154.49/20.10 ![X0,X1,X2]: (sK37_skl=s(sK38_skl)|sK37_skl='0'|~nat_succeeds(X0)|~'@<_succeeds'(X1,X2)|'@<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f447])).
% 154.49/20.10 fof(f449,plain,(
% 154.49/20.10 ![X0,X1,X2]: (nat_succeeds(sK38_skl)|sK37_skl='0'|~nat_succeeds(X0)|~'@<_succeeds'(X1,X2)|'@<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f447])).
% 154.49/20.10 fof(f450,plain,(
% 154.49/20.10 ![X0,X1,X2,X3,X4]: (~'@<_succeeds'(X0,X1)|'@<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))|sK37_skl='0'|~nat_succeeds(X2)|~'@<_succeeds'(X3,X4)|'@<_succeeds'('@+'(X2,X3),'@+'(X2,X4)))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f447])).
% 154.49/20.10 fof(f451,plain,(
% 154.49/20.10 ![X0,X1,X2]: ('@<_succeeds'(sK39_skl,sK40_skl)|~nat_succeeds(X0)|~'@<_succeeds'(X1,X2)|'@<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f447])).
% 154.49/20.10 fof(f452,plain,(
% 154.49/20.10 ![X0,X1,X2]: (~'@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))|~nat_succeeds(X0)|~'@<_succeeds'(X1,X2)|'@<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f447])).
% 154.49/20.10 fof(f453,plain,(
% 154.49/20.10 (?[Xx,Xy,Xz]: ((nat_succeeds(Xx)&'@<_succeeds'(Xy,Xz))&~'@<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))),
% 154.49/20.10 inference(pre_NNF_transformation,[status(thm)],[f105])).
% 154.49/20.10 fof(f454,plain,(
% 154.49/20.10 ((nat_succeeds(sK41_skl)&'@<_succeeds'(sK42_skl,sK43_skl))&~'@<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl)))),
% 154.49/20.10 inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl,sK43_skl]),skolemize(Xx,sK41_skl),skolemize(Xy,sK42_skl),skolemize(Xz,sK43_skl)],[f453])).
% 154.49/20.10 fof(f455,plain,(
% 154.49/20.10 nat_succeeds(sK41_skl)),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f454])).
% 154.49/20.10 fof(f456,plain,(
% 154.49/20.10 '@<_succeeds'(sK42_skl,sK43_skl)),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f454])).
% 154.49/20.10 fof(f457,plain,(
% 154.49/20.10 ~'@<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f454])).
% 154.49/20.10 fof(f482,plain,(
% 154.49/20.10 ![Xx1,Xx2,Xx3,Xx4]: ((~sP4_prd(Xx4,Xx3,Xx2,Xx1)|((Xx1=s(Xx3)&Xx2=s(Xx4))&'@<_succeeds'(Xx3,Xx4)))&(sP4_prd(Xx4,Xx3,Xx2,Xx1)|((~Xx1=s(Xx3)|~Xx2=s(Xx4))|~'@<_succeeds'(Xx3,Xx4))))),
% 154.49/20.10 inference(NNF_transformation,[status(thm)],[f211])).
% 154.49/20.10 fof(f483,plain,(
% 154.49/20.10 (![Xx1,Xx2,Xx3,Xx4]: (~sP4_prd(Xx4,Xx3,Xx2,Xx1)|((Xx1=s(Xx3)&Xx2=s(Xx4))&'@<_succeeds'(Xx3,Xx4))))&(![Xx1,Xx2,Xx3,Xx4]: (sP4_prd(Xx4,Xx3,Xx2,Xx1)|((~Xx1=s(Xx3)|~Xx2=s(Xx4))|~'@<_succeeds'(Xx3,Xx4))))),
% 154.49/20.10 inference(miniscoping,[status(thm)],[f482])).
% 154.49/20.10 fof(f487,plain,(
% 154.49/20.10 ![X0,X1,X2,X3]: (sP4_prd(X0,X1,X2,X3)|~X3=s(X1)|~X2=s(X0)|~'@<_succeeds'(X1,X0))),
% 154.49/20.10 inference(cnf_transformation,[status(thm)],[f483])).
% 154.49/20.10 fof(f494,definition,(
% 154.49/20.10 sQ0_spl <=> (sK37_skl=s(sK38_skl))),
% 154.49/20.10 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 154.49/20.10 fof(f495,plain,(
% 154.49/20.10 sK37_skl=s(sK38_skl)|~sQ0_spl),
% 154.49/20.10 inference(component_clause,[status(thm)],[f494])).
% 154.49/20.10 fof(f497,definition,(
% 154.49/20.10 sQ1_spl <=> (sK37_skl='0')),
% 154.49/20.10 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 154.49/20.10 fof(f498,plain,(
% 154.49/20.10 sK37_skl='0'|~sQ1_spl),
% 154.49/20.10 inference(component_clause,[status(thm)],[f497])).
% 154.49/20.10 fof(f500,definition,(
% 154.49/20.10 ![X0,X1,X2]: (sQ2_spl <=> (~nat_succeeds(X0)|~'@<_succeeds'(X1,X2)|'@<_succeeds'('@+'(X0,X1),'@+'(X0,X2))))),
% 154.49/20.10 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 154.49/20.10 fof(f501,plain,(
% 154.49/20.10 ![X0,X1,X2]: (~nat_succeeds(X0)|~'@<_succeeds'(X1,X2)|'@<_succeeds'('@+'(X0,X1),'@+'(X0,X2))|~sQ2_spl)),
% 154.49/20.10 inference(component_clause,[status(thm)],[f500])).
% 154.49/20.10 fof(f503,plain,(
% 154.49/20.10 sQ0_spl|sQ1_spl|sQ2_spl),
% 154.49/20.10 inference(split_clause,[status(thm)],[f448,f494,f497,f500])).
% 154.49/20.10 fof(f504,definition,(
% 154.49/20.10 sQ3_spl <=> (nat_succeeds(sK38_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f505,plain,(
% 154.49/20.11 nat_succeeds(sK38_skl)|~sQ3_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f504])).
% 154.49/20.11 fof(f507,plain,(
% 154.49/20.11 sQ3_spl|sQ1_spl|sQ2_spl),
% 154.49/20.11 inference(split_clause,[status(thm)],[f449,f504,f497,f500])).
% 154.49/20.11 fof(f508,definition,(
% 154.49/20.11 ![X0,X1]: (sQ4_spl <=> (~'@<_succeeds'(X0,X1)|'@<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f509,plain,(
% 154.49/20.11 ![X0,X1]: (~'@<_succeeds'(X0,X1)|'@<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))|~sQ4_spl)),
% 154.49/20.11 inference(component_clause,[status(thm)],[f508])).
% 154.49/20.11 fof(f511,plain,(
% 154.49/20.11 sQ4_spl|sQ1_spl|sQ2_spl),
% 154.49/20.11 inference(split_clause,[status(thm)],[f450,f508,f497,f500])).
% 154.49/20.11 fof(f512,definition,(
% 154.49/20.11 sQ5_spl <=> ('@<_succeeds'(sK39_skl,sK40_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f513,plain,(
% 154.49/20.11 '@<_succeeds'(sK39_skl,sK40_skl)|~sQ5_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f512])).
% 154.49/20.11 fof(f515,plain,(
% 154.49/20.11 sQ5_spl|sQ2_spl),
% 154.49/20.11 inference(split_clause,[status(thm)],[f451,f512,f500])).
% 154.49/20.11 fof(f516,definition,(
% 154.49/20.11 sQ6_spl <=> ('@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f518,plain,(
% 154.49/20.11 ~'@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))|sQ6_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f516])).
% 154.49/20.11 fof(f519,plain,(
% 154.49/20.11 ~sQ6_spl|sQ2_spl),
% 154.49/20.11 inference(split_clause,[status(thm)],[f452,f516,f500])).
% 154.49/20.11 fof(f546,plain,(
% 154.49/20.11 ![X0,X1]: (sP4_prd(X0,X1,s(X0),s(X1))|~'@<_succeeds'(X1,X0))),
% 154.49/20.11 inference(destructive_equality_resolution,[status(thm)],[f487])).
% 154.49/20.11 fof(f571,plain,(
% 154.49/20.11 '@+'(sK41_skl,'0')=sK41_skl),
% 154.49/20.11 inference(resolution,[status(thm)],[f314,f455])).
% 154.49/20.11 fof(f575,plain,(
% 154.49/20.11 ![X0]: (~nat_succeeds(X0)|'@+'(X0,sK41_skl)='@+'(sK41_skl,X0))),
% 154.49/20.11 inference(resolution,[status(thm)],[f318,f455])).
% 154.49/20.11 fof(f585,plain,(
% 154.49/20.11 nat_succeeds(sK42_skl)),
% 154.49/20.11 inference(resolution,[status(thm)],[f373,f456])).
% 154.49/20.11 fof(f597,plain,(
% 154.49/20.11 ![X0]: (~'@<_succeeds'(X0,X0))),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f389,f373])).
% 154.49/20.11 fof(f688,plain,(
% 154.49/20.11 '@+'(sK42_skl,sK41_skl)='@+'(sK41_skl,sK42_skl)),
% 154.49/20.11 inference(resolution,[status(thm)],[f585,f575])).
% 154.49/20.11 fof(f2215,plain,(
% 154.49/20.11 ~'@<_succeeds'('@+'(sK42_skl,sK41_skl),'@+'(sK41_skl,sK43_skl))),
% 154.49/20.11 inference(backward_demodulation,[status(thm)],[f688,f457])).
% 154.49/20.11 fof(f2308,plain,(
% 154.49/20.11 ![X0,X1]: (~'@<_succeeds'(X0,X1)|'@<_succeeds'(s(X0),s(X1)))),
% 154.49/20.11 inference(resolution,[status(thm)],[f546,f218])).
% 154.49/20.11 fof(f5188,plain,(
% 154.49/20.11 ![X0,X1]: (~'@<_succeeds'(X0,X1)|'@<_succeeds'('@+'(sK41_skl,X0),'@+'(sK41_skl,X1))|~sQ2_spl)),
% 154.49/20.11 inference(resolution,[status(thm)],[f501,f455])).
% 154.49/20.11 fof(f5492,plain,(
% 154.49/20.11 ![X0]: ('@=<_terminates'(X0,sK41_skl))),
% 154.49/20.11 inference(resolution,[status(thm)],[f403,f455])).
% 154.49/20.11 fof(f5494,plain,(
% 154.49/20.11 ![X0]: ('@=<_terminates'(sK41_skl,X0))),
% 154.49/20.11 inference(resolution,[status(thm)],[f400,f455])).
% 154.49/20.11 fof(f5532,plain,(
% 154.49/20.11 ![X0]: ('@<_terminates'(X0,sK41_skl))),
% 154.49/20.11 inference(resolution,[status(thm)],[f370,f455])).
% 154.49/20.11 fof(f5534,plain,(
% 154.49/20.11 ![X0]: ('@<_terminates'(sK41_skl,X0))),
% 154.49/20.11 inference(resolution,[status(thm)],[f367,f455])).
% 154.49/20.11 fof(f10520,plain,(
% 154.49/20.11 '@<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl))|~sQ2_spl),
% 154.49/20.11 inference(resolution,[status(thm)],[f5188,f456])).
% 154.49/20.11 fof(f10527,plain,(
% 154.49/20.11 '@<_succeeds'('@+'(sK42_skl,sK41_skl),'@+'(sK41_skl,sK43_skl))|~sQ2_spl),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f688,f10520])).
% 154.49/20.11 fof(f10528,plain,(
% 154.49/20.11 $false|~sQ2_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f10527,f2215])).
% 154.49/20.11 fof(f10529,plain,(
% 154.49/20.11 ~sQ2_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f10528])).
% 154.49/20.11 fof(f10628,plain,(
% 154.49/20.11 ~'@<_succeeds'('@+'('0',sK39_skl),'@+'(sK37_skl,sK40_skl))|~sQ1_spl|sQ6_spl),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f498,f518])).
% 154.49/20.11 fof(f10629,plain,(
% 154.49/20.11 ~'@<_succeeds'(sK39_skl,'@+'(sK37_skl,sK40_skl))|~sQ1_spl|sQ6_spl),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f305,f10628])).
% 154.49/20.11 fof(f10630,plain,(
% 154.49/20.11 ~'@<_succeeds'(sK39_skl,'@+'('0',sK40_skl))|~sQ1_spl|sQ6_spl),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f498,f10629])).
% 154.49/20.11 fof(f10631,plain,(
% 154.49/20.11 ~'@<_succeeds'(sK39_skl,sK40_skl)|~sQ1_spl|sQ6_spl),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f305,f10630])).
% 154.49/20.11 fof(f10632,plain,(
% 154.49/20.11 $false|~sQ5_spl|~sQ1_spl|sQ6_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f10631,f513])).
% 154.49/20.11 fof(f10633,plain,(
% 154.49/20.11 ~sQ5_spl|~sQ1_spl|sQ6_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f10632])).
% 154.49/20.11 fof(f11741,plain,(
% 154.49/20.11 ![X0]: ('@+'(s(sK38_skl),X0)=s('@+'(sK38_skl,X0))|~sQ3_spl)),
% 154.49/20.11 inference(resolution,[status(thm)],[f505,f308])).
% 154.49/20.11 fof(f11937,plain,(
% 154.49/20.11 ![X0]: ('@+'(sK37_skl,X0)=s('@+'(sK38_skl,X0))|~sQ0_spl|~sQ3_spl)),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f495,f11741])).
% 154.49/20.11 fof(f11950,plain,(
% 154.49/20.11 '@<_succeeds'('@+'(sK38_skl,sK39_skl),'@+'(sK38_skl,sK40_skl))|~sQ4_spl|~sQ5_spl),
% 154.49/20.11 inference(resolution,[status(thm)],[f509,f513])).
% 154.49/20.11 fof(f19351,definition,(
% 154.49/20.11 ![X0]: (sQ164_spl <=> ('0'=s(sK0_skl('0',X0,'0'))))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f19352,plain,(
% 154.49/20.11 ![X0]: ('0'=s(sK0_skl('0',X0,'0'))|~sQ164_spl)),
% 154.49/20.11 inference(component_clause,[status(thm)],[f19351])).
% 154.49/20.11 fof(f19355,plain,(
% 154.49/20.11 $false|~sQ164_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f19352,f106])).
% 154.49/20.11 fof(f19356,plain,(
% 154.49/20.11 ~sQ164_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f19355])).
% 154.49/20.11 fof(f20216,definition,(
% 154.49/20.11 ![X0]: (sQ172_spl <=> ('0'=s(sK2_skl('0',X0,'0'))))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f20217,plain,(
% 154.49/20.11 ![X0]: ('0'=s(sK2_skl('0',X0,'0'))|~sQ172_spl)),
% 154.49/20.11 inference(component_clause,[status(thm)],[f20216])).
% 154.49/20.11 fof(f20220,plain,(
% 154.49/20.11 $false|~sQ172_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f20217,f106])).
% 154.49/20.11 fof(f20221,plain,(
% 154.49/20.11 ~sQ172_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f20220])).
% 154.49/20.11 fof(f20954,definition,(
% 154.49/20.11 sQ202_spl <=> ('0'=s(sK19_skl(sK43_skl,'0')))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f20955,plain,(
% 154.49/20.11 '0'=s(sK19_skl(sK43_skl,'0'))|~sQ202_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f20954])).
% 154.49/20.11 fof(f20962,plain,(
% 154.49/20.11 $false|~sQ202_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f20955,f106])).
% 154.49/20.11 fof(f20963,plain,(
% 154.49/20.11 ~sQ202_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f20962])).
% 154.49/20.11 fof(f21974,definition,(
% 154.49/20.11 sQ240_spl <=> ('@<_succeeds'('@+'('0',sK41_skl),sK41_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f21975,plain,(
% 154.49/20.11 '@<_succeeds'('@+'('0',sK41_skl),sK41_skl)|~sQ240_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f21974])).
% 154.49/20.11 fof(f21980,definition,(
% 154.49/20.11 sQ242_spl <=> ('@<_succeeds'(sK41_skl,'@+'('0',sK41_skl)))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ242_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f21981,plain,(
% 154.49/20.11 '@<_succeeds'(sK41_skl,'@+'('0',sK41_skl))|~sQ242_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f21980])).
% 154.49/20.11 fof(f22021,plain,(
% 154.49/20.11 '@<_succeeds'(sK41_skl,sK41_skl)|~sQ242_spl),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f305,f21981])).
% 154.49/20.11 fof(f22022,plain,(
% 154.49/20.11 $false|~sQ242_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f22021,f597])).
% 154.49/20.11 fof(f22023,plain,(
% 154.49/20.11 ~sQ242_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f22022])).
% 154.49/20.11 fof(f22024,plain,(
% 154.49/20.11 '@<_succeeds'(sK41_skl,sK41_skl)|~sQ240_spl),
% 154.49/20.11 inference(forward_demodulation,[status(thm)],[f305,f21975])).
% 154.49/20.11 fof(f22025,plain,(
% 154.49/20.11 $false|~sQ240_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f22024,f597])).
% 154.49/20.11 fof(f22026,plain,(
% 154.49/20.11 ~sQ240_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f22025])).
% 154.49/20.11 fof(f26013,definition,(
% 154.49/20.11 sQ380_spl <=> ('0'=s(sK19_skl(sK37_skl,'0')))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ380_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f26014,plain,(
% 154.49/20.11 '0'=s(sK19_skl(sK37_skl,'0'))|~sQ380_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f26013])).
% 154.49/20.11 fof(f26020,plain,(
% 154.49/20.11 $false|~sQ380_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f26014,f106])).
% 154.49/20.11 fof(f26021,plain,(
% 154.49/20.11 ~sQ380_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f26020])).
% 154.49/20.11 fof(f26425,definition,(
% 154.49/20.11 sQ389_spl <=> ('@<_terminates'(sK41_skl,sK37_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f26427,plain,(
% 154.49/20.11 ~'@<_terminates'(sK41_skl,sK37_skl)|sQ389_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f26425])).
% 154.49/20.11 fof(f26453,plain,(
% 154.49/20.11 $false|sQ389_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f26427,f5534])).
% 154.49/20.11 fof(f26454,plain,(
% 154.49/20.11 sQ389_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f26453])).
% 154.49/20.11 fof(f26469,definition,(
% 154.49/20.11 sQ397_spl <=> ('@<_terminates'(sK37_skl,sK41_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ397_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f26471,plain,(
% 154.49/20.11 ~'@<_terminates'(sK37_skl,sK41_skl)|sQ397_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f26469])).
% 154.49/20.11 fof(f26491,plain,(
% 154.49/20.11 $false|sQ397_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f26471,f5532])).
% 154.49/20.11 fof(f26492,plain,(
% 154.49/20.11 sQ397_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f26491])).
% 154.49/20.11 fof(f26984,definition,(
% 154.49/20.11 sQ405_spl <=> ('0'=s(sK22_skl(sK37_skl,'0')))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ405_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f26985,plain,(
% 154.49/20.11 '0'=s(sK22_skl(sK37_skl,'0'))|~sQ405_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f26984])).
% 154.49/20.11 fof(f26989,plain,(
% 154.49/20.11 $false|~sQ405_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f26985,f106])).
% 154.49/20.11 fof(f26990,plain,(
% 154.49/20.11 ~sQ405_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f26989])).
% 154.49/20.11 fof(f27005,definition,(
% 154.49/20.11 sQ406_spl <=> ('@=<_terminates'(sK41_skl,sK37_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f27007,plain,(
% 154.49/20.11 ~'@=<_terminates'(sK41_skl,sK37_skl)|sQ406_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f27005])).
% 154.49/20.11 fof(f27033,plain,(
% 154.49/20.11 $false|sQ406_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f27007,f5494])).
% 154.49/20.11 fof(f27034,plain,(
% 154.49/20.11 sQ406_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f27033])).
% 154.49/20.11 fof(f27049,definition,(
% 154.49/20.11 sQ414_spl <=> ('@=<_terminates'(sK37_skl,sK41_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ414_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f27051,plain,(
% 154.49/20.11 ~'@=<_terminates'(sK37_skl,sK41_skl)|sQ414_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f27049])).
% 154.49/20.11 fof(f27071,plain,(
% 154.49/20.11 $false|sQ414_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f27051,f5492])).
% 154.49/20.11 fof(f27072,plain,(
% 154.49/20.11 sQ414_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f27071])).
% 154.49/20.11 fof(f27890,definition,(
% 154.49/20.11 sQ443_spl <=> (sK37_skl=sK37_skl)),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f27892,plain,(
% 154.49/20.11 ~sK37_skl=sK37_skl|sQ443_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f27890])).
% 154.49/20.11 fof(f27911,plain,(
% 154.49/20.11 $false|sQ443_spl),
% 154.49/20.11 inference(trivial_equality_resolution,[status(thm)],[f27892])).
% 154.49/20.11 fof(f27912,plain,(
% 154.49/20.11 sQ443_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f27911])).
% 154.49/20.11 fof(f28191,definition,(
% 154.49/20.11 sQ449_spl <=> ('@<_succeeds'(sK38_skl,sK38_skl))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f28192,plain,(
% 154.49/20.11 '@<_succeeds'(sK38_skl,sK38_skl)|~sQ449_spl),
% 154.49/20.11 inference(component_clause,[status(thm)],[f28191])).
% 154.49/20.11 fof(f28196,plain,(
% 154.49/20.11 $false|~sQ449_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f28192,f597])).
% 154.49/20.11 fof(f28197,plain,(
% 154.49/20.11 ~sQ449_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f28196])).
% 154.49/20.11 fof(f31381,definition,(
% 154.49/20.11 ![X0]: (sQ484_spl <=> ('0'=s(sK22_skl('@+'(s(sK41_skl),X0),'0'))))),
% 154.49/20.11 introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition])).
% 154.49/20.11 fof(f31382,plain,(
% 154.49/20.11 ![X0]: ('0'=s(sK22_skl('@+'(s(sK41_skl),X0),'0'))|~sQ484_spl)),
% 154.49/20.11 inference(component_clause,[status(thm)],[f31381])).
% 154.49/20.11 fof(f31386,plain,(
% 154.49/20.11 $false|~sQ484_spl),
% 154.49/20.11 inference(forward_subsumption_resolution,[status(thm)],[f31382,f106])).
% 154.49/20.11 fof(f31387,plain,(
% 154.49/20.11 ~sQ484_spl),
% 154.49/20.11 inference(contradiction_clause,[status(thm)],[f31386])).
% 154.49/20.15 fof(f31794,definition,(
% 154.49/20.15 sQ495_spl <=> (nat_succeeds('@+'(sK41_skl,'0')))),
% 154.49/20.15 introduced(definition,[new_symbols(definition,[sQ495_spl])],[split_symbol_definition])).
% 154.49/20.15 fof(f31796,plain,(
% 154.49/20.15 ~nat_succeeds('@+'(sK41_skl,'0'))|sQ495_spl),
% 154.49/20.15 inference(component_clause,[status(thm)],[f31794])).
% 154.49/20.15 fof(f31815,plain,(
% 154.49/20.15 ~nat_succeeds(sK41_skl)|sQ495_spl),
% 154.49/20.15 inference(forward_demodulation,[status(thm)],[f571,f31796])).
% 154.49/20.15 fof(f31816,plain,(
% 154.49/20.15 $false|sQ495_spl),
% 154.49/20.15 inference(forward_subsumption_resolution,[status(thm)],[f31815,f455])).
% 154.49/20.15 fof(f31817,plain,(
% 154.49/20.15 sQ495_spl),
% 154.49/20.15 inference(contradiction_clause,[status(thm)],[f31816])).
% 154.49/20.15 fof(f32515,definition,(
% 154.49/20.15 sQ519_spl <=> ('0'=s(sK7_skl(sK43_skl,s(sK35_skl(sK43_skl,'0')),'0')))),
% 154.49/20.15 introduced(definition,[new_symbols(definition,[sQ519_spl])],[split_symbol_definition])).
% 154.49/20.15 fof(f32516,plain,(
% 154.49/20.15 '0'=s(sK7_skl(sK43_skl,s(sK35_skl(sK43_skl,'0')),'0'))|~sQ519_spl),
% 154.49/20.15 inference(component_clause,[status(thm)],[f32515])).
% 154.49/20.15 fof(f32526,plain,(
% 154.49/20.15 $false|~sQ519_spl),
% 154.49/20.15 inference(forward_subsumption_resolution,[status(thm)],[f32516,f106])).
% 154.49/20.15 fof(f32527,plain,(
% 154.49/20.15 ~sQ519_spl),
% 154.49/20.15 inference(contradiction_clause,[status(thm)],[f32526])).
% 154.49/20.15 fof(f35369,plain,(
% 154.49/20.15 '@<_succeeds'(s('@+'(sK38_skl,sK39_skl)),s('@+'(sK38_skl,sK40_skl)))|~sQ4_spl|~sQ5_spl),
% 154.49/20.15 inference(resolution,[status(thm)],[f11950,f2308])).
% 154.49/20.15 fof(f35399,plain,(
% 154.49/20.15 '@<_succeeds'('@+'(sK37_skl,sK39_skl),s('@+'(sK38_skl,sK40_skl)))|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 154.49/20.15 inference(forward_demodulation,[status(thm)],[f11937,f35369])).
% 154.49/20.15 fof(f35400,plain,(
% 154.49/20.15 '@<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 154.49/20.15 inference(forward_demodulation,[status(thm)],[f11937,f35399])).
% 154.49/20.15 fof(f35401,plain,(
% 154.49/20.15 $false|sQ6_spl|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 154.49/20.15 inference(forward_subsumption_resolution,[status(thm)],[f35400,f518])).
% 154.49/20.15 fof(f35402,plain,(
% 154.49/20.15 sQ6_spl|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 154.49/20.15 inference(contradiction_clause,[status(thm)],[f35401])).
% 154.49/20.15 fof(f35403,plain,(
% 154.49/20.15 $false),
% 154.49/20.15 inference(sat_refutation,[status(thm)],[f503,f507,f511,f515,f519,f10529,f10633,f19356,f20221,f20963,f22023,f22026,f26021,f26454,f26492,f26990,f27034,f27072,f27912,f28197,f31387,f31817,f32527,f35402])).
% 154.49/20.15 % SZS output end CNFRefutation for theBenchmark.p
% 8.04/20.30 % Elapsed time: 19.905272 seconds
% 8.04/20.30 % CPU time: 156.965027 seconds
% 8.04/20.30 % Total memory used: 767.397 MB
% 8.04/20.30 % Net memory used: 678.638 MB
%------------------------------------------------------------------------------