%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX197+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:24 PM UTC 2026
% Result : Theorem 26.97s 8.88s
% Output : CNFRefutation 25.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 51 ( 30 unt; 2 def)
% Number of atoms : 72 ( 53 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 51 ( 30 ~; 18 |; 0 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 3 con; 0-3 aty)
% Number of variables : 117 ( 115 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f37,axiom,
! [X,X2] : nil != cons(X,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [C,Q,R] : opti2(if(C,Q,R)) = if(add(n(suc(zero)),C),R,Q),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
! [Y] : addNat(zero,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [Z,X2] : addNat(suc(Z),suc(X2)) = suc(addNat(Z,suc(X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [X,N] : eval(X,n(N)) = N,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [X,A,B] : eval(X,add(A,B)) = addNat(eval(X,A),eval(X,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X] : run(X,nil2) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [X,R,E] : run(X,cons2(print(E),R)) = cons(eval(X,E),run(X,R)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X,R,E4,Q,Q2,X3] :
( eval(X,E4) = suc(X3)
=> run(X,cons2(if(E4,Q,Q2),R)) = run(X,append(Q,R)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [Y] : append(nil2,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [Y,Z,Xs] : append(cons2(Z,Xs),Y) = cons2(Z,append(Xs,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,conjecture,
? [P] : run(nil,cons2(P,nil2)) != run(nil,cons2(opti2(P),nil2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,negated_conjecture,
~ ? [P] : run(nil,cons2(P,nil2)) != run(nil,cons2(opti2(P),nil2)),
inference(negated_conjecture,[status(cth)],[f74]) ).
fof(f112,plain,
! [X0,X1] : nil != cons(X0,X1),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f123,plain,
! [X0,X1,X2] : opti2(if(X0,X1,X2)) = if(add(n(suc(zero)),X0),X2,X1),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f127,plain,
! [X0] : addNat(zero,X0) = X0,
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f129,plain,
! [X0,X1] : addNat(suc(X0),suc(X1)) = suc(addNat(X0,suc(X1))),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f133,plain,
! [X0,X1] : eval(X0,n(X1)) = X1,
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f134,plain,
! [X0,X1,X2] : eval(X0,add(X1,X2)) = addNat(eval(X0,X1),eval(X0,X2)),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f141,plain,
! [X0] : run(X0,nil2) = nil,
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f142,plain,
! [X0,X1,X2] : run(X0,cons2(print(X1),X2)) = cons(eval(X0,X1),run(X0,X2)),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f148,plain,
! [X,R,E4,Q,Q2,X3] :
( run(X,cons2(if(E4,Q,Q2),R)) = run(X,append(Q,R))
| eval(X,E4) != suc(X3) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f149,plain,
! [X,E4] :
( ! [R,Q,Q2] : run(X,cons2(if(E4,Q,Q2),R)) = run(X,append(Q,R))
| ! [X3] : eval(X,E4) != suc(X3) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f150,plain,
! [X0,X1,X2,X3,X4,X5] :
( run(X0,cons2(if(X1,X3,X4),X5)) = run(X0,append(X3,X5))
| eval(X0,X1) != suc(X2) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f153,plain,
! [X0] : append(nil2,X0) = X0,
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f154,plain,
! [X0,X1,X2] : append(cons2(X0,X1),X2) = cons2(X0,append(X1,X2)),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f156,plain,
! [P] : run(nil,cons2(P,nil2)) = run(nil,cons2(opti2(P),nil2)),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f157,plain,
! [X0] : run(nil,cons2(X0,nil2)) = run(nil,cons2(opti2(X0),nil2)),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f456,plain,
! [X0,X1,X2] : eval(X0,add(n(X1),X2)) = addNat(X1,eval(X0,X2)),
inference(paramodulation,[status(thm)],[f133,f134]) ).
fof(f639,plain,
! [X0,X1,X2] : nil != run(X0,cons2(print(X1),X2)),
inference(paramodulation,[status(thm)],[f142,f112]) ).
fof(f1148,plain,
! [X0,X1,X2,X3,X4] : run(X0,cons2(if(n(suc(X1)),X2,X3),X4)) = run(X0,append(X2,X4)),
inference(resolution,[status(thm)],[f133,f150]) ).
fof(f13063,definition,
! [X1,X2] :
( sQ491_spl
<=> run(nil,append(X1,nil2)) = run(nil,append(X2,nil2)) ),
introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition]) ).
fof(f13064,plain,
! [X0,X1] :
( ~ sQ491_spl
| run(nil,append(X0,nil2)) = run(nil,append(X1,nil2)) ),
inference(component_clause,[status(thm)],[f13063]) ).
fof(f14935,plain,
! [X0] :
( ~ sQ491_spl
| run(nil,nil2) = run(nil,append(X0,nil2)) ),
inference(paramodulation,[status(thm)],[f153,f13064]) ).
fof(f14954,plain,
! [X0] :
( ~ sQ491_spl
| nil = run(nil,append(X0,nil2)) ),
inference(forward_demodulation,[status(thm)],[f141,f14935]) ).
fof(f14968,plain,
! [X0,X1] :
( ~ sQ491_spl
| nil = run(nil,cons2(X0,append(X1,nil2))) ),
inference(paramodulation,[status(thm)],[f154,f14954]) ).
fof(f15099,plain,
( ~ sQ491_spl
| $false ),
inference(resolution,[status(thm)],[f14968,f639]) ).
fof(f15157,plain,
~ sQ491_spl,
inference(contradiction_clause,[status(thm)],[f15099]) ).
fof(f17426,plain,
! [X0,X1,X2,X3,X4,X5] :
( run(X0,cons2(opti2(if(X1,X3,X4)),X5)) = run(X0,append(X4,X5))
| eval(X0,add(n(suc(zero)),X1)) != suc(X2) ),
inference(paramodulation,[status(thm)],[f123,f150]) ).
fof(f17556,plain,
! [X0,X1,X2,X3] :
( run(nil,cons2(if(X0,X2,X3),nil2)) = run(nil,append(X3,nil2))
| eval(nil,add(n(suc(zero)),X0)) != suc(X1) ),
inference(paramodulation,[status(thm)],[f157,f17426]) ).
fof(f19222,plain,
! [X0,X1,X2,X3] :
( run(nil,cons2(if(X0,X2,X3),nil2)) = run(nil,append(X3,nil2))
| addNat(suc(zero),eval(nil,X0)) != suc(X1) ),
inference(backward_demodulation,[status(thm)],[f456,f17556]) ).
fof(f30216,plain,
! [X0,X1,X2,X3] :
( run(nil,append(X2,nil2)) = run(nil,append(X3,nil2))
| addNat(suc(zero),eval(nil,n(suc(X0)))) != suc(X1) ),
inference(paramodulation,[status(thm)],[f1148,f19222]) ).
fof(f30239,definition,
! [X0,X1] :
( sQ1144_spl
<=> addNat(suc(zero),eval(nil,n(suc(X0)))) != suc(X1) ),
introduced(definition,[new_symbols(definition,[sQ1144_spl])],[split_symbol_definition]) ).
fof(f30240,plain,
! [X0,X1] :
( ~ sQ1144_spl
| addNat(suc(zero),eval(nil,n(suc(X0)))) != suc(X1) ),
inference(component_clause,[status(thm)],[f30239]) ).
fof(f30242,plain,
( sQ491_spl
| sQ1144_spl ),
inference(split_clause,[status(thm)],[f30216,f30239,f13063]) ).
fof(f30248,plain,
! [X0,X1] :
( ~ sQ1144_spl
| addNat(suc(zero),suc(X0)) != suc(X1) ),
inference(forward_demodulation,[status(thm)],[f133,f30240]) ).
fof(f30249,plain,
! [X0,X1] :
( ~ sQ1144_spl
| suc(addNat(zero,suc(X0))) != suc(X1) ),
inference(forward_demodulation,[status(thm)],[f129,f30248]) ).
fof(f30250,plain,
! [X0,X1] :
( ~ sQ1144_spl
| suc(suc(X0)) != suc(X1) ),
inference(forward_demodulation,[status(thm)],[f127,f30249]) ).
fof(f30253,plain,
( ~ sQ1144_spl
| $false ),
inference(equality_resolution,[status(thm)],[f30250]) ).
fof(f30254,plain,
~ sQ1144_spl,
inference(contradiction_clause,[status(thm)],[f30253]) ).
fof(f30255,plain,
$false,
inference(sat_refutation,[status(thm)],[f15157,f30242,f30254]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX197+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n002.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Mon Sep 21 10:35:23 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 26.97/8.88 % Refutation found
% 26.97/8.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 26.97/8.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.44/9.11 % Elapsed time: 3.724297 seconds
% 2.44/9.11 % CPU time: 28.455929 seconds
% 2.44/9.11 % Total memory used: 585.639 MB
% 2.44/9.11 % Net memory used: 558.973 MB
%------------------------------------------------------------------------------