%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM856+2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 01:43:58 PM UTC 2026
% Result : Theorem 29.22s 4.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM856+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 03:14:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 29.22/4.16 % Refutation found
% 29.22/4.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.22/4.16 % SZS output start CNFRefutation for theBenchmark
% 29.22/4.16 fof(f1,conjecture,(
% 29.22/4.16 greater(vmul(vd517,vd519),vmul(vd518,vd520)) ),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f2,negated_conjecture,(
% 29.22/4.16 ~(greater(vmul(vd517,vd519),vmul(vd518,vd520)) )),
% 29.22/4.16 inference(negated_conjecture,[status(cth)],[f1])).
% 29.22/4.16 fof(f3,axiom,(
% 29.22/4.16 ( ( greater(vd519,vd520)& geq(vd517,vd518) )| ( geq(vd519,vd520)& greater(vd517,vd518) ) ) ),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f4,axiom,(
% 29.22/4.16 (! [Vd501,Vd502,Vd504,Vd505] :( ( greater(Vd504,Vd505)& greater(Vd501,Vd502) )=> greater(vmul(Vd501,Vd504),vmul(Vd502,Vd505)) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f5,axiom,(
% 29.22/4.16 (! [Vd496,Vd497,Vd498] :( less(vmul(Vd496,Vd497),vmul(Vd498,Vd497))=> less(Vd496,Vd498) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f6,axiom,(
% 29.22/4.16 (! [Vd491,Vd492,Vd493] :( vmul(Vd491,Vd492) = vmul(Vd493,Vd492)=> Vd491 = Vd493 ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f7,axiom,(
% 29.22/4.16 (! [Vd486,Vd487,Vd488] :( greater(vmul(Vd486,Vd487),vmul(Vd488,Vd487))=> greater(Vd486,Vd488) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f8,axiom,(
% 29.22/4.16 (! [Vd456,Vd465,Vd466] :( less(Vd465,Vd466)=> less(vmul(Vd465,Vd456),vmul(Vd466,Vd456)) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f10,axiom,(
% 29.22/4.16 (! [Vd456,Vd457,Vd458] :( greater(Vd457,Vd458)=> greater(vmul(Vd457,Vd456),vmul(Vd458,Vd456)) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f13,axiom,(
% 29.22/4.16 (! [Vd418,Vd419] : vmul(Vd418,Vd419) = vmul(Vd419,Vd418) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f14,axiom,(
% 29.22/4.16 (! [Vd408,Vd409] : vmul(vsucc(Vd408),Vd409) = vplus(vmul(Vd408,Vd409),Vd409) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f15,axiom,(
% 29.22/4.16 (! [Vd400] : vmul(v1,Vd400) = Vd400 )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f16,axiom,(
% 29.22/4.16 (! [Vd396,Vd397] :( vmul(Vd396,vsucc(Vd397)) = vplus(vmul(Vd396,Vd397),Vd396)& vmul(Vd396,v1) = Vd396 ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f17,axiom,(
% 29.22/4.16 (! [Vd386,Vd387] :( less(Vd386,vplus(Vd387,v1))=> leq(Vd386,Vd387) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f18,axiom,(
% 29.22/4.16 (! [Vd375,Vd376] :( greater(Vd375,Vd376)=> geq(Vd375,vplus(Vd376,v1)) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f19,axiom,(
% 29.22/4.16 (! [Vd369] : geq(Vd369,v1) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f23,axiom,(
% 29.22/4.16 (! [Vd328,Vd329,Vd330] :( less(vplus(Vd328,Vd330),vplus(Vd329,Vd330))=> less(Vd328,Vd329) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f25,axiom,(
% 29.22/4.16 (! [Vd328,Vd329,Vd330] :( greater(vplus(Vd328,Vd330),vplus(Vd329,Vd330))=> greater(Vd328,Vd329) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f29,axiom,(
% 29.22/4.16 (! [Vd295,Vd296] : greater(vplus(Vd295,Vd296),Vd295) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f31,axiom,(
% 29.22/4.16 (! [Vd281,Vd282,Vd283] :( ( ( less(Vd282,Vd283)& leq(Vd281,Vd282) )| ( leq(Vd282,Vd283)& less(Vd281,Vd282) ) )=> less(Vd281,Vd283) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f32,axiom,(
% 29.22/4.16 (! [Vd262,Vd263,Vd265] :( ( less(Vd263,Vd265)& less(Vd262,Vd263) )=> less(Vd262,Vd265) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f34,axiom,(
% 29.22/4.16 (! [Vd254,Vd255] :( geq(Vd254,Vd255)=> leq(Vd255,Vd254) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f35,axiom,(
% 29.22/4.16 (! [Vd249,Vd250] :( leq(Vd250,Vd249)<=> ( less(Vd250,Vd249)| Vd250 = Vd249 ) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f36,axiom,(
% 29.22/4.16 (! [Vd244,Vd245] :( geq(Vd245,Vd244)<=> ( greater(Vd245,Vd244)| Vd245 = Vd244 ) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f37,axiom,(
% 29.22/4.16 (! [Vd226,Vd227] :( less(Vd226,Vd227)=> greater(Vd227,Vd226) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f38,axiom,(
% 29.22/4.16 (! [Vd208,Vd209] :( greater(Vd208,Vd209)=> less(Vd209,Vd208) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f39,axiom,(
% 29.22/4.16 (! [Vd203,Vd204] :( Vd203 = Vd204| greater(Vd203,Vd204)| less(Vd203,Vd204) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f40,axiom,(
% 29.22/4.16 (! [Vd203,Vd204] :( Vd203 != Vd204| ~ less(Vd203,Vd204) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f41,axiom,(
% 29.22/4.16 (! [Vd203,Vd204] :( ~ greater(Vd203,Vd204)| ~ less(Vd203,Vd204) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f42,axiom,(
% 29.22/4.16 (! [Vd203,Vd204] :( Vd203 != Vd204| ~ greater(Vd203,Vd204) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f43,axiom,(
% 29.22/4.16 (! [Vd198,Vd199] :( less(Vd199,Vd198)<=> (? [Vd201] : Vd198 = vplus(Vd199,Vd201) )) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f44,axiom,(
% 29.22/4.16 (! [Vd193,Vd194] :( greater(Vd194,Vd193)<=> (? [Vd196] : Vd194 = vplus(Vd193,Vd196) )) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f45,axiom,(
% 29.22/4.16 (! [Vd120,Vd121] :( Vd120 = Vd121| (? [Vd123] : Vd120 = vplus(Vd121,Vd123))| (? [Vd125] : Vd121 = vplus(Vd120,Vd125) )) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f47,axiom,(
% 29.22/4.16 (! [Vd120,Vd121] :( ~ (? [Vd123] : Vd120 = vplus(Vd121,Vd123))| ~ (? [Vd125] : Vd121 = vplus(Vd120,Vd125) )) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f51,axiom,(
% 29.22/4.16 (! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f52,axiom,(
% 29.22/4.16 (! [Vd68,Vd69] : vplus(vsucc(Vd68),Vd69) = vsucc(vplus(Vd68,Vd69)) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f53,axiom,(
% 29.22/4.16 (! [Vd59] : vplus(v1,Vd59) = vsucc(Vd59) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f55,axiom,(
% 29.22/4.16 (! [Vd42,Vd43] :( vplus(Vd42,vsucc(Vd43)) = vsucc(vplus(Vd42,Vd43))& vplus(Vd42,v1) = vsucc(Vd42) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f56,axiom,(
% 29.22/4.16 (! [Vd24] :( Vd24 != v1=> Vd24 = vsucc(vskolem2(Vd24)) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f57,axiom,(
% 29.22/4.16 (! [Vd16] : vsucc(Vd16) != Vd16 )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f58,axiom,(
% 29.22/4.16 (! [Vd7,Vd8] :( Vd7 != Vd8=> vsucc(Vd7) != vsucc(Vd8) ) )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f60,axiom,(
% 29.22/4.16 (! [Vd1] : vsucc(Vd1) != v1 )),
% 29.22/4.16 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.22/4.16 fof(f61,plain,(
% 29.22/4.16 ~greater(vmul(vd517,vd519),vmul(vd518,vd520))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f2])).
% 29.22/4.16 fof(f62,definition,(
% 29.22/4.16 sP0_prd<=>(greater(vd519,vd520)&geq(vd517,vd518))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 29.22/4.16 fof(f63,plain,(
% 29.22/4.16 sP0_prd|(geq(vd519,vd520)&greater(vd517,vd518))),
% 29.22/4.16 inference(formula_renaming,[status(thm)],[f3,f62])).
% 29.22/4.16 fof(f64,plain,(
% 29.22/4.16 sP0_prd|geq(vd519,vd520)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f63])).
% 29.22/4.16 fof(f65,plain,(
% 29.22/4.16 sP0_prd|greater(vd517,vd518)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f63])).
% 29.22/4.16 fof(f66,plain,(
% 29.22/4.16 ![Vd501,Vd502,Vd504,Vd505]: ((~greater(Vd504,Vd505)|~greater(Vd501,Vd502))|greater(vmul(Vd501,Vd504),vmul(Vd502,Vd505)))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 29.22/4.16 fof(f67,plain,(
% 29.22/4.16 ![X0,X1,X2,X3]: (~greater(X0,X1)|~greater(X2,X3)|greater(vmul(X2,X0),vmul(X3,X1)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f66])).
% 29.22/4.16 fof(f68,plain,(
% 29.22/4.16 ![Vd496,Vd497,Vd498]: (~less(vmul(Vd496,Vd497),vmul(Vd498,Vd497))|less(Vd496,Vd498))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 29.22/4.16 fof(f69,plain,(
% 29.22/4.16 ![Vd496,Vd498]: ((![Vd497]: ~less(vmul(Vd496,Vd497),vmul(Vd498,Vd497)))|less(Vd496,Vd498))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f68])).
% 29.22/4.16 fof(f70,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~less(vmul(X0,X1),vmul(X2,X1))|less(X0,X2))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f69])).
% 29.22/4.16 fof(f71,plain,(
% 29.22/4.16 ![Vd491,Vd492,Vd493]: (~vmul(Vd491,Vd492)=vmul(Vd493,Vd492)|Vd491=Vd493)),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 29.22/4.16 fof(f72,plain,(
% 29.22/4.16 ![Vd491,Vd493]: ((![Vd492]: ~vmul(Vd491,Vd492)=vmul(Vd493,Vd492))|Vd491=Vd493)),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f71])).
% 29.22/4.16 fof(f73,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~vmul(X0,X1)=vmul(X2,X1)|X0=X2)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f72])).
% 29.22/4.16 fof(f74,plain,(
% 29.22/4.16 ![Vd486,Vd487,Vd488]: (~greater(vmul(Vd486,Vd487),vmul(Vd488,Vd487))|greater(Vd486,Vd488))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 29.22/4.16 fof(f75,plain,(
% 29.22/4.16 ![Vd486,Vd488]: ((![Vd487]: ~greater(vmul(Vd486,Vd487),vmul(Vd488,Vd487)))|greater(Vd486,Vd488))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f74])).
% 29.22/4.16 fof(f76,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~greater(vmul(X0,X1),vmul(X2,X1))|greater(X0,X2))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f75])).
% 29.22/4.16 fof(f77,plain,(
% 29.22/4.16 ![Vd456,Vd465,Vd466]: (~less(Vd465,Vd466)|less(vmul(Vd465,Vd456),vmul(Vd466,Vd456)))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 29.22/4.16 fof(f78,plain,(
% 29.22/4.16 ![Vd465,Vd466]: (~less(Vd465,Vd466)|(![Vd456]: less(vmul(Vd465,Vd456),vmul(Vd466,Vd456))))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f77])).
% 29.22/4.16 fof(f79,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~less(X0,X1)|less(vmul(X0,X2),vmul(X1,X2)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f78])).
% 29.22/4.16 fof(f83,plain,(
% 29.22/4.16 ![Vd456,Vd457,Vd458]: (~greater(Vd457,Vd458)|greater(vmul(Vd457,Vd456),vmul(Vd458,Vd456)))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 29.22/4.16 fof(f84,plain,(
% 29.22/4.16 ![Vd457,Vd458]: (~greater(Vd457,Vd458)|(![Vd456]: greater(vmul(Vd457,Vd456),vmul(Vd458,Vd456))))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f83])).
% 29.22/4.16 fof(f85,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~greater(X0,X1)|greater(vmul(X0,X2),vmul(X1,X2)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f84])).
% 29.22/4.16 fof(f88,plain,(
% 29.22/4.16 ![X0,X1]: (vmul(X0,X1)=vmul(X1,X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f13])).
% 29.22/4.16 fof(f89,plain,(
% 29.22/4.16 ![X0,X1]: (vmul(vsucc(X0),X1)=vplus(vmul(X0,X1),X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f14])).
% 29.22/4.16 fof(f90,plain,(
% 29.22/4.16 ![X0]: (vmul(v1,X0)=X0)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f15])).
% 29.22/4.16 fof(f91,plain,(
% 29.22/4.16 (![Vd396,Vd397]: vmul(Vd396,vsucc(Vd397))=vplus(vmul(Vd396,Vd397),Vd396))&(![Vd396]: vmul(Vd396,v1)=Vd396)),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f16])).
% 29.22/4.16 fof(f92,plain,(
% 29.22/4.16 ![X0,X1]: (vmul(X0,vsucc(X1))=vplus(vmul(X0,X1),X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f91])).
% 29.22/4.16 fof(f93,plain,(
% 29.22/4.16 ![X0]: (vmul(X0,v1)=X0)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f91])).
% 29.22/4.16 fof(f94,plain,(
% 29.22/4.16 ![Vd386,Vd387]: (~less(Vd386,vplus(Vd387,v1))|leq(Vd386,Vd387))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 29.22/4.16 fof(f95,plain,(
% 29.22/4.16 ![X0,X1]: (~less(X0,vplus(X1,v1))|leq(X0,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f94])).
% 29.22/4.16 fof(f96,plain,(
% 29.22/4.16 ![Vd375,Vd376]: (~greater(Vd375,Vd376)|geq(Vd375,vplus(Vd376,v1)))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 29.22/4.16 fof(f97,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(X0,X1)|geq(X0,vplus(X1,v1)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f96])).
% 29.22/4.16 fof(f98,plain,(
% 29.22/4.16 ![X0]: (geq(X0,v1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f19])).
% 29.22/4.16 fof(f106,plain,(
% 29.22/4.16 ![Vd328,Vd329,Vd330]: (~less(vplus(Vd328,Vd330),vplus(Vd329,Vd330))|less(Vd328,Vd329))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 29.22/4.16 fof(f107,plain,(
% 29.22/4.16 ![Vd328,Vd329]: ((![Vd330]: ~less(vplus(Vd328,Vd330),vplus(Vd329,Vd330)))|less(Vd328,Vd329))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f106])).
% 29.22/4.16 fof(f108,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~less(vplus(X0,X1),vplus(X2,X1))|less(X0,X2))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f107])).
% 29.22/4.16 fof(f112,plain,(
% 29.22/4.16 ![Vd328,Vd329,Vd330]: (~greater(vplus(Vd328,Vd330),vplus(Vd329,Vd330))|greater(Vd328,Vd329))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 29.22/4.16 fof(f113,plain,(
% 29.22/4.16 ![Vd328,Vd329]: ((![Vd330]: ~greater(vplus(Vd328,Vd330),vplus(Vd329,Vd330)))|greater(Vd328,Vd329))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f112])).
% 29.22/4.16 fof(f114,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~greater(vplus(X0,X1),vplus(X2,X1))|greater(X0,X2))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f113])).
% 29.22/4.16 fof(f124,plain,(
% 29.22/4.16 ![X0,X1]: (greater(vplus(X0,X1),X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f29])).
% 29.22/4.16 fof(f128,plain,(
% 29.22/4.16 ![Vd281,Vd282,Vd283]: (((~less(Vd282,Vd283)|~leq(Vd281,Vd282))&(~leq(Vd282,Vd283)|~less(Vd281,Vd282)))|less(Vd281,Vd283))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 29.22/4.16 fof(f129,plain,(
% 29.22/4.16 ![Vd281,Vd283]: (((![Vd282]: (~less(Vd282,Vd283)|~leq(Vd281,Vd282)))&(![Vd282]: (~leq(Vd282,Vd283)|~less(Vd281,Vd282))))|less(Vd281,Vd283))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f128])).
% 29.22/4.16 fof(f131,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~leq(X0,X1)|~less(X2,X0)|less(X2,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f129])).
% 29.22/4.16 fof(f132,plain,(
% 29.22/4.16 ![Vd262,Vd263,Vd265]: ((~less(Vd263,Vd265)|~less(Vd262,Vd263))|less(Vd262,Vd265))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 29.22/4.16 fof(f133,plain,(
% 29.22/4.16 ![Vd262,Vd265]: ((![Vd263]: (~less(Vd263,Vd265)|~less(Vd262,Vd263)))|less(Vd262,Vd265))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f132])).
% 29.22/4.16 fof(f134,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~less(X0,X1)|~less(X2,X0)|less(X2,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f133])).
% 29.22/4.16 fof(f137,plain,(
% 29.22/4.16 ![Vd254,Vd255]: (~geq(Vd254,Vd255)|leq(Vd255,Vd254))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 29.22/4.16 fof(f138,plain,(
% 29.22/4.16 ![X0,X1]: (~geq(X0,X1)|leq(X1,X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f137])).
% 29.22/4.16 fof(f139,plain,(
% 29.22/4.16 ![Vd249,Vd250]: ((~leq(Vd250,Vd249)|(less(Vd250,Vd249)|Vd250=Vd249))&(leq(Vd250,Vd249)|(~less(Vd250,Vd249)&~Vd250=Vd249)))),
% 29.22/4.16 inference(NNF_transformation,[status(thm)],[f35])).
% 29.22/4.16 fof(f140,plain,(
% 29.22/4.16 (![Vd249,Vd250]: (~leq(Vd250,Vd249)|(less(Vd250,Vd249)|Vd250=Vd249)))&(![Vd249,Vd250]: (leq(Vd250,Vd249)|(~less(Vd250,Vd249)&~Vd250=Vd249)))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f139])).
% 29.22/4.16 fof(f141,plain,(
% 29.22/4.16 ![X0,X1]: (~leq(X0,X1)|less(X0,X1)|X0=X1)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f140])).
% 29.22/4.16 fof(f142,plain,(
% 29.22/4.16 ![X0,X1]: (leq(X0,X1)|~less(X0,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f140])).
% 29.22/4.16 fof(f144,plain,(
% 29.22/4.16 ![Vd244,Vd245]: ((~geq(Vd245,Vd244)|(greater(Vd245,Vd244)|Vd245=Vd244))&(geq(Vd245,Vd244)|(~greater(Vd245,Vd244)&~Vd245=Vd244)))),
% 29.22/4.16 inference(NNF_transformation,[status(thm)],[f36])).
% 29.22/4.16 fof(f145,plain,(
% 29.22/4.16 (![Vd244,Vd245]: (~geq(Vd245,Vd244)|(greater(Vd245,Vd244)|Vd245=Vd244)))&(![Vd244,Vd245]: (geq(Vd245,Vd244)|(~greater(Vd245,Vd244)&~Vd245=Vd244)))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f144])).
% 29.22/4.16 fof(f146,plain,(
% 29.22/4.16 ![X0,X1]: (~geq(X0,X1)|greater(X0,X1)|X0=X1)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f145])).
% 29.22/4.16 fof(f147,plain,(
% 29.22/4.16 ![X0,X1]: (geq(X0,X1)|~greater(X0,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f145])).
% 29.22/4.16 fof(f149,plain,(
% 29.22/4.16 ![Vd226,Vd227]: (~less(Vd226,Vd227)|greater(Vd227,Vd226))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 29.22/4.16 fof(f150,plain,(
% 29.22/4.16 ![X0,X1]: (~less(X0,X1)|greater(X1,X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f149])).
% 29.22/4.16 fof(f151,plain,(
% 29.22/4.16 ![Vd208,Vd209]: (~greater(Vd208,Vd209)|less(Vd209,Vd208))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 29.22/4.16 fof(f152,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(X0,X1)|less(X1,X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f151])).
% 29.22/4.16 fof(f153,plain,(
% 29.22/4.16 ![X0,X1]: (X0=X1|greater(X0,X1)|less(X0,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f39])).
% 29.22/4.16 fof(f154,plain,(
% 29.22/4.16 ![X0,X1]: (~X0=X1|~less(X0,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f40])).
% 29.22/4.16 fof(f155,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(X0,X1)|~less(X0,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f41])).
% 29.22/4.16 fof(f156,plain,(
% 29.22/4.16 ![X0,X1]: (~X0=X1|~greater(X0,X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f42])).
% 29.22/4.16 fof(f157,plain,(
% 29.22/4.16 ![Vd198,Vd199]: ((~less(Vd199,Vd198)|(?[Vd201]: Vd198=vplus(Vd199,Vd201)))&(less(Vd199,Vd198)|(![Vd201]: ~Vd198=vplus(Vd199,Vd201))))),
% 29.22/4.16 inference(NNF_transformation,[status(thm)],[f43])).
% 29.22/4.16 fof(f158,plain,(
% 29.22/4.16 (![Vd198,Vd199]: (~less(Vd199,Vd198)|(?[Vd201]: Vd198=vplus(Vd199,Vd201))))&(![Vd198,Vd199]: (less(Vd199,Vd198)|(![Vd201]: ~Vd198=vplus(Vd199,Vd201))))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f157])).
% 29.22/4.16 fof(f159,plain,(
% 29.22/4.16 (![Vd198,Vd199]: (~less(Vd199,Vd198)|Vd198=vplus(Vd199,sK0_skl(Vd199,Vd198))))&(![Vd198,Vd199]: (less(Vd199,Vd198)|(![Vd201]: ~Vd198=vplus(Vd199,Vd201))))),
% 29.22/4.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd201,sK0_skl(Vd199,Vd198))],[f158])).
% 29.22/4.16 fof(f161,plain,(
% 29.22/4.16 ![X0,X1,X2]: (less(X0,X1)|~X1=vplus(X0,X2))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f159])).
% 29.22/4.16 fof(f162,plain,(
% 29.22/4.16 ![Vd193,Vd194]: ((~greater(Vd194,Vd193)|(?[Vd196]: Vd194=vplus(Vd193,Vd196)))&(greater(Vd194,Vd193)|(![Vd196]: ~Vd194=vplus(Vd193,Vd196))))),
% 29.22/4.16 inference(NNF_transformation,[status(thm)],[f44])).
% 29.22/4.16 fof(f163,plain,(
% 29.22/4.16 (![Vd193,Vd194]: (~greater(Vd194,Vd193)|(?[Vd196]: Vd194=vplus(Vd193,Vd196))))&(![Vd193,Vd194]: (greater(Vd194,Vd193)|(![Vd196]: ~Vd194=vplus(Vd193,Vd196))))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f162])).
% 29.22/4.16 fof(f164,plain,(
% 29.22/4.16 (![Vd193,Vd194]: (~greater(Vd194,Vd193)|Vd194=vplus(Vd193,sK1_skl(Vd194,Vd193))))&(![Vd193,Vd194]: (greater(Vd194,Vd193)|(![Vd196]: ~Vd194=vplus(Vd193,Vd196))))),
% 29.22/4.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd196,sK1_skl(Vd194,Vd193))],[f163])).
% 29.22/4.16 fof(f165,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(X0,X1)|X0=vplus(X1,sK1_skl(X0,X1)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f164])).
% 29.22/4.16 fof(f167,plain,(
% 29.22/4.16 ![Vd120,Vd121]: ((Vd120=Vd121|Vd120=vplus(Vd121,sK2_skl(Vd121,Vd120)))|Vd121=vplus(Vd120,sK3_skl(Vd121,Vd120)))),
% 29.22/4.16 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(Vd123,sK2_skl(Vd121,Vd120)),skolemize(Vd125,sK3_skl(Vd121,Vd120))],[f45])).
% 29.22/4.16 fof(f168,plain,(
% 29.22/4.16 ![X0,X1]: (X0=X1|X0=vplus(X1,sK2_skl(X1,X0))|X1=vplus(X0,sK3_skl(X1,X0)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f167])).
% 29.22/4.16 fof(f171,plain,(
% 29.22/4.16 ![Vd120,Vd121]: ((![Vd123]: ~Vd120=vplus(Vd121,Vd123))|(![Vd125]: ~Vd121=vplus(Vd120,Vd125)))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 29.22/4.16 fof(f172,plain,(
% 29.22/4.16 ![X0,X1,X2,X3]: (~X0=vplus(X1,X2)|~X1=vplus(X0,X3))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f171])).
% 29.22/4.16 fof(f178,plain,(
% 29.22/4.16 ![X0,X1]: (vplus(X0,X1)=vplus(X1,X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f51])).
% 29.22/4.16 fof(f179,plain,(
% 29.22/4.16 ![X0,X1]: (vplus(vsucc(X0),X1)=vsucc(vplus(X0,X1)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f52])).
% 29.22/4.16 fof(f180,plain,(
% 29.22/4.16 ![X0]: (vplus(v1,X0)=vsucc(X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f53])).
% 29.22/4.16 fof(f182,plain,(
% 29.22/4.16 (![Vd42,Vd43]: vplus(Vd42,vsucc(Vd43))=vsucc(vplus(Vd42,Vd43)))&(![Vd42]: vplus(Vd42,v1)=vsucc(Vd42))),
% 29.22/4.16 inference(miniscoping,[status(thm)],[f55])).
% 29.22/4.16 fof(f184,plain,(
% 29.22/4.16 ![X0]: (vplus(X0,v1)=vsucc(X0))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f182])).
% 29.22/4.16 fof(f185,plain,(
% 29.22/4.16 ![Vd24]: (Vd24=v1|Vd24=vsucc(vskolem2(Vd24)))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 29.22/4.16 fof(f186,plain,(
% 29.22/4.16 ![X0]: (X0=v1|X0=vsucc(vskolem2(X0)))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f185])).
% 29.22/4.16 fof(f187,plain,(
% 29.22/4.16 ![X0]: (~vsucc(X0)=X0)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f57])).
% 29.22/4.16 fof(f188,plain,(
% 29.22/4.16 ![Vd7,Vd8]: (Vd7=Vd8|~vsucc(Vd7)=vsucc(Vd8))),
% 29.22/4.16 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 29.22/4.16 fof(f189,plain,(
% 29.22/4.16 ![X0,X1]: (X0=X1|~vsucc(X0)=vsucc(X1))),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f188])).
% 29.22/4.16 fof(f192,plain,(
% 29.22/4.16 ![X0]: (~vsucc(X0)=v1)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f60])).
% 29.22/4.16 fof(f193,plain,(
% 29.22/4.16 (~sP0_prd|(greater(vd519,vd520)&geq(vd517,vd518)))&(sP0_prd|(~greater(vd519,vd520)|~geq(vd517,vd518)))),
% 29.22/4.16 inference(NNF_transformation,[status(thm)],[f62])).
% 29.22/4.16 fof(f194,plain,(
% 29.22/4.16 ~sP0_prd|greater(vd519,vd520)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f193])).
% 29.22/4.16 fof(f195,plain,(
% 29.22/4.16 ~sP0_prd|geq(vd517,vd518)),
% 29.22/4.16 inference(cnf_transformation,[status(thm)],[f193])).
% 29.22/4.16 fof(f197,definition,(
% 29.22/4.16 sQ0_spl <=> (sP0_prd)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f200,definition,(
% 29.22/4.16 sQ1_spl <=> (geq(vd519,vd520))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f201,plain,(
% 29.22/4.16 geq(vd519,vd520)|~sQ1_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f200])).
% 29.22/4.16 fof(f203,plain,(
% 29.22/4.16 sQ0_spl|sQ1_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f64,f197,f200])).
% 29.22/4.16 fof(f204,definition,(
% 29.22/4.16 sQ2_spl <=> (greater(vd517,vd518))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f205,plain,(
% 29.22/4.16 greater(vd517,vd518)|~sQ2_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f204])).
% 29.22/4.16 fof(f207,plain,(
% 29.22/4.16 sQ0_spl|sQ2_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f65,f197,f204])).
% 29.22/4.16 fof(f208,definition,(
% 29.22/4.16 sQ3_spl <=> (greater(vd519,vd520))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f209,plain,(
% 29.22/4.16 greater(vd519,vd520)|~sQ3_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f208])).
% 29.22/4.16 fof(f211,plain,(
% 29.22/4.16 ~sQ0_spl|sQ3_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f194,f197,f208])).
% 29.22/4.16 fof(f212,definition,(
% 29.22/4.16 sQ4_spl <=> (geq(vd517,vd518))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f213,plain,(
% 29.22/4.16 geq(vd517,vd518)|~sQ4_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f212])).
% 29.22/4.16 fof(f215,plain,(
% 29.22/4.16 ~sQ0_spl|sQ4_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f195,f197,f212])).
% 29.22/4.16 fof(f219,plain,(
% 29.22/4.16 ![X0]: (~less(X0,X0))),
% 29.22/4.16 inference(destructive_equality_resolution,[status(thm)],[f154])).
% 29.22/4.16 fof(f220,plain,(
% 29.22/4.16 ![X0]: (~greater(X0,X0))),
% 29.22/4.16 inference(destructive_equality_resolution,[status(thm)],[f156])).
% 29.22/4.16 fof(f221,plain,(
% 29.22/4.16 ![X0,X1]: (less(X0,vplus(X0,X1)))),
% 29.22/4.16 inference(destructive_equality_resolution,[status(thm)],[f161])).
% 29.22/4.16 fof(f224,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~X0=vplus(vplus(X0,X1),X2))),
% 29.22/4.16 inference(destructive_equality_resolution,[status(thm)],[f172])).
% 29.22/4.16 fof(f232,plain,(
% 29.22/4.16 ~greater(vmul(vd517,vd519),vmul(vd520,vd518))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f61])).
% 29.22/4.16 fof(f233,plain,(
% 29.22/4.16 ~greater(vmul(vd519,vd517),vmul(vd518,vd520))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f61])).
% 29.22/4.16 fof(f238,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~vmul(X0,X1)=vmul(X2,X0)|X1=X2)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f73])).
% 29.22/4.16 fof(f247,plain,(
% 29.22/4.16 ![X0,X1,X2]: (~vmul(X0,X1)=vmul(X0,X2)|X1=X2)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f238])).
% 29.22/4.16 fof(f262,plain,(
% 29.22/4.16 ![X0]: (greater(vmul(vd517,X0),vmul(vd518,X0))|~sQ2_spl)),
% 29.22/4.16 inference(resolution,[status(thm)],[f85,f205])).
% 29.22/4.16 fof(f268,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(vmul(X0,X1),X1)|greater(X0,v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f76])).
% 29.22/4.16 fof(f269,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(X0,vmul(X1,X0))|greater(v1,X1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f76])).
% 29.22/4.16 fof(f272,plain,(
% 29.22/4.16 ![X0,X1]: (~vmul(X0,X1)=X0|X1=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f238])).
% 29.22/4.16 fof(f274,plain,(
% 29.22/4.16 ![X0,X1]: (~vmul(X0,X1)=X1|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f73])).
% 29.22/4.16 fof(f296,plain,(
% 29.22/4.16 ![X0,X1]: (~less(X0,vmul(X1,X0))|less(v1,X1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f70])).
% 29.22/4.16 fof(f300,plain,(
% 29.22/4.16 ![X0,X1]: (~less(vmul(X0,X1),X1)|less(X0,v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f70])).
% 29.22/4.16 fof(f331,plain,(
% 29.22/4.16 ~greater(vmul(vd519,vd517),vmul(vd520,vd518))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f232])).
% 29.22/4.16 fof(f342,definition,(
% 29.22/4.16 ![X0]: (sQ5_spl <=> (~X0=X0))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f343,plain,(
% 29.22/4.16 ![X0]: (~X0=X0|~sQ5_spl)),
% 29.22/4.16 inference(component_clause,[status(thm)],[f342])).
% 29.22/4.16 fof(f345,definition,(
% 29.22/4.16 sQ6_spl <=> (v1=v1)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f349,plain,(
% 29.22/4.16 $false|~sQ5_spl),
% 29.22/4.16 inference(trivial_equality_resolution,[status(thm)],[f343])).
% 29.22/4.16 fof(f350,plain,(
% 29.22/4.16 ~sQ5_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f349])).
% 29.22/4.16 fof(f352,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(X0,X1)|greater(vmul(X0,vd519),vmul(X1,vd520))|~sQ3_spl)),
% 29.22/4.16 inference(resolution,[status(thm)],[f209,f67])).
% 29.22/4.16 fof(f387,plain,(
% 29.22/4.16 leq(vd518,vd517)|~sQ4_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f138,f213])).
% 29.22/4.16 fof(f388,plain,(
% 29.22/4.16 ![X0]: (leq(v1,X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f138,f98])).
% 29.22/4.16 fof(f392,plain,(
% 29.22/4.16 ![X0,X1]: (leq(X0,vplus(X0,X1)))),
% 29.22/4.16 inference(resolution,[status(thm)],[f142,f221])).
% 29.22/4.16 fof(f402,plain,(
% 29.22/4.16 less(vd520,vd519)|~sQ3_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f152,f209])).
% 29.22/4.16 fof(f408,plain,(
% 29.22/4.16 ![X0,X1]: (~less(vplus(X0,X1),X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f155,f124])).
% 29.22/4.16 fof(f411,plain,(
% 29.22/4.16 ![X0]: (vmul(vsucc(v1),X0)=vplus(X0,X0))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f89])).
% 29.22/4.16 fof(f497,plain,(
% 29.22/4.16 ![X0]: (~greater(X0,X0)|greater(v1,v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f268])).
% 29.22/4.16 fof(f501,definition,(
% 29.22/4.16 ![X0]: (sQ7_spl <=> (~greater(X0,X0)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f504,definition,(
% 29.22/4.16 sQ8_spl <=> (greater(v1,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f505,plain,(
% 29.22/4.16 greater(v1,v1)|~sQ8_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f504])).
% 29.22/4.16 fof(f507,plain,(
% 29.22/4.16 sQ7_spl|sQ8_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f497,f501,f504])).
% 29.22/4.16 fof(f544,plain,(
% 29.22/4.16 ![X0,X1]: (~less(vplus(X0,X1),X1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f178,f408])).
% 29.22/4.16 fof(f546,plain,(
% 29.22/4.16 ![X0,X1]: (leq(X0,vplus(X1,X0)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f178,f392])).
% 29.22/4.16 fof(f547,plain,(
% 29.22/4.16 ![X0,X1]: (less(X0,vplus(X1,X0)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f178,f221])).
% 29.22/4.16 fof(f550,plain,(
% 29.22/4.16 ![X0,X1]: (greater(vplus(X0,X1),X1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f178,f124])).
% 29.22/4.16 fof(f571,plain,(
% 29.22/4.16 ![X0,X1]: (~less(vmul(X0,vsucc(X1)),X0))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f92,f544])).
% 29.22/4.16 fof(f605,plain,(
% 29.22/4.16 ![X0,X1]: (greater(vmul(X0,vsucc(X1)),X0))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f92,f550])).
% 29.22/4.16 fof(f609,plain,(
% 29.22/4.16 geq(vd519,vplus(vd520,v1))|~sQ3_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f97,f209])).
% 29.22/4.16 fof(f622,plain,(
% 29.22/4.16 ![X0]: (~less(vsucc(X0),v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f571])).
% 29.22/4.16 fof(f629,plain,(
% 29.22/4.16 ![X0]: (greater(vsucc(X0),v1))),
% 29.22/4.16 inference(resolution,[status(thm)],[f605,f268])).
% 29.22/4.16 fof(f661,plain,(
% 29.22/4.16 ![X0]: (less(v1,vsucc(X0)))),
% 29.22/4.16 inference(resolution,[status(thm)],[f629,f152])).
% 29.22/4.16 fof(f719,plain,(
% 29.22/4.16 ![X0]: (greater(vsucc(X0),X0))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f180,f550])).
% 29.22/4.16 fof(f720,plain,(
% 29.22/4.16 ![X0]: (less(X0,vsucc(X0)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f180,f547])).
% 29.22/4.16 fof(f721,plain,(
% 29.22/4.16 ![X0]: (leq(X0,vsucc(X0)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f180,f546])).
% 29.22/4.16 fof(f723,plain,(
% 29.22/4.16 ![X0]: (~less(vsucc(X0),X0))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f180,f544])).
% 29.22/4.16 fof(f731,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(vplus(X0,X1),vsucc(X1))|greater(X0,v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f180,f114])).
% 29.22/4.16 fof(f758,plain,(
% 29.22/4.16 ![X0,X1]: (~greater(X0,X1)|geq(X0,vsucc(X1)))),
% 29.22/4.16 inference(backward_demodulation,[status(thm)],[f184,f97])).
% 29.22/4.16 fof(f759,plain,(
% 29.22/4.16 ![X0,X1]: (~less(X0,vsucc(X1))|leq(X0,X1))),
% 29.22/4.16 inference(backward_demodulation,[status(thm)],[f184,f95])).
% 29.22/4.16 fof(f766,plain,(
% 29.22/4.16 ![X0,X1]: (~X0=vsucc(vplus(X0,X1)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f184,f224])).
% 29.22/4.16 fof(f776,plain,(
% 29.22/4.16 ![X0,X1]: (~X0=vplus(vsucc(X0),X1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f184,f224])).
% 29.22/4.16 fof(f802,plain,(
% 29.22/4.16 ![X0]: (~X0=vsucc(vsucc(X0)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f184,f766])).
% 29.22/4.16 fof(f815,plain,(
% 29.22/4.16 ![X0,X1]: (~less(vsucc(X0),vplus(X1,X0))|less(v1,X1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f180,f108])).
% 29.22/4.16 fof(f872,plain,(
% 29.22/4.16 geq(vd519,vsucc(vd520))|~sQ3_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f184,f609])).
% 29.22/4.16 fof(f875,plain,(
% 29.22/4.16 leq(vsucc(vd520),vd519)|~sQ3_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f872,f138])).
% 29.22/4.16 fof(f1081,plain,(
% 29.22/4.16 ![X0]: (vsucc(X0)=v1|X0=vskolem2(vsucc(X0)))),
% 29.22/4.16 inference(resolution,[status(thm)],[f186,f189])).
% 29.22/4.16 fof(f1092,plain,(
% 29.22/4.16 ![X0]: (~vskolem2(X0)=vsucc(X0)|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f802])).
% 29.22/4.16 fof(f1097,plain,(
% 29.22/4.16 ![X0]: (~less(X0,vskolem2(X0))|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f723])).
% 29.22/4.16 fof(f1099,plain,(
% 29.22/4.16 ![X0]: (leq(vskolem2(X0),X0)|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f721])).
% 29.22/4.16 fof(f1101,plain,(
% 29.22/4.16 ![X0]: (greater(X0,vskolem2(X0))|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f719])).
% 29.22/4.16 fof(f1105,plain,(
% 29.22/4.16 ![X0]: (less(v1,X0)|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f661])).
% 29.22/4.16 fof(f1106,plain,(
% 29.22/4.16 ![X0]: (greater(X0,v1)|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f629])).
% 29.22/4.16 fof(f1109,plain,(
% 29.22/4.16 ![X0]: (~less(X0,v1)|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f622])).
% 29.22/4.16 fof(f1115,plain,(
% 29.22/4.16 ![X0]: (X0=vskolem2(vsucc(X0)))),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f1081,f192])).
% 29.22/4.16 fof(f1146,plain,(
% 29.22/4.16 ![X0,X1]: (~leq(X0,X1)|~less(X1,X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f131,f219])).
% 29.22/4.16 fof(f1174,plain,(
% 29.22/4.16 ![X0,X1]: (~less(X0,X1)|~less(X1,X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f134,f219])).
% 29.22/4.16 fof(f1180,plain,(
% 29.22/4.16 less(vd518,vd517)|vd518=vd517|~sQ4_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f141,f387])).
% 29.22/4.16 fof(f1192,definition,(
% 29.22/4.16 sQ10_spl <=> (vsucc(vd520)=vd519)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1193,plain,(
% 29.22/4.16 vsucc(vd520)=vd519|~sQ10_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1192])).
% 29.22/4.16 fof(f1194,plain,(
% 29.22/4.16 ~vsucc(vd520)=vd519|sQ10_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1192])).
% 29.22/4.16 fof(f1196,definition,(
% 29.22/4.16 sQ11_spl <=> (less(vd520,vsucc(vd519)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1199,definition,(
% 29.22/4.16 sQ12_spl <=> (vd520=vsucc(vd519))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1200,plain,(
% 29.22/4.16 vd520=vsucc(vd519)|~sQ12_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1199])).
% 29.22/4.16 fof(f1203,definition,(
% 29.22/4.16 sQ13_spl <=> (less(vd520,vd519))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1206,definition,(
% 29.22/4.16 sQ14_spl <=> (vd520=vd519)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1207,plain,(
% 29.22/4.16 vd520=vd519|~sQ14_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1206])).
% 29.22/4.16 fof(f1210,definition,(
% 29.22/4.16 sQ15_spl <=> (less(vd518,vd517))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1211,plain,(
% 29.22/4.16 less(vd518,vd517)|~sQ15_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1210])).
% 29.22/4.16 fof(f1213,definition,(
% 29.22/4.16 sQ16_spl <=> (vd518=vd517)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1214,plain,(
% 29.22/4.16 vd518=vd517|~sQ16_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1213])).
% 29.22/4.16 fof(f1215,plain,(
% 29.22/4.16 ~vd518=vd517|sQ16_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1213])).
% 29.22/4.16 fof(f1216,plain,(
% 29.22/4.16 sQ15_spl|sQ16_spl|~sQ4_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1180,f1210,f1213,f212])).
% 29.22/4.16 fof(f1221,plain,(
% 29.22/4.16 greater(vd517,vd518)|~sQ15_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1211,f150])).
% 29.22/4.16 fof(f1229,plain,(
% 29.22/4.16 geq(vd517,vd518)|~sQ15_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1221,f147])).
% 29.22/4.16 fof(f1263,plain,(
% 29.22/4.16 v1=v1|v1=v1),
% 29.22/4.16 inference(resolution,[status(thm)],[f1109,f1105])).
% 29.22/4.16 fof(f1266,plain,(
% 29.22/4.16 sQ6_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1263,f345])).
% 29.22/4.16 fof(f1458,plain,(
% 29.22/4.16 ![X0]: (~leq(vsucc(X0),v1))),
% 29.22/4.16 inference(resolution,[status(thm)],[f1146,f661])).
% 29.22/4.16 fof(f1461,plain,(
% 29.22/4.16 ~leq(vd519,vd520)|~sQ3_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1146,f402])).
% 29.22/4.16 fof(f1462,plain,(
% 29.22/4.16 ![X0]: (~leq(vsucc(X0),X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f1146,f720])).
% 29.22/4.16 fof(f1472,plain,(
% 29.22/4.16 ![X0]: (~leq(X0,vskolem2(X0))|X0=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f186,f1462])).
% 29.22/4.16 fof(f1514,plain,(
% 29.22/4.16 greater(vd517,vd518)|vd517=vd518|~sQ4_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f146,f213])).
% 29.22/4.16 fof(f1517,definition,(
% 29.22/4.16 sQ17_spl <=> (greater(vsucc(vd519),vd520))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1518,plain,(
% 29.22/4.16 greater(vsucc(vd519),vd520)|~sQ17_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1517])).
% 29.22/4.16 fof(f1526,plain,(
% 29.22/4.16 sQ2_spl|sQ16_spl|~sQ4_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1514,f204,f1213,f212])).
% 29.22/4.16 fof(f1529,plain,(
% 29.22/4.16 vmul(vd519,vd517)=vmul(vd518,vd520)|less(vmul(vd519,vd517),vmul(vd518,vd520))),
% 29.22/4.16 inference(resolution,[status(thm)],[f153,f233])).
% 29.22/4.16 fof(f1531,plain,(
% 29.22/4.16 vmul(vd517,vd519)=vmul(vd518,vd520)|less(vmul(vd517,vd519),vmul(vd518,vd520))),
% 29.22/4.16 inference(resolution,[status(thm)],[f153,f61])).
% 29.22/4.16 fof(f1541,plain,(
% 29.22/4.16 ![X0,X1]: (X0=X1|less(X0,X1)|less(X1,X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f153,f152])).
% 29.22/4.16 fof(f1554,definition,(
% 29.22/4.16 sQ21_spl <=> (vmul(vd519,vd517)=vmul(vd518,vd520))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1557,definition,(
% 29.22/4.16 sQ22_spl <=> (less(vmul(vd519,vd517),vmul(vd518,vd520)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1560,plain,(
% 29.22/4.16 sQ21_spl|sQ22_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1529,f1554,f1557])).
% 29.22/4.16 fof(f1568,definition,(
% 29.22/4.16 sQ25_spl <=> (vmul(vd517,vd519)=vmul(vd518,vd520))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1569,plain,(
% 29.22/4.16 vmul(vd517,vd519)=vmul(vd518,vd520)|~sQ25_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1568])).
% 29.22/4.16 fof(f1570,plain,(
% 29.22/4.16 ~vmul(vd517,vd519)=vmul(vd518,vd520)|sQ25_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1568])).
% 29.22/4.16 fof(f1571,definition,(
% 29.22/4.16 sQ26_spl <=> (less(vmul(vd517,vd519),vmul(vd518,vd520)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1574,plain,(
% 29.22/4.16 sQ25_spl|sQ26_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1531,f1568,f1571])).
% 29.22/4.16 fof(f1597,plain,(
% 29.22/4.16 ~greater(vd519,vmul(vd518,vd520))|greater(v1,vd517)|~sQ25_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1569,f269])).
% 29.22/4.16 fof(f1608,plain,(
% 29.22/4.16 ~vmul(vd518,vd520)=vd519|vd517=v1|~sQ25_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1569,f274])).
% 29.22/4.16 fof(f1609,plain,(
% 29.22/4.16 ~vmul(vd518,vd520)=vd517|vd519=v1|~sQ25_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1569,f272])).
% 29.22/4.16 fof(f1623,definition,(
% 29.22/4.16 sQ27_spl <=> (greater(vd519,vmul(vd518,vd520)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1626,definition,(
% 29.22/4.16 sQ28_spl <=> (greater(v1,vd517))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1627,plain,(
% 29.22/4.16 greater(v1,vd517)|~sQ28_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1626])).
% 29.22/4.16 fof(f1628,plain,(
% 29.22/4.16 ~greater(v1,vd517)|sQ28_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1626])).
% 29.22/4.16 fof(f1629,plain,(
% 29.22/4.16 ~sQ27_spl|sQ28_spl|~sQ25_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1597,f1623,f1626,f1568])).
% 29.22/4.16 fof(f1633,definition,(
% 29.22/4.16 sQ30_spl <=> (greater(vd517,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1634,plain,(
% 29.22/4.16 greater(vd517,v1)|~sQ30_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1633])).
% 29.22/4.16 fof(f1635,plain,(
% 29.22/4.16 ~greater(vd517,v1)|sQ30_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1633])).
% 29.22/4.16 fof(f1637,definition,(
% 29.22/4.16 sQ31_spl <=> (vmul(vd518,vd520)=vd519)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1639,plain,(
% 29.22/4.16 ~vmul(vd518,vd520)=vd519|sQ31_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1637])).
% 29.22/4.16 fof(f1640,definition,(
% 29.22/4.16 sQ32_spl <=> (vd517=v1)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1641,plain,(
% 29.22/4.16 vd517=v1|~sQ32_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1640])).
% 29.22/4.16 fof(f1643,plain,(
% 29.22/4.16 ~sQ31_spl|sQ32_spl|~sQ25_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1608,f1637,f1640,f1568])).
% 29.22/4.16 fof(f1644,definition,(
% 29.22/4.16 sQ33_spl <=> (vmul(vd518,vd520)=vd517)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1647,definition,(
% 29.22/4.16 sQ34_spl <=> (vd519=v1)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1648,plain,(
% 29.22/4.16 vd519=v1|~sQ34_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1647])).
% 29.22/4.16 fof(f1649,plain,(
% 29.22/4.16 ~vd519=v1|sQ34_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1647])).
% 29.22/4.16 fof(f1650,plain,(
% 29.22/4.16 ~sQ33_spl|sQ34_spl|~sQ25_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1609,f1644,f1647,f1568])).
% 29.22/4.16 fof(f1676,plain,(
% 29.22/4.16 vd520=vskolem2(vd519)|~sQ10_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1193,f1115])).
% 29.22/4.16 fof(f1681,plain,(
% 29.22/4.16 ![X0]: (X0=vd520|~vsucc(X0)=vd519|~sQ10_spl)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1193,f189])).
% 29.22/4.16 fof(f1684,plain,(
% 29.22/4.16 ![X0]: (~vd520=vplus(vd519,X0)|~sQ10_spl)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1193,f776])).
% 29.22/4.16 fof(f1699,plain,(
% 29.22/4.16 greater(vd519,v1)|~sQ10_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1193,f629])).
% 29.22/4.16 fof(f1712,plain,(
% 29.22/4.16 vd519=vskolem2(vd520)|~sQ12_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1200,f1115])).
% 29.22/4.16 fof(f1746,plain,(
% 29.22/4.16 greater(vd518,vd518)|~sQ16_spl|~sQ2_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1214,f205])).
% 29.22/4.16 fof(f1747,plain,(
% 29.22/4.16 $false|~sQ16_spl|~sQ2_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f1746,f220])).
% 29.22/4.16 fof(f1748,plain,(
% 29.22/4.16 ~sQ16_spl|~sQ2_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f1747])).
% 29.22/4.16 fof(f1749,plain,(
% 29.22/4.16 greater(vd519,vd520)|vd519=vd520|~sQ1_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f201,f146])).
% 29.22/4.16 fof(f1753,plain,(
% 29.22/4.16 sQ3_spl|sQ14_spl|~sQ1_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1749,f208,f1206,f200])).
% 29.22/4.16 fof(f1757,plain,(
% 29.22/4.16 ~less(vd517,vd518)|~sQ2_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f205,f155])).
% 29.22/4.16 fof(f1758,plain,(
% 29.22/4.16 less(vd518,vd517)|~sQ2_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f205,f152])).
% 29.22/4.16 fof(f1759,plain,(
% 29.22/4.16 geq(vd517,vd518)|~sQ2_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f205,f147])).
% 29.22/4.16 fof(f1763,plain,(
% 29.22/4.16 sQ4_spl|~sQ2_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1759,f212,f204])).
% 29.22/4.16 fof(f1772,plain,(
% 29.22/4.16 ~leq(vd517,vd518)|~sQ2_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1758,f1146])).
% 29.22/4.16 fof(f1781,plain,(
% 29.22/4.16 greater(vd517,vd518)|vd517=vd518|~sQ15_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1229,f146])).
% 29.22/4.16 fof(f1785,plain,(
% 29.22/4.16 sQ2_spl|sQ16_spl|~sQ15_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1781,f204,f1213,f1210])).
% 29.22/4.16 fof(f1790,plain,(
% 29.22/4.16 vsucc(vd520)=vd520|~sQ14_spl|~sQ10_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1207,f1193])).
% 29.22/4.16 fof(f1791,plain,(
% 29.22/4.16 $false|~sQ14_spl|~sQ10_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f1790,f187])).
% 29.22/4.16 fof(f1792,plain,(
% 29.22/4.16 ~sQ14_spl|~sQ10_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f1791])).
% 29.22/4.16 fof(f1802,plain,(
% 29.22/4.16 ![X0]: (greater(vmul(vd519,X0),vmul(vd520,X0))|~sQ3_spl)),
% 29.22/4.16 inference(resolution,[status(thm)],[f209,f85])).
% 29.22/4.16 fof(f1813,plain,(
% 29.22/4.16 ![X0,X1]: (X0=vplus(X1,sK1_skl(X0,X1))|X0=X1|less(X0,X1))),
% 29.22/4.16 inference(resolution,[status(thm)],[f165,f153])).
% 29.22/4.16 fof(f1859,plain,(
% 29.22/4.16 ![X0,X1]: (less(X0,X1)|X1=X0|X0=vplus(X1,sK3_skl(X0,X1)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f168,f221])).
% 29.22/4.16 fof(f1862,plain,(
% 29.22/4.16 ![X0,X1]: (greater(X0,X1)|X0=X1|X1=vplus(X0,sK3_skl(X1,X0)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f168,f124])).
% 29.22/4.16 fof(f1925,plain,(
% 29.22/4.16 vmul(vd518,vd519)=vmul(vd518,vd520)|~sQ16_spl|~sQ25_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1214,f1569])).
% 29.22/4.16 fof(f1926,plain,(
% 29.22/4.16 vd519=vd520|~sQ16_spl|~sQ25_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1925,f247])).
% 29.22/4.16 fof(f1957,plain,(
% 29.22/4.16 sQ14_spl|~sQ16_spl|~sQ25_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f1926,f1206,f1213,f1568])).
% 29.22/4.16 fof(f1959,definition,(
% 29.22/4.16 sQ37_spl <=> (greater(v1,vd518))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1960,plain,(
% 29.22/4.16 greater(v1,vd518)|~sQ37_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1959])).
% 29.22/4.16 fof(f1961,plain,(
% 29.22/4.16 ~greater(v1,vd518)|sQ37_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1959])).
% 29.22/4.16 fof(f1963,definition,(
% 29.22/4.16 sQ38_spl <=> (greater(vd518,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1964,plain,(
% 29.22/4.16 greater(vd518,v1)|~sQ38_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1963])).
% 29.22/4.16 fof(f1965,plain,(
% 29.22/4.16 ~greater(vd518,v1)|sQ38_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1963])).
% 29.22/4.16 fof(f1970,definition,(
% 29.22/4.16 sQ39_spl <=> (vd518=v1)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f1971,plain,(
% 29.22/4.16 vd518=v1|~sQ39_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f1970])).
% 29.22/4.16 fof(f2170,plain,(
% 29.22/4.16 ![X0,X1]: (greater(vsucc(vplus(X0,X1)),X1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f179,f550])).
% 29.22/4.16 fof(f2375,definition,(
% 29.22/4.16 sQ46_spl <=> (vmul(vd520,vd518)=vd518)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f2377,plain,(
% 29.22/4.16 ~vmul(vd520,vd518)=vd518|sQ46_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f2375])).
% 29.22/4.16 fof(f2424,definition,(
% 29.22/4.16 sQ48_spl <=> (greater(v1,vd519))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f2431,definition,(
% 29.22/4.16 sQ50_spl <=> (greater(vd519,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f2432,plain,(
% 29.22/4.16 greater(vd519,v1)|~sQ50_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f2431])).
% 29.22/4.16 fof(f2433,plain,(
% 29.22/4.16 ~greater(vd519,v1)|sQ50_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f2431])).
% 29.22/4.16 fof(f2600,plain,(
% 29.22/4.16 ![X0]: (~less(X0,X0)|less(v1,v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f90,f296])).
% 29.22/4.16 fof(f2607,definition,(
% 29.22/4.16 ![X0]: (sQ53_spl <=> (~less(X0,X0)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f2610,definition,(
% 29.22/4.16 sQ54_spl <=> (less(v1,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f2611,plain,(
% 29.22/4.16 less(v1,v1)|~sQ54_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f2610])).
% 29.22/4.16 fof(f2613,plain,(
% 29.22/4.16 sQ53_spl|sQ54_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f2600,f2607,f2610])).
% 29.22/4.16 fof(f2618,plain,(
% 29.22/4.16 ~greater(vmul(vd519,vd518),vmul(vd520,vd518))|~sQ16_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1214,f331])).
% 29.22/4.16 fof(f2660,plain,(
% 29.22/4.16 ![X0]: (X0=v1|less(vskolem2(X0),X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f1101,f152])).
% 29.22/4.16 fof(f2661,plain,(
% 29.22/4.16 ![X0]: (X0=v1|geq(X0,vskolem2(X0)))),
% 29.22/4.16 inference(resolution,[status(thm)],[f1101,f147])).
% 29.22/4.16 fof(f2731,plain,(
% 29.22/4.16 ![X0]: (greater(vsucc(vsucc(X0)),X0))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f180,f2170])).
% 29.22/4.16 fof(f2814,plain,(
% 29.22/4.16 ![X0]: (geq(vsucc(vsucc(X0)),X0))),
% 29.22/4.16 inference(resolution,[status(thm)],[f2731,f147])).
% 29.22/4.16 fof(f3409,plain,(
% 29.22/4.16 leq(vsucc(vd520),v1)|~sQ34_spl|~sQ3_spl),
% 29.22/4.16 inference(backward_demodulation,[status(thm)],[f1648,f875])).
% 29.22/4.16 fof(f3430,plain,(
% 29.22/4.16 ~vmul(v1,vd520)=vd519|~sQ39_spl|sQ31_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1971,f1639])).
% 29.22/4.16 fof(f3431,plain,(
% 29.22/4.16 ~vd520=vd519|~sQ39_spl|sQ31_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f90,f3430])).
% 29.22/4.16 fof(f3432,plain,(
% 29.22/4.16 ~greater(vmul(vd517,vd519),vmul(v1,vd520))|~sQ39_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1971,f61])).
% 29.22/4.16 fof(f3433,plain,(
% 29.22/4.16 ~greater(vmul(vd517,vd519),vd520)|~sQ39_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f90,f3432])).
% 29.22/4.16 fof(f3434,plain,(
% 29.22/4.16 vmul(vd517,vd519)=vd520|less(vmul(vd517,vd519),vd520)|~sQ39_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f3433,f153])).
% 29.22/4.16 fof(f3437,definition,(
% 29.22/4.16 sQ63_spl <=> (vmul(vd517,vd519)=vd520)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f3438,plain,(
% 29.22/4.16 vmul(vd517,vd519)=vd520|~sQ63_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f3437])).
% 29.22/4.16 fof(f3440,definition,(
% 29.22/4.16 sQ64_spl <=> (less(vmul(vd517,vd519),vd520))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f3443,plain,(
% 29.22/4.16 sQ63_spl|sQ64_spl|~sQ39_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f3434,f3437,f3440,f1970])).
% 29.22/4.16 fof(f3519,plain,(
% 29.22/4.16 geq(vd518,vsucc(v1))|~sQ38_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1964,f758])).
% 29.22/4.16 fof(f3524,plain,(
% 29.22/4.16 ~less(vd518,v1)|~sQ38_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1964,f155])).
% 29.22/4.16 fof(f3525,plain,(
% 29.22/4.16 less(v1,vd518)|~sQ38_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1964,f152])).
% 29.22/4.16 fof(f3542,plain,(
% 29.22/4.16 ~less(v1,vd518)|~sQ37_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1960,f155])).
% 29.22/4.16 fof(f3554,plain,(
% 29.22/4.16 ~greater(vmul(vd517,vd520),vmul(vd518,vd520))|~sQ14_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1207,f61])).
% 29.22/4.16 fof(f3585,plain,(
% 29.22/4.16 ~greater(vd520,v1)|~sQ14_spl|sQ50_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1207,f2433])).
% 29.22/4.16 fof(f3612,plain,(
% 29.22/4.16 $false|~sQ38_spl|~sQ37_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f3542,f3525])).
% 29.22/4.16 fof(f3613,plain,(
% 29.22/4.16 ~sQ38_spl|~sQ37_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f3612])).
% 29.22/4.16 fof(f3615,plain,(
% 29.22/4.16 vd520=v1|less(vd520,v1)|~sQ14_spl|sQ50_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f3585,f153])).
% 29.22/4.16 fof(f3619,plain,(
% 29.22/4.16 vd518=v1|sQ38_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1965,f1106])).
% 29.22/4.16 fof(f3621,definition,(
% 29.22/4.16 sQ69_spl <=> (less(vd518,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f3622,plain,(
% 29.22/4.16 less(vd518,v1)|~sQ69_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f3621])).
% 29.22/4.16 fof(f3626,plain,(
% 29.22/4.16 ~sQ14_spl|~sQ39_spl|sQ31_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f3431,f1206,f1970,f1637])).
% 29.22/4.16 fof(f3631,definition,(
% 29.22/4.16 sQ70_spl <=> (vd520=v1)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f3632,plain,(
% 29.22/4.16 vd520=v1|~sQ70_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f3631])).
% 29.22/4.16 fof(f3634,definition,(
% 29.22/4.16 sQ71_spl <=> (less(vd520,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f3635,plain,(
% 29.22/4.16 less(vd520,v1)|~sQ71_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f3634])).
% 29.22/4.16 fof(f3636,plain,(
% 29.22/4.16 ~less(vd520,v1)|sQ71_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f3634])).
% 29.22/4.16 fof(f3637,plain,(
% 29.22/4.16 sQ70_spl|sQ71_spl|~sQ14_spl|sQ50_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f3615,f3631,f3634,f1206,f2431])).
% 29.22/4.16 fof(f3657,definition,(
% 29.22/4.16 sQ72_spl <=> (less(vd517,v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f3658,plain,(
% 29.22/4.16 less(vd517,v1)|~sQ72_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f3657])).
% 29.22/4.16 fof(f4004,plain,(
% 29.22/4.16 $false|~sQ34_spl|~sQ3_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f3409,f1458])).
% 29.22/4.16 fof(f4005,plain,(
% 29.22/4.16 ~sQ34_spl|~sQ3_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f4004])).
% 29.22/4.16 fof(f4009,plain,(
% 29.22/4.16 ~greater(vmul(vd517,v1),vmul(vd518,vd520))|~sQ34_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1648,f61])).
% 29.22/4.16 fof(f4010,plain,(
% 29.22/4.16 ~greater(vd517,vmul(vd518,vd520))|~sQ34_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f93,f4009])).
% 29.22/4.16 fof(f4015,plain,(
% 29.22/4.16 vd520=v1|~sQ34_spl|~sQ14_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f1648,f1207])).
% 29.22/4.16 fof(f4129,plain,(
% 29.22/4.16 geq(vd519,vsucc(v1))|~sQ50_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f2432,f758])).
% 29.22/4.16 fof(f4135,plain,(
% 29.22/4.16 less(v1,vd519)|~sQ50_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f2432,f152])).
% 29.22/4.16 fof(f4172,plain,(
% 29.22/4.16 vd519=v1|geq(vd519,vd520)|~sQ10_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1676,f2661])).
% 29.22/4.16 fof(f4186,plain,(
% 29.22/4.16 sQ34_spl|sQ1_spl|~sQ10_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f4172,f1647,f200,f1192])).
% 29.22/4.16 fof(f4302,plain,(
% 29.22/4.16 ![X0]: (less(vmul(v1,X0),vmul(vd519,X0))|~sQ50_spl)),
% 29.22/4.16 inference(resolution,[status(thm)],[f4135,f79])).
% 29.22/4.16 fof(f4305,plain,(
% 29.22/4.16 ![X0]: (less(X0,vmul(vd519,X0))|~sQ50_spl)),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f90,f4302])).
% 29.22/4.16 fof(f4313,plain,(
% 29.22/4.16 less(vd520,vsucc(vd519))|~sQ17_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1518,f152])).
% 29.22/4.16 fof(f4326,definition,(
% 29.22/4.16 sQ77_spl <=> (greater(vd517,vsucc(v1)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f4327,plain,(
% 29.22/4.16 greater(vd517,vsucc(v1))|~sQ77_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4326])).
% 29.22/4.16 fof(f4328,plain,(
% 29.22/4.16 ~greater(vd517,vsucc(v1))|sQ77_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4326])).
% 29.22/4.16 fof(f4329,definition,(
% 29.22/4.16 sQ78_spl <=> (vd517=vsucc(v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f4330,plain,(
% 29.22/4.16 vd517=vsucc(v1)|~sQ78_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4329])).
% 29.22/4.16 fof(f4348,plain,(
% 29.22/4.16 ~less(vd520,vd519)|less(vd517,v1)|~sQ63_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f3438,f300])).
% 29.22/4.16 fof(f4389,plain,(
% 29.22/4.16 ~sQ13_spl|sQ72_spl|~sQ63_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f4348,f1203,f3657,f3437])).
% 29.22/4.16 fof(f4390,definition,(
% 29.22/4.16 sQ79_spl <=> (less(v1,vd517))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f4391,plain,(
% 29.22/4.16 less(v1,vd517)|~sQ79_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4390])).
% 29.22/4.16 fof(f4541,plain,(
% 29.22/4.16 greater(vd519,vsucc(v1))|vd519=vsucc(v1)|~sQ50_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f4129,f146])).
% 29.22/4.16 fof(f4545,definition,(
% 29.22/4.16 sQ82_spl <=> (greater(vd519,vsucc(v1)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f4546,plain,(
% 29.22/4.16 greater(vd519,vsucc(v1))|~sQ82_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4545])).
% 29.22/4.16 fof(f4548,definition,(
% 29.22/4.16 sQ83_spl <=> (vd519=vsucc(v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f4549,plain,(
% 29.22/4.16 vd519=vsucc(v1)|~sQ83_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4548])).
% 29.22/4.16 fof(f4550,plain,(
% 29.22/4.16 ~vd519=vsucc(v1)|sQ83_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4548])).
% 29.22/4.16 fof(f4551,plain,(
% 29.22/4.16 sQ82_spl|sQ83_spl|~sQ50_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f4541,f4545,f4548,f2431])).
% 29.22/4.16 fof(f4559,plain,(
% 29.22/4.16 geq(vd517,vsucc(v1))|~sQ30_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1634,f758])).
% 29.22/4.16 fof(f4565,plain,(
% 29.22/4.16 less(v1,vd517)|~sQ30_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1634,f152])).
% 29.22/4.16 fof(f4568,plain,(
% 29.22/4.16 ![X0]: (greater(vmul(vd517,X0),vmul(v1,X0))|~sQ30_spl)),
% 29.22/4.16 inference(resolution,[status(thm)],[f1634,f85])).
% 29.22/4.16 fof(f4576,plain,(
% 29.22/4.16 ![X0]: (greater(vmul(vd517,X0),X0)|~sQ30_spl)),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f90,f4568])).
% 29.22/4.16 fof(f4591,plain,(
% 29.22/4.16 less(vd517,v1)|~sQ28_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1627,f152])).
% 29.22/4.16 fof(f4606,plain,(
% 29.22/4.16 ~leq(v1,vd517)|~sQ72_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f3658,f1146])).
% 29.22/4.16 fof(f4614,plain,(
% 29.22/4.16 $false|~sQ72_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f4606,f388])).
% 29.22/4.16 fof(f4615,plain,(
% 29.22/4.16 ~sQ72_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f4614])).
% 29.22/4.16 fof(f4640,plain,(
% 29.22/4.16 v1=vskolem2(vd519)|~sQ83_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f4549,f1115])).
% 29.22/4.16 fof(f4908,plain,(
% 29.22/4.16 v1=vd518|less(v1,vd518)|sQ37_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1961,f153])).
% 29.22/4.16 fof(f4909,definition,(
% 29.22/4.16 sQ85_spl <=> (less(v1,vd518))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f4910,plain,(
% 29.22/4.16 less(v1,vd518)|~sQ85_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f4909])).
% 29.22/4.16 fof(f4912,plain,(
% 29.22/4.16 sQ39_spl|sQ85_spl|sQ37_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f4908,f1970,f4909,f1959])).
% 29.22/4.16 fof(f4917,plain,(
% 29.22/4.16 ~leq(vd517,v1)|~sQ30_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f4565,f1146])).
% 29.22/4.16 fof(f4930,plain,(
% 29.22/4.16 ~greater(vmul(vd517,vd519),vmul(vd518,v1))|~sQ70_spl),
% 29.22/4.16 inference(backward_demodulation,[status(thm)],[f3632,f61])).
% 29.22/4.16 fof(f4932,plain,(
% 29.22/4.16 ~vsucc(v1)=vd519|~sQ70_spl|sQ10_spl),
% 29.22/4.16 inference(backward_demodulation,[status(thm)],[f3632,f1194])).
% 29.22/4.16 fof(f4933,plain,(
% 29.22/4.16 ~greater(vmul(vd517,vd519),vd518)|~sQ70_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f93,f4930])).
% 29.22/4.16 fof(f4936,plain,(
% 29.22/4.16 ~greater(vd517,vmul(vd518,v1))|~sQ70_spl|~sQ34_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f3632,f4010])).
% 29.22/4.16 fof(f4937,plain,(
% 29.22/4.16 ~greater(vd517,vd518)|~sQ70_spl|~sQ34_spl),
% 29.22/4.16 inference(forward_demodulation,[status(thm)],[f93,f4936])).
% 29.22/4.16 fof(f4938,plain,(
% 29.22/4.16 $false|~sQ2_spl|~sQ70_spl|~sQ34_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f4937,f205])).
% 29.22/4.16 fof(f4939,plain,(
% 29.22/4.16 ~sQ2_spl|~sQ70_spl|~sQ34_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f4938])).
% 29.22/4.16 fof(f4948,plain,(
% 29.22/4.16 ~greater(vmul(vd519,vd517),vmul(vd518,vd520))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f61])).
% 29.22/4.16 fof(f4953,plain,(
% 29.22/4.16 vd517=v1|sQ30_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1635,f1106])).
% 29.22/4.16 fof(f4959,plain,(
% 29.22/4.16 ~leq(v1,vd518)|sQ30_spl|~sQ2_spl),
% 29.22/4.16 inference(backward_demodulation,[status(thm)],[f4953,f1772])).
% 29.22/4.16 fof(f4967,plain,(
% 29.22/4.16 $false|sQ30_spl|~sQ2_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f4959,f388])).
% 29.22/4.16 fof(f4968,plain,(
% 29.22/4.16 sQ30_spl|~sQ2_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f4967])).
% 29.22/4.16 fof(f5129,plain,(
% 29.22/4.16 v1=vd517|less(v1,vd517)|sQ28_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1628,f153])).
% 29.22/4.16 fof(f5130,plain,(
% 29.22/4.16 sQ32_spl|sQ79_spl|sQ28_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5129,f1640,f4390,f1626])).
% 29.22/4.16 fof(f5137,plain,(
% 29.22/4.16 ~leq(v1,v1)|~sQ32_spl|~sQ30_spl),
% 29.22/4.16 inference(backward_demodulation,[status(thm)],[f1641,f4917])).
% 29.22/4.16 fof(f5147,plain,(
% 29.22/4.16 $false|~sQ32_spl|~sQ30_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f5137,f388])).
% 29.22/4.16 fof(f5148,plain,(
% 29.22/4.16 ~sQ32_spl|~sQ30_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f5147])).
% 29.22/4.16 fof(f5163,plain,(
% 29.22/4.16 geq(vd519,vsucc(v1))|~sQ10_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1699,f758])).
% 29.22/4.16 fof(f5213,plain,(
% 29.22/4.16 ~vskolem2(vd520)=vd519|vd520=v1|~sQ10_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1193,f1092])).
% 29.22/4.16 fof(f5264,definition,(
% 29.22/4.16 sQ86_spl <=> (vskolem2(vd520)=vd519)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5266,plain,(
% 29.22/4.16 ~vskolem2(vd520)=vd519|sQ86_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f5264])).
% 29.22/4.16 fof(f5267,plain,(
% 29.22/4.16 ~sQ86_spl|sQ70_spl|~sQ10_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5213,f5264,f3631,f1192])).
% 29.22/4.16 fof(f5299,plain,(
% 29.22/4.16 ~greater(vmul(vd519,vd517),vmul(vd518,vd520))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f61])).
% 29.22/4.16 fof(f5454,plain,(
% 29.22/4.16 ![X0]: (~less(vplus(X0,X0),X0)|less(vsucc(v1),v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f411,f300])).
% 29.22/4.16 fof(f5459,plain,(
% 29.22/4.16 ![X0]: (~less(X0,vplus(X0,X0))|less(v1,vsucc(v1)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f411,f296])).
% 29.22/4.16 fof(f5469,plain,(
% 29.22/4.16 ![X0]: (~greater(X0,vplus(X0,X0))|greater(v1,vsucc(v1)))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f411,f269])).
% 29.22/4.16 fof(f5475,plain,(
% 29.22/4.16 ![X0]: (~greater(vplus(X0,X0),X0)|greater(vsucc(v1),v1))),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f411,f268])).
% 29.22/4.16 fof(f5480,plain,(
% 29.22/4.16 ![X0]: (~vplus(X0,X0)=X0|vsucc(v1)=v1)),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f411,f274])).
% 29.22/4.16 fof(f5587,definition,(
% 29.22/4.16 ![X0]: (sQ87_spl <=> (~less(vplus(X0,X0),X0)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5590,definition,(
% 29.22/4.16 sQ88_spl <=> (less(vsucc(v1),v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5591,plain,(
% 29.22/4.16 less(vsucc(v1),v1)|~sQ88_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f5590])).
% 29.22/4.16 fof(f5593,plain,(
% 29.22/4.16 sQ87_spl|sQ88_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5454,f5587,f5590])).
% 29.22/4.16 fof(f5594,definition,(
% 29.22/4.16 ![X0]: (sQ89_spl <=> (~less(X0,vplus(X0,X0))))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5595,plain,(
% 29.22/4.16 ![X0]: (~less(X0,vplus(X0,X0))|~sQ89_spl)),
% 29.22/4.16 inference(component_clause,[status(thm)],[f5594])).
% 29.22/4.16 fof(f5597,definition,(
% 29.22/4.16 sQ90_spl <=> (less(v1,vsucc(v1)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5600,plain,(
% 29.22/4.16 sQ89_spl|sQ90_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5459,f5594,f5597])).
% 29.22/4.16 fof(f5601,definition,(
% 29.22/4.16 ![X0]: (sQ91_spl <=> (~greater(X0,vplus(X0,X0))))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5604,definition,(
% 29.22/4.16 sQ92_spl <=> (greater(v1,vsucc(v1)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5605,plain,(
% 29.22/4.16 greater(v1,vsucc(v1))|~sQ92_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f5604])).
% 29.22/4.16 fof(f5606,plain,(
% 29.22/4.16 ~greater(v1,vsucc(v1))|sQ92_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f5604])).
% 29.22/4.16 fof(f5607,plain,(
% 29.22/4.16 sQ91_spl|sQ92_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5469,f5601,f5604])).
% 29.22/4.16 fof(f5610,definition,(
% 29.22/4.16 ![X0]: (sQ93_spl <=> (~greater(vplus(X0,X0),X0)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5611,plain,(
% 29.22/4.16 ![X0]: (~greater(vplus(X0,X0),X0)|~sQ93_spl)),
% 29.22/4.16 inference(component_clause,[status(thm)],[f5610])).
% 29.22/4.16 fof(f5613,definition,(
% 29.22/4.16 sQ94_spl <=> (greater(vsucc(v1),v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5616,plain,(
% 29.22/4.16 sQ93_spl|sQ94_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5475,f5610,f5613])).
% 29.22/4.16 fof(f5624,definition,(
% 29.22/4.16 ![X0]: (sQ95_spl <=> (~vplus(X0,X0)=X0))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5627,definition,(
% 29.22/4.16 sQ96_spl <=> (vsucc(v1)=v1)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5628,plain,(
% 29.22/4.16 vsucc(v1)=v1|~sQ96_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f5627])).
% 29.22/4.16 fof(f5630,plain,(
% 29.22/4.16 sQ95_spl|sQ96_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5480,f5624,f5627])).
% 29.22/4.16 fof(f5637,plain,(
% 29.22/4.16 $false|~sQ93_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f5611,f550])).
% 29.22/4.16 fof(f5638,plain,(
% 29.22/4.16 ~sQ93_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f5637])).
% 29.22/4.16 fof(f5639,plain,(
% 29.22/4.16 $false|~sQ89_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f5595,f547])).
% 29.22/4.16 fof(f5640,plain,(
% 29.22/4.16 ~sQ89_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f5639])).
% 29.22/4.16 fof(f5641,plain,(
% 29.22/4.16 $false|~sQ96_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f5628,f192])).
% 29.22/4.16 fof(f5642,plain,(
% 29.22/4.16 ~sQ96_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f5641])).
% 29.22/4.16 fof(f5643,plain,(
% 29.22/4.16 $false|~sQ88_spl),
% 29.22/4.16 inference(forward_subsumption_resolution,[status(thm)],[f5591,f622])).
% 29.22/4.16 fof(f5644,plain,(
% 29.22/4.16 ~sQ88_spl),
% 29.22/4.16 inference(contradiction_clause,[status(thm)],[f5643])).
% 29.22/4.16 fof(f5851,plain,(
% 29.22/4.16 ~vmul(vd519,vd517)=vmul(vd518,vd520)|sQ25_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f88,f1570])).
% 29.22/4.16 fof(f5853,plain,(
% 29.22/4.16 ~sQ21_spl|sQ25_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5851,f1554,f1568])).
% 29.22/4.16 fof(f5876,definition,(
% 29.22/4.16 sQ98_spl <=> (vd519=vplus(v1,sK3_skl(vd519,v1)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5893,plain,(
% 29.22/4.16 vd519=vd520|vd519=vplus(vd520,sK2_skl(vd520,vd519))|~sQ10_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1684,f168])).
% 29.22/4.16 fof(f5894,plain,(
% 29.22/4.16 vd520=vd519|vd519=vplus(vd520,sK3_skl(vd519,vd520))|~sQ10_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f1684,f168])).
% 29.22/4.16 fof(f5901,definition,(
% 29.22/4.16 sQ99_spl <=> (vd519=vplus(vd520,sK2_skl(vd520,vd519)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5904,plain,(
% 29.22/4.16 sQ14_spl|sQ99_spl|~sQ10_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5893,f1206,f5901,f1192])).
% 29.22/4.16 fof(f5905,definition,(
% 29.22/4.16 sQ100_spl <=> (vd519=vplus(vd520,sK3_skl(vd519,vd520)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f5908,plain,(
% 29.22/4.16 sQ14_spl|sQ100_spl|~sQ10_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f5894,f1206,f5905,f1192])).
% 29.22/4.16 fof(f6091,plain,(
% 29.22/4.16 greater(vd518,vsucc(v1))|vd518=vsucc(v1)|~sQ38_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f3519,f146])).
% 29.22/4.16 fof(f6094,plain,(
% 29.22/4.16 leq(vsucc(v1),vd518)|~sQ38_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f3519,f138])).
% 29.22/4.16 fof(f6095,definition,(
% 29.22/4.16 sQ101_spl <=> (greater(vd518,vsucc(v1)))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f6096,plain,(
% 29.22/4.16 greater(vd518,vsucc(v1))|~sQ101_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f6095])).
% 29.22/4.16 fof(f6098,definition,(
% 29.22/4.16 sQ102_spl <=> (vd518=vsucc(v1))),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 29.22/4.16 fof(f6099,plain,(
% 29.22/4.16 vd518=vsucc(v1)|~sQ102_spl),
% 29.22/4.16 inference(component_clause,[status(thm)],[f6098])).
% 29.22/4.16 fof(f6101,plain,(
% 29.22/4.16 sQ101_spl|sQ102_spl|~sQ38_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f6091,f6095,f6098,f1963])).
% 29.22/4.16 fof(f6153,plain,(
% 29.22/4.16 ~less(vd519,vsucc(v1))|~sQ82_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f4546,f155])).
% 29.22/4.16 fof(f6445,plain,(
% 29.22/4.16 greater(vd517,vsucc(v1))|vd517=vsucc(v1)|~sQ30_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f4559,f146])).
% 29.22/4.16 fof(f6448,plain,(
% 29.22/4.16 leq(vsucc(v1),vd517)|~sQ30_spl),
% 29.22/4.16 inference(resolution,[status(thm)],[f4559,f138])).
% 29.22/4.16 fof(f6449,plain,(
% 29.22/4.16 sQ77_spl|sQ78_spl|~sQ30_spl),
% 29.22/4.16 inference(split_clause,[status(thm)],[f6445,f4326,f4329,f1633])).
% 29.22/4.16 fof(f6463,plain,(
% 29.22/4.16 ![X0]: (~less(vmul(vd517,X0),X0)|~sQ30_spl)),
% 29.22/4.16 inference(resolution,[status(thm)],[f4576,f155])).
% 29.22/4.16 fof(f6650,plain,(
% 29.22/4.16 vd520=vd520|~vd519=vd519|~sQ10_spl),
% 29.22/4.16 inference(paramodulation,[status(thm)],[f1193,f1681])).
% 29.22/4.16 fof(f6652,definition,(
% 29.22/4.16 sQ103_spl <=> (vskolem2(vd519)=vd520)),
% 29.22/4.16 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f6653,plain,(
% 29.22/4.17 vskolem2(vd519)=vd520|~sQ103_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f6652])).
% 29.22/4.17 fof(f6654,plain,(
% 29.22/4.17 ~vskolem2(vd519)=vd520|sQ103_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f6652])).
% 29.22/4.17 fof(f6656,definition,(
% 29.22/4.17 sQ104_spl <=> (vd520=vd520)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f6659,definition,(
% 29.22/4.17 sQ105_spl <=> (vd519=vd519)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f6661,plain,(
% 29.22/4.17 ~vd519=vd519|sQ105_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f6659])).
% 29.22/4.17 fof(f6662,plain,(
% 29.22/4.17 sQ104_spl|~sQ105_spl|~sQ10_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f6650,f6656,f6659,f1192])).
% 29.22/4.17 fof(f6817,definition,(
% 29.22/4.17 sQ107_spl <=> (vd517=vsucc(vd518))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f6818,plain,(
% 29.22/4.17 vd517=vsucc(vd518)|~sQ107_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f6817])).
% 29.22/4.17 fof(f6823,plain,(
% 29.22/4.17 greater(vd519,vsucc(v1))|vd519=vsucc(v1)|~sQ10_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f5163,f146])).
% 29.22/4.17 fof(f6827,plain,(
% 29.22/4.17 sQ82_spl|sQ83_spl|~sQ10_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f6823,f4545,f4548,f1192])).
% 29.22/4.17 fof(f7120,definition,(
% 29.22/4.17 sQ108_spl <=> (less(vsucc(v1),vd519))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7121,plain,(
% 29.22/4.17 less(vsucc(v1),vd519)|~sQ108_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f7120])).
% 29.22/4.17 fof(f7126,plain,(
% 29.22/4.17 geq(vd517,vd519)|~sQ83_spl|~sQ30_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f4549,f4559])).
% 29.22/4.17 fof(f7128,plain,(
% 29.22/4.17 greater(vd519,vd519)|~sQ83_spl|~sQ82_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f4549,f4546])).
% 29.22/4.17 fof(f7129,plain,(
% 29.22/4.17 geq(vd518,vd519)|~sQ83_spl|~sQ38_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f4549,f3519])).
% 29.22/4.17 fof(f7138,plain,(
% 29.22/4.17 v1=vd520|~vd519=vd519|~sQ10_spl|~sQ83_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f4549,f1681])).
% 29.22/4.17 fof(f7196,plain,(
% 29.22/4.17 $false|~sQ83_spl|~sQ82_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f7128,f220])).
% 29.22/4.17 fof(f7197,plain,(
% 29.22/4.17 ~sQ83_spl|~sQ82_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f7196])).
% 29.22/4.17 fof(f7331,plain,(
% 29.22/4.17 less(vsucc(v1),vd518)|vsucc(v1)=vd518|~sQ38_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f6094,f141])).
% 29.22/4.17 fof(f7334,definition,(
% 29.22/4.17 sQ109_spl <=> (less(vsucc(v1),vd518))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7337,plain,(
% 29.22/4.17 sQ109_spl|sQ102_spl|~sQ38_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7331,f7334,f6098,f1963])).
% 29.22/4.17 fof(f7339,plain,(
% 29.22/4.17 ~vd519=vd518|~sQ102_spl|sQ83_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f6099,f4550])).
% 29.22/4.17 fof(f7408,definition,(
% 29.22/4.17 sQ110_spl <=> (vd518=vd519)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7409,plain,(
% 29.22/4.17 vd518=vd519|~sQ110_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f7408])).
% 29.22/4.17 fof(f7446,plain,(
% 29.22/4.17 vsucc(v1)=vd519|~sQ70_spl|~sQ10_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f3632,f1193])).
% 29.22/4.17 fof(f7459,plain,(
% 29.22/4.17 sQ83_spl|~sQ70_spl|~sQ10_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7446,f4548,f3631,f1192])).
% 29.22/4.17 fof(f7464,plain,(
% 29.22/4.17 sQ70_spl|~sQ105_spl|~sQ10_spl|~sQ83_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7138,f3631,f6659,f1192,f4548])).
% 29.22/4.17 fof(f7479,plain,(
% 29.22/4.17 $false|sQ105_spl),
% 29.22/4.17 inference(trivial_equality_resolution,[status(thm)],[f6661])).
% 29.22/4.17 fof(f7480,plain,(
% 29.22/4.17 sQ105_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f7479])).
% 29.22/4.17 fof(f7482,plain,(
% 29.22/4.17 ~leq(vd519,v1)|vd519=v1|~sQ83_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f4640,f1472])).
% 29.22/4.17 fof(f7483,plain,(
% 29.22/4.17 leq(v1,vd519)|vd519=v1|~sQ83_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f4640,f1099])).
% 29.22/4.17 fof(f7484,plain,(
% 29.22/4.17 vd519=v1|geq(vd519,v1)|~sQ83_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f4640,f2661])).
% 29.22/4.17 fof(f7485,plain,(
% 29.22/4.17 vd519=v1|less(v1,vd519)|~sQ83_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f4640,f2660])).
% 29.22/4.17 fof(f7487,plain,(
% 29.22/4.17 ~less(vd519,v1)|vd519=v1|~sQ83_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f4640,f1097])).
% 29.22/4.17 fof(f7490,definition,(
% 29.22/4.17 sQ112_spl <=> (leq(vd519,v1))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7493,plain,(
% 29.22/4.17 ~sQ112_spl|sQ34_spl|~sQ83_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7482,f7490,f1647,f4548])).
% 29.22/4.17 fof(f7494,definition,(
% 29.22/4.17 sQ113_spl <=> (leq(v1,vd519))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7497,plain,(
% 29.22/4.17 sQ113_spl|sQ34_spl|~sQ83_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7483,f7494,f1647,f4548])).
% 29.22/4.17 fof(f7498,definition,(
% 29.22/4.17 sQ114_spl <=> (geq(vd519,v1))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7501,plain,(
% 29.22/4.17 sQ34_spl|sQ114_spl|~sQ83_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7484,f1647,f7498,f4548])).
% 29.22/4.17 fof(f7502,definition,(
% 29.22/4.17 sQ115_spl <=> (less(v1,vd519))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7505,plain,(
% 29.22/4.17 sQ34_spl|sQ115_spl|~sQ83_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7485,f1647,f7502,f4548])).
% 29.22/4.17 fof(f7507,definition,(
% 29.22/4.17 sQ116_spl <=> (less(vd519,v1))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7510,plain,(
% 29.22/4.17 ~sQ116_spl|sQ34_spl|~sQ83_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7487,f7507,f1647,f4548])).
% 29.22/4.17 fof(f7513,plain,(
% 29.22/4.17 greater(vd518,vd519)|vd518=vd519|~sQ83_spl|~sQ38_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7129,f146])).
% 29.22/4.17 fof(f7517,definition,(
% 29.22/4.17 sQ117_spl <=> (greater(vd518,vd519))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f7518,plain,(
% 29.22/4.17 greater(vd518,vd519)|~sQ117_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f7517])).
% 29.22/4.17 fof(f7519,plain,(
% 29.22/4.17 ~greater(vd518,vd519)|sQ117_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f7517])).
% 29.22/4.17 fof(f7520,plain,(
% 29.22/4.17 sQ117_spl|sQ110_spl|~sQ83_spl|~sQ38_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7513,f7517,f7408,f4548,f1963])).
% 29.22/4.17 fof(f7522,plain,(
% 29.22/4.17 sQ39_spl|sQ38_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f3619,f1970,f1963])).
% 29.22/4.17 fof(f7523,plain,(
% 29.22/4.17 v1=vd520|~sQ83_spl|~sQ103_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f4640,f6653])).
% 29.22/4.17 fof(f7538,plain,(
% 29.22/4.17 ~less(vd519,vd520)|~sQ3_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f209,f155])).
% 29.22/4.17 fof(f7894,plain,(
% 29.22/4.17 geq(vd518,vsucc(vd519))|~sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7518,f758])).
% 29.22/4.17 fof(f7899,plain,(
% 29.22/4.17 ~less(vd518,vd519)|~sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7518,f155])).
% 29.22/4.17 fof(f7900,plain,(
% 29.22/4.17 less(vd519,vd518)|~sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7518,f152])).
% 29.22/4.17 fof(f8097,definition,(
% 29.22/4.17 sQ120_spl <=> (less(vd519,vd518))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8098,plain,(
% 29.22/4.17 less(vd519,vd518)|~sQ120_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8097])).
% 29.22/4.17 fof(f8099,plain,(
% 29.22/4.17 ~less(vd519,vd518)|sQ120_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8097])).
% 29.22/4.17 fof(f8125,plain,(
% 29.22/4.17 greater(vd517,vd519)|vd517=vd519|~sQ83_spl|~sQ30_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7126,f146])).
% 29.22/4.17 fof(f8128,plain,(
% 29.22/4.17 leq(vd519,vd517)|~sQ83_spl|~sQ30_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7126,f138])).
% 29.22/4.17 fof(f8129,definition,(
% 29.22/4.17 sQ121_spl <=> (greater(vd517,vd519))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8130,plain,(
% 29.22/4.17 greater(vd517,vd519)|~sQ121_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8129])).
% 29.22/4.17 fof(f8132,definition,(
% 29.22/4.17 sQ122_spl <=> (vd517=vd519)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8133,plain,(
% 29.22/4.17 vd517=vd519|~sQ122_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8132])).
% 29.22/4.17 fof(f8135,plain,(
% 29.22/4.17 sQ121_spl|sQ122_spl|~sQ83_spl|~sQ30_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f8125,f8129,f8132,f4548,f1633])).
% 29.22/4.17 fof(f8186,plain,(
% 29.22/4.17 ~greater(vmul(vd519,vd517),vmul(vd518,v1))|~sQ83_spl|~sQ103_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f7523,f4948])).
% 29.22/4.17 fof(f8187,plain,(
% 29.22/4.17 ~greater(vmul(vd519,vd517),vd518)|~sQ83_spl|~sQ103_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f93,f8186])).
% 29.22/4.17 fof(f8188,plain,(
% 29.22/4.17 vmul(vd519,vd517)=vd518|less(vmul(vd519,vd517),vd518)|~sQ83_spl|~sQ103_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8187,f153])).
% 29.22/4.17 fof(f8189,definition,(
% 29.22/4.17 sQ123_spl <=> (vmul(vd519,vd517)=vd518)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8192,definition,(
% 29.22/4.17 sQ124_spl <=> (less(vmul(vd519,vd517),vd518))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8195,plain,(
% 29.22/4.17 sQ123_spl|sQ124_spl|~sQ83_spl|~sQ103_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f8188,f8189,f8192,f4548,f6652])).
% 29.22/4.17 fof(f8253,plain,(
% 29.22/4.17 less(vd519,vd517)|vd519=vd517|~sQ83_spl|~sQ30_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8128,f141])).
% 29.22/4.17 fof(f8256,definition,(
% 29.22/4.17 sQ125_spl <=> (less(vd519,vd517))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8257,plain,(
% 29.22/4.17 less(vd519,vd517)|~sQ125_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8256])).
% 29.22/4.17 fof(f8259,plain,(
% 29.22/4.17 sQ125_spl|sQ122_spl|~sQ83_spl|~sQ30_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f8253,f8256,f8132,f4548,f1633])).
% 29.22/4.17 fof(f8262,plain,(
% 29.22/4.17 ~greater(v1,vd519)|~sQ122_spl|sQ28_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f8133,f1628])).
% 29.22/4.17 fof(f8266,plain,(
% 29.22/4.17 ~less(vd519,vd518)|~sQ122_spl|~sQ2_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f8133,f1757])).
% 29.22/4.17 fof(f8270,plain,(
% 29.22/4.17 ~vd518=vd519|~sQ122_spl|sQ16_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f8133,f1215])).
% 29.22/4.17 fof(f8277,plain,(
% 29.22/4.17 $false|~sQ117_spl|~sQ122_spl|~sQ2_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f8266,f7900])).
% 29.22/4.17 fof(f8278,plain,(
% 29.22/4.17 ~sQ117_spl|~sQ122_spl|~sQ2_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f8277])).
% 29.22/4.17 fof(f8291,plain,(
% 29.22/4.17 ~greater(vmul(vd517,vd518),vd518)|~sQ110_spl|~sQ70_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f7409,f4933])).
% 29.22/4.17 fof(f8292,plain,(
% 29.22/4.17 vmul(vd517,vd518)=vd518|less(vmul(vd517,vd518),vd518)|~sQ110_spl|~sQ70_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8291,f153])).
% 29.22/4.17 fof(f8295,definition,(
% 29.22/4.17 sQ126_spl <=> (vmul(vd517,vd518)=vd518)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8296,plain,(
% 29.22/4.17 vmul(vd517,vd518)=vd518|~sQ126_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8295])).
% 29.22/4.17 fof(f8298,definition,(
% 29.22/4.17 sQ127_spl <=> (less(vmul(vd517,vd518),vd518))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8299,plain,(
% 29.22/4.17 less(vmul(vd517,vd518),vd518)|~sQ127_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8298])).
% 29.22/4.17 fof(f8300,plain,(
% 29.22/4.17 ~less(vmul(vd517,vd518),vd518)|sQ127_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f8298])).
% 29.22/4.17 fof(f8301,plain,(
% 29.22/4.17 sQ126_spl|sQ127_spl|~sQ110_spl|~sQ70_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f8292,f8295,f8298,f7408,f3631])).
% 29.22/4.17 fof(f8303,plain,(
% 29.22/4.17 ~vmul(v1,vd518)=vd518|~sQ83_spl|~sQ103_spl|sQ46_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f7523,f2377])).
% 29.22/4.17 fof(f8304,plain,(
% 29.22/4.17 ~vd518=vd518|~sQ83_spl|~sQ103_spl|sQ46_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f90,f8303])).
% 29.22/4.17 fof(f8305,plain,(
% 29.22/4.17 $false|~sQ83_spl|~sQ103_spl|sQ46_spl),
% 29.22/4.17 inference(trivial_equality_resolution,[status(thm)],[f8304])).
% 29.22/4.17 fof(f8306,plain,(
% 29.22/4.17 ~sQ83_spl|~sQ103_spl|sQ46_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f8305])).
% 29.22/4.17 fof(f8438,plain,(
% 29.22/4.17 geq(vsucc(vd519),vd520)|~sQ10_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f1193,f2814])).
% 29.22/4.17 fof(f8452,plain,(
% 29.22/4.17 ![X0]: (X0=vd520|~vsucc(X0)=vd519|~sQ10_spl)),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f1193,f189])).
% 29.22/4.17 fof(f8631,plain,(
% 29.22/4.17 ![X0]: (~greater(vsucc(X0),vsucc(X0))|greater(v1,v1))),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f180,f731])).
% 29.22/4.17 fof(f8650,definition,(
% 29.22/4.17 ![X0]: (sQ128_spl <=> (~greater(vsucc(X0),vsucc(X0))))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f8653,plain,(
% 29.22/4.17 sQ128_spl|sQ8_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f8631,f8650,f504])).
% 29.22/4.17 fof(f8654,plain,(
% 29.22/4.17 $false|~sQ8_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f505,f220])).
% 29.22/4.17 fof(f8655,plain,(
% 29.22/4.17 ~sQ8_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f8654])).
% 29.22/4.17 fof(f8704,plain,(
% 29.22/4.17 v1=vplus(vsucc(v1),sK1_skl(v1,vsucc(v1)))|~sQ92_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f5605,f165])).
% 29.22/4.17 fof(f8717,plain,(
% 29.22/4.17 v1=vsucc(vplus(v1,sK1_skl(v1,vsucc(v1))))|~sQ92_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f179,f8704])).
% 29.22/4.17 fof(f8718,plain,(
% 29.22/4.17 v1=vsucc(vsucc(sK1_skl(v1,vsucc(v1))))|~sQ92_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f180,f8717])).
% 29.22/4.17 fof(f8719,plain,(
% 29.22/4.17 $false|~sQ92_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f8718,f192])).
% 29.22/4.17 fof(f8720,plain,(
% 29.22/4.17 ~sQ92_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f8719])).
% 29.22/4.17 fof(f8767,plain,(
% 29.22/4.17 leq(vd520,vd519)|~sQ17_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f4313,f759])).
% 29.22/4.17 fof(f8769,plain,(
% 29.22/4.17 ~less(vsucc(vd519),vd520)|~sQ17_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f4313,f1174])).
% 29.22/4.17 fof(f8776,plain,(
% 29.22/4.17 leq(vd520,vsucc(vd519))|~sQ17_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f4313,f142])).
% 29.22/4.17 fof(f8837,plain,(
% 29.22/4.17 ![X0]: (~less(vmul(vd519,X0),X0)|~sQ50_spl)),
% 29.22/4.17 inference(resolution,[status(thm)],[f4305,f1174])).
% 29.22/4.17 fof(f8880,plain,(
% 29.22/4.17 ~less(vd517,vsucc(v1))|~sQ77_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f4327,f155])).
% 29.22/4.17 fof(f8902,plain,(
% 29.22/4.17 ~less(vd518,vsucc(v1))|~sQ101_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f6096,f155])).
% 29.22/4.17 fof(f9091,plain,(
% 29.22/4.17 ![X0]: (~less(vsucc(X0),vsucc(X0))|less(v1,v1))),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f180,f815])).
% 29.22/4.17 fof(f9108,definition,(
% 29.22/4.17 ![X0]: (sQ129_spl <=> (~less(vsucc(X0),vsucc(X0))))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f9111,plain,(
% 29.22/4.17 sQ129_spl|sQ54_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f9091,f9108,f2610])).
% 29.22/4.17 fof(f9112,plain,(
% 29.22/4.17 $false|~sQ54_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f2611,f219])).
% 29.22/4.17 fof(f9113,plain,(
% 29.22/4.17 ~sQ54_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f9112])).
% 29.22/4.17 fof(f9698,plain,(
% 29.22/4.17 vd518=vd520|~vd517=vd519|~sQ10_spl|~sQ107_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f6818,f1681])).
% 29.22/4.17 fof(f9723,plain,(
% 29.22/4.17 ~vskolem2(vd518)=vd517|vd518=v1|~sQ107_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f6818,f1092])).
% 29.22/4.17 fof(f9773,definition,(
% 29.22/4.17 sQ131_spl <=> (vd518=vd520)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f9776,plain,(
% 29.22/4.17 sQ131_spl|~sQ122_spl|~sQ10_spl|~sQ107_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f9698,f9773,f8132,f1192,f6817])).
% 29.22/4.17 fof(f9778,definition,(
% 29.22/4.17 sQ132_spl <=> (vskolem2(vd518)=vd517)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f9781,plain,(
% 29.22/4.17 ~sQ132_spl|sQ39_spl|~sQ107_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f9723,f9778,f1970,f6817])).
% 29.22/4.17 fof(f9807,plain,(
% 29.22/4.17 greater(vd517,vd517)|~sQ78_spl|~sQ77_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f4330,f4327])).
% 29.22/4.17 fof(f9811,plain,(
% 29.22/4.17 v1=vd520|~vd517=vd519|~sQ10_spl|~sQ78_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f4330,f1681])).
% 29.22/4.17 fof(f9886,plain,(
% 29.22/4.17 $false|~sQ78_spl|~sQ77_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f9807,f220])).
% 29.22/4.17 fof(f9887,plain,(
% 29.22/4.17 ~sQ78_spl|~sQ77_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f9886])).
% 29.22/4.17 fof(f9985,plain,(
% 29.22/4.17 ~sQ48_spl|~sQ122_spl|sQ28_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f8262,f2424,f8132,f1626])).
% 29.22/4.17 fof(f10007,plain,(
% 29.22/4.17 less(vd520,vd519)|vd520=vd519|~sQ17_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8767,f141])).
% 29.22/4.17 fof(f10010,plain,(
% 29.22/4.17 sQ13_spl|sQ14_spl|~sQ17_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f10007,f1203,f1206,f1517])).
% 29.22/4.17 fof(f10022,plain,(
% 29.22/4.17 less(vd520,vd519)|~sQ3_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f209,f152])).
% 29.22/4.17 fof(f10029,plain,(
% 29.22/4.17 ~greater(vmul(vd519,vd517),vmul(vd518,vd520))),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f88,f61])).
% 29.22/4.17 fof(f10069,plain,(
% 29.22/4.17 ~leq(vd518,v1)|~sQ85_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f4910,f1146])).
% 29.22/4.17 fof(f10600,plain,(
% 29.22/4.17 vd518=vd519|less(vd518,vd519)|sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7519,f153])).
% 29.22/4.17 fof(f10601,definition,(
% 29.22/4.17 sQ134_spl <=> (less(vd518,vd519))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f10602,plain,(
% 29.22/4.17 less(vd518,vd519)|~sQ134_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f10601])).
% 29.22/4.17 fof(f10604,plain,(
% 29.22/4.17 sQ110_spl|sQ134_spl|sQ117_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f10600,f7408,f10601,f7517])).
% 29.22/4.17 fof(f10714,plain,(
% 29.22/4.17 ~less(vd518,vd519)|~sQ120_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8098,f1174])).
% 29.22/4.17 fof(f10720,plain,(
% 29.22/4.17 greater(vd518,vd519)|~sQ120_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8098,f150])).
% 29.22/4.17 fof(f10723,plain,(
% 29.22/4.17 sQ117_spl|~sQ120_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f10720,f7517,f8097])).
% 29.22/4.17 fof(f10794,definition,(
% 29.22/4.17 ![X0]: (sQ135_spl <=> (~vsucc(X0)=vsucc(X0)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f10795,plain,(
% 29.22/4.17 ![X0]: (~vsucc(X0)=vsucc(X0)|~sQ135_spl)),
% 29.22/4.17 inference(component_clause,[status(thm)],[f10794])).
% 29.22/4.17 fof(f10813,plain,(
% 29.22/4.17 less(vd519,vd518)|~sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7518,f152])).
% 29.22/4.17 fof(f11127,plain,(
% 29.22/4.17 less(vsucc(v1),vd517)|vsucc(v1)=vd517|~sQ30_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f6448,f141])).
% 29.22/4.17 fof(f11130,definition,(
% 29.22/4.17 sQ136_spl <=> (less(vsucc(v1),vd517))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f11133,plain,(
% 29.22/4.17 sQ136_spl|sQ78_spl|~sQ30_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f11127,f11130,f4329,f1633])).
% 29.22/4.17 fof(f11134,plain,(
% 29.22/4.17 sQ70_spl|~sQ122_spl|~sQ10_spl|~sQ78_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f9811,f3631,f8132,f1192,f4329])).
% 29.22/4.17 fof(f11552,plain,(
% 29.22/4.17 greater(vd519,vsucc(v1))|~sQ108_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7121,f150])).
% 29.22/4.17 fof(f11629,plain,(
% 29.22/4.17 ~less(vd519,v1)|~sQ50_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f93,f8837])).
% 29.22/4.17 fof(f11681,plain,(
% 29.22/4.17 v1=vsucc(v1)|vsucc(v1)=vplus(v1,sK3_skl(vsucc(v1),v1))|sQ92_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f1862,f5606])).
% 29.22/4.17 fof(f11682,plain,(
% 29.22/4.17 v1=vd518|vd518=vplus(v1,sK3_skl(vd518,v1))|sQ37_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f1862,f1961])).
% 29.22/4.17 fof(f11692,plain,(
% 29.22/4.17 vmul(vd519,vd517)=vmul(vd518,vd520)|vmul(vd518,vd520)=vplus(vmul(vd519,vd517),sK3_skl(vmul(vd518,vd520),vmul(vd519,vd517)))),
% 29.22/4.17 inference(resolution,[status(thm)],[f1862,f5299])).
% 29.22/4.17 fof(f11694,plain,(
% 29.22/4.17 vmul(vd517,vd519)=vmul(vd518,vd520)|vmul(vd518,vd520)=vplus(vmul(vd517,vd519),sK3_skl(vmul(vd518,vd520),vmul(vd517,vd519)))),
% 29.22/4.17 inference(resolution,[status(thm)],[f1862,f61])).
% 29.22/4.17 fof(f11726,definition,(
% 29.22/4.17 sQ138_spl <=> (vsucc(v1)=vplus(v1,sK3_skl(vsucc(v1),v1)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f11729,plain,(
% 29.22/4.17 sQ96_spl|sQ138_spl|sQ92_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f11681,f5627,f11726,f5604])).
% 29.22/4.17 fof(f11730,definition,(
% 29.22/4.17 sQ139_spl <=> (vd518=vplus(v1,sK3_skl(vd518,v1)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f11733,plain,(
% 29.22/4.17 sQ39_spl|sQ139_spl|sQ37_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f11682,f1970,f11730,f1959])).
% 29.22/4.17 fof(f11734,definition,(
% 29.22/4.17 sQ140_spl <=> (vd517=vplus(v1,sK3_skl(vd517,v1)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f11746,definition,(
% 29.22/4.17 sQ141_spl <=> (vmul(vd518,vd520)=vplus(vmul(vd519,vd517),sK3_skl(vmul(vd518,vd520),vmul(vd519,vd517))))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f11749,plain,(
% 29.22/4.17 sQ21_spl|sQ141_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f11692,f1554,f11746])).
% 29.22/4.17 fof(f11754,definition,(
% 29.22/4.17 sQ143_spl <=> (vmul(vd518,vd520)=vplus(vmul(vd517,vd519),sK3_skl(vmul(vd518,vd520),vmul(vd517,vd519))))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f11757,plain,(
% 29.22/4.17 sQ25_spl|sQ143_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f11694,f1568,f11754])).
% 29.22/4.17 fof(f12046,plain,(
% 29.22/4.17 less(vd520,vsucc(vd519))|vd520=vsucc(vd519)|~sQ17_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8776,f141])).
% 29.22/4.17 fof(f12049,plain,(
% 29.22/4.17 sQ11_spl|sQ12_spl|~sQ17_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f12046,f1196,f1199,f1517])).
% 29.22/4.17 fof(f12368,plain,(
% 29.22/4.17 greater(vsucc(vd519),vd520)|vsucc(vd519)=vd520|~sQ10_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f8438,f146])).
% 29.22/4.17 fof(f12377,plain,(
% 29.22/4.17 sQ17_spl|sQ12_spl|~sQ10_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f12368,f1517,f1199,f1192])).
% 29.22/4.17 fof(f13399,plain,(
% 29.22/4.17 greater(vd518,vsucc(vd519))|vd518=vsucc(vd519)|~sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7894,f146])).
% 29.22/4.17 fof(f13402,plain,(
% 29.22/4.17 leq(vsucc(vd519),vd518)|~sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7894,f138])).
% 29.22/4.17 fof(f13406,definition,(
% 29.22/4.17 sQ144_spl <=> (greater(vd518,vsucc(vd519)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f13409,definition,(
% 29.22/4.17 sQ145_spl <=> (vd518=vsucc(vd519))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f13410,plain,(
% 29.22/4.17 vd518=vsucc(vd519)|~sQ145_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f13409])).
% 29.22/4.17 fof(f13412,plain,(
% 29.22/4.17 sQ144_spl|sQ145_spl|~sQ117_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f13399,f13406,f13409,f7517])).
% 29.22/4.17 fof(f13415,plain,(
% 29.22/4.17 $false|~sQ120_spl|~sQ134_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f10602,f10714])).
% 29.22/4.17 fof(f13416,plain,(
% 29.22/4.17 ~sQ120_spl|~sQ134_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f13415])).
% 29.22/4.17 fof(f14522,plain,(
% 29.22/4.17 less(vsucc(vd519),vd518)|vsucc(vd519)=vd518|~sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f13402,f141])).
% 29.22/4.17 fof(f14525,definition,(
% 29.22/4.17 sQ147_spl <=> (less(vsucc(vd519),vd518))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f14526,plain,(
% 29.22/4.17 less(vsucc(vd519),vd518)|~sQ147_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f14525])).
% 29.22/4.17 fof(f14528,plain,(
% 29.22/4.17 sQ147_spl|sQ145_spl|~sQ117_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f14522,f14525,f13409,f7517])).
% 29.22/4.17 fof(f14561,plain,(
% 29.22/4.17 vd518=vd519|vd519=vplus(vd518,sK3_skl(vd519,vd518))|sQ117_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f7519,f1862])).
% 29.22/4.17 fof(f14563,definition,(
% 29.22/4.17 sQ148_spl <=> (vd519=vplus(vd518,sK3_skl(vd519,vd518)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f14566,plain,(
% 29.22/4.17 sQ110_spl|sQ148_spl|sQ117_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f14561,f7408,f14563,f7517])).
% 29.22/4.17 fof(f14576,plain,(
% 29.22/4.17 vd519=vd520|~vd518=vd519|~sQ10_spl|~sQ145_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f13410,f8452])).
% 29.22/4.17 fof(f14607,plain,(
% 29.22/4.17 ~vskolem2(vd519)=vd518|vd519=v1|~sQ145_spl),
% 29.22/4.17 inference(paramodulation,[status(thm)],[f13410,f1092])).
% 29.22/4.17 fof(f14657,plain,(
% 29.22/4.17 sQ14_spl|~sQ110_spl|~sQ10_spl|~sQ145_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f14576,f1206,f7408,f1192,f13409])).
% 29.22/4.17 fof(f14659,definition,(
% 29.22/4.17 sQ149_spl <=> (vskolem2(vd519)=vd518)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f14661,plain,(
% 29.22/4.17 ~vskolem2(vd519)=vd518|sQ149_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f14659])).
% 29.22/4.17 fof(f14662,plain,(
% 29.22/4.17 ~sQ149_spl|sQ34_spl|~sQ145_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f14607,f14659,f1647,f13409])).
% 29.22/4.17 fof(f14907,plain,(
% 29.22/4.17 vd518=vsucc(v1)|less(vsucc(v1),vd518)|~sQ101_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f1541,f8902])).
% 29.22/4.17 fof(f14909,plain,(
% 29.22/4.17 vd519=vsucc(v1)|less(vsucc(v1),vd519)|~sQ82_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f1541,f6153])).
% 29.22/4.17 fof(f14912,plain,(
% 29.22/4.17 vd517=vsucc(v1)|less(vsucc(v1),vd517)|~sQ77_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f1541,f8880])).
% 29.22/4.17 fof(f15105,plain,(
% 29.22/4.17 sQ102_spl|sQ109_spl|~sQ101_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f14907,f6098,f7334,f6095])).
% 29.22/4.17 fof(f15107,plain,(
% 29.22/4.17 sQ83_spl|sQ108_spl|~sQ82_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f14909,f4548,f7120,f4545])).
% 29.22/4.17 fof(f15110,plain,(
% 29.22/4.17 sQ78_spl|sQ136_spl|~sQ77_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f14912,f4329,f11130,f4326])).
% 29.22/4.17 fof(f15129,plain,(
% 29.22/4.17 $false|~sQ135_spl),
% 29.22/4.17 inference(trivial_equality_resolution,[status(thm)],[f10795])).
% 29.22/4.17 fof(f15130,plain,(
% 29.22/4.17 ~sQ135_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f15129])).
% 29.22/4.17 fof(f15131,plain,(
% 29.22/4.17 $false|~sQ30_spl|~sQ127_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f8299,f6463])).
% 29.22/4.17 fof(f15132,plain,(
% 29.22/4.17 ~sQ30_spl|~sQ127_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f15131])).
% 29.22/4.17 fof(f15133,plain,(
% 29.22/4.17 $false|~sQ38_spl|~sQ69_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f3622,f3524])).
% 29.22/4.17 fof(f15134,plain,(
% 29.22/4.17 ~sQ38_spl|~sQ69_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f15133])).
% 29.22/4.17 fof(f15135,plain,(
% 29.22/4.17 sQ70_spl|~sQ34_spl|~sQ14_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f4015,f3631,f1647,f1206])).
% 29.22/4.17 fof(f15136,plain,(
% 29.22/4.17 $false|sQ86_spl|~sQ12_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f1712,f5266])).
% 29.22/4.17 fof(f15137,plain,(
% 29.22/4.17 sQ86_spl|~sQ12_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f15136])).
% 29.22/4.17 fof(f15138,plain,(
% 29.22/4.17 $false|~sQ2_spl|~sQ14_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f3554,f262])).
% 29.22/4.17 fof(f15139,plain,(
% 29.22/4.17 ~sQ2_spl|~sQ14_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f15138])).
% 29.22/4.17 fof(f15140,plain,(
% 29.22/4.17 $false|~sQ117_spl|sQ120_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f8099,f10813])).
% 29.22/4.17 fof(f15141,plain,(
% 29.22/4.17 ~sQ117_spl|sQ120_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f15140])).
% 29.22/4.17 fof(f15142,plain,(
% 29.22/4.17 sQ13_spl|~sQ3_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f10022,f1203,f208])).
% 29.22/4.17 fof(f15144,plain,(
% 29.22/4.17 sQ72_spl|~sQ28_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f4591,f3657,f1626])).
% 29.22/4.17 fof(f15147,plain,(
% 29.22/4.17 ~sQ110_spl|~sQ102_spl|sQ83_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f7339,f7408,f6098,f4548])).
% 29.22/4.17 fof(f15499,plain,(
% 29.22/4.17 vd519=v1|sQ50_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f2433,f1106])).
% 29.22/4.17 fof(f15504,plain,(
% 29.22/4.17 sQ34_spl|sQ50_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f15499,f1647,f2431])).
% 29.22/4.17 fof(f15510,plain,(
% 29.22/4.17 ~sQ110_spl|~sQ122_spl|sQ16_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f8270,f7408,f8132,f1213])).
% 29.22/4.17 fof(f15511,plain,(
% 29.22/4.17 sQ82_spl|~sQ108_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f11552,f4545,f7120])).
% 29.22/4.17 fof(f15530,plain,(
% 29.22/4.17 ~leq(v1,v1)|~sQ39_spl|~sQ85_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f1971,f10069])).
% 29.22/4.17 fof(f15532,plain,(
% 29.22/4.17 ~vskolem2(vd519)=v1|~sQ39_spl|sQ149_spl),
% 29.22/4.17 inference(backward_demodulation,[status(thm)],[f1971,f14661])).
% 29.22/4.17 fof(f15535,plain,(
% 29.22/4.17 $false|~sQ39_spl|~sQ85_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f15530,f388])).
% 29.22/4.17 fof(f15536,plain,(
% 29.22/4.17 ~sQ39_spl|~sQ85_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f15535])).
% 29.22/4.17 fof(f15652,plain,(
% 29.22/4.17 ~greater(vmul(vd519,vd519),vd520)|~sQ122_spl|~sQ39_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f8133,f3433])).
% 29.22/4.17 fof(f15655,plain,(
% 29.22/4.17 vmul(vd519,vd519)=vd520|vd520=vplus(vmul(vd519,vd519),sK3_skl(vd520,vmul(vd519,vd519)))|~sQ122_spl|~sQ39_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f15652,f1862])).
% 29.22/4.17 fof(f15656,plain,(
% 29.22/4.17 vmul(vd519,vd519)=vd520|less(vmul(vd519,vd519),vd520)|~sQ122_spl|~sQ39_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f15652,f153])).
% 29.22/4.17 fof(f15657,definition,(
% 29.22/4.17 sQ151_spl <=> (vmul(vd519,vd519)=vd520)),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f15660,definition,(
% 29.22/4.17 sQ152_spl <=> (vd520=vplus(vmul(vd519,vd519),sK3_skl(vd520,vmul(vd519,vd519))))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f15663,plain,(
% 29.22/4.17 sQ151_spl|sQ152_spl|~sQ122_spl|~sQ39_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f15655,f15657,f15660,f8132,f1970])).
% 29.22/4.17 fof(f15664,definition,(
% 29.22/4.17 sQ153_spl <=> (less(vmul(vd519,vd519),vd520))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f15667,plain,(
% 29.22/4.17 sQ151_spl|sQ153_spl|~sQ122_spl|~sQ39_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f15656,f15657,f15664,f8132,f1970])).
% 29.22/4.17 fof(f16142,definition,(
% 29.22/4.17 sQ154_spl <=> (vd519=vplus(v1,sK1_skl(vd519,v1)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f16368,plain,(
% 29.22/4.17 ~v1=vd520|~sQ83_spl|sQ103_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f4640,f6654])).
% 29.22/4.17 fof(f16401,plain,(
% 29.22/4.17 ~leq(v1,vd520)|~sQ71_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f3635,f1146])).
% 29.22/4.17 fof(f16725,plain,(
% 29.22/4.17 greater(vd519,vd519)|~sQ122_spl|~sQ121_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f8133,f8130])).
% 29.22/4.17 fof(f16726,plain,(
% 29.22/4.17 $false|~sQ122_spl|~sQ121_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f16725,f220])).
% 29.22/4.17 fof(f16727,plain,(
% 29.22/4.17 ~sQ122_spl|~sQ121_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f16726])).
% 29.22/4.17 fof(f16729,plain,(
% 29.22/4.17 less(vd519,vd519)|~sQ122_spl|~sQ125_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f8133,f8257])).
% 29.22/4.17 fof(f16730,plain,(
% 29.22/4.17 $false|~sQ122_spl|~sQ125_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f16729,f219])).
% 29.22/4.17 fof(f16731,plain,(
% 29.22/4.17 ~sQ122_spl|~sQ125_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f16730])).
% 29.22/4.17 fof(f16749,plain,(
% 29.22/4.17 ~v1=v1|~sQ83_spl|~sQ39_spl|sQ149_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f4640,f15532])).
% 29.22/4.17 fof(f16750,plain,(
% 29.22/4.17 $false|~sQ83_spl|~sQ39_spl|sQ149_spl),
% 29.22/4.17 inference(trivial_equality_resolution,[status(thm)],[f16749])).
% 29.22/4.17 fof(f16751,plain,(
% 29.22/4.17 ~sQ83_spl|~sQ39_spl|sQ149_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f16750])).
% 29.22/4.17 fof(f16863,plain,(
% 29.22/4.17 vd520=vplus(v1,sK1_skl(vd520,v1))|vd520=v1|sQ71_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f3636,f1813])).
% 29.22/4.17 fof(f16864,plain,(
% 29.22/4.17 v1=vd520|less(v1,vd520)|sQ71_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f3636,f1541])).
% 29.22/4.17 fof(f16871,definition,(
% 29.22/4.17 sQ159_spl <=> (vd520=vplus(v1,sK1_skl(vd520,v1)))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f16874,plain,(
% 29.22/4.17 sQ159_spl|sQ70_spl|sQ71_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f16863,f16871,f3631,f3634])).
% 29.22/4.17 fof(f16875,definition,(
% 29.22/4.17 sQ160_spl <=> (less(v1,vd520))),
% 29.22/4.17 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 29.22/4.17 fof(f16876,plain,(
% 29.22/4.17 less(v1,vd520)|~sQ160_spl),
% 29.22/4.17 inference(component_clause,[status(thm)],[f16875])).
% 29.22/4.17 fof(f16878,plain,(
% 29.22/4.17 sQ70_spl|sQ160_spl|sQ71_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f16864,f3631,f16875,f3634])).
% 29.22/4.17 fof(f16896,plain,(
% 29.22/4.17 $false|~sQ83_spl|sQ103_spl|~sQ70_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f3632,f16368])).
% 29.22/4.17 fof(f16897,plain,(
% 29.22/4.17 ~sQ83_spl|sQ103_spl|~sQ70_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f16896])).
% 29.22/4.17 fof(f16923,plain,(
% 29.22/4.17 greater(vd520,v1)|~sQ160_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f16876,f150])).
% 29.22/4.17 fof(f16954,plain,(
% 29.22/4.17 geq(vd520,vsucc(v1))|~sQ160_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f16923,f758])).
% 29.22/4.17 fof(f16969,plain,(
% 29.22/4.17 geq(vd520,vd519)|~sQ83_spl|~sQ160_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f4549,f16954])).
% 29.22/4.17 fof(f16984,plain,(
% 29.22/4.17 leq(vd519,vd520)|~sQ83_spl|~sQ160_spl),
% 29.22/4.17 inference(resolution,[status(thm)],[f16969,f138])).
% 29.22/4.17 fof(f16986,plain,(
% 29.22/4.17 $false|~sQ3_spl|~sQ83_spl|~sQ160_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f16984,f1461])).
% 29.22/4.17 fof(f16987,plain,(
% 29.22/4.17 ~sQ3_spl|~sQ83_spl|~sQ160_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f16986])).
% 29.22/4.17 fof(f16990,plain,(
% 29.22/4.17 vmul(vd519,vd518)=vd518|~sQ122_spl|~sQ126_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f8133,f8296])).
% 29.22/4.17 fof(f16991,plain,(
% 29.22/4.17 vmul(vd519,v1)=vd518|~sQ39_spl|~sQ122_spl|~sQ126_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f1971,f16990])).
% 29.22/4.17 fof(f16992,plain,(
% 29.22/4.17 vd519=vd518|~sQ39_spl|~sQ122_spl|~sQ126_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f93,f16991])).
% 29.22/4.17 fof(f16993,plain,(
% 29.22/4.17 vd519=v1|~sQ39_spl|~sQ122_spl|~sQ126_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f1971,f16992])).
% 29.22/4.17 fof(f16994,plain,(
% 29.22/4.17 $false|sQ34_spl|~sQ39_spl|~sQ122_spl|~sQ126_spl),
% 29.22/4.17 inference(forward_subsumption_resolution,[status(thm)],[f16993,f1649])).
% 29.22/4.17 fof(f16995,plain,(
% 29.22/4.17 sQ34_spl|~sQ39_spl|~sQ122_spl|~sQ126_spl),
% 29.22/4.17 inference(contradiction_clause,[status(thm)],[f16994])).
% 29.22/4.17 fof(f16996,plain,(
% 29.22/4.17 ~sQ83_spl|~sQ70_spl|sQ10_spl),
% 29.22/4.17 inference(split_clause,[status(thm)],[f4932,f4548,f3631,f1192])).
% 29.22/4.17 fof(f16998,plain,(
% 29.22/4.17 ~greater(vd517,vd519)|~sQ83_spl|sQ77_spl),
% 29.22/4.17 inference(forward_demodulation,[status(thm)],[f4549,f4328])).
% 29.22/4.18 fof(f17278,plain,(
% 29.22/4.18 $false|~sQ71_spl),
% 29.22/4.18 inference(forward_subsumption_resolution,[status(thm)],[f16401,f388])).
% 29.22/4.18 fof(f17279,plain,(
% 29.22/4.18 ~sQ71_spl),
% 29.22/4.18 inference(contradiction_clause,[status(thm)],[f17278])).
% 29.22/4.18 fof(f17281,plain,(
% 29.22/4.18 less(vsucc(vd519),v1)|~sQ39_spl|~sQ147_spl),
% 29.22/4.18 inference(forward_demodulation,[status(thm)],[f1971,f14526])).
% 29.22/4.18 fof(f17282,plain,(
% 29.22/4.18 $false|~sQ39_spl|~sQ147_spl),
% 29.22/4.18 inference(forward_subsumption_resolution,[status(thm)],[f17281,f622])).
% 29.22/4.18 fof(f17283,plain,(
% 29.22/4.18 ~sQ39_spl|~sQ147_spl),
% 29.22/4.18 inference(contradiction_clause,[status(thm)],[f17282])).
% 29.22/4.18 fof(f17584,definition,(
% 29.22/4.18 sQ164_spl <=> (vd517=vplus(v1,sK1_skl(vd517,v1)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f17670,plain,(
% 29.22/4.18 ~less(vd517,v1)|~sQ79_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f4391,f1174])).
% 29.22/4.18 fof(f17718,plain,(
% 29.22/4.18 ~sQ121_spl|~sQ83_spl|sQ77_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f16998,f8129,f4548,f4326])).
% 29.22/4.18 fof(f17767,plain,(
% 29.22/4.18 ~greater(vmul(vd519,vd517),vmul(vd518,v1))|~sQ70_spl),
% 29.22/4.18 inference(forward_demodulation,[status(thm)],[f3632,f10029])).
% 29.22/4.18 fof(f17768,plain,(
% 29.22/4.18 ~greater(vmul(vd519,vd517),vd518)|~sQ70_spl),
% 29.22/4.18 inference(forward_demodulation,[status(thm)],[f93,f17767])).
% 29.22/4.18 fof(f17771,plain,(
% 29.22/4.18 vmul(vd519,vd517)=vd518|vd518=vplus(vmul(vd519,vd517),sK3_skl(vd518,vmul(vd519,vd517)))|~sQ70_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f17768,f1862])).
% 29.22/4.18 fof(f17773,definition,(
% 29.22/4.18 sQ169_spl <=> (vd518=vplus(vmul(vd519,vd517),sK3_skl(vd518,vmul(vd519,vd517))))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f17776,plain,(
% 29.22/4.18 sQ123_spl|sQ169_spl|~sQ70_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f17771,f8189,f17773,f3631])).
% 29.22/4.18 fof(f17944,plain,(
% 29.22/4.18 v1=vd517|vd517=vplus(v1,sK3_skl(vd517,v1))|~sQ79_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f17670,f1859])).
% 29.22/4.18 fof(f17945,plain,(
% 29.22/4.18 vd517=vplus(v1,sK1_skl(vd517,v1))|vd517=v1|~sQ79_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f17670,f1813])).
% 29.22/4.18 fof(f17953,plain,(
% 29.22/4.18 sQ32_spl|sQ140_spl|~sQ79_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f17944,f1640,f11734,f4390])).
% 29.22/4.18 fof(f17954,plain,(
% 29.22/4.18 sQ164_spl|sQ32_spl|~sQ79_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f17945,f17584,f1640,f4390])).
% 29.22/4.18 fof(f18210,plain,(
% 29.22/4.18 vd519=vd518|vd518=vplus(vd519,sK3_skl(vd518,vd519))|~sQ117_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f7899,f1859])).
% 29.22/4.18 fof(f18211,plain,(
% 29.22/4.18 vd518=vplus(vd519,sK1_skl(vd518,vd519))|vd518=vd519|~sQ117_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f7899,f1813])).
% 29.22/4.18 fof(f18219,definition,(
% 29.22/4.18 sQ174_spl <=> (vd518=vplus(vd519,sK3_skl(vd518,vd519)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f18222,plain,(
% 29.22/4.18 sQ110_spl|sQ174_spl|~sQ117_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18210,f7408,f18219,f7517])).
% 29.22/4.18 fof(f18223,definition,(
% 29.22/4.18 sQ175_spl <=> (vd518=vplus(vd519,sK1_skl(vd518,vd519)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f18226,plain,(
% 29.22/4.18 sQ175_spl|sQ110_spl|~sQ117_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18211,f18223,f7408,f7517])).
% 29.22/4.18 fof(f18286,plain,(
% 29.22/4.18 vd518=vplus(v1,sK1_skl(vd518,v1))|vd518=v1|~sQ38_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f3524,f1813])).
% 29.22/4.18 fof(f18295,definition,(
% 29.22/4.18 sQ176_spl <=> (vd518=vplus(v1,sK1_skl(vd518,v1)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f18298,plain,(
% 29.22/4.18 sQ176_spl|sQ39_spl|~sQ38_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18286,f18295,f1970,f1963])).
% 29.22/4.18 fof(f18559,plain,(
% 29.22/4.18 v1=vd519|vd519=vplus(v1,sK3_skl(vd519,v1))|~sQ50_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f11629,f1859])).
% 29.22/4.18 fof(f18560,plain,(
% 29.22/4.18 vd519=vplus(v1,sK1_skl(vd519,v1))|vd519=v1|~sQ50_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f11629,f1813])).
% 29.22/4.18 fof(f18561,plain,(
% 29.22/4.18 v1=vd519|less(v1,vd519)|~sQ50_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f11629,f1541])).
% 29.22/4.18 fof(f18568,plain,(
% 29.22/4.18 sQ34_spl|sQ98_spl|~sQ50_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18559,f1647,f5876,f2431])).
% 29.22/4.18 fof(f18569,plain,(
% 29.22/4.18 sQ154_spl|sQ34_spl|~sQ50_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18560,f16142,f1647,f2431])).
% 29.22/4.18 fof(f18570,plain,(
% 29.22/4.18 sQ34_spl|sQ115_spl|~sQ50_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18561,f1647,f7502,f2431])).
% 29.22/4.18 fof(f18572,plain,(
% 29.22/4.18 vd518=vmul(vd517,vd518)|vmul(vd517,vd518)=vplus(vd518,sK3_skl(vmul(vd517,vd518),vd518))|sQ127_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f8300,f1859])).
% 29.22/4.18 fof(f18573,plain,(
% 29.22/4.18 vmul(vd517,vd518)=vplus(vd518,sK1_skl(vmul(vd517,vd518),vd518))|vmul(vd517,vd518)=vd518|sQ127_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f8300,f1813])).
% 29.22/4.18 fof(f18574,plain,(
% 29.22/4.18 vd518=vmul(vd517,vd518)|less(vd518,vmul(vd517,vd518))|sQ127_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f8300,f1541])).
% 29.22/4.18 fof(f18583,definition,(
% 29.22/4.18 sQ177_spl <=> (vmul(vd517,vd518)=vplus(vd518,sK3_skl(vmul(vd517,vd518),vd518)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f18586,plain,(
% 29.22/4.18 sQ126_spl|sQ177_spl|sQ127_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18572,f8295,f18583,f8298])).
% 29.22/4.18 fof(f18587,definition,(
% 29.22/4.18 sQ178_spl <=> (vmul(vd517,vd518)=vplus(vd518,sK1_skl(vmul(vd517,vd518),vd518)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f18590,plain,(
% 29.22/4.18 sQ178_spl|sQ126_spl|sQ127_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18573,f18587,f8295,f8298])).
% 29.22/4.18 fof(f18591,definition,(
% 29.22/4.18 sQ179_spl <=> (less(vd518,vmul(vd517,vd518)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f18594,plain,(
% 29.22/4.18 sQ126_spl|sQ179_spl|sQ127_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18574,f8295,f18591,f8298])).
% 29.22/4.18 fof(f18684,plain,(
% 29.22/4.18 v1=vd520|vd520=vplus(v1,sK3_skl(vd520,v1))|sQ71_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f3636,f1859])).
% 29.22/4.18 fof(f18693,definition,(
% 29.22/4.18 sQ180_spl <=> (vd520=vplus(v1,sK3_skl(vd520,v1)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f18696,plain,(
% 29.22/4.18 sQ70_spl|sQ180_spl|sQ71_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18684,f3631,f18693,f3634])).
% 29.22/4.18 fof(f18703,plain,(
% 29.22/4.18 vd520=vd519|vd519=vplus(vd520,sK3_skl(vd519,vd520))|~sQ3_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f7538,f1859])).
% 29.22/4.18 fof(f18712,plain,(
% 29.22/4.18 sQ14_spl|sQ100_spl|~sQ3_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f18703,f1206,f5905,f208])).
% 29.22/4.18 fof(f19196,plain,(
% 29.22/4.18 vd520=vsucc(vd519)|vsucc(vd519)=vplus(vd520,sK3_skl(vsucc(vd519),vd520))|~sQ17_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f8769,f1859])).
% 29.22/4.18 fof(f19197,plain,(
% 29.22/4.18 vsucc(vd519)=vplus(vd520,sK1_skl(vsucc(vd519),vd520))|vsucc(vd519)=vd520|~sQ17_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f8769,f1813])).
% 29.22/4.18 fof(f19205,definition,(
% 29.22/4.18 sQ181_spl <=> (vsucc(vd519)=vplus(vd520,sK3_skl(vsucc(vd519),vd520)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f19208,plain,(
% 29.22/4.18 sQ12_spl|sQ181_spl|~sQ17_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f19196,f1199,f19205,f1517])).
% 29.22/4.18 fof(f19209,definition,(
% 29.22/4.18 sQ182_spl <=> (vsucc(vd519)=vplus(vd520,sK1_skl(vsucc(vd519),vd520)))),
% 29.22/4.18 introduced(definition,[new_symbols(definition,[sQ182_spl])],[split_symbol_definition])).
% 29.22/4.18 fof(f19212,plain,(
% 29.22/4.18 sQ182_spl|sQ12_spl|~sQ17_spl),
% 29.22/4.18 inference(split_clause,[status(thm)],[f19197,f19209,f1199,f1517])).
% 29.22/4.18 fof(f19221,plain,(
% 29.22/4.18 greater(vmul(vd517,vd519),vmul(vd518,vd520))|~sQ3_spl|~sQ2_spl),
% 29.22/4.18 inference(resolution,[status(thm)],[f352,f205])).
% 29.22/4.18 fof(f19254,plain,(
% 29.22/4.18 $false|~sQ3_spl|~sQ2_spl),
% 29.22/4.18 inference(forward_subsumption_resolution,[status(thm)],[f19221,f61])).
% 29.22/4.18 fof(f19255,plain,(
% 29.22/4.18 ~sQ3_spl|~sQ2_spl),
% 29.22/4.18 inference(contradiction_clause,[status(thm)],[f19254])).
% 29.22/4.18 fof(f19273,plain,(
% 29.22/4.18 $false|~sQ3_spl|~sQ16_spl),
% 29.22/4.18 inference(forward_subsumption_resolution,[status(thm)],[f2618,f1802])).
% 29.22/4.18 fof(f19274,plain,(
% 29.22/4.18 ~sQ3_spl|~sQ16_spl),
% 29.22/4.18 inference(contradiction_clause,[status(thm)],[f19273])).
% 29.22/4.18 fof(f19275,plain,(
% 29.22/4.18 $false),
% 29.22/4.18 inference(sat_refutation,[status(thm)],[f203,f207,f211,f215,f350,f507,f1216,f1266,f1526,f1560,f1574,f1629,f1643,f1650,f1748,f1753,f1763,f1785,f1792,f1957,f2613,f3443,f3613,f3626,f3637,f4005,f4186,f4389,f4551,f4615,f4912,f4939,f4968,f5130,f5148,f5267,f5593,f5600,f5607,f5616,f5630,f5638,f5640,f5642,f5644,f5853,f5904,f5908,f6101,f6449,f6662,f6827,f7197,f7337,f7459,f7464,f7480,f7493,f7497,f7501,f7505,f7510,f7520,f7522,f8135,f8195,f8259,f8278,f8301,f8306,f8653,f8655,f8720,f9111,f9113,f9776,f9781,f9887,f9985,f10010,f10604,f10723,f11133,f11134,f11729,f11733,f11749,f11757,f12049,f12377,f13412,f13416,f14528,f14566,f14657,f14662,f15105,f15107,f15110,f15130,f15132,f15134,f15135,f15137,f15139,f15141,f15142,f15144,f15147,f15504,f15510,f15511,f15536,f15663,f15667,f16727,f16731,f16751,f16874,f16878,f16897,f16987,f16995,f16996,f17279,f17283,f17718,f17776,f17953,f17954,f18222,f18226,f18298,f18568,f18569,f18570,f18586,f18590,f18594,f18696,f18712,f19208,f19212,f19255,f19274])).
% 29.22/4.19 % SZS output end CNFRefutation for theBenchmark.p
% 1.00/4.20 % Elapsed time: 3.821038 seconds
% 1.00/4.20 % CPU time: 29.912310 seconds
% 1.00/4.20 % Total memory used: 323.481 MB
% 1.00/4.20 % Net memory used: 290.355 MB
%------------------------------------------------------------------------------