%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX217+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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 03:13:28 PM UTC 2026
% Result : Theorem 5.06s 1.40s
% Output : CNFRefutation 3.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 38
% Syntax : Number of formulae : 246 ( 49 unt; 17 def)
% Number of atoms : 559 ( 157 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 591 ( 278 ~; 291 |; 2 &)
% ( 18 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 9 ( 3 avg)
% Number of predicates : 20 ( 18 usr; 18 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-2 aty)
% Number of variables : 92 ( 88 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,X2] : head(cons(X,X2)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : proj1Suc(suc(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
i != o,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
half(zero) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
half(suc(zero)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [N] : half(suc(suc(N))) = suc(half(N)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
evenNat(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [N] :
( evenNat(suc(N))
<=> ~ evenNat(N) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
shw(zero) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Y] :
( evenNat(suc(Y))
=> shw(suc(Y)) = cons(o,shw(half(suc(Y)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Y] :
( ~ evenNat(suc(Y))
=> shw(suc(Y)) = cons(i,shw(half(suc(Y)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Y] : append(nil,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [Y] : addNat(zero,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Y,Z] : addNat(suc(Z),Y) = suc(addNat(Z,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X] : double(X) = addNat(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
rd(nil) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Xs] : rd(cons(i,Xs)) = suc(double(rd(Xs))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [Xs] : rd(cons(o,Xs)) = double(rd(Xs)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X,Y] : x(X,Y) = rd(append(shw(X),shw(Y))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,conjecture,
? [X,Y] : x(X,Y) != x(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
~ ? [X,Y] : x(X,Y) != x(Y,X),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f26,plain,
! [X0,X1] : head(cons(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f29,plain,
! [X0] : proj1Suc(suc(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f31,plain,
i != o,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f32,plain,
half(zero) = zero,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f33,plain,
half(suc(zero)) = zero,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f34,plain,
! [X0] : half(suc(suc(X0))) = suc(half(X0)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f35,plain,
evenNat(zero),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f36,plain,
! [N] :
( ( evenNat(N)
| evenNat(suc(N)) )
& ( ~ evenNat(N)
| ~ evenNat(suc(N)) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f37,plain,
( ! [N] :
( evenNat(N)
| evenNat(suc(N)) )
& ! [N] :
( ~ evenNat(N)
| ~ evenNat(suc(N)) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f38,plain,
! [X0] :
( ~ evenNat(X0)
| ~ evenNat(suc(X0)) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
! [X0] :
( evenNat(X0)
| evenNat(suc(X0)) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f40,plain,
shw(zero) = nil,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f41,plain,
! [Y] :
( shw(suc(Y)) = cons(o,shw(half(suc(Y))))
| ~ evenNat(suc(Y)) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f42,plain,
! [X0] :
( shw(suc(X0)) = cons(o,shw(half(suc(X0))))
| ~ evenNat(suc(X0)) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f43,plain,
! [Y] :
( shw(suc(Y)) = cons(i,shw(half(suc(Y))))
| evenNat(suc(Y)) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f44,plain,
! [X0] :
( shw(suc(X0)) = cons(i,shw(half(suc(X0))))
| evenNat(suc(X0)) ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f45,plain,
! [X0] : append(nil,X0) = X0,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f46,plain,
! [X0,X1,X2] : append(cons(X0,X1),X2) = cons(X0,append(X1,X2)),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f47,plain,
! [X0] : addNat(zero,X0) = X0,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f48,plain,
! [X0,X1] : addNat(suc(X0),X1) = suc(addNat(X0,X1)),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f49,plain,
! [X0] : double(X0) = addNat(X0,X0),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f50,plain,
rd(nil) = zero,
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f51,plain,
! [X0] : rd(cons(i,X0)) = suc(double(rd(X0))),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f52,plain,
! [X0] : rd(cons(o,X0)) = double(rd(X0)),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f53,plain,
! [X0,X1] : x(X0,X1) = rd(append(shw(X0),shw(X1))),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f54,plain,
! [X,Y] : x(X,Y) = x(Y,X),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f55,plain,
! [X0,X1] : x(X0,X1) = x(X1,X0),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f61,plain,
! [X0] : x(zero,X0) = rd(append(nil,shw(X0))),
inference(paramodulation,[status(thm)],[f40,f53]) ).
fof(f64,plain,
! [X0] : x(zero,X0) = rd(shw(X0)),
inference(backward_demodulation,[status(thm)],[f45,f61]) ).
fof(f65,plain,
double(zero) = zero,
inference(paramodulation,[status(thm)],[f47,f49]) ).
fof(f69,plain,
! [X0] : x(X0,zero) = rd(shw(X0)),
inference(paramodulation,[status(thm)],[f55,f64]) ).
fof(f92,plain,
! [X0] : double(suc(X0)) = suc(addNat(X0,suc(X0))),
inference(paramodulation,[status(thm)],[f49,f48]) ).
fof(f94,plain,
! [X0] :
( shw(suc(X0)) = cons(o,shw(half(suc(X0))))
| shw(suc(X0)) = cons(i,shw(half(suc(X0)))) ),
inference(resolution,[status(thm)],[f44,f42]) ).
fof(f96,plain,
! [X0] : double(suc(suc(X0))) = suc(suc(addNat(X0,suc(suc(X0))))),
inference(paramodulation,[status(thm)],[f48,f92]) ).
fof(f97,plain,
double(suc(zero)) = suc(suc(zero)),
inference(paramodulation,[status(thm)],[f47,f92]) ).
fof(f101,plain,
! [X0] :
( shw(suc(addNat(X0,suc(X0)))) = cons(o,shw(half(suc(addNat(X0,suc(X0))))))
| ~ evenNat(double(suc(X0))) ),
inference(paramodulation,[status(thm)],[f92,f42]) ).
fof(f102,plain,
! [X0] :
( evenNat(addNat(X0,suc(X0)))
| evenNat(double(suc(X0))) ),
inference(paramodulation,[status(thm)],[f92,f39]) ).
fof(f104,plain,
! [X0] :
( ~ evenNat(addNat(X0,suc(X0)))
| ~ evenNat(double(suc(X0))) ),
inference(paramodulation,[status(thm)],[f92,f38]) ).
fof(f105,plain,
! [X0] : proj1Suc(double(suc(X0))) = addNat(X0,suc(X0)),
inference(paramodulation,[status(thm)],[f92,f29]) ).
fof(f110,plain,
! [X0] :
( shw(double(suc(X0))) = cons(o,shw(half(suc(addNat(X0,suc(X0))))))
| ~ evenNat(double(suc(X0))) ),
inference(forward_demodulation,[status(thm)],[f92,f101]) ).
fof(f111,plain,
! [X0] :
( shw(double(suc(X0))) = cons(o,shw(half(double(suc(X0)))))
| ~ evenNat(double(suc(X0))) ),
inference(forward_demodulation,[status(thm)],[f92,f110]) ).
fof(f130,plain,
! [X0] :
( shw(suc(suc(X0))) = cons(o,shw(suc(half(X0))))
| shw(suc(suc(X0))) = cons(i,shw(half(suc(suc(X0))))) ),
inference(paramodulation,[status(thm)],[f34,f94]) ).
fof(f137,plain,
! [X0] :
( shw(suc(suc(X0))) = cons(o,shw(suc(half(X0))))
| shw(suc(suc(X0))) = cons(i,shw(suc(half(X0)))) ),
inference(forward_demodulation,[status(thm)],[f34,f130]) ).
fof(f138,definition,
( sQ0_spl
<=> shw(suc(zero)) = cons(i,shw(half(suc(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f139,plain,
( ~ sQ0_spl
| shw(suc(zero)) = cons(i,shw(half(suc(zero)))) ),
inference(component_clause,[status(thm)],[f138]) ).
fof(f145,plain,
( ~ sQ0_spl
| shw(suc(zero)) = cons(i,shw(zero)) ),
inference(forward_demodulation,[status(thm)],[f33,f139]) ).
fof(f146,plain,
( ~ sQ0_spl
| shw(suc(zero)) = cons(i,nil) ),
inference(forward_demodulation,[status(thm)],[f40,f145]) ).
fof(f156,plain,
! [X0] :
( ~ sQ0_spl
| x(X0,suc(zero)) = rd(append(shw(X0),cons(i,nil))) ),
inference(paramodulation,[status(thm)],[f146,f53]) ).
fof(f157,plain,
! [X0] :
( ~ sQ0_spl
| x(suc(zero),X0) = rd(append(cons(i,nil),shw(X0))) ),
inference(paramodulation,[status(thm)],[f146,f53]) ).
fof(f166,plain,
! [X0] :
( ~ sQ0_spl
| x(suc(zero),X0) = rd(cons(i,append(nil,shw(X0)))) ),
inference(forward_demodulation,[status(thm)],[f46,f157]) ).
fof(f167,plain,
! [X0] :
( ~ sQ0_spl
| x(suc(zero),X0) = suc(double(rd(append(nil,shw(X0))))) ),
inference(forward_demodulation,[status(thm)],[f51,f166]) ).
fof(f168,plain,
! [X0] :
( ~ sQ0_spl
| x(suc(zero),X0) = suc(double(rd(shw(X0)))) ),
inference(forward_demodulation,[status(thm)],[f45,f167]) ).
fof(f169,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(rd(cons(i,nil)))) ),
inference(paramodulation,[status(thm)],[f146,f168]) ).
fof(f173,plain,
! [X0] :
( ~ sQ0_spl
| proj1Suc(double(suc(double(rd(shw(X0)))))) = addNat(double(rd(shw(X0))),x(suc(zero),X0)) ),
inference(paramodulation,[status(thm)],[f168,f105]) ).
fof(f177,plain,
! [X0] :
( ~ sQ0_spl
| shw(suc(double(rd(shw(X0))))) = cons(i,shw(half(suc(double(rd(shw(X0)))))))
| evenNat(x(suc(zero),X0)) ),
inference(paramodulation,[status(thm)],[f168,f44]) ).
fof(f182,plain,
! [X0] :
( ~ sQ0_spl
| ~ evenNat(double(rd(shw(X0))))
| ~ evenNat(x(suc(zero),X0)) ),
inference(paramodulation,[status(thm)],[f168,f38]) ).
fof(f185,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(suc(double(rd(nil))))) ),
inference(forward_demodulation,[status(thm)],[f51,f169]) ).
fof(f186,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(suc(double(zero)))) ),
inference(forward_demodulation,[status(thm)],[f50,f185]) ).
fof(f187,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f65,f186]) ).
fof(f188,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(suc(suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f97,f187]) ).
fof(f194,plain,
! [X0] :
( ~ sQ0_spl
| proj1Suc(double(x(suc(zero),X0))) = addNat(double(rd(shw(X0))),x(suc(zero),X0)) ),
inference(forward_demodulation,[status(thm)],[f168,f173]) ).
fof(f195,plain,
! [X0] :
( ~ sQ0_spl
| shw(x(suc(zero),X0)) = cons(i,shw(half(suc(double(rd(shw(X0)))))))
| evenNat(x(suc(zero),X0)) ),
inference(forward_demodulation,[status(thm)],[f168,f177]) ).
fof(f196,plain,
! [X0] :
( ~ sQ0_spl
| shw(x(suc(zero),X0)) = cons(i,shw(half(x(suc(zero),X0))))
| evenNat(x(suc(zero),X0)) ),
inference(forward_demodulation,[status(thm)],[f168,f195]) ).
fof(f245,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = rd(append(cons(i,nil),cons(i,nil))) ),
inference(paramodulation,[status(thm)],[f146,f156]) ).
fof(f247,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = rd(cons(i,append(nil,cons(i,nil)))) ),
inference(forward_demodulation,[status(thm)],[f46,f245]) ).
fof(f248,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(rd(append(nil,cons(i,nil))))) ),
inference(forward_demodulation,[status(thm)],[f51,f247]) ).
fof(f249,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(rd(cons(i,nil)))) ),
inference(forward_demodulation,[status(thm)],[f45,f248]) ).
fof(f250,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(suc(double(rd(nil))))) ),
inference(forward_demodulation,[status(thm)],[f51,f249]) ).
fof(f251,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(suc(double(zero)))) ),
inference(forward_demodulation,[status(thm)],[f50,f250]) ).
fof(f252,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(double(suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f65,f251]) ).
fof(f253,plain,
( ~ sQ0_spl
| x(suc(zero),suc(zero)) = suc(suc(suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f97,f252]) ).
fof(f296,plain,
! [X0] :
( evenNat(proj1Suc(double(suc(X0))))
| evenNat(double(suc(X0))) ),
inference(forward_demodulation,[status(thm)],[f105,f102]) ).
fof(f298,plain,
( evenNat(proj1Suc(double(suc(zero))))
| evenNat(suc(suc(zero))) ),
inference(paramodulation,[status(thm)],[f97,f296]) ).
fof(f300,plain,
! [X0] :
( ~ sQ0_spl
| evenNat(proj1Suc(double(suc(double(rd(shw(X0)))))))
| evenNat(double(x(suc(zero),X0))) ),
inference(paramodulation,[status(thm)],[f168,f296]) ).
fof(f301,definition,
( sQ2_spl
<=> evenNat(suc(suc(zero))) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f302,plain,
( ~ sQ2_spl
| evenNat(suc(suc(zero))) ),
inference(component_clause,[status(thm)],[f301]) ).
fof(f304,definition,
( sQ3_spl
<=> evenNat(proj1Suc(double(suc(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f305,plain,
( ~ sQ3_spl
| evenNat(proj1Suc(double(suc(zero)))) ),
inference(component_clause,[status(thm)],[f304]) ).
fof(f307,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f298,f301,f304]) ).
fof(f309,plain,
! [X0] :
( ~ sQ0_spl
| evenNat(proj1Suc(double(x(suc(zero),X0))))
| evenNat(double(x(suc(zero),X0))) ),
inference(forward_demodulation,[status(thm)],[f168,f300]) ).
fof(f327,plain,
! [X0] :
( ~ evenNat(proj1Suc(double(suc(X0))))
| ~ evenNat(double(suc(X0))) ),
inference(forward_demodulation,[status(thm)],[f105,f104]) ).
fof(f329,plain,
( ~ evenNat(proj1Suc(suc(suc(zero))))
| ~ evenNat(double(suc(zero))) ),
inference(paramodulation,[status(thm)],[f97,f327]) ).
fof(f334,definition,
( sQ4_spl
<=> evenNat(double(suc(zero))) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( sQ4_spl
| ~ evenNat(double(suc(zero))) ),
inference(component_clause,[status(thm)],[f334]) ).
fof(f337,definition,
( sQ5_spl
<=> evenNat(proj1Suc(suc(suc(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( sQ5_spl
| ~ evenNat(proj1Suc(suc(suc(zero)))) ),
inference(component_clause,[status(thm)],[f337]) ).
fof(f340,plain,
( ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f329,f334,f337]) ).
fof(f343,plain,
( sQ4_spl
| ~ evenNat(suc(suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f97,f336]) ).
fof(f344,plain,
( sQ4_spl
| ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f343,f302]) ).
fof(f345,plain,
( sQ4_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f344]) ).
fof(f346,plain,
( ~ sQ3_spl
| evenNat(proj1Suc(suc(suc(zero)))) ),
inference(forward_demodulation,[status(thm)],[f97,f305]) ).
fof(f347,plain,
( ~ sQ3_spl
| evenNat(suc(zero)) ),
inference(forward_demodulation,[status(thm)],[f29,f346]) ).
fof(f348,plain,
( sQ5_spl
| ~ evenNat(suc(zero)) ),
inference(forward_demodulation,[status(thm)],[f29,f339]) ).
fof(f350,plain,
( ~ sQ3_spl
| ~ evenNat(zero) ),
inference(resolution,[status(thm)],[f347,f38]) ).
fof(f355,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f350,f35]) ).
fof(f356,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f355]) ).
fof(f360,plain,
( sQ5_spl
| shw(suc(zero)) = cons(i,shw(half(suc(zero)))) ),
inference(resolution,[status(thm)],[f348,f44]) ).
fof(f369,plain,
double(suc(suc(zero))) = suc(suc(suc(suc(zero)))),
inference(paramodulation,[status(thm)],[f47,f96]) ).
fof(f528,definition,
( sQ9_spl
<=> shw(x(suc(zero),zero)) = cons(i,shw(half(x(suc(zero),zero)))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( ~ sQ9_spl
| shw(x(suc(zero),zero)) = cons(i,shw(half(x(suc(zero),zero)))) ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f540,plain,
( ~ sQ9_spl
| shw(rd(shw(suc(zero)))) = cons(i,shw(half(x(suc(zero),zero)))) ),
inference(forward_demodulation,[status(thm)],[f69,f529]) ).
fof(f608,plain,
! [X0] :
( ~ sQ0_spl
| proj1Suc(double(x(suc(zero),X0))) = addNat(double(rd(shw(X0))),x(X0,suc(zero))) ),
inference(paramodulation,[status(thm)],[f55,f194]) ).
fof(f658,plain,
( ~ sQ0_spl
| shw(x(suc(zero),zero)) = cons(i,shw(half(x(suc(zero),zero))))
| evenNat(rd(shw(suc(zero)))) ),
inference(paramodulation,[status(thm)],[f69,f196]) ).
fof(f665,definition,
( sQ12_spl
<=> evenNat(rd(shw(suc(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f666,plain,
( ~ sQ12_spl
| evenNat(rd(shw(suc(zero)))) ),
inference(component_clause,[status(thm)],[f665]) ).
fof(f668,plain,
( ~ sQ0_spl
| sQ9_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f658,f665,f528,f138]) ).
fof(f750,plain,
! [X0] :
( ~ sQ0_spl
| shw(double(suc(double(rd(shw(X0)))))) = cons(o,shw(half(double(suc(double(rd(shw(X0))))))))
| ~ evenNat(double(x(suc(zero),X0))) ),
inference(paramodulation,[status(thm)],[f168,f111]) ).
fof(f761,plain,
! [X0] :
( ~ sQ0_spl
| shw(double(x(suc(zero),X0))) = cons(o,shw(half(double(suc(double(rd(shw(X0))))))))
| ~ evenNat(double(x(suc(zero),X0))) ),
inference(forward_demodulation,[status(thm)],[f168,f750]) ).
fof(f762,plain,
! [X0] :
( ~ sQ0_spl
| shw(double(x(suc(zero),X0))) = cons(o,shw(half(double(x(suc(zero),X0)))))
| ~ evenNat(double(x(suc(zero),X0))) ),
inference(forward_demodulation,[status(thm)],[f168,f761]) ).
fof(f824,plain,
( ~ sQ0_spl
| proj1Suc(double(x(suc(zero),suc(zero)))) = addNat(double(rd(cons(i,nil))),x(suc(zero),suc(zero))) ),
inference(paramodulation,[status(thm)],[f146,f608]) ).
fof(f831,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = addNat(double(rd(cons(i,nil))),x(suc(zero),suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f188,f824]) ).
fof(f832,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = addNat(double(suc(double(rd(nil)))),x(suc(zero),suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f51,f831]) ).
fof(f833,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = addNat(double(suc(double(zero))),x(suc(zero),suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f50,f832]) ).
fof(f834,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = addNat(double(suc(zero)),x(suc(zero),suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f65,f833]) ).
fof(f835,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = addNat(suc(suc(zero)),x(suc(zero),suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f97,f834]) ).
fof(f836,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = suc(addNat(suc(zero),x(suc(zero),suc(zero)))) ),
inference(forward_demodulation,[status(thm)],[f48,f835]) ).
fof(f837,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = suc(suc(addNat(zero,x(suc(zero),suc(zero))))) ),
inference(forward_demodulation,[status(thm)],[f48,f836]) ).
fof(f838,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = suc(suc(x(suc(zero),suc(zero)))) ),
inference(forward_demodulation,[status(thm)],[f47,f837]) ).
fof(f839,plain,
( ~ sQ0_spl
| proj1Suc(double(suc(suc(suc(zero))))) = suc(suc(suc(suc(suc(zero))))) ),
inference(forward_demodulation,[status(thm)],[f188,f838]) ).
fof(f879,plain,
( ~ sQ0_spl
| ~ evenNat(suc(suc(suc(suc(suc(zero))))))
| ~ evenNat(double(suc(suc(suc(zero))))) ),
inference(paramodulation,[status(thm)],[f839,f327]) ).
fof(f890,definition,
( sQ14_spl
<=> evenNat(double(suc(suc(suc(zero))))) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f891,plain,
( ~ sQ14_spl
| evenNat(double(suc(suc(suc(zero))))) ),
inference(component_clause,[status(thm)],[f890]) ).
fof(f892,plain,
( sQ14_spl
| ~ evenNat(double(suc(suc(suc(zero))))) ),
inference(component_clause,[status(thm)],[f890]) ).
fof(f893,definition,
( sQ15_spl
<=> evenNat(suc(suc(suc(suc(suc(zero)))))) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f895,plain,
( sQ15_spl
| ~ evenNat(suc(suc(suc(suc(suc(zero)))))) ),
inference(component_clause,[status(thm)],[f893]) ).
fof(f896,plain,
( ~ sQ0_spl
| ~ sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f879,f890,f893,f138]) ).
fof(f898,plain,
( sQ14_spl
| evenNat(proj1Suc(double(suc(suc(suc(zero)))))) ),
inference(resolution,[status(thm)],[f892,f296]) ).
fof(f900,plain,
( sQ14_spl
| ~ sQ0_spl
| evenNat(suc(suc(suc(suc(suc(zero)))))) ),
inference(forward_demodulation,[status(thm)],[f839,f898]) ).
fof(f941,plain,
( sQ14_spl
| ~ sQ0_spl
| ~ evenNat(suc(suc(suc(suc(zero))))) ),
inference(resolution,[status(thm)],[f900,f38]) ).
fof(f951,plain,
( sQ14_spl
| ~ sQ0_spl
| evenNat(suc(suc(suc(zero)))) ),
inference(resolution,[status(thm)],[f941,f39]) ).
fof(f960,plain,
( sQ14_spl
| ~ sQ0_spl
| ~ evenNat(suc(suc(zero))) ),
inference(resolution,[status(thm)],[f951,f38]) ).
fof(f965,plain,
( sQ14_spl
| ~ sQ0_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f960,f301,f138,f890]) ).
fof(f970,plain,
( sQ5_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f360,f138,f337]) ).
fof(f974,plain,
( ~ sQ9_spl
| shw(rd(shw(suc(zero)))) = cons(i,shw(half(rd(shw(suc(zero)))))) ),
inference(forward_demodulation,[status(thm)],[f69,f540]) ).
fof(f983,plain,
( ~ sQ0_spl
| x(suc(zero),zero) = suc(double(rd(nil))) ),
inference(paramodulation,[status(thm)],[f40,f168]) ).
fof(f1007,plain,
( ~ sQ0_spl
| rd(shw(suc(zero))) = suc(double(rd(nil))) ),
inference(forward_demodulation,[status(thm)],[f69,f983]) ).
fof(f1008,plain,
( ~ sQ0_spl
| rd(shw(suc(zero))) = suc(double(zero)) ),
inference(forward_demodulation,[status(thm)],[f50,f1007]) ).
fof(f1009,plain,
( ~ sQ0_spl
| rd(shw(suc(zero))) = suc(zero) ),
inference(forward_demodulation,[status(thm)],[f65,f1008]) ).
fof(f1099,plain,
( shw(suc(suc(zero))) = cons(o,shw(suc(half(zero))))
| shw(suc(suc(zero))) = cons(i,shw(suc(zero))) ),
inference(paramodulation,[status(thm)],[f32,f137]) ).
fof(f1116,definition,
( sQ26_spl
<=> shw(suc(suc(zero))) = cons(i,shw(suc(zero))) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1117,plain,
( ~ sQ26_spl
| shw(suc(suc(zero))) = cons(i,shw(suc(zero))) ),
inference(component_clause,[status(thm)],[f1116]) ).
fof(f1119,definition,
( sQ27_spl
<=> shw(suc(suc(zero))) = cons(o,shw(suc(half(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
( ~ sQ27_spl
| shw(suc(suc(zero))) = cons(o,shw(suc(half(zero)))) ),
inference(component_clause,[status(thm)],[f1119]) ).
fof(f1122,plain,
( sQ27_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f1099,f1116,f1119]) ).
fof(f1130,plain,
( ~ sQ9_spl
| ~ sQ0_spl
| shw(suc(zero)) = cons(i,shw(half(rd(shw(suc(zero)))))) ),
inference(forward_demodulation,[status(thm)],[f1009,f974]) ).
fof(f1131,plain,
( ~ sQ9_spl
| ~ sQ0_spl
| shw(suc(zero)) = cons(i,shw(half(suc(zero)))) ),
inference(forward_demodulation,[status(thm)],[f1009,f1130]) ).
fof(f1132,plain,
( ~ sQ9_spl
| ~ sQ0_spl
| shw(suc(zero)) = cons(i,shw(zero)) ),
inference(forward_demodulation,[status(thm)],[f33,f1131]) ).
fof(f1134,plain,
( ~ sQ9_spl
| ~ sQ0_spl
| shw(suc(zero)) = cons(i,nil) ),
inference(forward_demodulation,[status(thm)],[f40,f1132]) ).
fof(f1214,plain,
( ~ sQ27_spl
| shw(suc(suc(zero))) = cons(o,shw(suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f32,f1120]) ).
fof(f1215,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,cons(i,nil)) ),
inference(forward_demodulation,[status(thm)],[f1134,f1214]) ).
fof(f1393,plain,
( sQ15_spl
| evenNat(suc(suc(suc(suc(zero))))) ),
inference(resolution,[status(thm)],[f895,f39]) ).
fof(f1428,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| rd(shw(suc(suc(zero)))) = double(rd(cons(i,nil))) ),
inference(paramodulation,[status(thm)],[f1215,f52]) ).
fof(f1429,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| append(shw(suc(suc(zero))),X0) = cons(o,append(cons(i,nil),X0)) ),
inference(paramodulation,[status(thm)],[f1215,f46]) ).
fof(f1433,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| rd(shw(suc(suc(zero)))) = double(suc(double(rd(nil)))) ),
inference(forward_demodulation,[status(thm)],[f51,f1428]) ).
fof(f1434,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| rd(shw(suc(suc(zero)))) = double(suc(double(zero))) ),
inference(forward_demodulation,[status(thm)],[f50,f1433]) ).
fof(f1435,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| rd(shw(suc(suc(zero)))) = double(suc(zero)) ),
inference(forward_demodulation,[status(thm)],[f65,f1434]) ).
fof(f1436,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| rd(shw(suc(suc(zero)))) = suc(suc(zero)) ),
inference(forward_demodulation,[status(thm)],[f97,f1435]) ).
fof(f1437,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| append(shw(suc(suc(zero))),X0) = cons(o,cons(i,append(nil,X0))) ),
inference(forward_demodulation,[status(thm)],[f46,f1429]) ).
fof(f1438,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| append(shw(suc(suc(zero))),X0) = cons(o,cons(i,X0)) ),
inference(forward_demodulation,[status(thm)],[f45,f1437]) ).
fof(f1640,plain,
( ~ sQ26_spl
| ~ sQ9_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(i,cons(i,nil)) ),
inference(forward_demodulation,[status(thm)],[f1134,f1117]) ).
fof(f1677,plain,
( ~ sQ26_spl
| ~ sQ9_spl
| ~ sQ0_spl
| head(shw(suc(suc(zero)))) = i ),
inference(paramodulation,[status(thm)],[f1640,f26]) ).
fof(f1741,plain,
( ~ sQ12_spl
| ~ sQ0_spl
| evenNat(rd(cons(i,nil))) ),
inference(backward_demodulation,[status(thm)],[f146,f666]) ).
fof(f1761,plain,
( ~ sQ12_spl
| ~ sQ0_spl
| evenNat(suc(double(rd(nil)))) ),
inference(forward_demodulation,[status(thm)],[f51,f1741]) ).
fof(f1762,plain,
( ~ sQ12_spl
| ~ sQ0_spl
| evenNat(suc(double(zero))) ),
inference(forward_demodulation,[status(thm)],[f50,f1761]) ).
fof(f1763,plain,
( ~ sQ12_spl
| ~ sQ0_spl
| evenNat(suc(zero)) ),
inference(forward_demodulation,[status(thm)],[f65,f1762]) ).
fof(f1764,plain,
( ~ sQ12_spl
| ~ sQ0_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1763,f348]) ).
fof(f1765,plain,
( ~ sQ12_spl
| ~ sQ0_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1764]) ).
fof(f2891,definition,
( sQ62_spl
<=> evenNat(double(suc(suc(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f3639,plain,
( ~ sQ0_spl
| evenNat(proj1Suc(double(x(suc(zero),zero))))
| evenNat(double(rd(shw(suc(zero))))) ),
inference(paramodulation,[status(thm)],[f69,f309]) ).
fof(f3646,definition,
( sQ68_spl
<=> evenNat(double(rd(shw(suc(zero))))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f3649,definition,
( sQ69_spl
<=> evenNat(proj1Suc(double(x(suc(zero),zero)))) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f3650,plain,
( ~ sQ69_spl
| evenNat(proj1Suc(double(x(suc(zero),zero)))) ),
inference(component_clause,[status(thm)],[f3649]) ).
fof(f3652,plain,
( ~ sQ0_spl
| sQ69_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f3639,f3646,f3649,f138]) ).
fof(f3683,plain,
( sQ15_spl
| evenNat(double(suc(suc(zero)))) ),
inference(backward_demodulation,[status(thm)],[f369,f1393]) ).
fof(f3948,plain,
( sQ15_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f3683,f2891,f893]) ).
fof(f4703,definition,
( sQ101_spl
<=> evenNat(double(x(suc(zero),suc(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f4705,plain,
( sQ101_spl
| ~ evenNat(double(x(suc(zero),suc(zero)))) ),
inference(component_clause,[status(thm)],[f4703]) ).
fof(f4717,plain,
( sQ101_spl
| ~ sQ0_spl
| ~ evenNat(double(suc(suc(suc(zero))))) ),
inference(forward_demodulation,[status(thm)],[f253,f4705]) ).
fof(f4718,plain,
( sQ101_spl
| ~ sQ0_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4717,f891]) ).
fof(f4719,plain,
( sQ101_spl
| ~ sQ0_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f4718]) ).
fof(f5014,definition,
( sQ105_spl
<=> evenNat(x(suc(zero),suc(suc(zero)))) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f5016,plain,
( sQ105_spl
| ~ evenNat(x(suc(zero),suc(suc(zero)))) ),
inference(component_clause,[status(thm)],[f5014]) ).
fof(f5040,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| ~ evenNat(double(suc(suc(zero))))
| ~ evenNat(x(suc(zero),suc(suc(zero)))) ),
inference(paramodulation,[status(thm)],[f1436,f182]) ).
fof(f5044,plain,
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| ~ sQ62_spl
| ~ sQ105_spl ),
inference(split_clause,[status(thm)],[f5040,f5014,f2891,f138,f528,f1119]) ).
fof(f5048,plain,
( sQ105_spl
| ~ evenNat(x(suc(suc(zero)),suc(zero))) ),
inference(paramodulation,[status(thm)],[f55,f5016]) ).
fof(f7376,plain,
( ~ sQ0_spl
| shw(double(x(suc(zero),zero))) = cons(o,shw(half(double(x(suc(zero),zero)))))
| ~ evenNat(double(rd(shw(suc(zero))))) ),
inference(paramodulation,[status(thm)],[f69,f762]) ).
fof(f7383,definition,
( sQ139_spl
<=> shw(double(x(suc(zero),zero))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f7384,plain,
( ~ sQ139_spl
| shw(double(x(suc(zero),zero))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
inference(component_clause,[status(thm)],[f7383]) ).
fof(f7386,plain,
( ~ sQ0_spl
| sQ139_spl
| ~ sQ68_spl ),
inference(split_clause,[status(thm)],[f7376,f3646,f7383,f138]) ).
fof(f7389,plain,
( ~ sQ139_spl
| shw(double(rd(shw(suc(zero))))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
inference(forward_demodulation,[status(thm)],[f69,f7384]) ).
fof(f7390,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(double(rd(cons(i,nil)))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
inference(forward_demodulation,[status(thm)],[f146,f7389]) ).
fof(f7391,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(double(suc(double(rd(nil))))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
inference(forward_demodulation,[status(thm)],[f51,f7390]) ).
fof(f7392,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(double(suc(double(zero)))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
inference(forward_demodulation,[status(thm)],[f50,f7391]) ).
fof(f7393,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(double(suc(zero))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
inference(forward_demodulation,[status(thm)],[f65,f7392]) ).
fof(f7394,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(half(double(x(suc(zero),zero))))) ),
inference(forward_demodulation,[status(thm)],[f97,f7393]) ).
fof(f7395,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(half(double(rd(shw(suc(zero))))))) ),
inference(forward_demodulation,[status(thm)],[f69,f7394]) ).
fof(f7396,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(half(double(rd(cons(i,nil)))))) ),
inference(forward_demodulation,[status(thm)],[f146,f7395]) ).
fof(f7397,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(half(double(suc(double(rd(nil))))))) ),
inference(forward_demodulation,[status(thm)],[f51,f7396]) ).
fof(f7398,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(half(double(suc(double(zero)))))) ),
inference(forward_demodulation,[status(thm)],[f50,f7397]) ).
fof(f7399,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(half(double(suc(zero))))) ),
inference(forward_demodulation,[status(thm)],[f65,f7398]) ).
fof(f7400,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(half(suc(suc(zero))))) ),
inference(forward_demodulation,[status(thm)],[f97,f7399]) ).
fof(f7401,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(suc(half(zero)))) ),
inference(forward_demodulation,[status(thm)],[f34,f7400]) ).
fof(f7402,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,shw(suc(zero))) ),
inference(forward_demodulation,[status(thm)],[f32,f7401]) ).
fof(f7403,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| shw(suc(suc(zero))) = cons(o,cons(i,nil)) ),
inference(forward_demodulation,[status(thm)],[f146,f7402]) ).
fof(f10934,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| x(suc(suc(zero)),X0) = rd(cons(o,cons(i,shw(X0)))) ),
inference(paramodulation,[status(thm)],[f1438,f53]) ).
fof(f10948,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| x(suc(suc(zero)),X0) = double(rd(cons(i,shw(X0)))) ),
inference(forward_demodulation,[status(thm)],[f52,f10934]) ).
fof(f10949,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| x(suc(suc(zero)),X0) = double(suc(double(rd(shw(X0))))) ),
inference(forward_demodulation,[status(thm)],[f51,f10948]) ).
fof(f10950,plain,
! [X0] :
( ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| x(suc(suc(zero)),X0) = double(x(suc(zero),X0)) ),
inference(forward_demodulation,[status(thm)],[f168,f10949]) ).
fof(f10951,plain,
( sQ105_spl
| ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| ~ evenNat(double(x(suc(zero),suc(zero)))) ),
inference(backward_demodulation,[status(thm)],[f10950,f5048]) ).
fof(f10992,plain,
( sQ105_spl
| ~ sQ27_spl
| ~ sQ9_spl
| ~ sQ0_spl
| ~ sQ101_spl ),
inference(split_clause,[status(thm)],[f10951,f4703,f138,f528,f1119,f5014]) ).
fof(f11759,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| head(shw(suc(suc(zero)))) = o ),
inference(paramodulation,[status(thm)],[f7403,f26]) ).
fof(f11767,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| ~ sQ26_spl
| ~ sQ9_spl
| i = o ),
inference(forward_demodulation,[status(thm)],[f1677,f11759]) ).
fof(f11768,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| ~ sQ26_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11767,f31]) ).
fof(f11769,plain,
( ~ sQ139_spl
| ~ sQ0_spl
| ~ sQ26_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f11768]) ).
fof(f11770,plain,
( ~ sQ69_spl
| evenNat(proj1Suc(double(rd(shw(suc(zero)))))) ),
inference(forward_demodulation,[status(thm)],[f69,f3650]) ).
fof(f11771,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| evenNat(proj1Suc(double(rd(cons(i,nil))))) ),
inference(forward_demodulation,[status(thm)],[f146,f11770]) ).
fof(f11772,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| evenNat(proj1Suc(double(suc(double(rd(nil)))))) ),
inference(forward_demodulation,[status(thm)],[f51,f11771]) ).
fof(f11773,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| evenNat(proj1Suc(double(suc(double(zero))))) ),
inference(forward_demodulation,[status(thm)],[f50,f11772]) ).
fof(f11774,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| evenNat(proj1Suc(double(suc(zero)))) ),
inference(forward_demodulation,[status(thm)],[f65,f11773]) ).
fof(f11775,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| evenNat(proj1Suc(suc(suc(zero)))) ),
inference(forward_demodulation,[status(thm)],[f97,f11774]) ).
fof(f11776,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| evenNat(suc(zero)) ),
inference(forward_demodulation,[status(thm)],[f29,f11775]) ).
fof(f11777,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11776,f348]) ).
fof(f11778,plain,
( ~ sQ69_spl
| ~ sQ0_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f11777]) ).
fof(f11779,plain,
$false,
inference(sat_refutation,[status(thm)],[f307,f340,f345,f356,f668,f896,f965,f970,f1122,f1765,f3652,f3948,f4719,f5044,f7386,f10992,f11769,f11778]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX217+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n006.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 10:34:42 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 5.06/1.40 % Refutation found
% 5.06/1.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.06/1.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.93/1.47 % Elapsed time: 1.016673 seconds
% 3.93/1.47 % CPU time: 7.583507 seconds
% 3.93/1.47 % Total memory used: 259.408 MB
% 3.93/1.47 % Net memory used: 256.120 MB
%------------------------------------------------------------------------------