%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV486+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:51:00 PM UTC 2026
% Result : Theorem 17.76s 2.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV486+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n020.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 21 08:54:47 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.44 % Drodi V4.1.1
% 17.76/2.82 % Refutation found
% 17.76/2.82 % SZS status Theorem for theBenchmark: Theorem is valid
% 17.76/2.82 % SZS output start CNFRefutation for theBenchmark
% 17.76/2.82 fof(f1,axiom,(
% 17.76/2.82 (! [I,J] :( int_leq(I,J)<=> ( int_less(I,J)| I = J ) ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f2,axiom,(
% 17.76/2.82 (! [I,J,K] :( ( int_less(I,J)& int_less(J,K) )=> int_less(I,K) ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f3,axiom,(
% 17.76/2.82 (! [I,J] :( int_less(I,J)=> I != J ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f4,axiom,(
% 17.76/2.82 (! [I,J] :( int_less(I,J)| int_leq(J,I) ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f5,axiom,(
% 17.76/2.82 int_less(int_zero,int_one) ),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f6,axiom,(
% 17.76/2.82 (! [I,J] : plus(I,J) = plus(J,I) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f7,axiom,(
% 17.76/2.82 (! [I] : plus(I,int_zero) = I )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f8,axiom,(
% 17.76/2.82 (! [I1,J1,I2,J2] :( ( int_less(I1,J1)& int_leq(I2,J2) )=> int_leq(plus(I1,I2),plus(J1,J2)) ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f9,axiom,(
% 17.76/2.82 (! [I,J] :( int_less(I,J)<=> (? [K] :( plus(I,K) = J& int_less(int_zero,K) ) )) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f10,axiom,(
% 17.76/2.82 (! [I] :( int_less(int_zero,I)<=> int_leq(int_one,I) ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f11,axiom,(
% 17.76/2.82 real_zero != real_one ),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f12,hypothesis,(
% 17.76/2.82 (! [I,J] :( ( int_leq(int_one,I)& int_leq(I,n)& int_leq(int_one,J)& int_leq(J,n) )=> ( (! [C] :( ( int_less(int_zero,C)& I = plus(J,C) )=> (! [K] :( ( int_leq(int_one,K)& int_leq(K,J) )=> a(plus(K,C),K) = lu(plus(K,C),K) ) )))& (! [K] :( ( int_leq(int_one,K)& int_leq(K,J) )=> a(K,K) = real_one ))& (! [C] :( ( int_less(int_zero,C)& J = plus(I,C) )=> (! [K] :( ( int_leq(int_one,K)& int_leq(K,I) )=> a(K,plus(K,C)) = real_zero ) )) )) ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f13,conjecture,(
% 17.76/2.82 (! [I,J] :( ( int_leq(int_one,I)& int_less(I,J)& int_leq(J,n) )=> a(I,J) = real_zero ) )),
% 17.76/2.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.76/2.82 fof(f14,negated_conjecture,(
% 17.76/2.82 ~((! [I,J] :( ( int_leq(int_one,I)& int_less(I,J)& int_leq(J,n) )=> a(I,J) = real_zero ) ))),
% 17.76/2.82 inference(negated_conjecture,[status(cth)],[f13])).
% 17.76/2.82 fof(f15,plain,(
% 17.76/2.82 ![I,J]: ((~int_leq(I,J)|(int_less(I,J)|I=J))&(int_leq(I,J)|(~int_less(I,J)&~I=J)))),
% 17.76/2.82 inference(NNF_transformation,[status(thm)],[f1])).
% 17.76/2.82 fof(f16,plain,(
% 17.76/2.82 (![I,J]: (~int_leq(I,J)|(int_less(I,J)|I=J)))&(![I,J]: (int_leq(I,J)|(~int_less(I,J)&~I=J)))),
% 17.76/2.82 inference(miniscoping,[status(thm)],[f15])).
% 17.76/2.82 fof(f17,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(X0,X1)|int_less(X0,X1)|X0=X1)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f16])).
% 17.76/2.82 fof(f18,plain,(
% 17.76/2.82 ![X0,X1]: (int_leq(X0,X1)|~int_less(X0,X1))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f16])).
% 17.76/2.82 fof(f19,plain,(
% 17.76/2.82 ![X0,X1]: (int_leq(X0,X1)|~X0=X1)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f16])).
% 17.76/2.82 fof(f20,plain,(
% 17.76/2.82 ![I,J,K]: ((~int_less(I,J)|~int_less(J,K))|int_less(I,K))),
% 17.76/2.82 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 17.76/2.82 fof(f21,plain,(
% 17.76/2.82 ![I,K]: ((![J]: (~int_less(I,J)|~int_less(J,K)))|int_less(I,K))),
% 17.76/2.82 inference(miniscoping,[status(thm)],[f20])).
% 17.76/2.82 fof(f22,plain,(
% 17.76/2.82 ![X0,X1,X2]: (~int_less(X0,X1)|~int_less(X1,X2)|int_less(X0,X2))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f21])).
% 17.76/2.82 fof(f23,plain,(
% 17.76/2.82 ![I,J]: (~int_less(I,J)|~I=J)),
% 17.76/2.82 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 17.76/2.82 fof(f24,plain,(
% 17.76/2.82 ![X0,X1]: (~int_less(X0,X1)|~X0=X1)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f23])).
% 17.76/2.82 fof(f25,plain,(
% 17.76/2.82 ![X0,X1]: (int_less(X0,X1)|int_leq(X1,X0))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f4])).
% 17.76/2.82 fof(f26,plain,(
% 17.76/2.82 int_less(int_zero,int_one)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f5])).
% 17.76/2.82 fof(f27,plain,(
% 17.76/2.82 ![X0,X1]: (plus(X0,X1)=plus(X1,X0))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f6])).
% 17.76/2.82 fof(f28,plain,(
% 17.76/2.82 ![X0]: (plus(X0,int_zero)=X0)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f7])).
% 17.76/2.82 fof(f29,plain,(
% 17.76/2.82 ![I1,J1,I2,J2]: ((~int_less(I1,J1)|~int_leq(I2,J2))|int_leq(plus(I1,I2),plus(J1,J2)))),
% 17.76/2.82 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 17.76/2.82 fof(f30,plain,(
% 17.76/2.82 ![X0,X1,X2,X3]: (~int_less(X0,X1)|~int_leq(X2,X3)|int_leq(plus(X0,X2),plus(X1,X3)))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f29])).
% 17.76/2.82 fof(f31,plain,(
% 17.76/2.82 ![I,J]: ((~int_less(I,J)|(?[K]: (plus(I,K)=J&int_less(int_zero,K))))&(int_less(I,J)|(![K]: (~plus(I,K)=J|~int_less(int_zero,K)))))),
% 17.76/2.82 inference(NNF_transformation,[status(thm)],[f9])).
% 17.76/2.82 fof(f32,plain,(
% 17.76/2.82 (![I,J]: (~int_less(I,J)|(?[K]: (plus(I,K)=J&int_less(int_zero,K)))))&(![I,J]: (int_less(I,J)|(![K]: (~plus(I,K)=J|~int_less(int_zero,K)))))),
% 17.76/2.82 inference(miniscoping,[status(thm)],[f31])).
% 17.76/2.82 fof(f33,plain,(
% 17.76/2.82 (![I,J]: (~int_less(I,J)|(plus(I,sK0_skl(J,I))=J&int_less(int_zero,sK0_skl(J,I)))))&(![I,J]: (int_less(I,J)|(![K]: (~plus(I,K)=J|~int_less(int_zero,K)))))),
% 17.76/2.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(K,sK0_skl(J,I))],[f32])).
% 17.76/2.82 fof(f34,plain,(
% 17.76/2.82 ![X0,X1]: (~int_less(X0,X1)|plus(X0,sK0_skl(X1,X0))=X1)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f33])).
% 17.76/2.82 fof(f35,plain,(
% 17.76/2.82 ![X0,X1]: (~int_less(X0,X1)|int_less(int_zero,sK0_skl(X1,X0)))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f33])).
% 17.76/2.82 fof(f36,plain,(
% 17.76/2.82 ![X0,X1,X2]: (int_less(X0,X1)|~plus(X0,X2)=X1|~int_less(int_zero,X2))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f33])).
% 17.76/2.82 fof(f37,plain,(
% 17.76/2.82 ![I]: ((~int_less(int_zero,I)|int_leq(int_one,I))&(int_less(int_zero,I)|~int_leq(int_one,I)))),
% 17.76/2.82 inference(NNF_transformation,[status(thm)],[f10])).
% 17.76/2.82 fof(f38,plain,(
% 17.76/2.82 (![I]: (~int_less(int_zero,I)|int_leq(int_one,I)))&(![I]: (int_less(int_zero,I)|~int_leq(int_one,I)))),
% 17.76/2.82 inference(miniscoping,[status(thm)],[f37])).
% 17.76/2.82 fof(f39,plain,(
% 17.76/2.82 ![X0]: (~int_less(int_zero,X0)|int_leq(int_one,X0))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f38])).
% 17.76/2.82 fof(f40,plain,(
% 17.76/2.82 ![X0]: (int_less(int_zero,X0)|~int_leq(int_one,X0))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f38])).
% 17.76/2.82 fof(f41,plain,(
% 17.76/2.82 ~real_zero=real_one),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f11])).
% 17.76/2.82 fof(f42,plain,(
% 17.76/2.82 ![I,J]: ((((~int_leq(int_one,I)|~int_leq(I,n))|~int_leq(int_one,J))|~int_leq(J,n))|(((![C]: ((~int_less(int_zero,C)|~I=plus(J,C))|(![K]: ((~int_leq(int_one,K)|~int_leq(K,J))|a(plus(K,C),K)=lu(plus(K,C),K)))))&(![K]: ((~int_leq(int_one,K)|~int_leq(K,J))|a(K,K)=real_one)))&(![C]: ((~int_less(int_zero,C)|~J=plus(I,C))|(![K]: ((~int_leq(int_one,K)|~int_leq(K,I))|a(K,plus(K,C))=real_zero))))))),
% 17.76/2.82 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 17.76/2.82 fof(f43,plain,(
% 17.76/2.82 ![X0,X1,X2,X3]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,X1)|~int_leq(X1,n)|~int_less(int_zero,X2)|~X0=plus(X1,X2)|~int_leq(int_one,X3)|~int_leq(X3,X1)|a(plus(X3,X2),X3)=lu(plus(X3,X2),X3))),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f42])).
% 17.76/2.82 fof(f44,plain,(
% 17.76/2.82 ![X0,X1,X2]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,X1)|~int_leq(X1,n)|~int_leq(int_one,X2)|~int_leq(X2,X1)|a(X2,X2)=real_one)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f42])).
% 17.76/2.82 fof(f45,plain,(
% 17.76/2.82 ![X0,X1,X2,X3]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,X1)|~int_leq(X1,n)|~int_less(int_zero,X2)|~X1=plus(X0,X2)|~int_leq(int_one,X3)|~int_leq(X3,X0)|a(X3,plus(X3,X2))=real_zero)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f42])).
% 17.76/2.82 fof(f46,plain,(
% 17.76/2.82 (?[I,J]: (((int_leq(int_one,I)&int_less(I,J))&int_leq(J,n))&~a(I,J)=real_zero))),
% 17.76/2.82 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 17.76/2.82 fof(f47,plain,(
% 17.76/2.82 (((int_leq(int_one,sK1_skl)&int_less(sK1_skl,sK2_skl))&int_leq(sK2_skl,n))&~a(sK1_skl,sK2_skl)=real_zero)),
% 17.76/2.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(I,sK1_skl),skolemize(J,sK2_skl)],[f46])).
% 17.76/2.82 fof(f48,plain,(
% 17.76/2.82 int_leq(int_one,sK1_skl)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f47])).
% 17.76/2.82 fof(f49,plain,(
% 17.76/2.82 int_less(sK1_skl,sK2_skl)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f47])).
% 17.76/2.82 fof(f50,plain,(
% 17.76/2.82 int_leq(sK2_skl,n)),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f47])).
% 17.76/2.82 fof(f51,plain,(
% 17.76/2.82 ~a(sK1_skl,sK2_skl)=real_zero),
% 17.76/2.82 inference(cnf_transformation,[status(thm)],[f47])).
% 17.76/2.82 fof(f52,definition,(
% 17.76/2.82 ![X0]: (sQ0_spl <=> (~int_leq(int_one,X0)|~int_leq(X0,n)))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f53,plain,(
% 17.76/2.82 ![X0]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~sQ0_spl)),
% 17.76/2.82 inference(component_clause,[status(thm)],[f52])).
% 17.76/2.82 fof(f55,definition,(
% 17.76/2.82 ![X1,X2]: (sQ1_spl <=> (~int_leq(int_one,X1)|~int_leq(X1,n)|~int_leq(int_one,X2)|~int_leq(X2,X1)|a(X2,X2)=real_one))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f56,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,X1)|~int_leq(X1,X0)|a(X1,X1)=real_one|~sQ1_spl)),
% 17.76/2.82 inference(component_clause,[status(thm)],[f55])).
% 17.76/2.82 fof(f58,plain,(
% 17.76/2.82 sQ0_spl|sQ1_spl),
% 17.76/2.82 inference(split_clause,[status(thm)],[f44,f52,f55])).
% 17.76/2.82 fof(f59,plain,(
% 17.76/2.82 ![X0]: (int_leq(X0,X0))),
% 17.76/2.82 inference(destructive_equality_resolution,[status(thm)],[f19])).
% 17.76/2.82 fof(f60,plain,(
% 17.76/2.82 ![X0]: (~int_less(X0,X0))),
% 17.76/2.82 inference(destructive_equality_resolution,[status(thm)],[f24])).
% 17.76/2.82 fof(f61,plain,(
% 17.76/2.82 ![X0,X1]: (int_less(X0,plus(X0,X1))|~int_less(int_zero,X1))),
% 17.76/2.82 inference(destructive_equality_resolution,[status(thm)],[f36])).
% 17.76/2.82 fof(f62,plain,(
% 17.76/2.82 ![X0,X1,X2]: (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|~int_leq(int_one,X2)|~int_leq(X2,X0)|a(plus(X2,X1),X2)=lu(plus(X2,X1),X2))),
% 17.76/2.82 inference(destructive_equality_resolution,[status(thm)],[f43])).
% 17.76/2.82 fof(f63,plain,(
% 17.76/2.82 ![X0,X1,X2]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_less(int_zero,X1)|~int_leq(int_one,X2)|~int_leq(X2,X0)|a(X2,plus(X2,X1))=real_zero)),
% 17.76/2.82 inference(destructive_equality_resolution,[status(thm)],[f45])).
% 17.76/2.82 fof(f64,plain,(
% 17.76/2.82 int_less(int_one,sK1_skl)|int_one=sK1_skl),
% 17.76/2.82 inference(resolution,[status(thm)],[f17,f48])).
% 17.76/2.82 fof(f66,definition,(
% 17.76/2.82 sQ2_spl <=> (int_less(int_one,sK1_skl))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f67,plain,(
% 17.76/2.82 int_less(int_one,sK1_skl)|~sQ2_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f66])).
% 17.76/2.82 fof(f69,definition,(
% 17.76/2.82 sQ3_spl <=> (int_one=sK1_skl)),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f70,plain,(
% 17.76/2.82 int_one=sK1_skl|~sQ3_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f69])).
% 17.76/2.82 fof(f72,plain,(
% 17.76/2.82 sQ2_spl|sQ3_spl),
% 17.76/2.82 inference(split_clause,[status(thm)],[f64,f66,f69])).
% 17.76/2.82 fof(f73,plain,(
% 17.76/2.82 int_leq(sK1_skl,sK2_skl)),
% 17.76/2.82 inference(resolution,[status(thm)],[f18,f49])).
% 17.76/2.82 fof(f74,plain,(
% 17.76/2.82 int_leq(int_zero,int_one)),
% 17.76/2.82 inference(resolution,[status(thm)],[f26,f18])).
% 17.76/2.82 fof(f76,plain,(
% 17.76/2.82 ![X0]: (~int_less(sK2_skl,X0)|int_less(sK1_skl,X0))),
% 17.76/2.82 inference(resolution,[status(thm)],[f22,f49])).
% 17.76/2.82 fof(f78,plain,(
% 17.76/2.82 ![X0]: (~int_less(X0,sK1_skl)|int_less(X0,sK2_skl))),
% 17.76/2.82 inference(resolution,[status(thm)],[f22,f49])).
% 17.76/2.82 fof(f83,plain,(
% 17.76/2.82 ![X0,X1]: (int_leq(X0,X1)|int_leq(X1,X0))),
% 17.76/2.82 inference(resolution,[status(thm)],[f25,f18])).
% 17.76/2.82 fof(f85,plain,(
% 17.76/2.82 ![X0]: (X0=plus(int_zero,X0))),
% 17.76/2.82 inference(paramodulation,[status(thm)],[f28,f27])).
% 17.76/2.82 fof(f93,plain,(
% 17.76/2.82 int_less(sK2_skl,n)|sK2_skl=n),
% 17.76/2.82 inference(resolution,[status(thm)],[f50,f17])).
% 17.76/2.82 fof(f94,definition,(
% 17.76/2.82 sQ4_spl <=> (int_less(sK2_skl,n))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f95,plain,(
% 17.76/2.82 int_less(sK2_skl,n)|~sQ4_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f94])).
% 17.76/2.82 fof(f97,definition,(
% 17.76/2.82 sQ5_spl <=> (sK2_skl=n)),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f98,plain,(
% 17.76/2.82 sK2_skl=n|~sQ5_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f97])).
% 17.76/2.82 fof(f100,plain,(
% 17.76/2.82 sQ4_spl|sQ5_spl),
% 17.76/2.82 inference(split_clause,[status(thm)],[f93,f94,f97])).
% 17.76/2.82 fof(f113,definition,(
% 17.76/2.82 sQ8_spl <=> (int_less(int_zero,int_one))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f137,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(X0,X1)|int_leq(plus(int_zero,X0),plus(int_one,X1)))),
% 17.76/2.82 inference(resolution,[status(thm)],[f30,f26])).
% 17.76/2.82 fof(f146,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(X0,X1)|int_leq(X0,plus(int_one,X1)))),
% 17.76/2.82 inference(forward_demodulation,[status(thm)],[f85,f137])).
% 17.76/2.82 fof(f151,plain,(
% 17.76/2.82 plus(int_zero,sK0_skl(int_one,int_zero))=int_one),
% 17.76/2.82 inference(resolution,[status(thm)],[f34,f26])).
% 17.76/2.82 fof(f152,plain,(
% 17.76/2.82 plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))=sK2_skl),
% 17.76/2.82 inference(resolution,[status(thm)],[f34,f49])).
% 17.76/2.82 fof(f153,plain,(
% 17.76/2.82 ![X0,X1]: (plus(X0,sK0_skl(X1,X0))=X1|int_leq(X1,X0))),
% 17.76/2.82 inference(resolution,[status(thm)],[f34,f25])).
% 17.76/2.82 fof(f155,plain,(
% 17.76/2.82 sK0_skl(int_one,int_zero)=int_one),
% 17.76/2.82 inference(forward_demodulation,[status(thm)],[f85,f151])).
% 17.76/2.82 fof(f160,plain,(
% 17.76/2.82 int_less(int_zero,sK0_skl(sK2_skl,sK1_skl))),
% 17.76/2.82 inference(resolution,[status(thm)],[f35,f49])).
% 17.76/2.82 fof(f161,plain,(
% 17.76/2.82 ![X0,X1]: (int_less(int_zero,sK0_skl(X0,X1))|int_leq(X0,X1))),
% 17.76/2.82 inference(resolution,[status(thm)],[f35,f25])).
% 17.76/2.82 fof(f167,definition,(
% 17.76/2.82 sQ10_spl <=> (int_less(int_zero,sK1_skl))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f168,plain,(
% 17.76/2.82 int_less(int_zero,sK1_skl)|~sQ10_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f167])).
% 17.76/2.82 fof(f169,plain,(
% 17.76/2.82 ~int_less(int_zero,sK1_skl)|sQ10_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f167])).
% 17.76/2.82 fof(f170,definition,(
% 17.76/2.82 sQ11_spl <=> (int_zero=sK1_skl)),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f171,plain,(
% 17.76/2.82 int_zero=sK1_skl|~sQ11_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f170])).
% 17.76/2.82 fof(f189,plain,(
% 17.76/2.82 ![X0]: (plus(X0,sK1_skl)=X0|~sQ11_spl)),
% 17.76/2.82 inference(backward_demodulation,[status(thm)],[f171,f28])).
% 17.76/2.82 fof(f208,plain,(
% 17.76/2.82 int_less(sK1_skl,n)|~sQ4_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f76,f95])).
% 17.76/2.82 fof(f210,plain,(
% 17.76/2.82 int_less(int_zero,sK2_skl)|~sQ10_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f78,f168])).
% 17.76/2.82 fof(f211,plain,(
% 17.76/2.82 ![X0]: (int_less(X0,sK2_skl)|int_leq(sK1_skl,X0))),
% 17.76/2.82 inference(resolution,[status(thm)],[f78,f25])).
% 17.76/2.82 fof(f222,plain,(
% 17.76/2.82 int_less(int_one,sK2_skl)|~sQ2_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f67,f78])).
% 17.76/2.82 fof(f235,plain,(
% 17.76/2.82 ![X0,X1]: (int_less(X0,plus(X0,X1))|int_leq(X1,int_zero))),
% 17.76/2.82 inference(resolution,[status(thm)],[f61,f25])).
% 17.76/2.82 fof(f236,plain,(
% 17.76/2.82 ![X0]: (int_less(X0,plus(X0,int_one)))),
% 17.76/2.82 inference(resolution,[status(thm)],[f26,f61])).
% 17.76/2.82 fof(f267,plain,(
% 17.76/2.82 int_leq(sK1_skl,n)|~sQ4_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f208,f18])).
% 17.76/2.82 fof(f290,plain,(
% 17.76/2.82 int_leq(int_zero,sK2_skl)|~sQ10_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f210,f18])).
% 17.76/2.82 fof(f301,plain,(
% 17.76/2.82 int_leq(int_one,sK2_skl)|~sQ2_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f222,f18])).
% 17.76/2.82 fof(f354,plain,(
% 17.76/2.82 int_less(int_zero,sK1_skl)),
% 17.76/2.82 inference(resolution,[status(thm)],[f40,f48])).
% 17.76/2.82 fof(f358,plain,(
% 17.76/2.82 ![X0]: (int_leq(int_one,X0)|int_leq(X0,int_zero))),
% 17.76/2.82 inference(resolution,[status(thm)],[f39,f25])).
% 17.76/2.82 fof(f395,plain,(
% 17.76/2.82 int_leq(int_one,sK2_skl)|~sQ10_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f210,f39])).
% 17.76/2.82 fof(f411,plain,(
% 17.76/2.82 int_less(int_zero,sK2_skl)|~sQ2_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f301,f40])).
% 17.76/2.82 fof(f417,definition,(
% 17.76/2.82 sQ15_spl <=> (int_one=sK2_skl)),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f418,plain,(
% 17.76/2.82 int_one=sK2_skl|~sQ15_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f417])).
% 17.76/2.82 fof(f423,plain,(
% 17.76/2.82 ~int_leq(int_one,n)|~sQ0_spl),
% 17.76/2.82 inference(resolution,[status(thm)],[f53,f83])).
% 17.76/2.82 fof(f492,definition,(
% 17.76/2.82 sQ16_spl <=> (int_leq(sK1_skl,n))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f494,plain,(
% 17.76/2.82 ~int_leq(sK1_skl,n)|sQ16_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f492])).
% 17.76/2.82 fof(f495,definition,(
% 17.76/2.82 sQ17_spl <=> (int_leq(n,n))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f497,plain,(
% 17.76/2.82 ~int_leq(n,n)|sQ17_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f495])).
% 17.76/2.82 fof(f503,definition,(
% 17.76/2.82 sQ19_spl <=> (int_leq(sK1_skl,sK1_skl))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f505,plain,(
% 17.76/2.82 ~int_leq(sK1_skl,sK1_skl)|sQ19_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f503])).
% 17.76/2.82 fof(f513,definition,(
% 17.76/2.82 sQ21_spl <=> (int_leq(sK1_skl,sK2_skl))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f515,plain,(
% 17.76/2.82 ~int_leq(sK1_skl,sK2_skl)|sQ21_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f513])).
% 17.76/2.82 fof(f516,definition,(
% 17.76/2.82 sQ22_spl <=> (int_leq(sK2_skl,n))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f518,plain,(
% 17.76/2.82 ~int_leq(sK2_skl,n)|sQ22_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f516])).
% 17.76/2.82 fof(f530,definition,(
% 17.76/2.82 sQ25_spl <=> (int_leq(sK1_skl,int_zero))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f531,plain,(
% 17.76/2.82 int_leq(sK1_skl,int_zero)|~sQ25_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f530])).
% 17.76/2.82 fof(f533,definition,(
% 17.76/2.82 sQ26_spl <=> (int_leq(int_zero,n))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f535,plain,(
% 17.76/2.82 ~int_leq(int_zero,n)|sQ26_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f533])).
% 17.76/2.82 fof(f543,definition,(
% 17.76/2.82 sQ29_spl <=> (int_less(int_zero,int_zero))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f547,plain,(
% 17.76/2.82 $false|~sQ4_spl|sQ16_spl),
% 17.76/2.82 inference(forward_subsumption_resolution,[status(thm)],[f494,f267])).
% 17.76/2.82 fof(f548,plain,(
% 17.76/2.82 ~sQ4_spl|sQ16_spl),
% 17.76/2.82 inference(contradiction_clause,[status(thm)],[f547])).
% 17.76/2.82 fof(f549,plain,(
% 17.76/2.82 $false|sQ21_spl),
% 17.76/2.82 inference(forward_subsumption_resolution,[status(thm)],[f515,f73])).
% 17.76/2.82 fof(f550,plain,(
% 17.76/2.82 sQ21_spl),
% 17.76/2.82 inference(contradiction_clause,[status(thm)],[f549])).
% 17.76/2.82 fof(f551,plain,(
% 17.76/2.82 $false|sQ17_spl),
% 17.76/2.82 inference(forward_subsumption_resolution,[status(thm)],[f497,f59])).
% 17.76/2.82 fof(f552,plain,(
% 17.76/2.82 sQ17_spl),
% 17.76/2.82 inference(contradiction_clause,[status(thm)],[f551])).
% 17.76/2.82 fof(f565,plain,(
% 17.76/2.82 ![X0]: (~int_leq(int_one,n)|~int_leq(n,n)|~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(n,X0),plus(plus(n,X0),X0))=real_zero|int_leq(n,plus(n,X0)))),
% 17.76/2.82 inference(resolution,[status(thm)],[f63,f83])).
% 17.76/2.82 fof(f569,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_less(int_zero,X1)|~int_leq(sK1_skl,X0)|a(sK1_skl,plus(sK1_skl,X1))=real_zero)),
% 17.76/2.82 inference(resolution,[status(thm)],[f63,f48])).
% 17.76/2.82 fof(f570,plain,(
% 17.76/2.82 ![X0]: (~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|a(int_one,plus(int_one,X0))=real_zero)),
% 17.76/2.82 inference(resolution,[status(thm)],[f63,f83])).
% 17.76/2.82 fof(f575,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_less(int_zero,X1)|~int_leq(int_one,X0)|a(int_one,plus(int_one,X1))=real_zero)),
% 17.76/2.82 inference(resolution,[status(thm)],[f63,f59])).
% 17.76/2.82 fof(f577,plain,(
% 17.76/2.82 ![X0]: (~int_leq(int_one,sK2_skl)|~int_leq(sK2_skl,n)|~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,sK1_skl)|a(sK1_skl,plus(sK1_skl,X0))=real_zero)),
% 17.76/2.82 inference(resolution,[status(thm)],[f63,f73])).
% 17.76/2.82 fof(f578,plain,(
% 17.76/2.82 ![X0]: (~int_leq(int_one,n)|~int_leq(n,n)|~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(sK2_skl,plus(sK2_skl,X0))=real_zero)),
% 17.76/2.82 inference(resolution,[status(thm)],[f63,f50])).
% 17.76/2.82 fof(f584,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|~int_leq(X1,int_zero)|a(X1,plus(X1,X0))=real_zero)),
% 17.76/2.82 inference(paramodulation,[status(thm)],[f85,f63])).
% 17.76/2.82 fof(f588,definition,(
% 17.76/2.82 sQ30_spl <=> (int_leq(int_one,n))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f589,plain,(
% 17.76/2.82 int_leq(int_one,n)|~sQ30_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f588])).
% 17.76/2.82 fof(f590,plain,(
% 17.76/2.82 ~int_leq(int_one,n)|sQ30_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f588])).
% 17.76/2.82 fof(f591,definition,(
% 17.76/2.82 ![X0]: (sQ31_spl <=> (~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(n,X0),plus(plus(n,X0),X0))=real_zero|int_leq(n,plus(n,X0))))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f594,plain,(
% 17.76/2.82 ~sQ30_spl|~sQ17_spl|sQ31_spl),
% 17.76/2.82 inference(split_clause,[status(thm)],[f565,f588,f495,f591])).
% 17.76/2.82 fof(f596,definition,(
% 17.76/2.82 sQ32_spl <=> (int_leq(int_one,int_one))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f598,plain,(
% 17.76/2.82 ~int_leq(int_one,int_one)|sQ32_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f596])).
% 17.76/2.82 fof(f599,definition,(
% 17.76/2.82 ![X0]: (sQ33_spl <=> (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|a(int_one,plus(int_one,X0))=real_zero))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f602,plain,(
% 17.76/2.82 ~sQ32_spl|~sQ30_spl|sQ33_spl),
% 17.76/2.82 inference(split_clause,[status(thm)],[f570,f596,f588,f599])).
% 17.76/2.82 fof(f605,plain,(
% 17.76/2.82 ![X0,X1]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_less(int_zero,X1)|a(int_one,plus(int_one,X1))=real_zero)),
% 17.76/2.82 inference(duplicate_literals_removal,[status(thm)],[f575])).
% 17.76/2.82 fof(f606,definition,(
% 17.76/2.82 sQ34_spl <=> (int_leq(int_one,sK1_skl))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f608,plain,(
% 17.76/2.82 ~int_leq(int_one,sK1_skl)|sQ34_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f606])).
% 17.76/2.82 fof(f613,definition,(
% 17.76/2.82 sQ36_spl <=> (int_leq(int_one,sK2_skl))),
% 17.76/2.82 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 17.76/2.82 fof(f615,plain,(
% 17.76/2.82 ~int_leq(int_one,sK2_skl)|sQ36_spl),
% 17.76/2.82 inference(component_clause,[status(thm)],[f613])).
% 17.76/2.82 fof(f616,definition,(
% 17.76/2.82 ![X0]: (sQ37_spl <=> (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_less(int_zero,X0)|a(sK1_skl,plus(sK1_skl,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f619,plain,(
% 17.76/2.83 ~sQ36_spl|~sQ22_spl|sQ37_spl|~sQ34_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f577,f613,f516,f616,f606])).
% 17.76/2.83 fof(f620,definition,(
% 17.76/2.83 ![X0]: (sQ38_spl <=> (~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_less(int_zero,X0)|a(sK2_skl,plus(sK2_skl,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f623,plain,(
% 17.76/2.83 ~sQ30_spl|~sQ17_spl|sQ38_spl|~sQ36_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f578,f588,f495,f620,f613])).
% 17.76/2.83 fof(f627,definition,(
% 17.76/2.83 sQ39_spl <=> (int_leq(int_one,int_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f629,plain,(
% 17.76/2.83 ~int_leq(int_one,int_zero)|sQ39_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f627])).
% 17.76/2.83 fof(f630,definition,(
% 17.76/2.83 ![X0,X1]: (sQ40_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|~int_leq(X1,int_zero)|a(X1,plus(X1,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f633,plain,(
% 17.76/2.83 ~sQ39_spl|~sQ26_spl|sQ40_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f584,f627,f533,f630])).
% 17.76/2.83 fof(f638,plain,(
% 17.76/2.83 $false|~sQ10_spl|sQ36_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f615,f395])).
% 17.76/2.83 fof(f639,plain,(
% 17.76/2.83 ~sQ10_spl|sQ36_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f638])).
% 17.76/2.83 fof(f640,plain,(
% 17.76/2.83 $false|sQ34_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f608,f48])).
% 17.76/2.83 fof(f641,plain,(
% 17.76/2.83 sQ34_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f640])).
% 17.76/2.83 fof(f642,plain,(
% 17.76/2.83 $false|sQ22_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f518,f50])).
% 17.76/2.83 fof(f643,plain,(
% 17.76/2.83 sQ22_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f642])).
% 17.76/2.83 fof(f644,plain,(
% 17.76/2.83 $false|sQ32_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f598,f59])).
% 17.76/2.83 fof(f645,plain,(
% 17.76/2.83 sQ32_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f644])).
% 17.76/2.83 fof(f646,plain,(
% 17.76/2.83 $false|sQ19_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f505,f59])).
% 17.76/2.83 fof(f647,plain,(
% 17.76/2.83 sQ19_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f646])).
% 17.76/2.83 fof(f652,plain,(
% 17.76/2.83 ~int_leq(sK1_skl,sK2_skl)|~sQ5_spl|sQ16_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f98,f494])).
% 17.76/2.83 fof(f653,plain,(
% 17.76/2.83 ~int_leq(int_zero,sK2_skl)|~sQ5_spl|sQ26_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f98,f535])).
% 17.76/2.83 fof(f654,plain,(
% 17.76/2.83 ~int_leq(int_one,sK2_skl)|~sQ5_spl|sQ30_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f98,f590])).
% 17.76/2.83 fof(f668,plain,(
% 17.76/2.83 ~sQ21_spl|~sQ5_spl|sQ16_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f652,f513,f97,f492])).
% 17.76/2.83 fof(f669,plain,(
% 17.76/2.83 $false|~sQ10_spl|~sQ5_spl|sQ26_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f653,f290])).
% 17.76/2.83 fof(f670,plain,(
% 17.76/2.83 ~sQ10_spl|~sQ5_spl|sQ26_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f669])).
% 17.76/2.83 fof(f676,plain,(
% 17.76/2.83 ![X0]: (int_less(X0,plus(X0,sK1_skl)))),
% 17.76/2.83 inference(resolution,[status(thm)],[f354,f61])).
% 17.76/2.83 fof(f743,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,int_zero)|a(int_zero,plus(int_zero,X0))=real_zero)),
% 17.76/2.83 inference(resolution,[status(thm)],[f63,f74])).
% 17.76/2.83 fof(f762,definition,(
% 17.76/2.83 ![X0]: (sQ42_spl <=> (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|a(int_zero,plus(int_zero,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f765,plain,(
% 17.76/2.83 ~sQ32_spl|~sQ30_spl|sQ42_spl|~sQ39_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f743,f596,f588,f762,f627])).
% 17.76/2.83 fof(f819,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(n,X0))|~int_leq(int_one,n)|~int_leq(n,n)|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(plus(n,X0),X0),plus(n,X0))=lu(plus(plus(n,X0),X0),plus(n,X0))|int_leq(n,plus(n,X0)))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f83])).
% 17.76/2.83 fof(f825,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_less(int_zero,X0)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f83])).
% 17.76/2.83 fof(f830,plain,(
% 17.76/2.83 ![X0,X1]: (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|~int_leq(int_one,X0)|a(plus(int_one,X1),int_one)=lu(plus(int_one,X1),int_one))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f59])).
% 17.76/2.83 fof(f832,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_less(int_zero,X0)|~int_leq(int_one,int_zero)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f74])).
% 17.76/2.83 fof(f833,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_leq(int_one,n)|~int_leq(n,n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(plus(sK2_skl,X0),sK2_skl)=lu(plus(sK2_skl,X0),sK2_skl))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f50])).
% 17.76/2.83 fof(f836,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_leq(int_one,sK2_skl)|~int_leq(sK2_skl,n)|~int_less(int_zero,X0)|~int_leq(int_one,sK1_skl)|a(plus(sK1_skl,X0),sK1_skl)=lu(plus(sK1_skl,X0),sK1_skl))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f73])).
% 17.76/2.83 fof(f842,plain,(
% 17.76/2.83 ![X0,X1]: (~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|~int_leq(X1,int_zero)|a(plus(X1,X0),X1)=lu(plus(X1,X0),X1))),
% 17.76/2.83 inference(paramodulation,[status(thm)],[f85,f62])).
% 17.76/2.83 fof(f844,plain,(
% 17.76/2.83 ![X0,X1,X2]: (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X1,X0),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|~int_leq(int_one,X2)|~int_leq(X2,X0)|a(plus(X2,X1),X2)=lu(plus(X2,X1),X2))),
% 17.76/2.83 inference(paramodulation,[status(thm)],[f27,f62])).
% 17.76/2.83 fof(f846,definition,(
% 17.76/2.83 ![X0]: (sQ45_spl <=> (~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(plus(n,X0),X0),plus(n,X0))=lu(plus(plus(n,X0),X0),plus(n,X0))|int_leq(n,plus(n,X0))))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f849,plain,(
% 17.76/2.83 sQ45_spl|~sQ30_spl|~sQ17_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f819,f846,f588,f495])).
% 17.76/2.83 fof(f851,definition,(
% 17.76/2.83 ![X0]: (sQ46_spl <=> (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f854,plain,(
% 17.76/2.83 sQ46_spl|~sQ32_spl|~sQ30_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f825,f851,f596,f588])).
% 17.76/2.83 fof(f857,plain,(
% 17.76/2.83 ![X0,X1]: (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|a(plus(int_one,X1),int_one)=lu(plus(int_one,X1),int_one))),
% 17.76/2.83 inference(duplicate_literals_removal,[status(thm)],[f830])).
% 17.76/2.83 fof(f862,definition,(
% 17.76/2.83 ![X0]: (sQ48_spl <=> (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f865,plain,(
% 17.76/2.83 sQ48_spl|~sQ32_spl|~sQ30_spl|~sQ39_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f832,f862,f596,f588,f627])).
% 17.76/2.83 fof(f866,definition,(
% 17.76/2.83 ![X0]: (sQ49_spl <=> (~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_less(int_zero,X0)|a(plus(sK2_skl,X0),sK2_skl)=lu(plus(sK2_skl,X0),sK2_skl)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f869,plain,(
% 17.76/2.83 sQ49_spl|~sQ30_spl|~sQ17_spl|~sQ36_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f833,f866,f588,f495,f613])).
% 17.76/2.83 fof(f878,definition,(
% 17.76/2.83 ![X0]: (sQ52_spl <=> (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_less(int_zero,X0)|a(plus(sK1_skl,X0),sK1_skl)=lu(plus(sK1_skl,X0),sK1_skl)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f881,plain,(
% 17.76/2.83 sQ52_spl|~sQ36_spl|~sQ22_spl|~sQ34_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f836,f878,f613,f516,f606])).
% 17.76/2.83 fof(f885,definition,(
% 17.76/2.83 ![X0,X1]: (sQ53_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|~int_leq(X1,int_zero)|a(plus(X1,X0),X1)=lu(plus(X1,X0),X1)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f888,plain,(
% 17.76/2.83 sQ53_spl|~sQ39_spl|~sQ26_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f842,f885,f627,f533])).
% 17.76/2.83 fof(f897,plain,(
% 17.76/2.83 ~int_leq(int_one,n)|a(int_one,int_one)=real_one|~sQ1_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f83])).
% 17.76/2.83 fof(f902,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,n)|~int_leq(int_one,X0)|~int_leq(X0,int_one)|a(X0,X0)=real_one|~sQ1_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f59])).
% 17.76/2.83 fof(f903,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,sK2_skl)|~int_leq(int_one,X0)|~int_leq(X0,sK2_skl)|a(X0,X0)=real_one|~sQ1_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f50])).
% 17.76/2.83 fof(f908,plain,(
% 17.76/2.83 ~int_leq(int_one,n)|~int_leq(int_one,n)|a(n,n)=real_one|~sQ1_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f59])).
% 17.76/2.83 fof(f909,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,n)|~int_leq(int_one,X0)|~int_leq(X0,n)|a(X0,X0)=real_one|~sQ1_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f59])).
% 17.76/2.83 fof(f919,plain,(
% 17.76/2.83 ~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_leq(int_one,int_zero)|a(int_zero,int_zero)=real_one|~sQ1_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f74])).
% 17.76/2.83 fof(f920,plain,(
% 17.76/2.83 ~int_leq(int_one,n)|~int_leq(n,n)|~int_leq(int_one,sK2_skl)|a(sK2_skl,sK2_skl)=real_one|~sQ1_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f50])).
% 17.76/2.83 fof(f923,plain,(
% 17.76/2.83 ~int_leq(int_one,sK2_skl)|~int_leq(sK2_skl,n)|~int_leq(int_one,sK1_skl)|a(sK1_skl,sK1_skl)=real_one|~sQ1_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f56,f73])).
% 17.76/2.83 fof(f929,definition,(
% 17.76/2.83 sQ55_spl <=> (int_leq(sK2_skl,sK2_skl))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f931,plain,(
% 17.76/2.83 ~int_leq(sK2_skl,sK2_skl)|sQ55_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f929])).
% 17.76/2.83 fof(f932,definition,(
% 17.76/2.83 sQ56_spl <=> (a(sK2_skl,sK2_skl)=real_one)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f936,definition,(
% 17.76/2.83 ![X0]: (sQ57_spl <=> (~int_leq(int_one,X0)|~int_leq(X0,sK2_skl)|a(X0,X0)=real_one))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f940,definition,(
% 17.76/2.83 sQ58_spl <=> (a(sK1_skl,sK1_skl)=real_one)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f948,definition,(
% 17.76/2.83 sQ60_spl <=> (a(int_one,int_one)=real_one)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f949,plain,(
% 17.76/2.83 a(int_one,int_one)=real_one|~sQ60_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f948])).
% 17.76/2.83 fof(f951,plain,(
% 17.76/2.83 ~sQ30_spl|sQ60_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f897,f588,f948,f55])).
% 17.76/2.83 fof(f954,definition,(
% 17.76/2.83 ![X0]: (sQ61_spl <=> (~int_leq(int_one,X0)|~int_leq(X0,int_one)|a(X0,X0)=real_one))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f957,plain,(
% 17.76/2.83 ~sQ30_spl|sQ61_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f902,f588,f954,f55])).
% 17.76/2.83 fof(f958,plain,(
% 17.76/2.83 ~sQ36_spl|sQ57_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f903,f613,f936,f55])).
% 17.76/2.83 fof(f962,definition,(
% 17.76/2.83 sQ63_spl <=> (a(n,n)=real_one)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f967,plain,(
% 17.76/2.83 ~sQ30_spl|sQ63_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f908,f588,f962,f55])).
% 17.76/2.83 fof(f968,definition,(
% 17.76/2.83 ![X0]: (sQ64_spl <=> (~int_leq(int_one,X0)|~int_leq(X0,n)|a(X0,X0)=real_one))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f971,plain,(
% 17.76/2.83 ~sQ30_spl|sQ64_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f909,f588,f968,f55])).
% 17.76/2.83 fof(f987,definition,(
% 17.76/2.83 sQ68_spl <=> (a(int_zero,int_zero)=real_one)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f991,plain,(
% 17.76/2.83 ~sQ32_spl|~sQ30_spl|~sQ39_spl|sQ68_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f919,f596,f588,f627,f987,f55])).
% 17.76/2.83 fof(f992,plain,(
% 17.76/2.83 ~sQ30_spl|~sQ17_spl|~sQ36_spl|sQ56_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f920,f588,f495,f613,f932,f55])).
% 17.76/2.83 fof(f995,plain,(
% 17.76/2.83 ~sQ36_spl|~sQ22_spl|~sQ34_spl|sQ58_spl|~sQ1_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f923,f613,f516,f606,f940,f55])).
% 17.76/2.83 fof(f999,plain,(
% 17.76/2.83 ~sQ36_spl|~sQ5_spl|sQ30_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f654,f613,f97,f588])).
% 17.76/2.83 fof(f1176,definition,(
% 17.76/2.83 sQ69_spl <=> (int_less(int_zero,sK2_skl))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1179,definition,(
% 17.76/2.83 sQ70_spl <=> (int_zero=sK2_skl)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1180,plain,(
% 17.76/2.83 int_zero=sK2_skl|~sQ70_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1179])).
% 17.76/2.83 fof(f1218,definition,(
% 17.76/2.83 ![X0]: (sQ71_spl <=> (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_less(int_zero,X0)|a(int_zero,plus(int_zero,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1302,definition,(
% 17.76/2.83 ![X0]: (sQ73_spl <=> (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_less(int_zero,X0)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1320,plain,(
% 17.76/2.83 ![X0]: (plus(n,sK0_skl(plus(n,X0),n))=plus(n,X0)|~int_leq(int_one,plus(n,X0))|~int_leq(int_one,n)|~int_leq(n,n)|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(plus(n,X0),X0),plus(n,X0))=lu(plus(plus(n,X0),X0),plus(n,X0)))),
% 17.76/2.83 inference(resolution,[status(thm)],[f153,f62])).
% 17.76/2.83 fof(f1322,plain,(
% 17.76/2.83 ![X0]: (plus(n,sK0_skl(plus(n,X0),n))=plus(n,X0)|~int_leq(int_one,n)|~int_leq(n,n)|~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(n,X0),plus(plus(n,X0),X0))=real_zero)),
% 17.76/2.83 inference(resolution,[status(thm)],[f153,f63])).
% 17.76/2.83 fof(f1346,definition,(
% 17.76/2.83 ![X0]: (sQ75_spl <=> (plus(n,sK0_skl(plus(n,X0),n))=plus(n,X0)|~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(plus(n,X0),X0),plus(n,X0))=lu(plus(plus(n,X0),X0),plus(n,X0))))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1349,plain,(
% 17.76/2.83 sQ75_spl|~sQ30_spl|~sQ17_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f1320,f1346,f588,f495])).
% 17.76/2.83 fof(f1350,definition,(
% 17.76/2.83 ![X0]: (sQ76_spl <=> (plus(n,sK0_skl(plus(n,X0),n))=plus(n,X0)|~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(n,X0))|a(plus(n,X0),plus(plus(n,X0),X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1353,plain,(
% 17.76/2.83 sQ76_spl|~sQ30_spl|~sQ17_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f1322,f1350,f588,f495])).
% 17.76/2.83 fof(f1428,definition,(
% 17.76/2.83 sQ82_spl <=> (n=int_one)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1429,plain,(
% 17.76/2.83 n=int_one|~sQ82_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1428])).
% 17.76/2.83 fof(f1453,plain,(
% 17.76/2.83 ![X0]: (int_less(X0,X0)|int_leq(int_zero,int_zero))),
% 17.76/2.83 inference(paramodulation,[status(thm)],[f28,f235])).
% 17.76/2.83 fof(f1458,definition,(
% 17.76/2.83 ![X0]: (sQ83_spl <=> (int_less(X0,X0)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1459,plain,(
% 17.76/2.83 ![X0]: (int_less(X0,X0)|~sQ83_spl)),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1458])).
% 17.76/2.83 fof(f1461,definition,(
% 17.76/2.83 sQ84_spl <=> (int_leq(int_zero,int_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1464,plain,(
% 17.76/2.83 sQ83_spl|sQ84_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f1453,f1458,f1461])).
% 17.76/2.83 fof(f1465,plain,(
% 17.76/2.83 $false|~sQ83_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f1459,f60])).
% 17.76/2.83 fof(f1466,plain,(
% 17.76/2.83 ~sQ83_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f1465])).
% 17.76/2.83 fof(f1467,plain,(
% 17.76/2.83 int_less(int_one,sK2_skl)|~sQ2_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f78,f67])).
% 17.76/2.83 fof(f1470,plain,(
% 17.76/2.83 int_less(int_zero,int_one)|int_leq(int_one,int_zero)),
% 17.76/2.83 inference(paramodulation,[status(thm)],[f155,f161])).
% 17.76/2.83 fof(f1471,plain,(
% 17.76/2.83 sQ8_spl|sQ39_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f1470,f113,f627])).
% 17.76/2.83 fof(f1491,plain,(
% 17.76/2.83 int_less(sK1_skl,plus(sK2_skl,int_one))),
% 17.76/2.83 inference(resolution,[status(thm)],[f76,f236])).
% 17.76/2.83 fof(f1516,definition,(
% 17.76/2.83 sQ86_spl <=> (int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl))))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1518,plain,(
% 17.76/2.83 ~int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)))|sQ86_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1516])).
% 17.76/2.83 fof(f1519,definition,(
% 17.76/2.83 sQ87_spl <=> (int_less(int_zero,sK0_skl(sK2_skl,sK1_skl)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1521,plain,(
% 17.76/2.83 ~int_less(int_zero,sK0_skl(sK2_skl,sK1_skl))|sQ87_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1519])).
% 17.76/2.83 fof(f1530,plain,(
% 17.76/2.83 $false|sQ87_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f1521,f160])).
% 17.76/2.83 fof(f1531,plain,(
% 17.76/2.83 sQ87_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f1530])).
% 17.76/2.83 fof(f1532,plain,(
% 17.76/2.83 ~int_leq(int_one,sK2_skl)|sQ86_spl),
% 17.76/2.83 inference(forward_demodulation,[status(thm)],[f152,f1518])).
% 17.76/2.83 fof(f1533,plain,(
% 17.76/2.83 $false|~sQ2_spl|sQ86_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f1532,f301])).
% 17.76/2.83 fof(f1534,plain,(
% 17.76/2.83 ~sQ2_spl|sQ86_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f1533])).
% 17.76/2.83 fof(f1735,definition,(
% 17.76/2.83 sQ91_spl <=> (int_leq(sK2_skl,int_one))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1736,plain,(
% 17.76/2.83 int_leq(sK2_skl,int_one)|~sQ91_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1735])).
% 17.76/2.83 fof(f1737,plain,(
% 17.76/2.83 ~int_leq(sK2_skl,int_one)|sQ91_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1735])).
% 17.76/2.83 fof(f1863,plain,(
% 17.76/2.83 $false|sQ55_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f931,f59])).
% 17.76/2.83 fof(f1864,plain,(
% 17.76/2.83 sQ55_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f1863])).
% 17.76/2.83 fof(f1956,definition,(
% 17.76/2.83 sQ119_spl <=> (int_leq(sK2_skl,int_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f1957,plain,(
% 17.76/2.83 int_leq(sK2_skl,int_zero)|~sQ119_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f1956])).
% 17.76/2.83 fof(f2044,definition,(
% 17.76/2.83 ![X0]: (sQ128_spl <=> (int_leq(int_one,X0)|~int_leq(int_one,X0)|a(X0,X0)=real_one))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2077,plain,(
% 17.76/2.83 ![X0,X1]: (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|~int_leq(int_one,int_one)|a(plus(int_one,X1),int_one)=lu(plus(int_one,X1),int_one)|int_leq(X0,int_zero))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f358])).
% 17.76/2.83 fof(f2079,plain,(
% 17.76/2.83 ![X0,X1]: (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|a(plus(X1,X0),X1)=lu(plus(X1,X0),X1)|int_leq(int_one,X1))),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f358])).
% 17.76/2.83 fof(f2109,definition,(
% 17.76/2.83 ![X0,X1]: (sQ130_spl <=> (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|a(plus(int_one,X1),int_one)=lu(plus(int_one,X1),int_one)|int_leq(X0,int_zero)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2112,plain,(
% 17.76/2.83 sQ130_spl|~sQ32_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2077,f2109,f596])).
% 17.76/2.83 fof(f2114,definition,(
% 17.76/2.83 ![X0,X1]: (sQ131_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|a(plus(X1,X0),X1)=lu(plus(X1,X0),X1)|int_leq(int_one,X1)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2117,plain,(
% 17.76/2.83 sQ131_spl|~sQ39_spl|~sQ26_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2079,f2114,f627,f533])).
% 17.76/2.83 fof(f2148,plain,(
% 17.76/2.83 ![X0,X1]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_less(int_zero,X1)|~int_leq(int_one,int_one)|a(int_one,plus(int_one,X1))=real_zero|int_leq(X0,int_zero))),
% 17.76/2.83 inference(resolution,[status(thm)],[f63,f358])).
% 17.76/2.83 fof(f2150,plain,(
% 17.76/2.83 ![X0,X1]: (~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|a(X1,plus(X1,X0))=real_zero|int_leq(int_one,X1))),
% 17.76/2.83 inference(resolution,[status(thm)],[f63,f358])).
% 17.76/2.83 fof(f2180,definition,(
% 17.76/2.83 ![X0,X1]: (sQ133_spl <=> (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X0,X1),n)|~int_less(int_zero,X1)|a(int_one,plus(int_one,X1))=real_zero|int_leq(X0,int_zero)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2183,plain,(
% 17.76/2.83 sQ133_spl|~sQ32_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2148,f2180,f596])).
% 17.76/2.83 fof(f2185,definition,(
% 17.76/2.83 ![X0,X1]: (sQ134_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|a(X1,plus(X1,X0))=real_zero|int_leq(int_one,X1)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2188,plain,(
% 17.76/2.83 ~sQ39_spl|~sQ26_spl|sQ134_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2150,f627,f533,f2185])).
% 17.76/2.83 fof(f2204,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(sK2_skl,plus(sK2_skl,X0))=real_zero|~sQ119_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f1957,f63])).
% 17.76/2.83 fof(f2205,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(plus(sK2_skl,X0),sK2_skl)=lu(plus(sK2_skl,X0),sK2_skl)|~sQ119_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f1957,f62])).
% 17.76/2.83 fof(f2209,plain,(
% 17.76/2.83 int_less(sK2_skl,int_zero)|sK2_skl=int_zero|~sQ119_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f1957,f17])).
% 17.76/2.83 fof(f2210,definition,(
% 17.76/2.83 ![X0]: (sQ135_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|a(sK2_skl,plus(sK2_skl,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2213,plain,(
% 17.76/2.83 ~sQ39_spl|~sQ26_spl|sQ135_spl|~sQ36_spl|~sQ119_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2204,f627,f533,f2210,f613,f1956])).
% 17.76/2.83 fof(f2214,definition,(
% 17.76/2.83 ![X0]: (sQ136_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|a(plus(sK2_skl,X0),sK2_skl)=lu(plus(sK2_skl,X0),sK2_skl)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2217,plain,(
% 17.76/2.83 sQ136_spl|~sQ39_spl|~sQ26_spl|~sQ36_spl|~sQ119_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2205,f2214,f627,f533,f613,f1956])).
% 17.76/2.83 fof(f2221,definition,(
% 17.76/2.83 sQ137_spl <=> (int_less(sK2_skl,int_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2222,plain,(
% 17.76/2.83 int_less(sK2_skl,int_zero)|~sQ137_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f2221])).
% 17.76/2.83 fof(f2224,plain,(
% 17.76/2.83 sQ137_spl|sQ70_spl|~sQ119_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2209,f2221,f1179,f1956])).
% 17.76/2.83 fof(f2235,plain,(
% 17.76/2.83 ~int_leq(int_one,sK2_skl)|~sQ70_spl|sQ39_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f1180,f629])).
% 17.76/2.83 fof(f2237,plain,(
% 17.76/2.83 int_less(sK2_skl,sK2_skl)|~sQ70_spl|~sQ2_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f1180,f411])).
% 17.76/2.83 fof(f2246,plain,(
% 17.76/2.83 ![X0]: (X0=plus(sK2_skl,X0)|~sQ70_spl)),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f1180,f85])).
% 17.76/2.83 fof(f2330,plain,(
% 17.76/2.83 ~sQ36_spl|~sQ70_spl|sQ39_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2235,f613,f1179,f627])).
% 17.76/2.83 fof(f2331,plain,(
% 17.76/2.83 $false|~sQ70_spl|~sQ2_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f2237,f60])).
% 17.76/2.83 fof(f2332,plain,(
% 17.76/2.83 ~sQ70_spl|~sQ2_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f2331])).
% 17.76/2.83 fof(f2403,plain,(
% 17.76/2.83 int_leq(sK2_skl,int_one)|~sQ82_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f1429,f50])).
% 17.76/2.83 fof(f2482,plain,(
% 17.76/2.83 $false|sQ91_spl|~sQ82_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f2403,f1737])).
% 17.76/2.83 fof(f2483,plain,(
% 17.76/2.83 sQ91_spl|~sQ82_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f2482])).
% 17.76/2.83 fof(f2514,plain,(
% 17.76/2.83 int_less(sK1_skl,int_zero)|~sQ137_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f2222,f76])).
% 17.76/2.83 fof(f2523,plain,(
% 17.76/2.83 int_leq(sK2_skl,int_zero)|~sQ137_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f2222,f18])).
% 17.76/2.83 fof(f2663,plain,(
% 17.76/2.83 int_less(int_zero,sK0_skl(sK1_skl,int_zero))),
% 17.76/2.83 inference(resolution,[status(thm)],[f354,f35])).
% 17.76/2.83 fof(f2668,plain,(
% 17.76/2.83 plus(int_zero,sK0_skl(sK1_skl,int_zero))=sK1_skl),
% 17.76/2.83 inference(resolution,[status(thm)],[f354,f34])).
% 17.76/2.83 fof(f2676,plain,(
% 17.76/2.83 sK0_skl(sK1_skl,int_zero)=sK1_skl),
% 17.76/2.83 inference(forward_demodulation,[status(thm)],[f85,f2668])).
% 17.76/2.83 fof(f2705,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(sK2_skl,plus(sK2_skl,X0))=real_zero|~sQ91_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f1736,f63])).
% 17.76/2.83 fof(f2709,plain,(
% 17.76/2.83 int_less(sK2_skl,int_one)|sK2_skl=int_one|~sQ91_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f1736,f17])).
% 17.76/2.83 fof(f2710,definition,(
% 17.76/2.83 ![X0]: (sQ139_spl <=> (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(int_one,X0),n)|~int_less(int_zero,X0)|a(sK2_skl,plus(sK2_skl,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2713,plain,(
% 17.76/2.83 ~sQ32_spl|~sQ30_spl|sQ139_spl|~sQ36_spl|~sQ91_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2705,f596,f588,f2710,f613,f1735])).
% 17.76/2.83 fof(f2714,definition,(
% 17.76/2.83 sQ140_spl <=> (int_less(sK2_skl,int_one))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f2717,plain,(
% 17.76/2.83 sQ140_spl|sQ15_spl|~sQ91_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f2709,f2714,f417,f1735])).
% 17.76/2.83 fof(f2865,plain,(
% 17.76/2.83 int_less(sK2_skl,sK2_skl)|~sQ15_spl|~sQ2_spl),
% 17.76/2.83 inference(forward_demodulation,[status(thm)],[f418,f1467])).
% 17.76/2.83 fof(f2866,plain,(
% 17.76/2.83 $false|~sQ15_spl|~sQ2_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f2865,f60])).
% 17.76/2.83 fof(f2867,plain,(
% 17.76/2.83 ~sQ15_spl|~sQ2_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f2866])).
% 17.76/2.83 fof(f3042,plain,(
% 17.76/2.83 int_leq(sK1_skl,int_zero)|~sQ137_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f2514,f18])).
% 17.76/2.83 fof(f3046,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(sK2_skl,plus(sK2_skl,X0))=real_zero|~sQ137_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f2523,f63])).
% 17.76/2.83 fof(f3051,plain,(
% 17.76/2.83 ~sQ39_spl|~sQ26_spl|sQ135_spl|~sQ36_spl|~sQ137_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3046,f627,f533,f2210,f613,f2221])).
% 17.76/2.83 fof(f3146,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(plus(sK2_skl,X0),sK2_skl)=lu(plus(sK2_skl,X0),sK2_skl)|~sQ137_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f2523])).
% 17.76/2.83 fof(f3172,plain,(
% 17.76/2.83 sQ136_spl|~sQ39_spl|~sQ26_spl|~sQ36_spl|~sQ137_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3146,f2214,f627,f533,f613,f2221])).
% 17.76/2.83 fof(f3224,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_leq(int_one,n)|~int_leq(n,n)|~int_less(int_zero,X0)|~int_leq(int_one,int_one)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one)|~sQ30_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f589,f62])).
% 17.76/2.83 fof(f3227,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,n)|~int_leq(n,n)|~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,int_one)|a(int_one,plus(int_one,X0))=real_zero|~sQ30_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f589,f63])).
% 17.76/2.83 fof(f3231,plain,(
% 17.76/2.83 int_less(int_one,n)|int_one=n|~sQ30_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f589,f17])).
% 17.76/2.83 fof(f3241,definition,(
% 17.76/2.83 ![X0]: (sQ145_spl <=> (~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_less(int_zero,X0)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f3244,plain,(
% 17.76/2.83 sQ145_spl|~sQ30_spl|~sQ17_spl|~sQ32_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3224,f3241,f588,f495,f596])).
% 17.76/2.83 fof(f3247,definition,(
% 17.76/2.83 ![X0]: (sQ146_spl <=> (~int_leq(int_one,plus(n,X0))|~int_leq(plus(n,X0),n)|~int_less(int_zero,X0)|a(int_one,plus(int_one,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f3250,plain,(
% 17.76/2.83 ~sQ30_spl|~sQ17_spl|sQ146_spl|~sQ32_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3227,f588,f495,f3247,f596])).
% 17.76/2.83 fof(f3251,definition,(
% 17.76/2.83 sQ147_spl <=> (int_less(int_one,n))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f3254,plain,(
% 17.76/2.83 sQ147_spl|sQ82_spl|~sQ30_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3231,f3251,f1428,f588])).
% 17.76/2.83 fof(f3393,definition,(
% 17.76/2.83 sQ150_spl <=> (int_leq(int_one,plus(sK1_skl,int_zero)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f3395,plain,(
% 17.76/2.83 ~int_leq(int_one,plus(sK1_skl,int_zero))|sQ150_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f3393])).
% 17.76/2.83 fof(f3400,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_less(int_zero,X0)|~int_leq(int_one,sK1_skl)|a(plus(sK1_skl,X0),sK1_skl)=lu(plus(sK1_skl,X0),sK1_skl)|~sQ137_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f3042,f62])).
% 17.76/2.83 fof(f3402,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,sK1_skl)|a(sK1_skl,plus(sK1_skl,X0))=real_zero|~sQ137_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f3042,f63])).
% 17.76/2.83 fof(f3406,plain,(
% 17.76/2.83 int_less(sK1_skl,int_zero)|sK1_skl=int_zero|~sQ137_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f3042,f17])).
% 17.76/2.83 fof(f3407,definition,(
% 17.76/2.83 ![X0]: (sQ152_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|a(plus(sK1_skl,X0),sK1_skl)=lu(plus(sK1_skl,X0),sK1_skl)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f3410,plain,(
% 17.76/2.83 sQ152_spl|~sQ39_spl|~sQ26_spl|~sQ34_spl|~sQ137_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3400,f3407,f627,f533,f606,f2221])).
% 17.76/2.83 fof(f3412,definition,(
% 17.76/2.83 ![X0]: (sQ153_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(int_zero,X0),n)|~int_less(int_zero,X0)|a(sK1_skl,plus(sK1_skl,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f3415,plain,(
% 17.76/2.83 ~sQ39_spl|~sQ26_spl|sQ153_spl|~sQ34_spl|~sQ137_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3402,f627,f533,f3412,f606,f2221])).
% 17.76/2.83 fof(f3419,definition,(
% 17.76/2.83 sQ154_spl <=> (int_less(sK1_skl,int_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f3422,plain,(
% 17.76/2.83 sQ154_spl|sQ11_spl|~sQ137_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3406,f3419,f170,f2221])).
% 17.76/2.83 fof(f3481,plain,(
% 17.76/2.83 ![X0]: (int_less(X0,X0)|~sQ11_spl)),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f189,f676])).
% 17.76/2.83 fof(f3651,plain,(
% 17.76/2.83 sQ83_spl|~sQ11_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3481,f1458,f170])).
% 17.76/2.83 fof(f3672,plain,(
% 17.76/2.83 int_less(int_zero,sK1_skl)),
% 17.76/2.83 inference(forward_demodulation,[status(thm)],[f2676,f2663])).
% 17.76/2.83 fof(f3696,plain,(
% 17.76/2.83 ~int_leq(sK1_skl,sK2_skl)|~sQ3_spl|sQ86_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f70,f1532])).
% 17.76/2.83 fof(f3714,plain,(
% 17.76/2.83 int_less(sK1_skl,plus(sK2_skl,sK1_skl))|~sQ3_spl),
% 17.76/2.83 inference(backward_demodulation,[status(thm)],[f70,f1491])).
% 17.76/2.83 fof(f4074,plain,(
% 17.76/2.83 ~sQ30_spl|~sQ0_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f423,f588,f52])).
% 17.76/2.83 fof(f4085,plain,(
% 17.76/2.83 $false|sQ10_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f169,f3672])).
% 17.76/2.83 fof(f4086,plain,(
% 17.76/2.83 sQ10_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f4085])).
% 17.76/2.83 fof(f4251,plain,(
% 17.76/2.83 ~sQ21_spl|~sQ3_spl|sQ86_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f3696,f513,f69,f1516])).
% 17.76/2.83 fof(f4254,plain,(
% 17.76/2.83 int_less(sK1_skl,sK1_skl)|~sQ70_spl|~sQ3_spl),
% 17.76/2.83 inference(forward_demodulation,[status(thm)],[f2246,f3714])).
% 17.76/2.83 fof(f4255,plain,(
% 17.76/2.83 $false|~sQ70_spl|~sQ3_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f4254,f60])).
% 17.76/2.83 fof(f4256,plain,(
% 17.76/2.83 ~sQ70_spl|~sQ3_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f4255])).
% 17.76/2.83 fof(f4427,plain,(
% 17.76/2.83 ~int_leq(sK1_skl,n)|~sQ3_spl|sQ30_spl),
% 17.76/2.83 inference(forward_demodulation,[status(thm)],[f70,f590])).
% 17.76/2.83 fof(f4464,plain,(
% 17.76/2.83 ~sQ16_spl|~sQ3_spl|sQ30_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f4427,f492,f69,f588])).
% 17.76/2.83 fof(f4543,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,sK2_skl)|~int_leq(sK2_skl,n)|~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_less(int_zero,X0)|~int_leq(int_one,int_zero)|a(int_zero,plus(int_zero,X0))=real_zero|~sQ10_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f290,f63])).
% 17.76/2.83 fof(f4546,plain,(
% 17.76/2.83 int_less(int_zero,sK2_skl)|int_zero=sK2_skl|~sQ10_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f290,f17])).
% 17.76/2.83 fof(f4547,plain,(
% 17.76/2.83 ~sQ36_spl|~sQ22_spl|sQ71_spl|~sQ39_spl|~sQ10_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f4543,f613,f516,f1218,f627,f167])).
% 17.76/2.83 fof(f4550,plain,(
% 17.76/2.83 sQ69_spl|sQ70_spl|~sQ10_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f4546,f1176,f1179,f167])).
% 17.76/2.83 fof(f4842,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(sK2_skl,X0),n)|~int_leq(int_one,sK2_skl)|~int_leq(sK2_skl,n)|~int_less(int_zero,X0)|~int_leq(int_one,int_zero)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero)|~sQ10_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f62,f290])).
% 17.76/2.83 fof(f4869,plain,(
% 17.76/2.83 sQ73_spl|~sQ36_spl|~sQ22_spl|~sQ39_spl|~sQ10_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f4842,f1302,f613,f516,f627,f167])).
% 17.76/2.83 fof(f4956,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_less(int_zero,X0)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one))),
% 17.76/2.83 inference(paramodulation,[status(thm)],[f85,f857])).
% 17.76/2.83 fof(f4961,definition,(
% 17.76/2.83 ![X0]: (sQ155_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_less(int_zero,X0)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f4964,plain,(
% 17.76/2.83 sQ155_spl|~sQ39_spl|~sQ26_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f4956,f4961,f627,f533])).
% 17.76/2.83 fof(f4966,definition,(
% 17.76/2.83 ![X0]: (sQ156_spl <=> (~int_leq(int_one,plus(X0,int_zero))|~int_leq(X0,n)|~int_leq(int_one,X0)|~int_leq(X0,n)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f4967,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(X0,int_zero))|~int_leq(X0,n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~sQ156_spl)),
% 17.76/2.83 inference(component_clause,[status(thm)],[f4966])).
% 17.76/2.83 fof(f4973,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_less(int_zero,X0)|a(int_one,plus(int_one,X0))=real_zero)),
% 17.76/2.83 inference(paramodulation,[status(thm)],[f85,f605])).
% 17.76/2.83 fof(f4975,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,plus(X0,int_zero))|~int_leq(X0,n)|~int_less(int_zero,int_zero)|a(int_one,plus(int_one,int_zero))=real_zero)),
% 17.76/2.83 inference(paramodulation,[status(thm)],[f28,f605])).
% 17.76/2.83 fof(f4978,definition,(
% 17.76/2.83 ![X0]: (sQ157_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(X0,n)|~int_less(int_zero,X0)|a(int_one,plus(int_one,X0))=real_zero))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f4981,plain,(
% 17.76/2.83 ~sQ39_spl|~sQ26_spl|sQ157_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f4973,f627,f533,f4978])).
% 17.76/2.83 fof(f4986,definition,(
% 17.76/2.83 sQ159_spl <=> (a(int_one,plus(int_one,int_zero))=real_zero)),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f4987,plain,(
% 17.76/2.83 a(int_one,plus(int_one,int_zero))=real_zero|~sQ159_spl),
% 17.76/2.83 inference(component_clause,[status(thm)],[f4986])).
% 17.76/2.83 fof(f4989,plain,(
% 17.76/2.83 sQ156_spl|~sQ29_spl|sQ159_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f4975,f4966,f543,f4986])).
% 17.76/2.83 fof(f5037,plain,(
% 17.76/2.83 int_leq(sK2_skl,plus(int_one,int_zero))|~sQ137_spl),
% 17.76/2.83 inference(resolution,[status(thm)],[f146,f2523])).
% 17.76/2.83 fof(f5048,plain,(
% 17.76/2.83 int_leq(sK2_skl,int_one)|~sQ137_spl),
% 17.76/2.83 inference(forward_demodulation,[status(thm)],[f28,f5037])).
% 17.76/2.83 fof(f5049,plain,(
% 17.76/2.83 $false|sQ91_spl|~sQ137_spl),
% 17.76/2.83 inference(forward_subsumption_resolution,[status(thm)],[f5048,f1737])).
% 17.76/2.83 fof(f5050,plain,(
% 17.76/2.83 sQ91_spl|~sQ137_spl),
% 17.76/2.83 inference(contradiction_clause,[status(thm)],[f5049])).
% 17.76/2.83 fof(f5051,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(n,X0))|~int_leq(int_one,n)|~int_leq(n,n)|~int_less(int_zero,X0)|~int_leq(int_one,plus(X0,n))|a(plus(plus(X0,n),X0),plus(X0,n))=lu(plus(plus(X0,n),X0),plus(X0,n))|plus(n,sK0_skl(plus(X0,n),n))=plus(X0,n))),
% 17.76/2.83 inference(resolution,[status(thm)],[f844,f153])).
% 17.76/2.83 fof(f5053,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(n,X0))|~int_leq(int_one,n)|~int_leq(n,n)|~int_less(int_zero,X0)|~int_leq(int_one,plus(X0,n))|a(plus(plus(X0,n),X0),plus(X0,n))=lu(plus(plus(X0,n),X0),plus(X0,n))|int_leq(n,plus(X0,n)))),
% 17.76/2.83 inference(resolution,[status(thm)],[f844,f83])).
% 17.76/2.83 fof(f5061,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(X0,int_one),n)|~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_less(int_zero,X0)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one))),
% 17.76/2.83 inference(resolution,[status(thm)],[f844,f83])).
% 17.76/2.83 fof(f5069,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(X0,sK2_skl),n)|~int_leq(int_one,sK2_skl)|~int_leq(sK2_skl,n)|~int_less(int_zero,X0)|~int_leq(int_one,int_zero)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero)|~sQ10_spl)),
% 17.76/2.83 inference(resolution,[status(thm)],[f844,f290])).
% 17.76/2.83 fof(f5072,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(n,X0))|~int_leq(plus(X0,n),n)|~int_leq(int_one,n)|~int_leq(n,n)|~int_less(int_zero,X0)|~int_leq(int_one,sK2_skl)|a(plus(sK2_skl,X0),sK2_skl)=lu(plus(sK2_skl,X0),sK2_skl))),
% 17.76/2.83 inference(resolution,[status(thm)],[f844,f50])).
% 17.76/2.83 fof(f5074,plain,(
% 17.76/2.83 ![X0]: (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(X0,sK2_skl),n)|~int_leq(int_one,sK2_skl)|~int_leq(sK2_skl,n)|~int_less(int_zero,X0)|~int_leq(int_one,sK1_skl)|a(plus(sK1_skl,X0),sK1_skl)=lu(plus(sK1_skl,X0),sK1_skl))),
% 17.76/2.83 inference(resolution,[status(thm)],[f844,f73])).
% 17.76/2.83 fof(f5086,definition,(
% 17.76/2.83 ![X0]: (sQ160_spl <=> (~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(X0,n))|a(plus(plus(X0,n),X0),plus(X0,n))=lu(plus(plus(X0,n),X0),plus(X0,n))|plus(n,sK0_skl(plus(X0,n),n))=plus(X0,n)))),
% 17.76/2.83 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 17.76/2.83 fof(f5089,plain,(
% 17.76/2.83 sQ160_spl|~sQ30_spl|~sQ17_spl),
% 17.76/2.83 inference(split_clause,[status(thm)],[f5051,f5086,f588,f495])).
% 17.76/2.83 fof(f5090,definition,(
% 17.76/2.83 ![X0]: (sQ161_spl <=> (~int_leq(int_one,plus(n,X0))|~int_less(int_zero,X0)|~int_leq(int_one,plus(X0,n))|a(plus(plus(X0,n),X0),plus(X0,n))=lu(plus(plus(X0,n),X0),plus(X0,n))|int_leq(n,plus(X0,n))))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5093,plain,(
% 17.76/2.84 sQ161_spl|~sQ30_spl|~sQ17_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5053,f5090,f588,f495])).
% 17.76/2.84 fof(f5095,definition,(
% 17.76/2.84 ![X0]: (sQ162_spl <=> (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(X0,int_one),n)|~int_less(int_zero,X0)|a(plus(int_one,X0),int_one)=lu(plus(int_one,X0),int_one)))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5099,plain,(
% 17.76/2.84 sQ162_spl|~sQ32_spl|~sQ30_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5061,f5095,f596,f588])).
% 17.76/2.84 fof(f5111,definition,(
% 17.76/2.84 ![X0]: (sQ165_spl <=> (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(X0,sK2_skl),n)|~int_less(int_zero,X0)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero)))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5114,plain,(
% 17.76/2.84 sQ165_spl|~sQ36_spl|~sQ22_spl|~sQ39_spl|~sQ10_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5069,f5111,f613,f516,f627,f167])).
% 17.76/2.84 fof(f5123,definition,(
% 17.76/2.84 ![X0]: (sQ168_spl <=> (~int_leq(int_one,plus(n,X0))|~int_leq(plus(X0,n),n)|~int_less(int_zero,X0)|a(plus(sK2_skl,X0),sK2_skl)=lu(plus(sK2_skl,X0),sK2_skl)))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5126,plain,(
% 17.76/2.84 sQ168_spl|~sQ30_spl|~sQ17_spl|~sQ36_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5072,f5123,f588,f495,f613])).
% 17.76/2.84 fof(f5131,definition,(
% 17.76/2.84 ![X0]: (sQ170_spl <=> (~int_leq(int_one,plus(sK2_skl,X0))|~int_leq(plus(X0,sK2_skl),n)|~int_less(int_zero,X0)|a(plus(sK1_skl,X0),sK1_skl)=lu(plus(sK1_skl,X0),sK1_skl)))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5134,plain,(
% 17.76/2.84 sQ170_spl|~sQ36_spl|~sQ22_spl|~sQ34_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5074,f5131,f613,f516,f606])).
% 17.76/2.84 fof(f5153,plain,(
% 17.76/2.84 ![X0]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~sQ156_spl)),
% 17.76/2.84 inference(forward_demodulation,[status(thm)],[f28,f4967])).
% 17.76/2.84 fof(f5154,plain,(
% 17.76/2.84 ![X0]: (~int_leq(int_one,X0)|~int_leq(X0,n)|~sQ156_spl)),
% 17.76/2.84 inference(duplicate_literals_removal,[status(thm)],[f5153])).
% 17.76/2.84 fof(f5283,definition,(
% 17.76/2.84 sQ177_spl <=> (int_leq(int_zero,int_one))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5285,plain,(
% 17.76/2.84 ~int_leq(int_zero,int_one)|sQ177_spl),
% 17.76/2.84 inference(component_clause,[status(thm)],[f5283])).
% 17.76/2.84 fof(f5295,plain,(
% 17.76/2.84 $false|sQ177_spl),
% 17.76/2.84 inference(forward_subsumption_resolution,[status(thm)],[f5285,f74])).
% 17.76/2.84 fof(f5296,plain,(
% 17.76/2.84 sQ177_spl),
% 17.76/2.84 inference(contradiction_clause,[status(thm)],[f5295])).
% 17.76/2.84 fof(f5302,plain,(
% 17.76/2.84 ![X0]: (int_leq(sK1_skl,int_zero)|int_less(X0,plus(X0,sK2_skl)))),
% 17.76/2.84 inference(resolution,[status(thm)],[f211,f61])).
% 17.76/2.84 fof(f5320,definition,(
% 17.76/2.84 ![X0]: (sQ178_spl <=> (int_less(X0,plus(X0,sK2_skl))))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5323,plain,(
% 17.76/2.84 sQ25_spl|sQ178_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5302,f530,f5320])).
% 17.76/2.84 fof(f5339,definition,(
% 17.76/2.84 sQ180_spl <=> (int_less(n,int_zero))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5340,plain,(
% 17.76/2.84 int_less(n,int_zero)|~sQ180_spl),
% 17.76/2.84 inference(component_clause,[status(thm)],[f5339])).
% 17.76/2.84 fof(f5342,definition,(
% 17.76/2.84 sQ181_spl <=> (n=int_zero)),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5343,plain,(
% 17.76/2.84 n=int_zero|~sQ181_spl),
% 17.76/2.84 inference(component_clause,[status(thm)],[f5342])).
% 17.76/2.84 fof(f5356,plain,(
% 17.76/2.84 int_leq(sK2_skl,int_zero)|~sQ181_spl),
% 17.76/2.84 inference(backward_demodulation,[status(thm)],[f5343,f50])).
% 17.76/2.84 fof(f5357,plain,(
% 17.76/2.84 int_less(int_zero,int_zero)|~sQ181_spl|~sQ180_spl),
% 17.76/2.84 inference(backward_demodulation,[status(thm)],[f5343,f5340])).
% 17.76/2.84 fof(f5425,plain,(
% 17.76/2.84 sQ119_spl|~sQ181_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5356,f1956,f5342])).
% 17.76/2.84 fof(f5426,plain,(
% 17.76/2.84 $false|~sQ181_spl|~sQ180_spl),
% 17.76/2.84 inference(forward_subsumption_resolution,[status(thm)],[f5357,f60])).
% 17.76/2.84 fof(f5427,plain,(
% 17.76/2.84 ~sQ181_spl|~sQ180_spl),
% 17.76/2.84 inference(contradiction_clause,[status(thm)],[f5426])).
% 17.76/2.84 fof(f5428,plain,(
% 17.76/2.84 sQ0_spl|~sQ156_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5154,f52,f4966])).
% 17.76/2.84 fof(f5506,plain,(
% 17.76/2.84 int_less(sK1_skl,int_zero)|sK1_skl=int_zero|~sQ25_spl),
% 17.76/2.84 inference(resolution,[status(thm)],[f531,f17])).
% 17.76/2.84 fof(f5512,plain,(
% 17.76/2.84 sQ154_spl|sQ11_spl|~sQ25_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5506,f3419,f170,f530])).
% 17.76/2.84 fof(f5633,plain,(
% 17.76/2.84 ![X0]: (~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_leq(int_one,X0)|a(X0,X0)=real_one|int_leq(int_one,X0)|~sQ1_spl)),
% 17.76/2.84 inference(resolution,[status(thm)],[f56,f358])).
% 17.76/2.84 fof(f5686,plain,(
% 17.76/2.84 ~sQ39_spl|~sQ26_spl|sQ128_spl|~sQ1_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5633,f627,f533,f2044,f55])).
% 17.76/2.84 fof(f5838,plain,(
% 17.76/2.84 ![X0]: (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(X0,int_one),n)|~int_leq(int_one,int_one)|~int_leq(int_one,n)|~int_less(int_zero,X0)|~int_leq(int_one,int_zero)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero))),
% 17.76/2.84 inference(resolution,[status(thm)],[f844,f74])).
% 17.76/2.84 fof(f5843,plain,(
% 17.76/2.84 ![X0,X1]: (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X1,X0),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|~int_leq(int_one,int_one)|a(plus(int_one,X1),int_one)=lu(plus(int_one,X1),int_one)|int_leq(X0,int_zero))),
% 17.76/2.84 inference(resolution,[status(thm)],[f844,f358])).
% 17.76/2.84 fof(f5846,plain,(
% 17.76/2.84 ![X0,X1]: (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(X0,int_zero),n)|~int_leq(int_one,int_zero)|~int_leq(int_zero,n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|a(plus(X1,X0),X1)=lu(plus(X1,X0),X1)|int_leq(int_one,X1))),
% 17.76/2.84 inference(resolution,[status(thm)],[f844,f358])).
% 17.76/2.84 fof(f5877,definition,(
% 17.76/2.84 ![X0]: (sQ189_spl <=> (~int_leq(int_one,plus(int_one,X0))|~int_leq(plus(X0,int_one),n)|~int_less(int_zero,X0)|a(plus(int_zero,X0),int_zero)=lu(plus(int_zero,X0),int_zero)))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5880,plain,(
% 17.76/2.84 sQ189_spl|~sQ32_spl|~sQ30_spl|~sQ39_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5838,f5877,f596,f588,f627])).
% 17.76/2.84 fof(f5885,definition,(
% 17.76/2.84 ![X0,X1]: (sQ190_spl <=> (~int_leq(int_one,plus(X0,X1))|~int_leq(plus(X1,X0),n)|~int_leq(int_one,X0)|~int_leq(X0,n)|~int_less(int_zero,X1)|a(plus(int_one,X1),int_one)=lu(plus(int_one,X1),int_one)|int_leq(X0,int_zero)))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5888,plain,(
% 17.76/2.84 sQ190_spl|~sQ32_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5843,f5885,f596])).
% 17.76/2.84 fof(f5891,definition,(
% 17.76/2.84 ![X0,X1]: (sQ191_spl <=> (~int_leq(int_one,plus(int_zero,X0))|~int_leq(plus(X0,int_zero),n)|~int_less(int_zero,X0)|~int_leq(int_one,X1)|a(plus(X1,X0),X1)=lu(plus(X1,X0),X1)|int_leq(int_one,X1)))),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5894,plain,(
% 17.76/2.84 sQ191_spl|~sQ39_spl|~sQ26_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5846,f5891,f627,f533])).
% 17.76/2.84 fof(f5923,plain,(
% 17.76/2.84 real_zero=real_one|~sQ159_spl|~sQ60_spl),
% 17.76/2.84 inference(backward_demodulation,[status(thm)],[f5924,f949])).
% 17.76/2.84 fof(f5924,plain,(
% 17.76/2.84 a(int_one,int_one)=real_zero|~sQ159_spl),
% 17.76/2.84 inference(forward_demodulation,[status(thm)],[f28,f4987])).
% 17.76/2.84 fof(f5925,plain,(
% 17.76/2.84 ~int_leq(int_one,sK1_skl)|sQ150_spl),
% 17.76/2.84 inference(forward_demodulation,[status(thm)],[f28,f3395])).
% 17.76/2.84 fof(f5926,plain,(
% 17.76/2.84 $false|sQ150_spl),
% 17.76/2.84 inference(forward_subsumption_resolution,[status(thm)],[f5925,f48])).
% 17.76/2.84 fof(f5927,plain,(
% 17.76/2.84 sQ150_spl),
% 17.76/2.84 inference(contradiction_clause,[status(thm)],[f5926])).
% 17.76/2.84 fof(f5928,plain,(
% 17.76/2.84 $false|~sQ159_spl|~sQ60_spl),
% 17.76/2.84 inference(forward_subsumption_resolution,[status(thm)],[f5923,f41])).
% 17.76/2.84 fof(f5929,plain,(
% 17.76/2.84 ~sQ159_spl|~sQ60_spl),
% 17.76/2.84 inference(contradiction_clause,[status(thm)],[f5928])).
% 17.76/2.84 fof(f5953,plain,(
% 17.76/2.84 ~int_leq(int_one,sK1_skl)|~int_leq(sK1_skl,n)|~int_leq(int_one,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)))|~int_leq(sK2_skl,n)|~int_less(int_zero,sK0_skl(sK2_skl,sK1_skl))|~int_leq(sK1_skl,sK1_skl)|a(sK1_skl,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)))=real_zero),
% 17.76/2.84 inference(paramodulation,[status(thm)],[f152,f569])).
% 17.76/2.84 fof(f5961,definition,(
% 17.76/2.84 sQ193_spl <=> (a(sK1_skl,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)))=real_zero)),
% 17.76/2.84 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 17.76/2.84 fof(f5962,plain,(
% 17.76/2.84 a(sK1_skl,plus(sK1_skl,sK0_skl(sK2_skl,sK1_skl)))=real_zero|~sQ193_spl),
% 17.76/2.84 inference(component_clause,[status(thm)],[f5961])).
% 17.76/2.84 fof(f5964,plain,(
% 17.76/2.84 ~sQ34_spl|~sQ16_spl|~sQ86_spl|~sQ22_spl|~sQ87_spl|~sQ19_spl|sQ193_spl),
% 17.76/2.84 inference(split_clause,[status(thm)],[f5953,f606,f492,f1516,f516,f1519,f503,f5961])).
% 17.76/2.84 fof(f5972,plain,(
% 17.76/2.84 a(sK1_skl,sK2_skl)=real_zero|~sQ193_spl),
% 17.76/2.84 inference(forward_demodulation,[status(thm)],[f152,f5962])).
% 17.76/2.84 fof(f5973,plain,(
% 17.76/2.84 $false|~sQ193_spl),
% 17.76/2.84 inference(forward_subsumption_resolution,[status(thm)],[f5972,f51])).
% 17.76/2.84 fof(f5974,plain,(
% 17.76/2.84 ~sQ193_spl),
% 17.76/2.84 inference(contradiction_clause,[status(thm)],[f5973])).
% 17.76/2.84 fof(f5975,plain,(
% 17.76/2.84 $false),
% 17.76/2.84 inference(sat_refutation,[status(thm)],[f58,f72,f100,f548,f550,f552,f594,f602,f619,f623,f633,f639,f641,f643,f645,f647,f668,f670,f765,f849,f854,f865,f869,f881,f888,f951,f957,f958,f967,f971,f991,f992,f995,f999,f1349,f1353,f1464,f1466,f1471,f1531,f1534,f1864,f2112,f2117,f2183,f2188,f2213,f2217,f2224,f2330,f2332,f2483,f2713,f2717,f2867,f3051,f3172,f3244,f3250,f3254,f3410,f3415,f3422,f3651,f4074,f4086,f4251,f4256,f4464,f4547,f4550,f4869,f4964,f4981,f4989,f5050,f5089,f5093,f5099,f5114,f5126,f5134,f5296,f5323,f5425,f5427,f5428,f5512,f5686,f5880,f5888,f5894,f5927,f5929,f5964,f5974])).
% 17.76/2.84 % SZS output end CNFRefutation for theBenchmark.p
% 17.76/2.87 % Elapsed time: 2.418688 seconds
% 17.76/2.87 % CPU time: 18.610165 seconds
% 17.76/2.87 % Total memory used: 178.899 MB
% 17.76/2.87 % Net memory used: 162.401 MB
%------------------------------------------------------------------------------