%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV102+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 : n006.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 0.20s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV102+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n006.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 08:30:58 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.50 % Drodi V4.1.1
% 0.20/0.53 % Refutation found
% 0.20/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.20/0.53 fof(f3,axiom,(
% 0.20/0.53 (! [X] : ~ gt(X,X) )),
% 0.20/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.53 fof(f48,axiom,(
% 0.20/0.53 (! [X,U,VAL] : a_select2(tptp_update2(X,U,VAL),U) = VAL )),
% 0.20/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.53 fof(f49,axiom,(
% 0.20/0.53 (! [I,U,X,VAL,VAL2] :( ( I != U& a_select2(X,U) = VAL )=> a_select2(tptp_update2(X,I,VAL2),U) = VAL ) )),
% 0.20/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.53 fof(f53,conjecture,(
% 0.20/0.53 ( ( a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_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(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_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(rho_defuse,n0,use),n1,use),n2,use),n0) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n1) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n2) = use ) ) ),
% 0.20/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.53 fof(f54,negated_conjecture,(
% 0.20/0.53 ~(( ( a_select2(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_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(sigma_defuse,n0) = use& a_select2(sigma_defuse,n1) = use& a_select2(sigma_defuse,n2) = use& a_select2(sigma_defuse,n3) = use& a_select2(sigma_defuse,n4) = use& a_select2(sigma_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(rho_defuse,n0,use),n1,use),n2,use),n0) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n1) = use& a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n2) = use ) ) )),
% 0.20/0.53 inference(negated_conjecture,[status(cth)],[f53])).
% 0.20/0.53 fof(f65,axiom,(
% 0.20/0.53 gt(n2,n0) ),
% 0.20/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.53 fof(f69,axiom,(
% 0.20/0.53 gt(n2,n1) ),
% 0.20/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.53 fof(f91,plain,(
% 0.20/0.53 ![X0]: (~gt(X0,X0))),
% 0.20/0.53 inference(cnf_transformation,[status(thm)],[f3])).
% 0.20/0.53 fof(f233,plain,(
% 0.20/0.53 ![X0,X1,X2]: (a_select2(tptp_update2(X0,X1,X2),X1)=X2)),
% 0.20/0.53 inference(cnf_transformation,[status(thm)],[f48])).
% 0.20/0.53 fof(f234,plain,(
% 0.20/0.53 ![I,U,X,VAL,VAL2]: ((I=U|~a_select2(X,U)=VAL)|a_select2(tptp_update2(X,I,VAL2),U)=VAL)),
% 0.20/0.53 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.20/0.53 fof(f235,plain,(
% 0.20/0.53 ![I,U,X,VAL]: ((I=U|~a_select2(X,U)=VAL)|(![VAL2]: a_select2(tptp_update2(X,I,VAL2),U)=VAL))),
% 0.20/0.53 inference(miniscoping,[status(thm)],[f234])).
% 0.20/0.53 fof(f236,plain,(
% 0.20/0.53 ![X0,X1,X2,X3,X4]: (X0=X1|~a_select2(X2,X1)=X3|a_select2(tptp_update2(X2,X0,X4),X1)=X3)),
% 0.20/0.53 inference(cnf_transformation,[status(thm)],[f235])).
% 0.20/0.53 fof(f244,plain,(
% 0.20/0.53 ((((((((((((a_select2(sigma_defuse,n0)=use&a_select2(sigma_defuse,n1)=use)&a_select2(sigma_defuse,n2)=use)&a_select2(sigma_defuse,n3)=use)&a_select2(sigma_defuse,n4)=use)&a_select2(sigma_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(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use)|~a_select2(sigma_defuse,n2)=use)|~a_select2(sigma_defuse,n3)=use)|~a_select2(sigma_defuse,n4)=use)|~a_select2(sigma_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(rho_defuse,n0,use),n1,use),n2,use),n0)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n1)=use)|~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n2)=use))),
% 0.20/0.54 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.20/0.54 fof(f245,plain,(
% 0.20/0.54 a_select2(sigma_defuse,n0)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f246,plain,(
% 0.20/0.54 a_select2(sigma_defuse,n1)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f247,plain,(
% 0.20/0.54 a_select2(sigma_defuse,n2)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f248,plain,(
% 0.20/0.54 a_select2(sigma_defuse,n3)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f249,plain,(
% 0.20/0.54 a_select2(sigma_defuse,n4)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f250,plain,(
% 0.20/0.54 a_select2(sigma_defuse,n5)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f251,plain,(
% 0.20/0.54 a_select3(u_defuse,n0,n0)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f252,plain,(
% 0.20/0.54 a_select3(u_defuse,n1,n0)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f253,plain,(
% 0.20/0.54 a_select3(u_defuse,n2,n0)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f254,plain,(
% 0.20/0.54 a_select2(xinit_defuse,n3)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f255,plain,(
% 0.20/0.54 a_select2(xinit_defuse,n4)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f256,plain,(
% 0.20/0.54 a_select2(xinit_defuse,n5)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f257,plain,(
% 0.20/0.54 ~a_select2(sigma_defuse,n0)=use|~a_select2(sigma_defuse,n1)=use|~a_select2(sigma_defuse,n2)=use|~a_select2(sigma_defuse,n3)=use|~a_select2(sigma_defuse,n4)=use|~a_select2(sigma_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(rho_defuse,n0,use),n1,use),n2,use),n0)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n1)=use|~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n2)=use),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f244])).
% 0.20/0.54 fof(f268,plain,(
% 0.20/0.54 gt(n2,n0)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f65])).
% 0.20/0.54 fof(f272,plain,(
% 0.20/0.54 gt(n2,n1)),
% 0.20/0.54 inference(cnf_transformation,[status(thm)],[f69])).
% 0.20/0.54 fof(f332,definition,(
% 0.20/0.54 sQ0_spl <=> (a_select2(sigma_defuse,n0)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f334,plain,(
% 0.20/0.54 ~a_select2(sigma_defuse,n0)=use|sQ0_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f332])).
% 0.20/0.54 fof(f335,definition,(
% 0.20/0.54 sQ1_spl <=> (a_select2(sigma_defuse,n1)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f337,plain,(
% 0.20/0.54 ~a_select2(sigma_defuse,n1)=use|sQ1_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f335])).
% 0.20/0.54 fof(f338,definition,(
% 0.20/0.54 sQ2_spl <=> (a_select2(sigma_defuse,n2)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f340,plain,(
% 0.20/0.54 ~a_select2(sigma_defuse,n2)=use|sQ2_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f338])).
% 0.20/0.54 fof(f341,definition,(
% 0.20/0.54 sQ3_spl <=> (a_select2(sigma_defuse,n3)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f343,plain,(
% 0.20/0.54 ~a_select2(sigma_defuse,n3)=use|sQ3_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f341])).
% 0.20/0.54 fof(f344,definition,(
% 0.20/0.54 sQ4_spl <=> (a_select2(sigma_defuse,n4)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f346,plain,(
% 0.20/0.54 ~a_select2(sigma_defuse,n4)=use|sQ4_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f344])).
% 0.20/0.54 fof(f347,definition,(
% 0.20/0.54 sQ5_spl <=> (a_select2(sigma_defuse,n5)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f349,plain,(
% 0.20/0.54 ~a_select2(sigma_defuse,n5)=use|sQ5_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f347])).
% 0.20/0.54 fof(f350,definition,(
% 0.20/0.54 sQ6_spl <=> (a_select3(u_defuse,n0,n0)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f352,plain,(
% 0.20/0.54 ~a_select3(u_defuse,n0,n0)=use|sQ6_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f350])).
% 0.20/0.54 fof(f353,definition,(
% 0.20/0.54 sQ7_spl <=> (a_select3(u_defuse,n1,n0)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f355,plain,(
% 0.20/0.54 ~a_select3(u_defuse,n1,n0)=use|sQ7_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f353])).
% 0.20/0.54 fof(f356,definition,(
% 0.20/0.54 sQ8_spl <=> (a_select3(u_defuse,n2,n0)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f358,plain,(
% 0.20/0.54 ~a_select3(u_defuse,n2,n0)=use|sQ8_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f356])).
% 0.20/0.54 fof(f359,definition,(
% 0.20/0.54 sQ9_spl <=> (a_select2(xinit_defuse,n3)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f361,plain,(
% 0.20/0.54 ~a_select2(xinit_defuse,n3)=use|sQ9_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f359])).
% 0.20/0.54 fof(f362,definition,(
% 0.20/0.54 sQ10_spl <=> (a_select2(xinit_defuse,n4)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f364,plain,(
% 0.20/0.54 ~a_select2(xinit_defuse,n4)=use|sQ10_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f362])).
% 0.20/0.54 fof(f365,definition,(
% 0.20/0.54 sQ11_spl <=> (a_select2(xinit_defuse,n5)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f367,plain,(
% 0.20/0.54 ~a_select2(xinit_defuse,n5)=use|sQ11_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f365])).
% 0.20/0.54 fof(f368,definition,(
% 0.20/0.54 sQ12_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n0)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f370,plain,(
% 0.20/0.54 ~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n0)=use|sQ12_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f368])).
% 0.20/0.54 fof(f371,definition,(
% 0.20/0.54 sQ13_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n1)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f373,plain,(
% 0.20/0.54 ~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n1)=use|sQ13_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f371])).
% 0.20/0.54 fof(f374,definition,(
% 0.20/0.54 sQ14_spl <=> (a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n2)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f376,plain,(
% 0.20/0.54 ~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n2)=use|sQ14_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f374])).
% 0.20/0.54 fof(f377,plain,(
% 0.20/0.54 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl),
% 0.20/0.54 inference(split_clause,[status(thm)],[f257,f332,f335,f338,f341,f344,f347,f350,f353,f356,f359,f362,f365,f368,f371,f374])).
% 0.20/0.54 fof(f379,plain,(
% 0.20/0.54 ![X0,X1,X2,X3]: (X0=X1|a_select2(tptp_update2(X2,X0,X3),X1)=a_select2(X2,X1))),
% 0.20/0.54 inference(destructive_equality_resolution,[status(thm)],[f236])).
% 0.20/0.54 fof(f442,definition,(
% 0.20/0.54 sQ17_spl <=> (n0=n1)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f443,plain,(
% 0.20/0.54 n0=n1|~sQ17_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f442])).
% 0.20/0.54 fof(f445,definition,(
% 0.20/0.54 sQ18_spl <=> (n0=n2)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f446,plain,(
% 0.20/0.54 n0=n2|~sQ18_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f445])).
% 0.20/0.54 fof(f529,plain,(
% 0.20/0.54 ~use=use|sQ14_spl),
% 0.20/0.54 inference(forward_demodulation,[status(thm)],[f233,f376])).
% 0.20/0.54 fof(f530,plain,(
% 0.20/0.54 $false|sQ14_spl),
% 0.20/0.54 inference(trivial_equality_resolution,[status(thm)],[f529])).
% 0.20/0.54 fof(f531,plain,(
% 0.20/0.54 sQ14_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f530])).
% 0.20/0.54 fof(f626,plain,(
% 0.20/0.54 ~a_select2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n1)=use|n2=n1|sQ13_spl),
% 0.20/0.54 inference(paramodulation,[status(thm)],[f379,f373])).
% 0.20/0.54 fof(f627,definition,(
% 0.20/0.54 sQ25_spl <=> (a_select2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n1)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f629,plain,(
% 0.20/0.54 ~a_select2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n1)=use|sQ25_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f627])).
% 0.20/0.54 fof(f630,definition,(
% 0.20/0.54 sQ26_spl <=> (n2=n1)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f631,plain,(
% 0.20/0.54 n2=n1|~sQ26_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f630])).
% 0.20/0.54 fof(f633,plain,(
% 0.20/0.54 ~sQ25_spl|sQ26_spl|sQ13_spl),
% 0.20/0.54 inference(split_clause,[status(thm)],[f626,f627,f630,f371])).
% 0.20/0.54 fof(f634,plain,(
% 0.20/0.54 ~use=use|sQ25_spl),
% 0.20/0.54 inference(forward_demodulation,[status(thm)],[f233,f629])).
% 0.20/0.54 fof(f635,plain,(
% 0.20/0.54 $false|sQ25_spl),
% 0.20/0.54 inference(trivial_equality_resolution,[status(thm)],[f634])).
% 0.20/0.54 fof(f636,plain,(
% 0.20/0.54 sQ25_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f635])).
% 0.20/0.54 fof(f641,plain,(
% 0.20/0.54 gt(n2,n2)|~sQ26_spl),
% 0.20/0.54 inference(backward_demodulation,[status(thm)],[f631,f272])).
% 0.20/0.54 fof(f651,plain,(
% 0.20/0.54 $false|~sQ26_spl),
% 0.20/0.54 inference(forward_subsumption_resolution,[status(thm)],[f641,f91])).
% 0.20/0.54 fof(f652,plain,(
% 0.20/0.54 ~sQ26_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f651])).
% 0.20/0.54 fof(f653,plain,(
% 0.20/0.54 ~a_select2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n0)=use|n2=n0|sQ12_spl),
% 0.20/0.54 inference(paramodulation,[status(thm)],[f379,f370])).
% 0.20/0.54 fof(f654,definition,(
% 0.20/0.54 sQ27_spl <=> (a_select2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n0)=use)),
% 0.20/0.54 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.20/0.54 fof(f656,plain,(
% 0.20/0.54 ~a_select2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n0)=use|sQ27_spl),
% 0.20/0.54 inference(component_clause,[status(thm)],[f654])).
% 0.20/0.54 fof(f657,plain,(
% 0.20/0.54 ~sQ27_spl|sQ18_spl|sQ12_spl),
% 0.20/0.54 inference(split_clause,[status(thm)],[f653,f654,f445,f368])).
% 0.20/0.54 fof(f658,plain,(
% 0.20/0.54 ~use=use|sQ11_spl),
% 0.20/0.54 inference(forward_demodulation,[status(thm)],[f256,f367])).
% 0.20/0.54 fof(f659,plain,(
% 0.20/0.54 $false|sQ11_spl),
% 0.20/0.54 inference(trivial_equality_resolution,[status(thm)],[f658])).
% 0.20/0.54 fof(f660,plain,(
% 0.20/0.54 sQ11_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f659])).
% 0.20/0.54 fof(f661,plain,(
% 0.20/0.54 ~use=use|sQ10_spl),
% 0.20/0.54 inference(forward_demodulation,[status(thm)],[f255,f364])).
% 0.20/0.54 fof(f662,plain,(
% 0.20/0.54 $false|sQ10_spl),
% 0.20/0.54 inference(trivial_equality_resolution,[status(thm)],[f661])).
% 0.20/0.54 fof(f663,plain,(
% 0.20/0.54 sQ10_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f662])).
% 0.20/0.54 fof(f664,plain,(
% 0.20/0.54 ~use=use|sQ9_spl),
% 0.20/0.54 inference(forward_demodulation,[status(thm)],[f254,f361])).
% 0.20/0.54 fof(f665,plain,(
% 0.20/0.54 $false|sQ9_spl),
% 0.20/0.54 inference(trivial_equality_resolution,[status(thm)],[f664])).
% 0.20/0.54 fof(f666,plain,(
% 0.20/0.54 sQ9_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f665])).
% 0.20/0.54 fof(f667,plain,(
% 0.20/0.54 ~use=use|sQ8_spl),
% 0.20/0.54 inference(forward_demodulation,[status(thm)],[f253,f358])).
% 0.20/0.54 fof(f668,plain,(
% 0.20/0.54 $false|sQ8_spl),
% 0.20/0.54 inference(trivial_equality_resolution,[status(thm)],[f667])).
% 0.20/0.54 fof(f669,plain,(
% 0.20/0.54 sQ8_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f668])).
% 0.20/0.54 fof(f751,plain,(
% 0.20/0.54 ~use=use|sQ7_spl),
% 0.20/0.54 inference(forward_demodulation,[status(thm)],[f252,f355])).
% 0.20/0.54 fof(f752,plain,(
% 0.20/0.54 $false|sQ7_spl),
% 0.20/0.54 inference(trivial_equality_resolution,[status(thm)],[f751])).
% 0.20/0.54 fof(f753,plain,(
% 0.20/0.54 sQ7_spl),
% 0.20/0.54 inference(contradiction_clause,[status(thm)],[f752])).
% 0.20/0.55 fof(f754,plain,(
% 0.20/0.55 ~use=use|sQ6_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f251,f352])).
% 0.20/0.55 fof(f755,plain,(
% 0.20/0.55 $false|sQ6_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f754])).
% 0.20/0.55 fof(f756,plain,(
% 0.20/0.55 sQ6_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f755])).
% 0.20/0.55 fof(f757,plain,(
% 0.20/0.55 ~use=use|sQ5_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f250,f349])).
% 0.20/0.55 fof(f758,plain,(
% 0.20/0.55 $false|sQ5_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f757])).
% 0.20/0.55 fof(f759,plain,(
% 0.20/0.55 sQ5_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f758])).
% 0.20/0.55 fof(f760,plain,(
% 0.20/0.55 ~use=use|sQ4_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f249,f346])).
% 0.20/0.55 fof(f761,plain,(
% 0.20/0.55 $false|sQ4_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f760])).
% 0.20/0.55 fof(f762,plain,(
% 0.20/0.55 sQ4_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f761])).
% 0.20/0.55 fof(f763,plain,(
% 0.20/0.55 ~use=use|sQ3_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f248,f343])).
% 0.20/0.55 fof(f764,plain,(
% 0.20/0.55 $false|sQ3_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f763])).
% 0.20/0.55 fof(f765,plain,(
% 0.20/0.55 sQ3_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f764])).
% 0.20/0.55 fof(f766,plain,(
% 0.20/0.55 ~use=use|sQ2_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f247,f340])).
% 0.20/0.55 fof(f767,plain,(
% 0.20/0.55 $false|sQ2_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f766])).
% 0.20/0.55 fof(f768,plain,(
% 0.20/0.55 sQ2_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f767])).
% 0.20/0.55 fof(f769,plain,(
% 0.20/0.55 ~use=use|sQ1_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f246,f337])).
% 0.20/0.55 fof(f770,plain,(
% 0.20/0.55 $false|sQ1_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f769])).
% 0.20/0.55 fof(f771,plain,(
% 0.20/0.55 sQ1_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f770])).
% 0.20/0.55 fof(f772,plain,(
% 0.20/0.55 ~use=use|sQ0_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f245,f334])).
% 0.20/0.55 fof(f773,plain,(
% 0.20/0.55 $false|sQ0_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f772])).
% 0.20/0.55 fof(f774,plain,(
% 0.20/0.55 sQ0_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f773])).
% 0.20/0.55 fof(f800,plain,(
% 0.20/0.55 gt(n2,n2)|~sQ18_spl),
% 0.20/0.55 inference(backward_demodulation,[status(thm)],[f446,f268])).
% 0.20/0.55 fof(f816,plain,(
% 0.20/0.55 $false|~sQ18_spl),
% 0.20/0.55 inference(forward_subsumption_resolution,[status(thm)],[f800,f91])).
% 0.20/0.55 fof(f817,plain,(
% 0.20/0.55 ~sQ18_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f816])).
% 0.20/0.55 fof(f871,plain,(
% 0.20/0.55 ~a_select2(tptp_update2(tptp_update2(tptp_update2(rho_defuse,n0,use),n1,use),n2,use),n1)=use|~sQ17_spl|sQ12_spl),
% 0.20/0.55 inference(backward_demodulation,[status(thm)],[f443,f370])).
% 0.20/0.55 fof(f874,plain,(
% 0.20/0.55 ~sQ13_spl|~sQ17_spl|sQ12_spl),
% 0.20/0.55 inference(split_clause,[status(thm)],[f871,f371,f442,f368])).
% 0.20/0.55 fof(f934,plain,(
% 0.20/0.55 ~a_select2(tptp_update2(rho_defuse,n0,use),n0)=use|n1=n0|sQ27_spl),
% 0.20/0.55 inference(paramodulation,[status(thm)],[f379,f656])).
% 0.20/0.55 fof(f935,definition,(
% 0.20/0.55 sQ36_spl <=> (a_select2(tptp_update2(rho_defuse,n0,use),n0)=use)),
% 0.20/0.55 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.20/0.55 fof(f937,plain,(
% 0.20/0.55 ~a_select2(tptp_update2(rho_defuse,n0,use),n0)=use|sQ36_spl),
% 0.20/0.55 inference(component_clause,[status(thm)],[f935])).
% 0.20/0.55 fof(f938,plain,(
% 0.20/0.55 ~sQ36_spl|sQ17_spl|sQ27_spl),
% 0.20/0.55 inference(split_clause,[status(thm)],[f934,f935,f442,f654])).
% 0.20/0.55 fof(f939,plain,(
% 0.20/0.55 ~use=use|sQ36_spl),
% 0.20/0.55 inference(forward_demodulation,[status(thm)],[f233,f937])).
% 0.20/0.55 fof(f940,plain,(
% 0.20/0.55 $false|sQ36_spl),
% 0.20/0.55 inference(trivial_equality_resolution,[status(thm)],[f939])).
% 0.20/0.55 fof(f941,plain,(
% 0.20/0.55 sQ36_spl),
% 0.20/0.55 inference(contradiction_clause,[status(thm)],[f940])).
% 0.20/0.55 fof(f942,plain,(
% 0.20/0.55 $false),
% 0.20/0.55 inference(sat_refutation,[status(thm)],[f377,f531,f633,f636,f652,f657,f660,f663,f666,f669,f753,f756,f759,f762,f765,f768,f771,f774,f817,f874,f938,f941])).
% 0.20/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/0.58 % Elapsed time: 0.101913 seconds
% 0.20/0.58 % CPU time: 0.197234 seconds
% 0.20/0.58 % Total memory used: 48.489 MB
% 0.20/0.58 % Net memory used: 48.348 MB
%------------------------------------------------------------------------------