%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV103+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:46:39 PM UTC 2026
% Result : Theorem 0.13s 0.59s
% Output : CNFRefutation 1.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 62
% Syntax : Number of formulae : 259 ( 73 unt; 42 def)
% Number of atoms : 556 ( 236 equ)
% Maximal formula atoms : 18 ( 2 avg)
% Number of connectives : 480 ( 183 ~; 213 |; 39 &)
% ( 42 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 45 ( 43 usr; 43 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 10 con; 0-3 aty)
% Number of variables : 41 ( 41 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X] : ~ gt(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [X] : plus(X,n3) = succ(succ(succ(X))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X] : plus(X,n4) = succ(succ(succ(succ(X)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [X] : plus(X,n5) = succ(succ(succ(succ(succ(X))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [X,U,VAL] : a_select2(tptp_update2(X,U,VAL),U) = VAL,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [I,U,X,VAL,VAL2] :
( ( a_select2(X,U) = VAL
& I != U )
=> a_select2(tptp_update2(X,I,VAL2),U) = VAL ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
( ( a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,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),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),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),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),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),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),n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ ( ( a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,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),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),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),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),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),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),n0) = use
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f55,axiom,
gt(n5,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
gt(n4,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
gt(n5,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
gt(n1,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
gt(n2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
gt(n3,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
gt(n2,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
gt(n4,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
gt(n5,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
gt(n3,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
gt(n4,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
gt(n5,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
succ(succ(succ(succ(succ(n0))))) = n5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f204,plain,
! [X0] : plus(X0,n3) = succ(succ(succ(X0))),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f206,plain,
! [X0] : plus(X0,n4) = succ(succ(succ(succ(X0)))),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f208,plain,
! [X0] : plus(X0,n5) = succ(succ(succ(succ(succ(X0))))),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f233,plain,
! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f234,plain,
! [I,U,X,VAL,VAL2] :
( a_select2(tptp_update2(X,I,VAL2),U) = VAL
| a_select2(X,U) != VAL
| I = U ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f235,plain,
! [I,U,X,VAL] :
( ! [VAL2] : a_select2(tptp_update2(X,I,VAL2),U) = VAL
| a_select2(X,U) != VAL
| I = U ),
inference(miniscoping,[status(thm)],[f234]) ).
fof(f236,plain,
! [X0,X1,X2,X3,X4] :
( a_select2(tptp_update2(X2,X0,X4),X1) = X3
| a_select2(X2,X1) != X3
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f235]) ).
fof(f244,plain,
( ( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use )
& a_select2(xinit_defuse,n5) = use
& a_select2(xinit_defuse,n4) = use
& a_select2(xinit_defuse,n3) = use
& a_select3(u_defuse,n2,n0) = use
& a_select3(u_defuse,n1,n0) = use
& a_select3(u_defuse,n0,n0) = use ),
inference(pre_NNF_transformation,[status(thm)],[f54]) ).
fof(f245,plain,
a_select3(u_defuse,n0,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f246,plain,
a_select3(u_defuse,n1,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f247,plain,
a_select3(u_defuse,n2,n0) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f248,plain,
a_select2(xinit_defuse,n3) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f249,plain,
a_select2(xinit_defuse,n4) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f250,plain,
a_select2(xinit_defuse,n5) = use,
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f251,plain,
( 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
| 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),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),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),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),n0) != use
| a_select2(xinit_defuse,n5) != use
| a_select2(xinit_defuse,n4) != use
| a_select2(xinit_defuse,n3) != use
| a_select3(u_defuse,n2,n0) != use
| a_select3(u_defuse,n1,n0) != use
| a_select3(u_defuse,n0,n0) != use ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f252,plain,
gt(n5,n4),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f259,plain,
gt(n4,n0),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f260,plain,
gt(n5,n0),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f261,plain,
gt(n1,n0),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f262,plain,
gt(n2,n0),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f263,plain,
gt(n3,n0),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f266,plain,
gt(n2,n1),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f268,plain,
gt(n4,n2),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f269,plain,
gt(n5,n2),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f270,plain,
gt(n3,n2),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f271,plain,
gt(n4,n3),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f272,plain,
gt(n5,n3),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f286,plain,
succ(succ(succ(succ(succ(n0))))) = n5,
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f326,definition,
( sQ0_spl
<=> a_select3(u_defuse,n0,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f328,plain,
( sQ0_spl
| a_select3(u_defuse,n0,n0) != use ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f329,definition,
( sQ1_spl
<=> a_select3(u_defuse,n1,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( sQ1_spl
| a_select3(u_defuse,n1,n0) != use ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,definition,
( sQ2_spl
<=> a_select3(u_defuse,n2,n0) = use ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f334,plain,
( sQ2_spl
| a_select3(u_defuse,n2,n0) != use ),
inference(component_clause,[status(thm)],[f332]) ).
fof(f335,definition,
( sQ3_spl
<=> a_select2(xinit_defuse,n3) = use ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f337,plain,
( sQ3_spl
| a_select2(xinit_defuse,n3) != use ),
inference(component_clause,[status(thm)],[f335]) ).
fof(f338,definition,
( sQ4_spl
<=> a_select2(xinit_defuse,n4) = use ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f340,plain,
( sQ4_spl
| a_select2(xinit_defuse,n4) != use ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,definition,
( sQ5_spl
<=> a_select2(xinit_defuse,n5) = use ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( sQ5_spl
| a_select2(xinit_defuse,n5) != use ),
inference(component_clause,[status(thm)],[f341]) ).
fof(f344,definition,
( 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 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f346,plain,
( 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 ),
inference(component_clause,[status(thm)],[f344]) ).
fof(f347,definition,
( 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 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f349,plain,
( 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 ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f350,definition,
( 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 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f352,plain,
( 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 ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f353,definition,
( 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 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( 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 ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f356,definition,
( 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 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f358,plain,
( 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 ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,definition,
( 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 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f361,plain,
( 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 ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f362,plain,
( ~ sQ11_spl
| ~ sQ10_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| ~ sQ6_spl
| ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f251,f326,f329,f332,f335,f338,f341,f344,f347,f350,f353,f356,f359]) ).
fof(f365,plain,
! [X0] : plus(X0,n4) = plus(succ(X0),n3),
inference(forward_demodulation,[status(thm)],[f204,f206]) ).
fof(f368,plain,
! [X0] : plus(X0,n5) = plus(succ(succ(X0)),n3),
inference(forward_demodulation,[status(thm)],[f204,f208]) ).
fof(f369,plain,
! [X0] : plus(X0,n5) = plus(succ(X0),n4),
inference(forward_demodulation,[status(thm)],[f365,f368]) ).
fof(f374,plain,
! [X0,X1,X2,X3] :
( a_select2(tptp_update2(X2,X0,X3),X1) = a_select2(X2,X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f236]) ).
fof(f377,plain,
plus(succ(succ(n0)),n3) = n5,
inference(forward_demodulation,[status(thm)],[f204,f286]) ).
fof(f378,plain,
plus(succ(n0),n4) = n5,
inference(forward_demodulation,[status(thm)],[f365,f377]) ).
fof(f379,plain,
plus(n0,n5) = n5,
inference(forward_demodulation,[status(thm)],[f369,f378]) ).
fof(f382,plain,
( sQ11_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f361]) ).
fof(f383,plain,
( sQ11_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f382]) ).
fof(f384,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f383]) ).
fof(f393,definition,
( sQ13_spl
<=> n1 = n0 ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f394,plain,
( ~ sQ13_spl
| n1 = n0 ),
inference(component_clause,[status(thm)],[f393]) ).
fof(f402,definition,
( sQ15_spl
<=> n2 = n0 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( ~ sQ15_spl
| n2 = n0 ),
inference(component_clause,[status(thm)],[f402]) ).
fof(f406,definition,
( sQ16_spl
<=> n2 = n1 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f407,plain,
( ~ sQ16_spl
| n2 = n1 ),
inference(component_clause,[status(thm)],[f406]) ).
fof(f422,definition,
( sQ19_spl
<=> n4 = n0 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f423,plain,
( ~ sQ19_spl
| n4 = n0 ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f426,definition,
( sQ20_spl
<=> n4 = n1 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f427,plain,
( ~ sQ20_spl
| n4 = n1 ),
inference(component_clause,[status(thm)],[f426]) ).
fof(f430,definition,
( sQ21_spl
<=> n4 = n2 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( ~ sQ21_spl
| n4 = n2 ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f434,definition,
( sQ22_spl
<=> n4 = n3 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( ~ sQ22_spl
| n4 = n3 ),
inference(component_clause,[status(thm)],[f434]) ).
fof(f446,definition,
( sQ24_spl
<=> n5 = n0 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f447,plain,
( ~ sQ24_spl
| n5 = n0 ),
inference(component_clause,[status(thm)],[f446]) ).
fof(f450,definition,
( sQ25_spl
<=> n5 = n1 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f451,plain,
( ~ sQ25_spl
| n5 = n1 ),
inference(component_clause,[status(thm)],[f450]) ).
fof(f454,definition,
( sQ26_spl
<=> n5 = n2 ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( ~ sQ26_spl
| n5 = n2 ),
inference(component_clause,[status(thm)],[f454]) ).
fof(f458,definition,
( sQ27_spl
<=> n5 = n3 ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f459,plain,
( ~ sQ27_spl
| n5 = n3 ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f462,definition,
( sQ28_spl
<=> n5 = n4 ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f463,plain,
( ~ sQ28_spl
| n5 = n4 ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f472,definition,
( sQ30_spl
<=> n3 = n0 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f473,plain,
( ~ sQ30_spl
| n3 = n0 ),
inference(component_clause,[status(thm)],[f472]) ).
fof(f476,definition,
( sQ31_spl
<=> n3 = n1 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( ~ sQ31_spl
| n3 = n1 ),
inference(component_clause,[status(thm)],[f476]) ).
fof(f480,definition,
( sQ32_spl
<=> n3 = n2 ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f481,plain,
( ~ sQ32_spl
| n3 = n2 ),
inference(component_clause,[status(thm)],[f480]) ).
fof(f552,plain,
( sQ10_spl
| n5 = n4
| 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 ),
inference(paramodulation,[status(thm)],[f374,f358]) ).
fof(f553,definition,
( sQ42_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 ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f555,plain,
( sQ42_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 ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,plain,
( sQ10_spl
| sQ28_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f552,f553,f462,f356]) ).
fof(f557,plain,
( sQ42_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f555]) ).
fof(f558,plain,
( sQ42_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f557]) ).
fof(f559,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f558]) ).
fof(f562,plain,
( ~ sQ28_spl
| gt(n4,n4) ),
inference(backward_demodulation,[status(thm)],[f463,f252]) ).
fof(f576,plain,
( ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f562,f91]) ).
fof(f577,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f576]) ).
fof(f578,plain,
( sQ9_spl
| n5 = n3
| 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 ),
inference(paramodulation,[status(thm)],[f374,f355]) ).
fof(f579,definition,
( sQ43_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 ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f581,plain,
( sQ43_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 ),
inference(component_clause,[status(thm)],[f579]) ).
fof(f582,plain,
( sQ9_spl
| sQ27_spl
| ~ sQ43_spl ),
inference(split_clause,[status(thm)],[f578,f579,f458,f353]) ).
fof(f587,plain,
( sQ43_spl
| n4 = n3
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3) != use ),
inference(paramodulation,[status(thm)],[f374,f581]) ).
fof(f588,definition,
( sQ44_spl
<=> a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3) = use ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f590,plain,
( sQ44_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n3) != use ),
inference(component_clause,[status(thm)],[f588]) ).
fof(f591,plain,
( sQ43_spl
| sQ22_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f587,f588,f434,f579]) ).
fof(f592,plain,
( sQ44_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f590]) ).
fof(f593,plain,
( sQ44_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f592]) ).
fof(f594,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f593]) ).
fof(f595,plain,
( sQ5_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f250,f343]) ).
fof(f596,plain,
( sQ5_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f595]) ).
fof(f597,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f596]) ).
fof(f598,plain,
( sQ4_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f249,f340]) ).
fof(f599,plain,
( sQ4_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f598]) ).
fof(f600,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f599]) ).
fof(f601,plain,
( sQ3_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f248,f337]) ).
fof(f602,plain,
( sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f601]) ).
fof(f603,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f602]) ).
fof(f604,plain,
( sQ2_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f247,f334]) ).
fof(f605,plain,
( sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f604]) ).
fof(f606,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f605]) ).
fof(f607,plain,
( sQ1_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f246,f331]) ).
fof(f608,plain,
( sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f607]) ).
fof(f609,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f608]) ).
fof(f610,plain,
( sQ0_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f245,f328]) ).
fof(f611,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f610]) ).
fof(f612,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f611]) ).
fof(f624,plain,
( ~ sQ27_spl
| gt(n3,n3) ),
inference(backward_demodulation,[status(thm)],[f459,f272]) ).
fof(f640,plain,
( ~ sQ22_spl
| gt(n3,n3) ),
inference(backward_demodulation,[status(thm)],[f435,f271]) ).
fof(f654,plain,
( ~ sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f624,f91]) ).
fof(f655,plain,
~ sQ27_spl,
inference(contradiction_clause,[status(thm)],[f654]) ).
fof(f657,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f640,f91]) ).
fof(f658,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f657]) ).
fof(f667,plain,
( sQ8_spl
| n5 = n2
| 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 ),
inference(paramodulation,[status(thm)],[f374,f352]) ).
fof(f668,definition,
( sQ45_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 ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f670,plain,
( sQ45_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 ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f671,plain,
( sQ8_spl
| sQ26_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f667,f668,f454,f350]) ).
fof(f672,plain,
( sQ45_spl
| n4 = n2
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2) != use ),
inference(paramodulation,[status(thm)],[f374,f670]) ).
fof(f673,definition,
( sQ46_spl
<=> a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2) = use ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f675,plain,
( sQ46_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n2) != use ),
inference(component_clause,[status(thm)],[f673]) ).
fof(f676,plain,
( sQ45_spl
| sQ21_spl
| ~ sQ46_spl ),
inference(split_clause,[status(thm)],[f672,f673,f430,f668]) ).
fof(f690,plain,
( ~ sQ26_spl
| gt(n2,n2) ),
inference(backward_demodulation,[status(thm)],[f455,f269]) ).
fof(f697,plain,
( ~ sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f690,f91]) ).
fof(f698,plain,
~ sQ26_spl,
inference(contradiction_clause,[status(thm)],[f697]) ).
fof(f699,plain,
( sQ46_spl
| n3 = n2
| a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n2) != use ),
inference(paramodulation,[status(thm)],[f374,f675]) ).
fof(f700,definition,
( sQ47_spl
<=> a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n2) = use ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f702,plain,
( sQ47_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n2) != use ),
inference(component_clause,[status(thm)],[f700]) ).
fof(f703,plain,
( sQ46_spl
| sQ32_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f699,f700,f480,f673]) ).
fof(f704,plain,
( sQ47_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f702]) ).
fof(f705,plain,
( sQ47_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f704]) ).
fof(f706,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f705]) ).
fof(f721,plain,
( ~ sQ21_spl
| gt(n2,n2) ),
inference(backward_demodulation,[status(thm)],[f431,f268]) ).
fof(f746,plain,
( ~ sQ32_spl
| gt(n2,n2) ),
inference(backward_demodulation,[status(thm)],[f481,f270]) ).
fof(f762,plain,
( ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f746,f91]) ).
fof(f763,plain,
~ sQ32_spl,
inference(contradiction_clause,[status(thm)],[f762]) ).
fof(f775,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f721,f91]) ).
fof(f776,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f775]) ).
fof(f844,plain,
( sQ6_spl
| n5 = n0
| 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 ),
inference(paramodulation,[status(thm)],[f374,f346]) ).
fof(f845,definition,
( sQ55_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 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f847,plain,
( sQ55_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 ),
inference(component_clause,[status(thm)],[f845]) ).
fof(f848,plain,
( sQ6_spl
| sQ24_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f844,f845,f446,f344]) ).
fof(f861,plain,
( sQ7_spl
| n5 = n1
| 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 ),
inference(paramodulation,[status(thm)],[f374,f349]) ).
fof(f862,definition,
( sQ56_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 ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ56_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 ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f865,plain,
( sQ7_spl
| sQ25_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f861,f862,f450,f347]) ).
fof(f946,plain,
( ~ sQ24_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f447,f260]) ).
fof(f977,plain,
( sQ55_spl
| n4 = n0
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0) != use ),
inference(paramodulation,[status(thm)],[f374,f847]) ).
fof(f978,definition,
( sQ69_spl
<=> a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0) = use ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f980,plain,
( sQ69_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n0) != use ),
inference(component_clause,[status(thm)],[f978]) ).
fof(f981,plain,
( sQ55_spl
| sQ19_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f977,f978,f422,f845]) ).
fof(f1006,plain,
( ~ sQ19_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f423,f259]) ).
fof(f1027,plain,
( sQ69_spl
| n3 = n0
| a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0) != use ),
inference(paramodulation,[status(thm)],[f374,f980]) ).
fof(f1028,definition,
( sQ70_spl
<=> a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0) = use ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
( sQ70_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n0) != use ),
inference(component_clause,[status(thm)],[f1028]) ).
fof(f1031,plain,
( sQ69_spl
| sQ30_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f1027,f1028,f472,f978]) ).
fof(f1032,plain,
( sQ70_spl
| n2 = n0
| a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0) != use ),
inference(paramodulation,[status(thm)],[f374,f1030]) ).
fof(f1033,definition,
( sQ71_spl
<=> a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0) = use ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1035,plain,
( sQ71_spl
| a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n0) != use ),
inference(component_clause,[status(thm)],[f1033]) ).
fof(f1036,plain,
( sQ70_spl
| sQ15_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f1032,f1033,f402,f1028]) ).
fof(f1058,plain,
( ~ sQ30_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f473,f263]) ).
fof(f1066,plain,
( sQ71_spl
| n1 = n0
| a_select2(tptp_update2(sigma_defuse,n0,use),n0) != use ),
inference(paramodulation,[status(thm)],[f374,f1035]) ).
fof(f1067,definition,
( sQ72_spl
<=> a_select2(tptp_update2(sigma_defuse,n0,use),n0) = use ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1069,plain,
( sQ72_spl
| a_select2(tptp_update2(sigma_defuse,n0,use),n0) != use ),
inference(component_clause,[status(thm)],[f1067]) ).
fof(f1070,plain,
( sQ71_spl
| sQ13_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f1066,f1067,f393,f1033]) ).
fof(f1071,plain,
( sQ72_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f1069]) ).
fof(f1072,plain,
( sQ72_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1071]) ).
fof(f1073,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f1072]) ).
fof(f1074,plain,
( ~ sQ15_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f403,f262]) ).
fof(f1100,plain,
( ~ sQ13_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f394,f261]) ).
fof(f1115,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1074,f91]) ).
fof(f1116,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1115]) ).
fof(f1117,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1100,f91]) ).
fof(f1118,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1117]) ).
fof(f1133,plain,
( ~ sQ25_spl
| plus(n0,n5) = n1 ),
inference(backward_demodulation,[status(thm)],[f451,f379]) ).
fof(f1159,plain,
( ~ sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f946,f91]) ).
fof(f1160,plain,
~ sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1159]) ).
fof(f1167,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1058,f91]) ).
fof(f1168,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1167]) ).
fof(f1188,plain,
( sQ7_spl
| ~ sQ25_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),n1,use),n1) != use ),
inference(backward_demodulation,[status(thm)],[f1192,f349]) ).
fof(f1192,plain,
( ~ sQ25_spl
| n5 = n1 ),
inference(forward_demodulation,[status(thm)],[f379,f1133]) ).
fof(f1201,plain,
( sQ7_spl
| ~ sQ25_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f1188]) ).
fof(f1202,plain,
( sQ7_spl
| ~ sQ25_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1201]) ).
fof(f1203,plain,
( sQ7_spl
| ~ sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f1202]) ).
fof(f1263,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1006,f91]) ).
fof(f1264,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1263]) ).
fof(f1287,plain,
( sQ56_spl
| n4 = n1
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1) != use ),
inference(paramodulation,[status(thm)],[f374,f864]) ).
fof(f1288,definition,
( sQ73_spl
<=> a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1) = use ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1290,plain,
( sQ73_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1) != use ),
inference(component_clause,[status(thm)],[f1288]) ).
fof(f1291,plain,
( sQ56_spl
| sQ20_spl
| ~ sQ73_spl ),
inference(split_clause,[status(thm)],[f1287,f1288,f426,f862]) ).
fof(f1292,plain,
( sQ56_spl
| ~ sQ20_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n3,use),n1,use),n1) != use ),
inference(backward_demodulation,[status(thm)],[f427,f864]) ).
fof(f1322,plain,
( sQ56_spl
| ~ sQ20_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f1292]) ).
fof(f1323,plain,
( sQ56_spl
| ~ sQ20_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1322]) ).
fof(f1324,plain,
( sQ56_spl
| ~ sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f1323]) ).
fof(f1325,plain,
( sQ73_spl
| n3 = n1
| a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1) != use ),
inference(paramodulation,[status(thm)],[f374,f1290]) ).
fof(f1326,definition,
( sQ74_spl
<=> a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1) = use ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f1328,plain,
( sQ74_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1) != use ),
inference(component_clause,[status(thm)],[f1326]) ).
fof(f1329,plain,
( sQ73_spl
| sQ31_spl
| ~ sQ74_spl ),
inference(split_clause,[status(thm)],[f1325,f1326,f476,f1288]) ).
fof(f1330,plain,
( sQ74_spl
| n2 = n1
| a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n1) != use ),
inference(paramodulation,[status(thm)],[f374,f1328]) ).
fof(f1331,definition,
( sQ75_spl
<=> a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n1) = use ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1333,plain,
( sQ75_spl
| a_select2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n1) != use ),
inference(component_clause,[status(thm)],[f1331]) ).
fof(f1334,plain,
( sQ74_spl
| sQ16_spl
| ~ sQ75_spl ),
inference(split_clause,[status(thm)],[f1330,f1331,f406,f1326]) ).
fof(f1335,plain,
( sQ75_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f1333]) ).
fof(f1336,plain,
( sQ75_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1335]) ).
fof(f1337,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f1336]) ).
fof(f1338,plain,
( sQ73_spl
| ~ sQ31_spl
| a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(sigma_defuse,n0,use),n1,use),n2,use),n1,use),n1) != use ),
inference(backward_demodulation,[status(thm)],[f477,f1290]) ).
fof(f1375,plain,
( ~ sQ16_spl
| gt(n1,n1) ),
inference(backward_demodulation,[status(thm)],[f407,f266]) ).
fof(f1382,plain,
( sQ73_spl
| ~ sQ31_spl
| use != use ),
inference(forward_demodulation,[status(thm)],[f233,f1338]) ).
fof(f1383,plain,
( sQ73_spl
| ~ sQ31_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1382]) ).
fof(f1384,plain,
( sQ73_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f1383]) ).
fof(f1385,plain,
( ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1375,f91]) ).
fof(f1386,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1385]) ).
fof(f1387,plain,
$false,
inference(sat_refutation,[status(thm)],[f362,f384,f556,f559,f577,f582,f591,f594,f597,f600,f603,f606,f609,f612,f655,f658,f671,f676,f698,f703,f706,f763,f776,f848,f865,f981,f1031,f1036,f1070,f1073,f1116,f1118,f1160,f1168,f1203,f1264,f1291,f1324,f1329,f1334,f1337,f1384,f1386]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV103+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:30:50 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.59 % Refutation found
% 0.13/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.43/0.62 % Elapsed time: 0.245952 seconds
% 1.43/0.62 % CPU time: 1.671762 seconds
% 1.43/0.62 % Total memory used: 131.148 MB
% 1.43/0.62 % Net memory used: 128.305 MB
%------------------------------------------------------------------------------