%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX033+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 : n009.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:34 PM UTC 2026
% Result : Theorem 21.75s 3.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX033+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.13/0.39 % Computer : n009.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Mon Sep 21 10:22:29 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 21.75/3.22 % Refutation found
% 21.75/3.22 % SZS status Theorem for theBenchmark: Theorem is valid
% 21.75/3.22 % SZS output start CNFRefutation for theBenchmark
% 21.75/3.22 fof(f1,axiom,(
% 21.75/3.22 (! [Xx3] : '0' != s(Xx3) )),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f2,axiom,(
% 21.75/3.22 (! [Xx4,Xx5] :( s(Xx4) = s(Xx5)=> Xx4 = Xx5 ) )),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f3,axiom,(
% 21.75/3.22 gr('0') ),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f27,axiom,(
% 21.75/3.22 (! [Xx1] :( nat_succeeds(Xx1)<=> ( (? [Xx2] :( Xx1 = s(Xx2)& nat_succeeds(Xx2) ))| Xx1 = '0' ) ) )),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f45,axiom,(
% 21.75/3.22 (! [Xy] : '@+'('0',Xy) = Xy )),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f46,axiom,(
% 21.75/3.22 (! [Xx,Xy] :( nat_succeeds(Xx)=> '@+'(s(Xx),Xy) = s('@+'(Xx,Xy)) ) )),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f47,axiom,(
% 21.75/3.22 (! [Xx,Xy] :( ( nat_succeeds(Xx)& nat_succeeds(Xy) )=> nat_succeeds('@+'(Xx,Xy)) ) )),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f52,axiom,(
% 21.75/3.22 ( (! [Xx] :( ( (? [Xx2] :( Xx = s(Xx2)& nat_succeeds(Xx2)& (! [Xy,Xz] :( '@+'(Xx2,Xy) = '@+'(Xx2,Xz)=> Xy = Xz ) )))| Xx = '0' )=> (! [Xy,Xz] :( '@+'(Xx,Xy) = '@+'(Xx,Xz)=> Xy = Xz ) )))=> (! [Xx] :( nat_succeeds(Xx)=> (! [Xy,Xz] :( '@+'(Xx,Xy) = '@+'(Xx,Xz)=> Xy = Xz ) )) )) ),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f53,conjecture,(
% 21.75/3.22 (! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& '@+'(Xx,Xy) = '@+'(Xx,Xz) )=> Xy = Xz ) )),
% 21.75/3.22 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.75/3.22 fof(f54,negated_conjecture,(
% 21.75/3.22 ~((! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& '@+'(Xx,Xy) = '@+'(Xx,Xz) )=> Xy = Xz ) ))),
% 21.75/3.22 inference(negated_conjecture,[status(cth)],[f53])).
% 21.75/3.22 fof(f55,plain,(
% 21.75/3.22 ![X0]: (~'0'=s(X0))),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f1])).
% 21.75/3.22 fof(f56,plain,(
% 21.75/3.22 ![Xx4,Xx5]: (~s(Xx4)=s(Xx5)|Xx4=Xx5)),
% 21.75/3.22 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 21.75/3.22 fof(f57,plain,(
% 21.75/3.22 ![X0,X1]: (~s(X0)=s(X1)|X0=X1)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f56])).
% 21.75/3.22 fof(f58,plain,(
% 21.75/3.22 gr('0')),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f3])).
% 21.75/3.22 fof(f186,plain,(
% 21.75/3.22 ![Xx1]: ((~nat_succeeds(Xx1)|((?[Xx2]: (Xx1=s(Xx2)&nat_succeeds(Xx2)))|Xx1='0'))&(nat_succeeds(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|~nat_succeeds(Xx2)))&~Xx1='0')))),
% 21.75/3.22 inference(NNF_transformation,[status(thm)],[f27])).
% 21.75/3.22 fof(f187,plain,(
% 21.75/3.22 (![Xx1]: (~nat_succeeds(Xx1)|((?[Xx2]: (Xx1=s(Xx2)&nat_succeeds(Xx2)))|Xx1='0')))&(![Xx1]: (nat_succeeds(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|~nat_succeeds(Xx2)))&~Xx1='0')))),
% 21.75/3.22 inference(miniscoping,[status(thm)],[f186])).
% 21.75/3.22 fof(f188,plain,(
% 21.75/3.22 (![Xx1]: (~nat_succeeds(Xx1)|((Xx1=s(sK27_skl(Xx1))&nat_succeeds(sK27_skl(Xx1)))|Xx1='0')))&(![Xx1]: (nat_succeeds(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|~nat_succeeds(Xx2)))&~Xx1='0')))),
% 21.75/3.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(Xx2,sK27_skl(Xx1))],[f187])).
% 21.75/3.22 fof(f191,plain,(
% 21.75/3.22 ![X0,X1]: (nat_succeeds(X0)|~X0=s(X1)|~nat_succeeds(X1))),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f188])).
% 21.75/3.22 fof(f192,plain,(
% 21.75/3.22 ![X0]: (nat_succeeds(X0)|~X0='0')),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f188])).
% 21.75/3.22 fof(f254,plain,(
% 21.75/3.22 ![X0]: ('@+'('0',X0)=X0)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f45])).
% 21.75/3.22 fof(f255,plain,(
% 21.75/3.22 ![Xx,Xy]: (~nat_succeeds(Xx)|'@+'(s(Xx),Xy)=s('@+'(Xx,Xy)))),
% 21.75/3.22 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 21.75/3.22 fof(f256,plain,(
% 21.75/3.22 ![Xx]: (~nat_succeeds(Xx)|(![Xy]: '@+'(s(Xx),Xy)=s('@+'(Xx,Xy))))),
% 21.75/3.22 inference(miniscoping,[status(thm)],[f255])).
% 21.75/3.22 fof(f257,plain,(
% 21.75/3.22 ![X0,X1]: (~nat_succeeds(X0)|'@+'(s(X0),X1)=s('@+'(X0,X1)))),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f256])).
% 21.75/3.22 fof(f258,plain,(
% 21.75/3.22 ![Xx,Xy]: ((~nat_succeeds(Xx)|~nat_succeeds(Xy))|nat_succeeds('@+'(Xx,Xy)))),
% 21.75/3.22 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 21.75/3.22 fof(f259,plain,(
% 21.75/3.22 ![X0,X1]: (~nat_succeeds(X0)|~nat_succeeds(X1)|nat_succeeds('@+'(X0,X1)))),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f258])).
% 21.75/3.22 fof(f268,plain,(
% 21.75/3.22 (?[Xx]: (((?[Xx2]: ((Xx=s(Xx2)&nat_succeeds(Xx2))&(![Xy,Xz]: (~'@+'(Xx2,Xy)='@+'(Xx2,Xz)|Xy=Xz))))|Xx='0')&(?[Xy,Xz]: ('@+'(Xx,Xy)='@+'(Xx,Xz)&~Xy=Xz))))|(![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: (~'@+'(Xx,Xy)='@+'(Xx,Xz)|Xy=Xz))))),
% 21.75/3.22 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 21.75/3.22 fof(f269,plain,(
% 21.75/3.22 ((((sK31_skl=s(sK32_skl)&nat_succeeds(sK32_skl))&(![Xy,Xz]: (~'@+'(sK32_skl,Xy)='@+'(sK32_skl,Xz)|Xy=Xz)))|sK31_skl='0')&('@+'(sK31_skl,sK33_skl)='@+'(sK31_skl,sK34_skl)&~sK33_skl=sK34_skl))|(![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: (~'@+'(Xx,Xy)='@+'(Xx,Xz)|Xy=Xz))))),
% 21.75/3.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl,sK33_skl,sK34_skl]),skolemize(Xx,sK31_skl),skolemize(Xx2,sK32_skl),skolemize(Xy,sK33_skl),skolemize(Xz,sK34_skl)],[f268])).
% 21.75/3.22 fof(f270,plain,(
% 21.75/3.22 ![X0,X1,X2]: (sK31_skl=s(sK32_skl)|sK31_skl='0'|~nat_succeeds(X0)|~'@+'(X0,X1)='@+'(X0,X2)|X1=X2)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f269])).
% 21.75/3.22 fof(f271,plain,(
% 21.75/3.22 ![X0,X1,X2]: (nat_succeeds(sK32_skl)|sK31_skl='0'|~nat_succeeds(X0)|~'@+'(X0,X1)='@+'(X0,X2)|X1=X2)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f269])).
% 21.75/3.22 fof(f272,plain,(
% 21.75/3.22 ![X0,X1,X2,X3,X4]: (~'@+'(sK32_skl,X0)='@+'(sK32_skl,X1)|X0=X1|sK31_skl='0'|~nat_succeeds(X2)|~'@+'(X2,X3)='@+'(X2,X4)|X3=X4)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f269])).
% 21.75/3.22 fof(f273,plain,(
% 21.75/3.22 ![X0,X1,X2]: ('@+'(sK31_skl,sK33_skl)='@+'(sK31_skl,sK34_skl)|~nat_succeeds(X0)|~'@+'(X0,X1)='@+'(X0,X2)|X1=X2)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f269])).
% 21.75/3.22 fof(f274,plain,(
% 21.75/3.22 ![X0,X1,X2]: (~sK33_skl=sK34_skl|~nat_succeeds(X0)|~'@+'(X0,X1)='@+'(X0,X2)|X1=X2)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f269])).
% 21.75/3.22 fof(f275,plain,(
% 21.75/3.22 (?[Xx,Xy,Xz]: ((nat_succeeds(Xx)&'@+'(Xx,Xy)='@+'(Xx,Xz))&~Xy=Xz))),
% 21.75/3.22 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 21.75/3.22 fof(f276,plain,(
% 21.75/3.22 ?[Xy,Xz]: ((?[Xx]: (nat_succeeds(Xx)&'@+'(Xx,Xy)='@+'(Xx,Xz)))&~Xy=Xz)),
% 21.75/3.22 inference(miniscoping,[status(thm)],[f275])).
% 21.75/3.22 fof(f277,plain,(
% 21.75/3.22 ((nat_succeeds(sK37_skl)&'@+'(sK37_skl,sK35_skl)='@+'(sK37_skl,sK36_skl))&~sK35_skl=sK36_skl)),
% 21.75/3.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl,sK36_skl,sK37_skl]),skolemize(Xy,sK35_skl),skolemize(Xz,sK36_skl),skolemize(Xx,sK37_skl)],[f276])).
% 21.75/3.22 fof(f278,plain,(
% 21.75/3.22 nat_succeeds(sK37_skl)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f277])).
% 21.75/3.22 fof(f279,plain,(
% 21.75/3.22 '@+'(sK37_skl,sK35_skl)='@+'(sK37_skl,sK36_skl)),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f277])).
% 21.75/3.22 fof(f280,plain,(
% 21.75/3.22 ~sK35_skl=sK36_skl),
% 21.75/3.22 inference(cnf_transformation,[status(thm)],[f277])).
% 21.75/3.22 fof(f317,definition,(
% 21.75/3.22 sQ0_spl <=> (sK31_skl=s(sK32_skl))),
% 21.75/3.22 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 21.75/3.22 fof(f318,plain,(
% 21.75/3.22 sK31_skl=s(sK32_skl)|~sQ0_spl),
% 21.75/3.22 inference(component_clause,[status(thm)],[f317])).
% 21.75/3.22 fof(f320,definition,(
% 21.75/3.22 sQ1_spl <=> (sK31_skl='0')),
% 21.75/3.22 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 21.75/3.22 fof(f321,plain,(
% 21.75/3.22 sK31_skl='0'|~sQ1_spl),
% 21.75/3.22 inference(component_clause,[status(thm)],[f320])).
% 21.75/3.22 fof(f323,definition,(
% 21.75/3.22 ![X0,X1,X2]: (sQ2_spl <=> (~nat_succeeds(X0)|~'@+'(X0,X1)='@+'(X0,X2)|X1=X2))),
% 21.75/3.22 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f324,plain,(
% 21.75/3.23 ![X0,X1,X2]: (~nat_succeeds(X0)|~'@+'(X0,X1)='@+'(X0,X2)|X1=X2|~sQ2_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f323])).
% 21.75/3.23 fof(f326,plain,(
% 21.75/3.23 sQ0_spl|sQ1_spl|sQ2_spl),
% 21.75/3.23 inference(split_clause,[status(thm)],[f270,f317,f320,f323])).
% 21.75/3.23 fof(f327,definition,(
% 21.75/3.23 sQ3_spl <=> (nat_succeeds(sK32_skl))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f328,plain,(
% 21.75/3.23 nat_succeeds(sK32_skl)|~sQ3_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f327])).
% 21.75/3.23 fof(f330,plain,(
% 21.75/3.23 sQ3_spl|sQ1_spl|sQ2_spl),
% 21.75/3.23 inference(split_clause,[status(thm)],[f271,f327,f320,f323])).
% 21.75/3.23 fof(f331,definition,(
% 21.75/3.23 ![X0,X1]: (sQ4_spl <=> (~'@+'(sK32_skl,X0)='@+'(sK32_skl,X1)|X0=X1))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f332,plain,(
% 21.75/3.23 ![X0,X1]: (~'@+'(sK32_skl,X0)='@+'(sK32_skl,X1)|X0=X1|~sQ4_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f331])).
% 21.75/3.23 fof(f334,plain,(
% 21.75/3.23 sQ4_spl|sQ1_spl|sQ2_spl),
% 21.75/3.23 inference(split_clause,[status(thm)],[f272,f331,f320,f323])).
% 21.75/3.23 fof(f335,definition,(
% 21.75/3.23 sQ5_spl <=> ('@+'(sK31_skl,sK33_skl)='@+'(sK31_skl,sK34_skl))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f336,plain,(
% 21.75/3.23 '@+'(sK31_skl,sK33_skl)='@+'(sK31_skl,sK34_skl)|~sQ5_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f335])).
% 21.75/3.23 fof(f338,plain,(
% 21.75/3.23 sQ5_spl|sQ2_spl),
% 21.75/3.23 inference(split_clause,[status(thm)],[f273,f335,f323])).
% 21.75/3.23 fof(f339,definition,(
% 21.75/3.23 sQ6_spl <=> (sK33_skl=sK34_skl)),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f341,plain,(
% 21.75/3.23 ~sK33_skl=sK34_skl|sQ6_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f339])).
% 21.75/3.23 fof(f342,plain,(
% 21.75/3.23 ~sQ6_spl|sQ2_spl),
% 21.75/3.23 inference(split_clause,[status(thm)],[f274,f339,f323])).
% 21.75/3.23 fof(f358,plain,(
% 21.75/3.23 ![X0]: (nat_succeeds(s(X0))|~nat_succeeds(X0))),
% 21.75/3.23 inference(destructive_equality_resolution,[status(thm)],[f191])).
% 21.75/3.23 fof(f359,plain,(
% 21.75/3.23 nat_succeeds('0')),
% 21.75/3.23 inference(destructive_equality_resolution,[status(thm)],[f192])).
% 21.75/3.23 fof(f373,plain,(
% 21.75/3.23 ![X0,X1]: (~nat_succeeds(X0)|nat_succeeds('@+'(X0,s(X1)))|~nat_succeeds(X1))),
% 21.75/3.23 inference(resolution,[status(thm)],[f259,f358])).
% 21.75/3.23 fof(f418,plain,(
% 21.75/3.23 ![X0]: (~nat_succeeds(X0)|nat_succeeds('@+'(X0,s(sK37_skl))))),
% 21.75/3.23 inference(resolution,[status(thm)],[f373,f278])).
% 21.75/3.23 fof(f533,definition,(
% 21.75/3.23 sQ9_spl <=> (nat_succeeds(sK37_skl))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f535,plain,(
% 21.75/3.23 ~nat_succeeds(sK37_skl)|sQ9_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f533])).
% 21.75/3.23 fof(f767,plain,(
% 21.75/3.23 ![X0,X1]: (~'@+'(sK37_skl,X0)='@+'(sK37_skl,X1)|X0=X1|~sQ2_spl)),
% 21.75/3.23 inference(resolution,[status(thm)],[f324,f278])).
% 21.75/3.23 fof(f777,plain,(
% 21.75/3.23 sK35_skl=sK36_skl|~sQ2_spl),
% 21.75/3.23 inference(resolution,[status(thm)],[f767,f279])).
% 21.75/3.23 fof(f784,plain,(
% 21.75/3.23 $false|~sQ2_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f777,f280])).
% 21.75/3.23 fof(f785,plain,(
% 21.75/3.23 ~sQ2_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f784])).
% 21.75/3.23 fof(f925,plain,(
% 21.75/3.23 '@+'('0',sK33_skl)='@+'(sK31_skl,sK34_skl)|~sQ1_spl|~sQ5_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f321,f336])).
% 21.75/3.23 fof(f926,plain,(
% 21.75/3.23 sK33_skl='@+'(sK31_skl,sK34_skl)|~sQ1_spl|~sQ5_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f254,f925])).
% 21.75/3.23 fof(f927,plain,(
% 21.75/3.23 sK33_skl='@+'('0',sK34_skl)|~sQ1_spl|~sQ5_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f321,f926])).
% 21.75/3.23 fof(f928,plain,(
% 21.75/3.23 sK33_skl=sK34_skl|~sQ1_spl|~sQ5_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f254,f927])).
% 21.75/3.23 fof(f998,plain,(
% 21.75/3.23 ~sK34_skl=sK34_skl|~sQ1_spl|~sQ5_spl|sQ6_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f928,f341])).
% 21.75/3.23 fof(f999,plain,(
% 21.75/3.23 $false|~sQ1_spl|~sQ5_spl|sQ6_spl),
% 21.75/3.23 inference(trivial_equality_resolution,[status(thm)],[f998])).
% 21.75/3.23 fof(f1000,plain,(
% 21.75/3.23 ~sQ1_spl|~sQ5_spl|sQ6_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f999])).
% 21.75/3.23 fof(f1074,plain,(
% 21.75/3.23 ![X0]: ('@+'(s(sK32_skl),X0)=s('@+'(sK32_skl,X0))|~sQ3_spl)),
% 21.75/3.23 inference(resolution,[status(thm)],[f328,f257])).
% 21.75/3.23 fof(f1217,plain,(
% 21.75/3.23 ![X0,X1]: (~s(X0)='@+'(s(sK32_skl),X1)|X0='@+'(sK32_skl,X1)|~sQ3_spl)),
% 21.75/3.23 inference(paramodulation,[status(thm)],[f1074,f57])).
% 21.75/3.23 fof(f1300,definition,(
% 21.75/3.23 sQ28_spl <=> (sK37_skl='0')),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f1301,plain,(
% 21.75/3.23 sK37_skl='0'|~sQ28_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f1300])).
% 21.75/3.23 fof(f1370,plain,(
% 21.75/3.23 $false|sQ9_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f535,f278])).
% 21.75/3.23 fof(f1371,plain,(
% 21.75/3.23 sQ9_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f1370])).
% 21.75/3.23 fof(f1432,plain,(
% 21.75/3.23 '@+'(sK37_skl,sK35_skl)='@+'('0',sK36_skl)|~sQ28_spl),
% 21.75/3.23 inference(backward_demodulation,[status(thm)],[f1301,f279])).
% 21.75/3.23 fof(f1548,plain,(
% 21.75/3.23 '@+'('0',sK35_skl)='@+'('0',sK36_skl)|~sQ28_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f1301,f1432])).
% 21.75/3.23 fof(f1549,plain,(
% 21.75/3.23 sK35_skl='@+'('0',sK36_skl)|~sQ28_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f254,f1548])).
% 21.75/3.23 fof(f1550,plain,(
% 21.75/3.23 sK35_skl=sK36_skl|~sQ28_spl),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f254,f1549])).
% 21.75/3.23 fof(f1551,plain,(
% 21.75/3.23 $false|~sQ28_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f1550,f280])).
% 21.75/3.23 fof(f1552,plain,(
% 21.75/3.23 ~sQ28_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f1551])).
% 21.75/3.23 fof(f1756,definition,(
% 21.75/3.23 sQ40_spl <=> (nat_succeeds('0'))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f1758,plain,(
% 21.75/3.23 ~nat_succeeds('0')|sQ40_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f1756])).
% 21.75/3.23 fof(f1763,plain,(
% 21.75/3.23 $false|sQ40_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f1758,f359])).
% 21.75/3.23 fof(f1764,plain,(
% 21.75/3.23 sQ40_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f1763])).
% 21.75/3.23 fof(f2209,definition,(
% 21.75/3.23 sQ52_spl <=> (gr('0'))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f2211,plain,(
% 21.75/3.23 ~gr('0')|sQ52_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f2209])).
% 21.75/3.23 fof(f2235,definition,(
% 21.75/3.23 sQ56_spl <=> ('@+'(sK37_skl,s(sK37_skl))='@+'(sK37_skl,s(sK37_skl)))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f2237,plain,(
% 21.75/3.23 ~'@+'(sK37_skl,s(sK37_skl))='@+'(sK37_skl,s(sK37_skl))|sQ56_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f2235])).
% 21.75/3.23 fof(f2242,plain,(
% 21.75/3.23 $false|sQ56_spl),
% 21.75/3.23 inference(trivial_equality_resolution,[status(thm)],[f2237])).
% 21.75/3.23 fof(f2243,plain,(
% 21.75/3.23 sQ56_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f2242])).
% 21.75/3.23 fof(f2383,definition,(
% 21.75/3.23 sQ63_spl <=> (s(sK37_skl)=s(sK37_skl))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f2385,plain,(
% 21.75/3.23 ~s(sK37_skl)=s(sK37_skl)|sQ63_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f2383])).
% 21.75/3.23 fof(f2394,plain,(
% 21.75/3.23 $false|sQ63_spl),
% 21.75/3.23 inference(trivial_equality_resolution,[status(thm)],[f2385])).
% 21.75/3.23 fof(f2395,plain,(
% 21.75/3.23 sQ63_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f2394])).
% 21.75/3.23 fof(f2587,plain,(
% 21.75/3.23 ![X0]: ('@+'(sK31_skl,X0)=s('@+'(sK32_skl,X0))|~sQ0_spl|~sQ3_spl)),
% 21.75/3.23 inference(forward_demodulation,[status(thm)],[f318,f1074])).
% 21.75/3.23 fof(f2896,definition,(
% 21.75/3.23 sQ80_spl <=> (s('0')='0')),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f2897,plain,(
% 21.75/3.23 s('0')='0'|~sQ80_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f2896])).
% 21.75/3.23 fof(f2908,plain,(
% 21.75/3.23 $false|~sQ80_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f2897,f55])).
% 21.75/3.23 fof(f2909,plain,(
% 21.75/3.23 ~sQ80_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f2908])).
% 21.75/3.23 fof(f3187,definition,(
% 21.75/3.23 sQ94_spl <=> ('@+'(sK37_skl,sK32_skl)='@+'(sK37_skl,sK32_skl))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f3189,plain,(
% 21.75/3.23 ~'@+'(sK37_skl,sK32_skl)='@+'(sK37_skl,sK32_skl)|sQ94_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f3187])).
% 21.75/3.23 fof(f3194,plain,(
% 21.75/3.23 $false|sQ94_spl),
% 21.75/3.23 inference(trivial_equality_resolution,[status(thm)],[f3189])).
% 21.75/3.23 fof(f3195,plain,(
% 21.75/3.23 sQ94_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f3194])).
% 21.75/3.23 fof(f3431,definition,(
% 21.75/3.23 sQ106_spl <=> (nat_succeeds('@+'(sK37_skl,s(sK37_skl))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f3433,plain,(
% 21.75/3.23 ~nat_succeeds('@+'(sK37_skl,s(sK37_skl)))|sQ106_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f3431])).
% 21.75/3.23 fof(f3893,definition,(
% 21.75/3.23 sQ136_spl <=> ('@+'(sK37_skl,sK31_skl)='@+'(sK37_skl,sK31_skl))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f3895,plain,(
% 21.75/3.23 ~'@+'(sK37_skl,sK31_skl)='@+'(sK37_skl,sK31_skl)|sQ136_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f3893])).
% 21.75/3.23 fof(f3921,plain,(
% 21.75/3.23 $false|sQ136_spl),
% 21.75/3.23 inference(trivial_equality_resolution,[status(thm)],[f3895])).
% 21.75/3.23 fof(f3922,plain,(
% 21.75/3.23 sQ136_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f3921])).
% 21.75/3.23 fof(f3951,definition,(
% 21.75/3.23 ![X0]: (sQ144_spl <=> ('0'=s(sK0_skl('0',X0,'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f3952,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK0_skl('0',X0,'0'))|~sQ144_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f3951])).
% 21.75/3.23 fof(f3955,plain,(
% 21.75/3.23 $false|~sQ144_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f3952,f55])).
% 21.75/3.23 fof(f3956,plain,(
% 21.75/3.23 ~sQ144_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f3955])).
% 21.75/3.23 fof(f4085,definition,(
% 21.75/3.23 ![X0]: (sQ151_spl <=> ('0'=s(sK2_skl('0',X0,'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f4086,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK2_skl('0',X0,'0'))|~sQ151_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f4085])).
% 21.75/3.23 fof(f4089,plain,(
% 21.75/3.23 $false|~sQ151_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f4086,f55])).
% 21.75/3.23 fof(f4090,plain,(
% 21.75/3.23 ~sQ151_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f4089])).
% 21.75/3.23 fof(f4222,definition,(
% 21.75/3.23 ![X0]: (sQ170_spl <=> ('0'=s(sK7_skl(sK30_skl(X0,'0'),X0,'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f4223,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK7_skl(sK30_skl(X0,'0'),X0,'0'))|~sQ170_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f4222])).
% 21.75/3.23 fof(f4226,definition,(
% 21.75/3.23 ![X0]: (sQ171_spl <=> ('0'=s(sK7_skl(X0,X0,'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f4227,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK7_skl(X0,X0,'0'))|~sQ171_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f4226])).
% 21.75/3.23 fof(f4230,plain,(
% 21.75/3.23 $false|~sQ171_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f4227,f55])).
% 21.75/3.23 fof(f4231,plain,(
% 21.75/3.23 ~sQ171_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f4230])).
% 21.75/3.23 fof(f4232,plain,(
% 21.75/3.23 $false|~sQ170_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f4223,f55])).
% 21.75/3.23 fof(f4233,plain,(
% 21.75/3.23 ~sQ170_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f4232])).
% 21.75/3.23 fof(f4974,definition,(
% 21.75/3.23 ![X0]: (sQ236_spl <=> ('0'=s(sK9_skl(X0,X0,'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f4975,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK9_skl(X0,X0,'0'))|~sQ236_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f4974])).
% 21.75/3.23 fof(f4978,plain,(
% 21.75/3.23 $false|~sQ236_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f4975,f55])).
% 21.75/3.23 fof(f4979,plain,(
% 21.75/3.23 ~sQ236_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f4978])).
% 21.75/3.23 fof(f5182,definition,(
% 21.75/3.23 ![X0]: (sQ247_spl <=> ('0'=s(sK19_skl(s(X0),'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ247_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f5183,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK19_skl(s(X0),'0'))|~sQ247_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f5182])).
% 21.75/3.23 fof(f5186,plain,(
% 21.75/3.23 $false|~sQ247_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f5183,f55])).
% 21.75/3.23 fof(f5187,plain,(
% 21.75/3.23 ~sQ247_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f5186])).
% 21.75/3.23 fof(f5367,definition,(
% 21.75/3.23 ![X0]: (sQ255_spl <=> ('0'=s(sK22_skl(s(X0),'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f5368,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK22_skl(s(X0),'0'))|~sQ255_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f5367])).
% 21.75/3.23 fof(f5371,plain,(
% 21.75/3.23 $false|~sQ255_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f5368,f55])).
% 21.75/3.23 fof(f5372,plain,(
% 21.75/3.23 ~sQ255_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f5371])).
% 21.75/3.23 fof(f5402,definition,(
% 21.75/3.23 ![X0]: (sQ259_spl <=> ('0'=s(sK19_skl('@+'(s(sK37_skl),X0),'0'))))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f5403,plain,(
% 21.75/3.23 ![X0]: ('0'=s(sK19_skl('@+'(s(sK37_skl),X0),'0'))|~sQ259_spl)),
% 21.75/3.23 inference(component_clause,[status(thm)],[f5402])).
% 21.75/3.23 fof(f5407,plain,(
% 21.75/3.23 $false|~sQ259_spl),
% 21.75/3.23 inference(forward_subsumption_resolution,[status(thm)],[f5403,f55])).
% 21.75/3.23 fof(f5408,plain,(
% 21.75/3.23 ~sQ259_spl),
% 21.75/3.23 inference(contradiction_clause,[status(thm)],[f5407])).
% 21.75/3.23 fof(f6645,definition,(
% 21.75/3.23 sQ336_spl <=> ('0'=s(sK22_skl(sK31_skl,'0')))),
% 21.75/3.23 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 21.75/3.23 fof(f6646,plain,(
% 21.75/3.23 '0'=s(sK22_skl(sK31_skl,'0'))|~sQ336_spl),
% 21.75/3.23 inference(component_clause,[status(thm)],[f6645])).
% 21.75/3.23 fof(f6650,plain,(
% 21.75/3.23 $false|~sQ336_spl),
% 21.75/3.26 inference(forward_subsumption_resolution,[status(thm)],[f6646,f55])).
% 21.75/3.26 fof(f6651,plain,(
% 21.75/3.26 ~sQ336_spl),
% 21.75/3.26 inference(contradiction_clause,[status(thm)],[f6650])).
% 21.75/3.26 fof(f6980,definition,(
% 21.75/3.26 sQ374_spl <=> (sK31_skl=sK31_skl)),
% 21.75/3.26 introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition])).
% 21.75/3.26 fof(f6982,plain,(
% 21.75/3.26 ~sK31_skl=sK31_skl|sQ374_spl),
% 21.75/3.26 inference(component_clause,[status(thm)],[f6980])).
% 21.75/3.26 fof(f7005,plain,(
% 21.75/3.26 $false|sQ374_spl),
% 21.75/3.26 inference(trivial_equality_resolution,[status(thm)],[f6982])).
% 21.75/3.26 fof(f7006,plain,(
% 21.75/3.26 sQ374_spl),
% 21.75/3.26 inference(contradiction_clause,[status(thm)],[f7005])).
% 21.75/3.26 fof(f7911,plain,(
% 21.75/3.26 $false|sQ52_spl),
% 21.75/3.26 inference(forward_subsumption_resolution,[status(thm)],[f2211,f58])).
% 21.75/3.26 fof(f7912,plain,(
% 21.75/3.26 sQ52_spl),
% 21.75/3.26 inference(contradiction_clause,[status(thm)],[f7911])).
% 21.75/3.26 fof(f8538,plain,(
% 21.75/3.26 ![X0,X1]: (~s(X0)='@+'(sK31_skl,X1)|X0='@+'(sK32_skl,X1)|~sQ0_spl|~sQ3_spl)),
% 21.75/3.26 inference(forward_demodulation,[status(thm)],[f318,f1217])).
% 21.75/3.26 fof(f8544,plain,(
% 21.75/3.26 ![X0,X1]: (~'@+'(sK31_skl,X0)='@+'(sK31_skl,X1)|'@+'(sK32_skl,X0)='@+'(sK32_skl,X1)|~sQ0_spl|~sQ3_spl)),
% 21.75/3.26 inference(paramodulation,[status(thm)],[f2587,f8538])).
% 21.75/3.26 fof(f8571,definition,(
% 21.75/3.26 sQ473_spl <=> ('0'=s(sK22_skl(sK37_skl,'0')))),
% 21.75/3.26 introduced(definition,[new_symbols(definition,[sQ473_spl])],[split_symbol_definition])).
% 21.75/3.26 fof(f8572,plain,(
% 21.75/3.26 '0'=s(sK22_skl(sK37_skl,'0'))|~sQ473_spl),
% 21.75/3.26 inference(component_clause,[status(thm)],[f8571])).
% 21.75/3.26 fof(f8576,plain,(
% 21.75/3.26 $false|~sQ473_spl),
% 21.75/3.26 inference(forward_subsumption_resolution,[status(thm)],[f8572,f55])).
% 21.75/3.26 fof(f8577,plain,(
% 21.75/3.26 ~sQ473_spl),
% 21.75/3.26 inference(contradiction_clause,[status(thm)],[f8576])).
% 21.75/3.26 fof(f9585,plain,(
% 21.75/3.26 nat_succeeds('@+'(sK37_skl,s(sK37_skl)))),
% 21.75/3.26 inference(resolution,[status(thm)],[f418,f278])).
% 21.75/3.26 fof(f9590,plain,(
% 21.75/3.26 $false|sQ106_spl),
% 21.75/3.26 inference(forward_subsumption_resolution,[status(thm)],[f9585,f3433])).
% 21.75/3.26 fof(f9591,plain,(
% 21.75/3.26 sQ106_spl),
% 21.75/3.26 inference(contradiction_clause,[status(thm)],[f9590])).
% 21.75/3.26 fof(f13380,plain,(
% 21.75/3.26 '@+'(sK32_skl,sK33_skl)='@+'(sK32_skl,sK34_skl)|~sQ0_spl|~sQ3_spl|~sQ5_spl),
% 21.75/3.26 inference(resolution,[status(thm)],[f8544,f336])).
% 21.75/3.26 fof(f13515,definition,(
% 21.75/3.26 sQ869_spl <=> (s(sK37_skl)='0')),
% 21.75/3.26 introduced(definition,[new_symbols(definition,[sQ869_spl])],[split_symbol_definition])).
% 21.75/3.26 fof(f13516,plain,(
% 21.75/3.26 s(sK37_skl)='0'|~sQ869_spl),
% 21.75/3.26 inference(component_clause,[status(thm)],[f13515])).
% 21.75/3.26 fof(f13528,plain,(
% 21.75/3.26 $false|~sQ869_spl),
% 21.75/3.26 inference(forward_subsumption_resolution,[status(thm)],[f13516,f55])).
% 21.75/3.26 fof(f13529,plain,(
% 21.75/3.26 ~sQ869_spl),
% 21.75/3.26 inference(contradiction_clause,[status(thm)],[f13528])).
% 21.75/3.26 fof(f15641,plain,(
% 21.75/3.26 sK33_skl=sK34_skl|~sQ0_spl|~sQ3_spl|~sQ5_spl|~sQ4_spl),
% 21.75/3.26 inference(resolution,[status(thm)],[f13380,f332])).
% 21.75/3.26 fof(f15662,plain,(
% 21.75/3.26 $false|sQ6_spl|~sQ0_spl|~sQ3_spl|~sQ5_spl|~sQ4_spl),
% 21.75/3.26 inference(forward_subsumption_resolution,[status(thm)],[f15641,f341])).
% 21.75/3.26 fof(f15663,plain,(
% 21.75/3.26 sQ6_spl|~sQ0_spl|~sQ3_spl|~sQ5_spl|~sQ4_spl),
% 21.75/3.26 inference(contradiction_clause,[status(thm)],[f15662])).
% 21.75/3.26 fof(f15664,plain,(
% 21.75/3.26 $false),
% 21.75/3.26 inference(sat_refutation,[status(thm)],[f326,f330,f334,f338,f342,f785,f1000,f1371,f1552,f1764,f2243,f2395,f2909,f3195,f3922,f3956,f4090,f4231,f4233,f4979,f5187,f5372,f5408,f6651,f7006,f7912,f8577,f9591,f13529,f15663])).
% 21.75/3.26 % SZS output end CNFRefutation for theBenchmark.p
% 21.75/3.27 % Elapsed time: 2.844673 seconds
% 21.75/3.27 % CPU time: 22.105339 seconds
% 21.75/3.27 % Total memory used: 283.346 MB
% 21.75/3.27 % Net memory used: 266.432 MB
%------------------------------------------------------------------------------