%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV103+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:50:04 PM UTC 2026
% Result : Theorem 1.03s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV103+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.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.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 08:28:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 1.03/0.59 % Refutation found
% 1.03/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.03/0.59 % SZS output start CNFRefutation for theBenchmark
% 1.03/0.59 fof(f3,axiom,(
% 1.03/0.59 (! [X] : ~ gt(X,X) )),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f6,axiom,(
% 1.03/0.59 (! [X,Y] :( lt(X,Y)<=> gt(Y,X) ) )),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f11,axiom,(
% 1.03/0.59 (! [X] : gt(succ(X),X) )),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f48,axiom,(
% 1.03/0.59 (! [X,U,VAL] : a_select2(tptp_update2(X,U,VAL),U) = VAL )),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f49,axiom,(
% 1.03/0.59 (! [I,U,X,VAL,VAL2] :( ( I != U& a_select2(X,U) = VAL )=> a_select2(tptp_update2(X,I,VAL2),U) = VAL ) )),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f53,conjecture,(
% 1.03/0.59 ( ( a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use )=> ( a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f54,negated_conjecture,(
% 1.03/0.59 ~(( ( a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use )=> ( a_select3(u_defuse,n0,n0) = use& a_select3(u_defuse,n1,n0) = use& a_select3(u_defuse,n2,n0) = use& a_select2(xinit_defuse,n3) = use& a_select2(xinit_defuse,n4) = use& a_select2(xinit_defuse,n5) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ) )),
% 1.03/0.59 inference(negated_conjecture,[status(cth)],[f53])).
% 1.03/0.59 fof(f55,axiom,(
% 1.03/0.59 gt(n5,n4) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f62,axiom,(
% 1.03/0.59 gt(n4,n0) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f63,axiom,(
% 1.03/0.59 gt(n5,n0) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f64,axiom,(
% 1.03/0.59 gt(n1,n0) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f65,axiom,(
% 1.03/0.59 gt(n2,n0) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f67,axiom,(
% 1.03/0.59 gt(n4,n1) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f68,axiom,(
% 1.03/0.59 gt(n5,n1) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f69,axiom,(
% 1.03/0.59 gt(n2,n1) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f70,axiom,(
% 1.03/0.59 gt(n3,n1) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f71,axiom,(
% 1.03/0.59 gt(n4,n2) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f72,axiom,(
% 1.03/0.59 gt(n5,n2) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f74,axiom,(
% 1.03/0.59 gt(n4,n3) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f75,axiom,(
% 1.03/0.59 gt(n5,n3) ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f85,axiom,(
% 1.03/0.59 succ(succ(n0)) = n2 ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f86,axiom,(
% 1.03/0.59 succ(succ(succ(n0))) = n3 ),
% 1.03/0.59 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.03/0.59 fof(f91,plain,(
% 1.03/0.59 ![X0]: (~gt(X0,X0))),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f3])).
% 1.03/0.59 fof(f96,plain,(
% 1.03/0.59 ![X,Y]: ((~lt(X,Y)|gt(Y,X))&(lt(X,Y)|~gt(Y,X)))),
% 1.03/0.59 inference(NNF_transformation,[status(thm)],[f6])).
% 1.03/0.59 fof(f97,plain,(
% 1.03/0.59 (![X,Y]: (~lt(X,Y)|gt(Y,X)))&(![X,Y]: (lt(X,Y)|~gt(Y,X)))),
% 1.03/0.59 inference(miniscoping,[status(thm)],[f96])).
% 1.03/0.59 fof(f98,plain,(
% 1.03/0.59 ![X0,X1]: (~lt(X0,X1)|gt(X1,X0))),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f97])).
% 1.03/0.59 fof(f99,plain,(
% 1.03/0.59 ![X0,X1]: (lt(X0,X1)|~gt(X1,X0))),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f97])).
% 1.03/0.59 fof(f112,plain,(
% 1.03/0.59 ![X0]: (gt(succ(X0),X0))),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f11])).
% 1.03/0.59 fof(f233,plain,(
% 1.03/0.59 ![X0,X1,X2]: (a_select2(tptp_update2(X0,X1,X2),X1)=X2)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f48])).
% 1.03/0.59 fof(f234,plain,(
% 1.03/0.59 ![I,U,X,VAL,VAL2]: ((I=U|~a_select2(X,U)=VAL)|a_select2(tptp_update2(X,I,VAL2),U)=VAL)),
% 1.03/0.59 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 1.03/0.59 fof(f235,plain,(
% 1.03/0.59 ![I,U,X,VAL]: ((I=U|~a_select2(X,U)=VAL)|(![VAL2]: a_select2(tptp_update2(X,I,VAL2),U)=VAL))),
% 1.03/0.59 inference(miniscoping,[status(thm)],[f234])).
% 1.03/0.59 fof(f236,plain,(
% 1.03/0.59 ![X0,X1,X2,X3,X4]: (X0=X1|~a_select2(X2,X1)=X3|a_select2(tptp_update2(X2,X0,X4),X1)=X3)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f235])).
% 1.03/0.59 fof(f244,plain,(
% 1.03/0.59 ((((((a_select3(u_defuse,n0,n0)=use&a_select3(u_defuse,n1,n0)=use)&a_select3(u_defuse,n2,n0)=use)&a_select2(xinit_defuse,n3)=use)&a_select2(xinit_defuse,n4)=use)&a_select2(xinit_defuse,n5)=use)&(((((((((((~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use)|~a_select3(u_defuse,n2,n0)=use)|~a_select2(xinit_defuse,n3)=use)|~a_select2(xinit_defuse,n4)=use)|~a_select2(xinit_defuse,n5)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use))),
% 1.03/0.59 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 1.03/0.59 fof(f245,plain,(
% 1.03/0.59 a_select3(u_defuse,n0,n0)=use),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f244])).
% 1.03/0.59 fof(f246,plain,(
% 1.03/0.59 a_select3(u_defuse,n1,n0)=use),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f244])).
% 1.03/0.59 fof(f247,plain,(
% 1.03/0.59 a_select3(u_defuse,n2,n0)=use),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f244])).
% 1.03/0.59 fof(f248,plain,(
% 1.03/0.59 a_select2(xinit_defuse,n3)=use),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f244])).
% 1.03/0.59 fof(f249,plain,(
% 1.03/0.59 a_select2(xinit_defuse,n4)=use),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f244])).
% 1.03/0.59 fof(f250,plain,(
% 1.03/0.59 a_select2(xinit_defuse,n5)=use),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f244])).
% 1.03/0.59 fof(f251,plain,(
% 1.03/0.59 ~a_select3(u_defuse,n0,n0)=use|~a_select3(u_defuse,n1,n0)=use|~a_select3(u_defuse,n2,n0)=use|~a_select2(xinit_defuse,n3)=use|~a_select2(xinit_defuse,n4)=use|~a_select2(xinit_defuse,n5)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f244])).
% 1.03/0.59 fof(f252,plain,(
% 1.03/0.59 gt(n5,n4)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f55])).
% 1.03/0.59 fof(f259,plain,(
% 1.03/0.59 gt(n4,n0)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f62])).
% 1.03/0.59 fof(f260,plain,(
% 1.03/0.59 gt(n5,n0)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f63])).
% 1.03/0.59 fof(f261,plain,(
% 1.03/0.59 gt(n1,n0)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f64])).
% 1.03/0.59 fof(f262,plain,(
% 1.03/0.59 gt(n2,n0)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f65])).
% 1.03/0.59 fof(f264,plain,(
% 1.03/0.59 gt(n4,n1)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f67])).
% 1.03/0.59 fof(f265,plain,(
% 1.03/0.59 gt(n5,n1)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f68])).
% 1.03/0.59 fof(f266,plain,(
% 1.03/0.59 gt(n2,n1)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f69])).
% 1.03/0.59 fof(f267,plain,(
% 1.03/0.59 gt(n3,n1)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f70])).
% 1.03/0.59 fof(f268,plain,(
% 1.03/0.59 gt(n4,n2)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f71])).
% 1.03/0.59 fof(f269,plain,(
% 1.03/0.59 gt(n5,n2)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f72])).
% 1.03/0.59 fof(f271,plain,(
% 1.03/0.59 gt(n4,n3)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f74])).
% 1.03/0.59 fof(f272,plain,(
% 1.03/0.59 gt(n5,n3)),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f75])).
% 1.03/0.59 fof(f288,plain,(
% 1.03/0.59 succ(succ(n0))=n2),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f85])).
% 1.03/0.59 fof(f289,plain,(
% 1.03/0.59 succ(succ(succ(n0)))=n3),
% 1.03/0.59 inference(cnf_transformation,[status(thm)],[f86])).
% 1.03/0.59 fof(f326,definition,(
% 1.03/0.59 sQ0_spl <=> (a_select3(u_defuse,n0,n0)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f328,plain,(
% 1.03/0.59 ~a_select3(u_defuse,n0,n0)=use|sQ0_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f326])).
% 1.03/0.59 fof(f329,definition,(
% 1.03/0.59 sQ1_spl <=> (a_select3(u_defuse,n1,n0)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f331,plain,(
% 1.03/0.59 ~a_select3(u_defuse,n1,n0)=use|sQ1_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f329])).
% 1.03/0.59 fof(f332,definition,(
% 1.03/0.59 sQ2_spl <=> (a_select3(u_defuse,n2,n0)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f334,plain,(
% 1.03/0.59 ~a_select3(u_defuse,n2,n0)=use|sQ2_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f332])).
% 1.03/0.59 fof(f335,definition,(
% 1.03/0.59 sQ3_spl <=> (a_select2(xinit_defuse,n3)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f337,plain,(
% 1.03/0.59 ~a_select2(xinit_defuse,n3)=use|sQ3_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f335])).
% 1.03/0.59 fof(f338,definition,(
% 1.03/0.59 sQ4_spl <=> (a_select2(xinit_defuse,n4)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f340,plain,(
% 1.03/0.59 ~a_select2(xinit_defuse,n4)=use|sQ4_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f338])).
% 1.03/0.59 fof(f341,definition,(
% 1.03/0.59 sQ5_spl <=> (a_select2(xinit_defuse,n5)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f343,plain,(
% 1.03/0.59 ~a_select2(xinit_defuse,n5)=use|sQ5_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f341])).
% 1.03/0.59 fof(f344,definition,(
% 1.03/0.59 sQ6_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f346,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)=use|sQ6_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f344])).
% 1.03/0.59 fof(f347,definition,(
% 1.03/0.59 sQ7_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f349,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)=use|sQ7_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f347])).
% 1.03/0.59 fof(f350,definition,(
% 1.03/0.59 sQ8_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f352,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)=use|sQ8_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f350])).
% 1.03/0.59 fof(f353,definition,(
% 1.03/0.59 sQ9_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f355,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)=use|sQ9_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f353])).
% 1.03/0.59 fof(f356,definition,(
% 1.03/0.59 sQ10_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f358,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)=use|sQ10_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f356])).
% 1.03/0.59 fof(f359,definition,(
% 1.03/0.59 sQ11_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f361,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)=use|sQ11_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f359])).
% 1.03/0.59 fof(f362,plain,(
% 1.03/0.59 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f251,f326,f329,f332,f335,f338,f341,f344,f347,f350,f353,f356,f359])).
% 1.03/0.59 fof(f364,plain,(
% 1.03/0.59 ![X0,X1,X2,X3]: (X0=X1|a_select2(tptp_update2(X2,X0,X3),X1)=a_select2(X2,X1))),
% 1.03/0.59 inference(destructive_equality_resolution,[status(thm)],[f236])).
% 1.03/0.59 fof(f403,plain,(
% 1.03/0.59 ~use=use|sQ11_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f233,f361])).
% 1.03/0.59 fof(f404,plain,(
% 1.03/0.59 $false|sQ11_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f403])).
% 1.03/0.59 fof(f405,plain,(
% 1.03/0.59 sQ11_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f404])).
% 1.03/0.59 fof(f406,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n4)=use|n5=n4|sQ10_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f358])).
% 1.03/0.59 fof(f407,definition,(
% 1.03/0.59 sQ12_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n4)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f409,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n4)=use|sQ12_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f407])).
% 1.03/0.59 fof(f410,definition,(
% 1.03/0.59 sQ13_spl <=> (n5=n4)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f411,plain,(
% 1.03/0.59 n5=n4|~sQ13_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f410])).
% 1.03/0.59 fof(f413,plain,(
% 1.03/0.59 ~sQ12_spl|sQ13_spl|sQ10_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f406,f407,f410,f356])).
% 1.03/0.59 fof(f414,plain,(
% 1.03/0.59 ~use=use|sQ12_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f233,f409])).
% 1.03/0.59 fof(f415,plain,(
% 1.03/0.59 $false|sQ12_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f414])).
% 1.03/0.59 fof(f416,plain,(
% 1.03/0.59 sQ12_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f415])).
% 1.03/0.59 fof(f421,plain,(
% 1.03/0.59 gt(n5,n5)|~sQ13_spl),
% 1.03/0.59 inference(backward_demodulation,[status(thm)],[f411,f252])).
% 1.03/0.59 fof(f423,plain,(
% 1.03/0.59 $false|~sQ13_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f421,f91])).
% 1.03/0.59 fof(f424,plain,(
% 1.03/0.59 ~sQ13_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f423])).
% 1.03/0.59 fof(f425,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|n5=n3|sQ9_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f355])).
% 1.03/0.59 fof(f426,definition,(
% 1.03/0.59 sQ14_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f428,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n3)=use|sQ14_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f426])).
% 1.03/0.59 fof(f429,definition,(
% 1.03/0.59 sQ15_spl <=> (n5=n3)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f430,plain,(
% 1.03/0.59 n5=n3|~sQ15_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f429])).
% 1.03/0.59 fof(f432,plain,(
% 1.03/0.59 ~sQ14_spl|sQ15_spl|sQ9_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f425,f426,f429,f353])).
% 1.03/0.59 fof(f441,plain,(
% 1.03/0.59 gt(n5,n5)|~sQ15_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f430,f272])).
% 1.03/0.59 fof(f442,plain,(
% 1.03/0.59 $false|~sQ15_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f441,f91])).
% 1.03/0.59 fof(f443,plain,(
% 1.03/0.59 ~sQ15_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f442])).
% 1.03/0.59 fof(f457,definition,(
% 1.03/0.59 sQ18_spl <=> (n0=n1)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f458,plain,(
% 1.03/0.59 n0=n1|~sQ18_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f457])).
% 1.03/0.59 fof(f460,definition,(
% 1.03/0.59 sQ19_spl <=> (n0=n2)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f461,plain,(
% 1.03/0.59 n0=n2|~sQ19_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f460])).
% 1.03/0.59 fof(f463,definition,(
% 1.03/0.59 sQ20_spl <=> (n0=n3)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f464,plain,(
% 1.03/0.59 n0=n3|~sQ20_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f463])).
% 1.03/0.59 fof(f466,definition,(
% 1.03/0.59 sQ21_spl <=> (n0=n4)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f467,plain,(
% 1.03/0.59 n0=n4|~sQ21_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f466])).
% 1.03/0.59 fof(f475,definition,(
% 1.03/0.59 sQ23_spl <=> (n0=n5)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f476,plain,(
% 1.03/0.59 n0=n5|~sQ23_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f475])).
% 1.03/0.59 fof(f481,plain,(
% 1.03/0.59 gt(n4,n4)|~sQ21_spl),
% 1.03/0.59 inference(backward_demodulation,[status(thm)],[f467,f259])).
% 1.03/0.59 fof(f495,plain,(
% 1.03/0.59 $false|~sQ21_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f481,f91])).
% 1.03/0.59 fof(f496,plain,(
% 1.03/0.59 ~sQ21_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f495])).
% 1.03/0.59 fof(f539,definition,(
% 1.03/0.59 sQ25_spl <=> (n4=n3)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f540,plain,(
% 1.03/0.59 n4=n3|~sQ25_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f539])).
% 1.03/0.59 fof(f557,plain,(
% 1.03/0.59 gt(n4,n4)|~sQ25_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f540,f271])).
% 1.03/0.59 fof(f558,plain,(
% 1.03/0.59 $false|~sQ25_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f557,f91])).
% 1.03/0.59 fof(f559,plain,(
% 1.03/0.59 ~sQ25_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f558])).
% 1.03/0.59 fof(f596,plain,(
% 1.03/0.59 lt(n0,n2)),
% 1.03/0.59 inference(resolution,[status(thm)],[f262,f99])).
% 1.03/0.59 fof(f598,plain,(
% 1.03/0.59 lt(n0,n1)),
% 1.03/0.59 inference(resolution,[status(thm)],[f261,f99])).
% 1.03/0.59 fof(f624,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3)=use|n4=n3|sQ14_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f428])).
% 1.03/0.59 fof(f625,definition,(
% 1.03/0.59 sQ28_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f627,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3)=use|sQ28_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f625])).
% 1.03/0.59 fof(f628,plain,(
% 1.03/0.59 ~sQ28_spl|sQ25_spl|sQ14_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f624,f625,f539,f426])).
% 1.03/0.59 fof(f629,plain,(
% 1.03/0.59 ~use=use|sQ28_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f233,f627])).
% 1.03/0.59 fof(f630,plain,(
% 1.03/0.59 $false|sQ28_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f629])).
% 1.03/0.59 fof(f631,plain,(
% 1.03/0.59 sQ28_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f630])).
% 1.03/0.59 fof(f632,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|n5=n2|sQ8_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f352])).
% 1.03/0.59 fof(f633,definition,(
% 1.03/0.59 sQ29_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f635,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n2)=use|sQ29_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f633])).
% 1.03/0.59 fof(f636,definition,(
% 1.03/0.59 sQ30_spl <=> (n5=n2)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f637,plain,(
% 1.03/0.59 n5=n2|~sQ30_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f636])).
% 1.03/0.59 fof(f639,plain,(
% 1.03/0.59 ~sQ29_spl|sQ30_spl|sQ8_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f632,f633,f636,f350])).
% 1.03/0.59 fof(f644,plain,(
% 1.03/0.59 lt(n0,n5)),
% 1.03/0.59 inference(resolution,[status(thm)],[f260,f99])).
% 1.03/0.59 fof(f649,plain,(
% 1.03/0.59 lt(n1,n4)),
% 1.03/0.59 inference(resolution,[status(thm)],[f264,f99])).
% 1.03/0.59 fof(f652,plain,(
% 1.03/0.59 lt(n1,n5)),
% 1.03/0.59 inference(resolution,[status(thm)],[f265,f99])).
% 1.03/0.59 fof(f658,plain,(
% 1.03/0.59 gt(n5,n5)|~sQ30_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f637,f269])).
% 1.03/0.59 fof(f659,plain,(
% 1.03/0.59 $false|~sQ30_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f658,f91])).
% 1.03/0.59 fof(f660,plain,(
% 1.03/0.59 ~sQ30_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f659])).
% 1.03/0.59 fof(f662,plain,(
% 1.03/0.59 lt(n1,n2)),
% 1.03/0.59 inference(resolution,[status(thm)],[f266,f99])).
% 1.03/0.59 fof(f746,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|n4=n2|sQ29_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f635])).
% 1.03/0.59 fof(f747,definition,(
% 1.03/0.59 sQ33_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f749,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2)=use|sQ33_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f747])).
% 1.03/0.59 fof(f750,definition,(
% 1.03/0.59 sQ34_spl <=> (n4=n2)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f751,plain,(
% 1.03/0.59 n4=n2|~sQ34_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f750])).
% 1.03/0.59 fof(f753,plain,(
% 1.03/0.59 ~sQ33_spl|sQ34_spl|sQ29_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f746,f747,f750,f633])).
% 1.03/0.59 fof(f770,plain,(
% 1.03/0.59 gt(n2,n0)),
% 1.03/0.59 inference(resolution,[status(thm)],[f596,f98])).
% 1.03/0.59 fof(f783,definition,(
% 1.03/0.59 sQ36_spl <=> (n2=n1)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f784,plain,(
% 1.03/0.59 n2=n1|~sQ36_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f783])).
% 1.03/0.59 fof(f867,definition,(
% 1.03/0.59 sQ41_spl <=> (n2=n3)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f868,plain,(
% 1.03/0.59 n2=n3|~sQ41_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f867])).
% 1.03/0.59 fof(f926,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n2)=use|n3=n2|sQ33_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f749])).
% 1.03/0.59 fof(f927,definition,(
% 1.03/0.59 sQ45_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n2)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f929,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n2)=use|sQ45_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f927])).
% 1.03/0.59 fof(f930,plain,(
% 1.03/0.59 ~sQ45_spl|sQ41_spl|sQ33_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f926,f927,f867,f747])).
% 1.03/0.59 fof(f931,plain,(
% 1.03/0.59 ~use=use|sQ45_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f233,f929])).
% 1.03/0.59 fof(f932,plain,(
% 1.03/0.59 $false|sQ45_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f931])).
% 1.03/0.59 fof(f933,plain,(
% 1.03/0.59 sQ45_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f932])).
% 1.03/0.59 fof(f967,plain,(
% 1.03/0.59 succ(succ(n0))=n3|~sQ41_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f868,f288])).
% 1.03/0.59 fof(f972,plain,(
% 1.03/0.59 succ(n3)=n3|~sQ41_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f967,f289])).
% 1.03/0.59 fof(f976,plain,(
% 1.03/0.59 gt(n3,n3)|~sQ41_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f972,f112])).
% 1.03/0.59 fof(f977,plain,(
% 1.03/0.59 $false|~sQ41_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f976,f91])).
% 1.03/0.59 fof(f978,plain,(
% 1.03/0.59 ~sQ41_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f977])).
% 1.03/0.59 fof(f1004,plain,(
% 1.03/0.59 gt(n5,n0)),
% 1.03/0.59 inference(resolution,[status(thm)],[f644,f98])).
% 1.03/0.59 fof(f1026,definition,(
% 1.03/0.59 sQ50_spl <=> (n1=n4)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1027,plain,(
% 1.03/0.59 n1=n4|~sQ50_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1026])).
% 1.03/0.59 fof(f1034,plain,(
% 1.03/0.59 lt(n4,n4)|~sQ50_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f1027,f649])).
% 1.03/0.59 fof(f1035,plain,(
% 1.03/0.59 gt(n4,n4)|~sQ50_spl),
% 1.03/0.59 inference(resolution,[status(thm)],[f1034,f98])).
% 1.03/0.59 fof(f1036,plain,(
% 1.03/0.59 $false|~sQ50_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1035,f91])).
% 1.03/0.59 fof(f1037,plain,(
% 1.03/0.59 ~sQ50_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1036])).
% 1.03/0.59 fof(f1082,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|n5=n1|sQ7_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f349])).
% 1.03/0.59 fof(f1083,definition,(
% 1.03/0.59 sQ53_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1085,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n1)=use|sQ53_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1083])).
% 1.03/0.59 fof(f1086,definition,(
% 1.03/0.59 sQ54_spl <=> (n5=n1)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1087,plain,(
% 1.03/0.59 n5=n1|~sQ54_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1086])).
% 1.03/0.59 fof(f1089,plain,(
% 1.03/0.59 ~sQ53_spl|sQ54_spl|sQ7_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f1082,f1083,f1086,f347])).
% 1.03/0.59 fof(f1092,plain,(
% 1.03/0.59 lt(n5,n5)|~sQ54_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f1087,f652])).
% 1.03/0.59 fof(f1093,plain,(
% 1.03/0.59 gt(n5,n5)|~sQ54_spl),
% 1.03/0.59 inference(resolution,[status(thm)],[f1092,f98])).
% 1.03/0.59 fof(f1094,plain,(
% 1.03/0.59 $false|~sQ54_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1093,f91])).
% 1.03/0.59 fof(f1095,plain,(
% 1.03/0.59 ~sQ54_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1094])).
% 1.03/0.59 fof(f1170,plain,(
% 1.03/0.59 lt(n2,n2)|~sQ36_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f784,f662])).
% 1.03/0.59 fof(f1171,plain,(
% 1.03/0.59 gt(n2,n2)|~sQ36_spl),
% 1.03/0.59 inference(resolution,[status(thm)],[f1170,f98])).
% 1.03/0.59 fof(f1172,plain,(
% 1.03/0.59 $false|~sQ36_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1171,f91])).
% 1.03/0.59 fof(f1173,plain,(
% 1.03/0.59 ~sQ36_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1172])).
% 1.03/0.59 fof(f1236,plain,(
% 1.03/0.59 gt(n4,n4)|~sQ34_spl),
% 1.03/0.59 inference(backward_demodulation,[status(thm)],[f751,f268])).
% 1.03/0.59 fof(f1244,plain,(
% 1.03/0.59 $false|~sQ34_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1236,f91])).
% 1.03/0.59 fof(f1245,plain,(
% 1.03/0.59 ~sQ34_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1244])).
% 1.03/0.59 fof(f1358,plain,(
% 1.03/0.59 gt(n2,n2)|~sQ19_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f461,f770])).
% 1.03/0.59 fof(f1359,plain,(
% 1.03/0.59 $false|~sQ19_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1358,f91])).
% 1.03/0.59 fof(f1360,plain,(
% 1.03/0.59 ~sQ19_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1359])).
% 1.03/0.59 fof(f1449,definition,(
% 1.03/0.59 sQ76_spl <=> (n1=n3)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1450,plain,(
% 1.03/0.59 n1=n3|~sQ76_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1449])).
% 1.03/0.59 fof(f1518,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|n4=n1|sQ53_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f1085])).
% 1.03/0.59 fof(f1519,definition,(
% 1.03/0.59 sQ78_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1521,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1)=use|sQ78_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1519])).
% 1.03/0.59 fof(f1522,plain,(
% 1.03/0.59 ~sQ78_spl|sQ50_spl|sQ53_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f1518,f1519,f1026,f1083])).
% 1.03/0.59 fof(f1527,plain,(
% 1.03/0.59 gt(n1,n0)),
% 1.03/0.59 inference(resolution,[status(thm)],[f598,f98])).
% 1.03/0.59 fof(f1736,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1)=use|n3=n1|sQ78_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f1521])).
% 1.03/0.59 fof(f1737,definition,(
% 1.03/0.59 sQ84_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1739,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1)=use|sQ84_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1737])).
% 1.03/0.59 fof(f1740,plain,(
% 1.03/0.59 ~sQ84_spl|sQ76_spl|sQ78_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f1736,f1737,f1449,f1519])).
% 1.03/0.59 fof(f1741,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n1)=use|n2=n1|sQ84_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f1739])).
% 1.03/0.59 fof(f1742,definition,(
% 1.03/0.59 sQ85_spl <=> (a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n1)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1744,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n1)=use|sQ85_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1742])).
% 1.03/0.59 fof(f1745,plain,(
% 1.03/0.59 ~sQ85_spl|sQ36_spl|sQ84_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f1741,f1742,f783,f1737])).
% 1.03/0.59 fof(f1746,plain,(
% 1.03/0.59 ~use=use|sQ85_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f233,f1744])).
% 1.03/0.59 fof(f1747,plain,(
% 1.03/0.59 $false|sQ85_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f1746])).
% 1.03/0.59 fof(f1748,plain,(
% 1.03/0.59 sQ85_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1747])).
% 1.03/0.59 fof(f1749,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|n5=n0|sQ6_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f346])).
% 1.03/0.59 fof(f1750,definition,(
% 1.03/0.59 sQ86_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use)),
% 1.03/0.59 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 1.03/0.59 fof(f1752,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n0)=use|sQ86_spl),
% 1.03/0.59 inference(component_clause,[status(thm)],[f1750])).
% 1.03/0.59 fof(f1753,plain,(
% 1.03/0.59 ~sQ86_spl|sQ23_spl|sQ6_spl),
% 1.03/0.59 inference(split_clause,[status(thm)],[f1749,f1750,f475,f344])).
% 1.03/0.59 fof(f1754,plain,(
% 1.03/0.59 ~use=use|sQ5_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f250,f343])).
% 1.03/0.59 fof(f1755,plain,(
% 1.03/0.59 $false|sQ5_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f1754])).
% 1.03/0.59 fof(f1756,plain,(
% 1.03/0.59 sQ5_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1755])).
% 1.03/0.59 fof(f1757,plain,(
% 1.03/0.59 ~use=use|sQ4_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f249,f340])).
% 1.03/0.59 fof(f1758,plain,(
% 1.03/0.59 $false|sQ4_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f1757])).
% 1.03/0.59 fof(f1759,plain,(
% 1.03/0.59 sQ4_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1758])).
% 1.03/0.59 fof(f1760,plain,(
% 1.03/0.59 ~use=use|sQ3_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f248,f337])).
% 1.03/0.59 fof(f1761,plain,(
% 1.03/0.59 $false|sQ3_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f1760])).
% 1.03/0.59 fof(f1762,plain,(
% 1.03/0.59 sQ3_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1761])).
% 1.03/0.59 fof(f1763,plain,(
% 1.03/0.59 ~use=use|sQ2_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f247,f334])).
% 1.03/0.59 fof(f1764,plain,(
% 1.03/0.59 $false|sQ2_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f1763])).
% 1.03/0.59 fof(f1765,plain,(
% 1.03/0.59 sQ2_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1764])).
% 1.03/0.59 fof(f1766,plain,(
% 1.03/0.59 ~use=use|sQ1_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f246,f331])).
% 1.03/0.59 fof(f1767,plain,(
% 1.03/0.59 $false|sQ1_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f1766])).
% 1.03/0.59 fof(f1768,plain,(
% 1.03/0.59 sQ1_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1767])).
% 1.03/0.59 fof(f1769,plain,(
% 1.03/0.59 ~use=use|sQ0_spl),
% 1.03/0.59 inference(forward_demodulation,[status(thm)],[f245,f328])).
% 1.03/0.59 fof(f1770,plain,(
% 1.03/0.59 $false|sQ0_spl),
% 1.03/0.59 inference(trivial_equality_resolution,[status(thm)],[f1769])).
% 1.03/0.59 fof(f1771,plain,(
% 1.03/0.59 sQ0_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1770])).
% 1.03/0.59 fof(f1776,plain,(
% 1.03/0.59 gt(n3,n3)|~sQ76_spl),
% 1.03/0.59 inference(backward_demodulation,[status(thm)],[f1450,f267])).
% 1.03/0.59 fof(f1796,plain,(
% 1.03/0.59 $false|~sQ76_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f1776,f91])).
% 1.03/0.59 fof(f1797,plain,(
% 1.03/0.59 ~sQ76_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f1796])).
% 1.03/0.59 fof(f2090,plain,(
% 1.03/0.59 gt(n5,n5)|~sQ23_spl),
% 1.03/0.59 inference(backward_demodulation,[status(thm)],[f476,f1004])).
% 1.03/0.59 fof(f2110,plain,(
% 1.03/0.59 $false|~sQ23_spl),
% 1.03/0.59 inference(forward_subsumption_resolution,[status(thm)],[f2090,f91])).
% 1.03/0.59 fof(f2111,plain,(
% 1.03/0.59 ~sQ23_spl),
% 1.03/0.59 inference(contradiction_clause,[status(thm)],[f2110])).
% 1.03/0.59 fof(f2293,plain,(
% 1.03/0.59 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|n4=n0|sQ86_spl),
% 1.03/0.59 inference(paramodulation,[status(thm)],[f364,f1752])).
% 1.03/0.59 fof(f2294,definition,(
% 1.03/0.59 sQ98_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use)),
% 1.03/0.60 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 1.03/0.60 fof(f2296,plain,(
% 1.03/0.60 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0)=use|sQ98_spl),
% 1.03/0.60 inference(component_clause,[status(thm)],[f2294])).
% 1.03/0.60 fof(f2297,plain,(
% 1.03/0.60 ~sQ98_spl|sQ21_spl|sQ86_spl),
% 1.03/0.60 inference(split_clause,[status(thm)],[f2293,f2294,f466,f1750])).
% 1.03/0.60 fof(f2455,plain,(
% 1.03/0.60 ~a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0)=use|n3=n0|sQ98_spl),
% 1.03/0.60 inference(paramodulation,[status(thm)],[f364,f2296])).
% 1.03/0.60 fof(f2456,definition,(
% 1.03/0.60 sQ110_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0)=use)),
% 1.03/0.60 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 1.03/0.60 fof(f2458,plain,(
% 1.03/0.60 ~a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0)=use|sQ110_spl),
% 1.03/0.60 inference(component_clause,[status(thm)],[f2456])).
% 1.03/0.60 fof(f2459,plain,(
% 1.03/0.60 ~sQ110_spl|sQ20_spl|sQ98_spl),
% 1.03/0.60 inference(split_clause,[status(thm)],[f2455,f2456,f463,f2294])).
% 1.03/0.60 fof(f2465,plain,(
% 1.03/0.60 ~a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3)=use|~sQ20_spl|sQ98_spl),
% 1.03/0.60 inference(backward_demodulation,[status(thm)],[f464,f2296])).
% 1.03/0.60 fof(f2482,plain,(
% 1.03/0.60 ~sQ28_spl|~sQ20_spl|sQ98_spl),
% 1.03/0.60 inference(split_clause,[status(thm)],[f2465,f625,f463,f2294])).
% 1.03/0.60 fof(f2561,plain,(
% 1.03/0.60 gt(n1,n1)|~sQ18_spl),
% 1.03/0.60 inference(forward_demodulation,[status(thm)],[f458,f1527])).
% 1.03/0.60 fof(f2562,plain,(
% 1.03/0.60 $false|~sQ18_spl),
% 1.03/0.60 inference(forward_subsumption_resolution,[status(thm)],[f2561,f91])).
% 1.03/0.60 fof(f2563,plain,(
% 1.03/0.60 ~sQ18_spl),
% 1.03/0.60 inference(contradiction_clause,[status(thm)],[f2562])).
% 1.03/0.60 fof(f2572,plain,(
% 1.03/0.60 ~a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0)=use|n2=n0|sQ110_spl),
% 1.03/0.60 inference(paramodulation,[status(thm)],[f364,f2458])).
% 1.03/0.60 fof(f2573,definition,(
% 1.03/0.60 sQ113_spl <=> (a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0)=use)),
% 1.03/0.61 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 1.03/0.61 fof(f2575,plain,(
% 1.03/0.61 ~a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0)=use|sQ113_spl),
% 1.03/0.61 inference(component_clause,[status(thm)],[f2573])).
% 1.03/0.61 fof(f2576,plain,(
% 1.03/0.61 ~sQ113_spl|sQ19_spl|sQ110_spl),
% 1.03/0.61 inference(split_clause,[status(thm)],[f2572,f2573,f460,f2456])).
% 1.03/0.61 fof(f2577,plain,(
% 1.03/0.61 ~a_select2(tptp_update2(sigma_defuse,n0,use),n0)=use|n1=n0|sQ113_spl),
% 1.03/0.61 inference(paramodulation,[status(thm)],[f364,f2575])).
% 1.03/0.61 fof(f2578,definition,(
% 1.03/0.61 sQ114_spl <=> (a_select2(tptp_update2(sigma_defuse,n0,use),n0)=use)),
% 1.03/0.61 introduced(definition,[new_symbols(definition,[sQ114_spl])],[split_symbol_definition])).
% 1.03/0.61 fof(f2580,plain,(
% 1.03/0.61 ~a_select2(tptp_update2(sigma_defuse,n0,use),n0)=use|sQ114_spl),
% 1.03/0.61 inference(component_clause,[status(thm)],[f2578])).
% 1.03/0.61 fof(f2581,plain,(
% 1.03/0.61 ~sQ114_spl|sQ18_spl|sQ113_spl),
% 1.03/0.61 inference(split_clause,[status(thm)],[f2577,f2578,f457,f2573])).
% 1.03/0.61 fof(f2582,plain,(
% 1.03/0.61 ~use=use|sQ114_spl),
% 1.03/0.61 inference(forward_demodulation,[status(thm)],[f233,f2580])).
% 1.03/0.61 fof(f2583,plain,(
% 1.03/0.61 $false|sQ114_spl),
% 1.03/0.61 inference(trivial_equality_resolution,[status(thm)],[f2582])).
% 1.03/0.61 fof(f2584,plain,(
% 1.03/0.61 sQ114_spl),
% 1.03/0.61 inference(contradiction_clause,[status(thm)],[f2583])).
% 1.03/0.61 fof(f2585,plain,(
% 1.03/0.61 $false),
% 1.03/0.61 inference(sat_refutation,[status(thm)],[f362,f405,f413,f416,f424,f432,f443,f496,f559,f628,f631,f639,f660,f753,f930,f933,f978,f1037,f1089,f1095,f1173,f1245,f1360,f1522,f1740,f1745,f1748,f1753,f1756,f1759,f1762,f1765,f1768,f1771,f1797,f2111,f2297,f2459,f2482,f2563,f2576,f2581,f2584])).
% 1.03/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 1.03/0.61 % Elapsed time: 0.235803 seconds
% 1.03/0.61 % CPU time: 1.523142 seconds
% 1.03/0.61 % Total memory used: 127.841 MB
% 1.03/0.61 % Net memory used: 125.198 MB
%------------------------------------------------------------------------------