%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV204+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:14 PM UTC 2026
% Result : Theorem 0.07s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV204+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 08:34:22 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.07/0.45 % Refutation found
% 0.07/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.07/0.45 fof(f3,axiom,(
% 0.07/0.45 (! [X] : ~ gt(X,X) )),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f4,axiom,(
% 0.07/0.45 (! [X] : leq(X,X) )),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f8,axiom,(
% 0.07/0.45 (! [X,Y] :( gt(Y,X)=> leq(X,Y) ) )),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f9,axiom,(
% 0.07/0.45 (! [X,Y] :( ( leq(X,Y)& X != Y )=> gt(Y,X) ) )),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f53,conjecture,(
% 0.07/0.45 ( ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = 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(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n2)& leq(B,n998) )=> a_select3(u_defuse,A,B) = use ))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,n2)& leq(D,n998) )=> a_select3(z_defuse,C,D) = use ) ))=> (! [E] :( ( leq(n0,E)& leq(E,n2) )=> a_select2(rho_defuse,E) = use ) )) ),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f54,negated_conjecture,(
% 0.07/0.45 ~(( ( a_select2(rho_defuse,n0) = use& a_select2(rho_defuse,n1) = use& a_select2(rho_defuse,n2) = 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(xinit_mean_defuse,n0) = use& a_select2(xinit_mean_defuse,n1) = use& a_select2(xinit_mean_defuse,n2) = use& a_select2(xinit_mean_defuse,n3) = use& a_select2(xinit_mean_defuse,n4) = use& a_select2(xinit_mean_defuse,n5) = use& a_select2(xinit_noise_defuse,n0) = use& a_select2(xinit_noise_defuse,n1) = use& a_select2(xinit_noise_defuse,n2) = use& a_select2(xinit_noise_defuse,n3) = use& a_select2(xinit_noise_defuse,n4) = use& a_select2(xinit_noise_defuse,n5) = use& (! [A,B] :( ( leq(n0,A)& leq(n0,B)& leq(A,n2)& leq(B,n998) )=> a_select3(u_defuse,A,B) = use ))& (! [C,D] :( ( leq(n0,C)& leq(n0,D)& leq(C,n2)& leq(D,n998) )=> a_select3(z_defuse,C,D) = use ) ))=> (! [E] :( ( leq(n0,E)& leq(E,n2) )=> a_select2(rho_defuse,E) = use ) )) )),
% 0.07/0.45 inference(negated_conjecture,[status(cth)],[f53])).
% 0.07/0.45 fof(f60,axiom,(
% 0.07/0.45 gt(n998,tptp_minus_1) ),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f65,axiom,(
% 0.07/0.45 gt(n4,n0) ),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f68,axiom,(
% 0.07/0.45 gt(n1,n0) ),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f69,axiom,(
% 0.07/0.45 gt(n2,n0) ),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f71,axiom,(
% 0.07/0.45 gt(n4,n1) ),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f81,axiom,(
% 0.07/0.45 gt(n5,n3) ),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f87,axiom,(
% 0.07/0.45 (! [X] :( ( leq(n0,X)& leq(X,n2) )=> ( X = n0| X = n1| X = n2 ) ) )),
% 0.07/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/0.45 fof(f98,plain,(
% 0.07/0.45 ![X0]: (~gt(X0,X0))),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.07/0.45 fof(f99,plain,(
% 0.07/0.45 ![X0]: (leq(X0,X0))),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.07/0.45 fof(f111,plain,(
% 0.07/0.45 ![X,Y]: (~gt(Y,X)|leq(X,Y))),
% 0.07/0.45 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.07/0.45 fof(f112,plain,(
% 0.07/0.45 ![X0,X1]: (~gt(X0,X1)|leq(X1,X0))),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f111])).
% 0.07/0.45 fof(f113,plain,(
% 0.07/0.45 ![X,Y]: ((~leq(X,Y)|X=Y)|gt(Y,X))),
% 0.07/0.45 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.07/0.45 fof(f114,plain,(
% 0.07/0.45 ![X0,X1]: (~leq(X0,X1)|X0=X1|gt(X1,X0))),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f113])).
% 0.07/0.45 fof(f251,plain,(
% 0.07/0.45 (((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=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(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n2))|~leq(B,n998))|a_select3(u_defuse,A,B)=use)))&(![C,D]: ((((~leq(n0,C)|~leq(n0,D))|~leq(C,n2))|~leq(D,n998))|a_select3(z_defuse,C,D)=use)))&(?[E]: ((leq(n0,E)&leq(E,n2))&~a_select2(rho_defuse,E)=use)))),
% 0.07/0.45 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.07/0.45 fof(f252,plain,(
% 0.07/0.45 ((((((((((((((((((((((((((((a_select2(rho_defuse,n0)=use&a_select2(rho_defuse,n1)=use)&a_select2(rho_defuse,n2)=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(xinit_mean_defuse,n0)=use)&a_select2(xinit_mean_defuse,n1)=use)&a_select2(xinit_mean_defuse,n2)=use)&a_select2(xinit_mean_defuse,n3)=use)&a_select2(xinit_mean_defuse,n4)=use)&a_select2(xinit_mean_defuse,n5)=use)&a_select2(xinit_noise_defuse,n0)=use)&a_select2(xinit_noise_defuse,n1)=use)&a_select2(xinit_noise_defuse,n2)=use)&a_select2(xinit_noise_defuse,n3)=use)&a_select2(xinit_noise_defuse,n4)=use)&a_select2(xinit_noise_defuse,n5)=use)&(![A,B]: ((((~leq(n0,A)|~leq(n0,B))|~leq(A,n2))|~leq(B,n998))|a_select3(u_defuse,A,B)=use)))&(![C,D]: ((((~leq(n0,C)|~leq(n0,D))|~leq(C,n2))|~leq(D,n998))|a_select3(z_defuse,C,D)=use)))&((leq(n0,sK23_skl)&leq(sK23_skl,n2))&~a_select2(rho_defuse,sK23_skl)=use)),
% 0.07/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(E,sK23_skl)],[f251])).
% 0.07/0.45 fof(f253,plain,(
% 0.07/0.45 a_select2(rho_defuse,n0)=use),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f252])).
% 0.07/0.45 fof(f254,plain,(
% 0.07/0.45 a_select2(rho_defuse,n1)=use),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f252])).
% 0.07/0.45 fof(f255,plain,(
% 0.07/0.45 a_select2(rho_defuse,n2)=use),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f252])).
% 0.07/0.45 fof(f282,plain,(
% 0.07/0.45 leq(n0,sK23_skl)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f252])).
% 0.07/0.45 fof(f283,plain,(
% 0.07/0.45 leq(sK23_skl,n2)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f252])).
% 0.07/0.45 fof(f284,plain,(
% 0.07/0.45 ~a_select2(rho_defuse,sK23_skl)=use),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f252])).
% 0.07/0.45 fof(f290,plain,(
% 0.07/0.45 gt(n998,tptp_minus_1)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f60])).
% 0.07/0.45 fof(f295,plain,(
% 0.07/0.45 gt(n4,n0)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f65])).
% 0.07/0.45 fof(f298,plain,(
% 0.07/0.45 gt(n1,n0)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f68])).
% 0.07/0.45 fof(f299,plain,(
% 0.07/0.45 gt(n2,n0)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f69])).
% 0.07/0.45 fof(f301,plain,(
% 0.07/0.45 gt(n4,n1)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f71])).
% 0.07/0.45 fof(f311,plain,(
% 0.07/0.45 gt(n5,n3)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f81])).
% 0.07/0.45 fof(f321,plain,(
% 0.07/0.45 ![X]: ((~leq(n0,X)|~leq(X,n2))|((X=n0|X=n1)|X=n2))),
% 0.07/0.45 inference(pre_NNF_transformation,[status(thm)],[f87])).
% 0.07/0.45 fof(f322,plain,(
% 0.07/0.45 ![X0]: (~leq(n0,X0)|~leq(X0,n2)|X0=n0|X0=n1|X0=n2)),
% 0.07/0.45 inference(cnf_transformation,[status(thm)],[f321])).
% 0.07/0.45 fof(f414,plain,(
% 0.07/0.45 sK23_skl=n2|gt(n2,sK23_skl)),
% 0.07/0.45 inference(resolution,[status(thm)],[f114,f283])).
% 0.07/0.45 fof(f417,definition,(
% 0.07/0.45 sQ0_spl <=> (sK23_skl=n2)),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f418,plain,(
% 0.07/0.45 sK23_skl=n2|~sQ0_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f417])).
% 0.07/0.45 fof(f420,definition,(
% 0.07/0.45 sQ1_spl <=> (gt(n2,sK23_skl))),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f421,plain,(
% 0.07/0.45 gt(n2,sK23_skl)|~sQ1_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f420])).
% 0.07/0.45 fof(f423,plain,(
% 0.07/0.45 sQ0_spl|sQ1_spl),
% 0.07/0.45 inference(split_clause,[status(thm)],[f414,f417,f420])).
% 0.07/0.45 fof(f424,definition,(
% 0.07/0.45 sQ2_spl <=> (n0=sK23_skl)),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f425,plain,(
% 0.07/0.45 n0=sK23_skl|~sQ2_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f424])).
% 0.07/0.45 fof(f435,plain,(
% 0.07/0.45 a_select2(rho_defuse,sK23_skl)=use|~sQ2_spl),
% 0.07/0.45 inference(backward_demodulation,[status(thm)],[f425,f253])).
% 0.07/0.45 fof(f441,plain,(
% 0.07/0.45 a_select2(rho_defuse,sK23_skl)=use|~sQ0_spl),
% 0.07/0.45 inference(backward_demodulation,[status(thm)],[f418,f255])).
% 0.07/0.45 fof(f564,plain,(
% 0.07/0.45 leq(sK23_skl,n2)|~sQ1_spl),
% 0.07/0.45 inference(resolution,[status(thm)],[f421,f112])).
% 0.07/0.45 fof(f636,definition,(
% 0.07/0.45 sQ5_spl <=> (leq(sK23_skl,n2))),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f638,plain,(
% 0.07/0.45 ~leq(sK23_skl,n2)|sQ5_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f636])).
% 0.07/0.45 fof(f711,definition,(
% 0.07/0.45 sQ13_spl <=> (sK23_skl=n1)),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f712,plain,(
% 0.07/0.45 sK23_skl=n1|~sQ13_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f711])).
% 0.07/0.45 fof(f727,definition,(
% 0.07/0.45 sQ18_spl <=> (n0=n1)),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f728,plain,(
% 0.07/0.45 n0=n1|~sQ18_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f727])).
% 0.07/0.45 fof(f730,definition,(
% 0.07/0.45 sQ19_spl <=> (n0=n2)),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f731,plain,(
% 0.07/0.45 n0=n2|~sQ19_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f730])).
% 0.07/0.45 fof(f736,definition,(
% 0.07/0.45 sQ21_spl <=> (n0=n4)),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f737,plain,(
% 0.07/0.45 n0=n4|~sQ21_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f736])).
% 0.07/0.45 fof(f740,plain,(
% 0.07/0.45 $false|~sQ2_spl),
% 0.07/0.45 inference(forward_subsumption_resolution,[status(thm)],[f435,f284])).
% 0.07/0.45 fof(f741,plain,(
% 0.07/0.45 ~sQ2_spl),
% 0.07/0.45 inference(contradiction_clause,[status(thm)],[f740])).
% 0.07/0.45 fof(f742,plain,(
% 0.07/0.45 $false|~sQ0_spl),
% 0.07/0.45 inference(forward_subsumption_resolution,[status(thm)],[f441,f284])).
% 0.07/0.45 fof(f743,plain,(
% 0.07/0.45 ~sQ0_spl),
% 0.07/0.45 inference(contradiction_clause,[status(thm)],[f742])).
% 0.07/0.45 fof(f810,definition,(
% 0.07/0.45 sQ27_spl <=> (leq(n0,n0))),
% 0.07/0.45 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.07/0.45 fof(f812,plain,(
% 0.07/0.45 ~leq(n0,n0)|sQ27_spl),
% 0.07/0.45 inference(component_clause,[status(thm)],[f810])).
% 0.07/0.45 fof(f841,plain,(
% 0.07/0.45 a_select2(rho_defuse,sK23_skl)=use|~sQ13_spl),
% 0.07/0.45 inference(backward_demodulation,[status(thm)],[f712,f254])).
% 0.07/0.45 fof(f843,plain,(
% 0.07/0.45 $false|~sQ13_spl),
% 0.07/0.45 inference(forward_subsumption_resolution,[status(thm)],[f841,f284])).
% 0.07/0.45 fof(f844,plain,(
% 0.07/0.45 ~sQ13_spl),
% 0.07/0.45 inference(contradiction_clause,[status(thm)],[f843])).
% 0.07/0.45 fof(f846,plain,(
% 0.07/0.45 ~leq(sK23_skl,n2)|sK23_skl=n0|sK23_skl=n1|sK23_skl=n2),
% 0.07/0.45 inference(resolution,[status(thm)],[f322,f282])).
% 0.07/0.45 fof(f848,plain,(
% 0.07/0.45 ~sQ5_spl|sQ2_spl|sQ13_spl|sQ0_spl),
% 0.07/0.45 inference(split_clause,[status(thm)],[f846,f636,f424,f711,f417])).
% 0.07/0.45 fof(f854,definition,(
% 0.07/0.45 sQ30_spl <=> (leq(sK23_skl,sK23_skl))),
% 0.07/0.46 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.07/0.46 fof(f856,plain,(
% 0.07/0.46 ~leq(sK23_skl,sK23_skl)|sQ30_spl),
% 0.07/0.46 inference(component_clause,[status(thm)],[f854])).
% 0.07/0.46 fof(f861,definition,(
% 0.07/0.46 sQ32_spl <=> (leq(n0,sK23_skl))),
% 0.07/0.46 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.07/0.46 fof(f863,plain,(
% 0.07/0.46 ~leq(n0,sK23_skl)|sQ32_spl),
% 0.07/0.46 inference(component_clause,[status(thm)],[f861])).
% 0.07/0.46 fof(f865,plain,(
% 0.07/0.46 $false|sQ32_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f863,f282])).
% 0.07/0.46 fof(f866,plain,(
% 0.07/0.46 sQ32_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f865])).
% 0.07/0.46 fof(f867,plain,(
% 0.07/0.46 $false|sQ30_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f856,f99])).
% 0.07/0.46 fof(f868,plain,(
% 0.07/0.46 sQ30_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f867])).
% 0.07/0.46 fof(f869,plain,(
% 0.07/0.46 $false|sQ27_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f812,f99])).
% 0.07/0.46 fof(f870,plain,(
% 0.07/0.46 sQ27_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f869])).
% 0.07/0.46 fof(f1046,plain,(
% 0.07/0.46 gt(n0,n0)|~sQ18_spl),
% 0.07/0.46 inference(backward_demodulation,[status(thm)],[f728,f298])).
% 0.07/0.46 fof(f1048,plain,(
% 0.07/0.46 $false|~sQ18_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1046,f98])).
% 0.07/0.46 fof(f1049,plain,(
% 0.07/0.46 ~sQ18_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f1048])).
% 0.07/0.46 fof(f1073,plain,(
% 0.07/0.46 gt(n0,n0)|~sQ21_spl),
% 0.07/0.46 inference(forward_demodulation,[status(thm)],[f737,f295])).
% 0.07/0.46 fof(f1074,plain,(
% 0.07/0.46 $false|~sQ21_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1073,f98])).
% 0.07/0.46 fof(f1075,plain,(
% 0.07/0.46 ~sQ21_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f1074])).
% 0.07/0.46 fof(f1094,plain,(
% 0.07/0.46 gt(n0,n0)|~sQ19_spl),
% 0.07/0.46 inference(forward_demodulation,[status(thm)],[f731,f299])).
% 0.07/0.46 fof(f1095,plain,(
% 0.07/0.46 $false|~sQ19_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1094,f98])).
% 0.07/0.46 fof(f1096,plain,(
% 0.07/0.46 ~sQ19_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f1095])).
% 0.07/0.46 fof(f1184,definition,(
% 0.07/0.46 sQ46_spl <=> (tptp_minus_1=n998)),
% 0.07/0.46 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.07/0.46 fof(f1185,plain,(
% 0.07/0.46 tptp_minus_1=n998|~sQ46_spl),
% 0.07/0.46 inference(component_clause,[status(thm)],[f1184])).
% 0.07/0.46 fof(f1199,plain,(
% 0.07/0.46 gt(tptp_minus_1,tptp_minus_1)|~sQ46_spl),
% 0.07/0.46 inference(backward_demodulation,[status(thm)],[f1185,f290])).
% 0.07/0.46 fof(f1207,plain,(
% 0.07/0.46 $false|~sQ46_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1199,f98])).
% 0.07/0.46 fof(f1208,plain,(
% 0.07/0.46 ~sQ46_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f1207])).
% 0.07/0.46 fof(f1333,definition,(
% 0.07/0.46 sQ57_spl <=> (n3=n5)),
% 0.07/0.46 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.07/0.46 fof(f1334,plain,(
% 0.07/0.46 n3=n5|~sQ57_spl),
% 0.07/0.46 inference(component_clause,[status(thm)],[f1333])).
% 0.07/0.46 fof(f1490,plain,(
% 0.07/0.46 gt(n3,n3)|~sQ57_spl),
% 0.07/0.46 inference(forward_demodulation,[status(thm)],[f1334,f311])).
% 0.07/0.46 fof(f1491,plain,(
% 0.07/0.46 $false|~sQ57_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1490,f98])).
% 0.07/0.46 fof(f1492,plain,(
% 0.07/0.46 ~sQ57_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f1491])).
% 0.07/0.46 fof(f1547,definition,(
% 0.07/0.46 sQ71_spl <=> (n1=n4)),
% 0.07/0.46 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.07/0.46 fof(f1548,plain,(
% 0.07/0.46 n1=n4|~sQ71_spl),
% 0.07/0.46 inference(component_clause,[status(thm)],[f1547])).
% 0.07/0.46 fof(f1556,plain,(
% 0.07/0.46 gt(n1,n1)|~sQ71_spl),
% 0.07/0.46 inference(backward_demodulation,[status(thm)],[f1548,f301])).
% 0.07/0.46 fof(f1557,plain,(
% 0.07/0.46 $false|~sQ71_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f1556,f98])).
% 0.07/0.46 fof(f1558,plain,(
% 0.07/0.46 ~sQ71_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f1557])).
% 0.07/0.46 fof(f1572,plain,(
% 0.07/0.46 $false|~sQ1_spl|sQ5_spl),
% 0.07/0.46 inference(forward_subsumption_resolution,[status(thm)],[f638,f564])).
% 0.07/0.46 fof(f1573,plain,(
% 0.07/0.46 ~sQ1_spl|sQ5_spl),
% 0.07/0.46 inference(contradiction_clause,[status(thm)],[f1572])).
% 0.07/0.46 fof(f1574,plain,(
% 0.07/0.46 $false),
% 0.07/0.46 inference(sat_refutation,[status(thm)],[f423,f741,f743,f844,f848,f866,f868,f870,f1049,f1075,f1096,f1208,f1492,f1558,f1573])).
% 0.07/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.07/0.46 % Elapsed time: 0.162688 seconds
% 0.07/0.46 % CPU time: 1.066233 seconds
% 0.07/0.46 % Total memory used: 130.340 MB
% 0.07/0.46 % Net memory used: 126.846 MB
%------------------------------------------------------------------------------