%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Unsatisfiable 249.92s 32.07s
% Output : CNFRefutation 167.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 25
% Syntax : Number of formulae : 117 ( 117 unt; 0 def)
% Number of atoms : 117 ( 116 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 6 con; 0-2 aty)
% Number of variables : 88 ( 88 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Y] : aux(Y,btrue) = cons(o,shw(half(suc(Y)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [Y] : aux(Y,bfalse) = cons(i,shw(half(suc(Y)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
notb(btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
notb(bfalse) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
half(zero) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
half(suc(zero)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [N] : half(suc(suc(N))) = suc(half(N)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
evenNat(zero) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [N] : evenNat(suc(N)) = notb(evenNat(N)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
shw(zero) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Y] : shw(suc(Y)) = aux(Y,evenNat(suc(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Y] : append(nil,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Z,Xs,Y] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Y] : addNat(zero,Y) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [Z,Y] : addNat(suc(Z),Y) = suc(addNat(Z,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X] : double(X) = addNat(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
rd(nil) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Xs] : rd(cons(i,Xs)) = suc(double(rd(Xs))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [Xs] : rd(cons(o,Xs)) = double(rd(Xs)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X,Y] : x(X,Y) = rd(append(shw(X),shw(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X,Y] : sat_comm(X,Y) = eq(x(X,Y),x(Y,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X,Y] : eq(suc(X),suc(Y)) = eq(X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X] : eq(zero,suc(X)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [X] : eq2(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
! [X,Y] : eq2(sat_comm(X,Y),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,plain,
! [X0] : aux(X0,btrue) = cons(o,shw(half(suc(X0)))),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f34,plain,
! [X0] : aux(X0,bfalse) = cons(i,shw(half(suc(X0)))),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f35,plain,
notb(btrue) = bfalse,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f36,plain,
notb(bfalse) = btrue,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f37,plain,
half(zero) = zero,
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f38,plain,
half(suc(zero)) = zero,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f39,plain,
! [X0] : half(suc(suc(X0))) = suc(half(X0)),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f40,plain,
evenNat(zero) = btrue,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f41,plain,
! [X0] : evenNat(suc(X0)) = notb(evenNat(X0)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f42,plain,
shw(zero) = nil,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f43,plain,
! [X0] : shw(suc(X0)) = aux(X0,evenNat(suc(X0))),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f44,plain,
! [X0] : append(nil,X0) = X0,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f45,plain,
! [X0,X1,X2] : append(cons(X0,X1),X2) = cons(X0,append(X1,X2)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f46,plain,
! [X0] : addNat(zero,X0) = X0,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f47,plain,
! [X0,X1] : addNat(suc(X0),X1) = suc(addNat(X0,X1)),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f48,plain,
! [X0] : double(X0) = addNat(X0,X0),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f49,plain,
rd(nil) = zero,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f50,plain,
! [X0] : rd(cons(i,X0)) = suc(double(rd(X0))),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f51,plain,
! [X0] : rd(cons(o,X0)) = double(rd(X0)),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f52,plain,
! [X0,X1] : x(X0,X1) = rd(append(shw(X0),shw(X1))),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f53,plain,
! [X0,X1] : sat_comm(X0,X1) = eq(x(X0,X1),x(X1,X0)),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f58,plain,
! [X0,X1] : eq(suc(X0),suc(X1)) = eq(X0,X1),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f59,plain,
! [X0] : eq(zero,suc(X0)) = bfalse,
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f62,plain,
! [X0] : eq2(X0,X0) = btrue,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f64,plain,
! [X0,X1] : eq2(sat_comm(X0,X1),bfalse) != btrue,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f71,plain,
aux(zero,bfalse) = cons(i,shw(zero)),
inference(paramodulation,[status(thm)],[f38,f34]) ).
fof(f73,plain,
aux(zero,bfalse) = cons(i,nil),
inference(forward_demodulation,[status(thm)],[f42,f71]) ).
fof(f75,plain,
double(zero) = zero,
inference(paramodulation,[status(thm)],[f46,f48]) ).
fof(f78,plain,
! [X0] : aux(suc(X0),btrue) = cons(o,shw(suc(half(X0)))),
inference(paramodulation,[status(thm)],[f39,f33]) ).
fof(f79,plain,
! [X0] : addNat(suc(zero),X0) = suc(X0),
inference(paramodulation,[status(thm)],[f46,f47]) ).
fof(f88,plain,
suc(suc(zero)) = double(suc(zero)),
inference(paramodulation,[status(thm)],[f48,f79]) ).
fof(f89,plain,
! [X0] : addNat(suc(suc(zero)),X0) = suc(suc(X0)),
inference(paramodulation,[status(thm)],[f79,f47]) ).
fof(f97,plain,
! [X0,X1,X2] : eq(addNat(X0,X1),X2) = eq(addNat(suc(X0),X1),suc(X2)),
inference(paramodulation,[status(thm)],[f47,f58]) ).
fof(f98,plain,
! [X0,X1,X2] : eq(X0,addNat(X1,X2)) = eq(suc(X0),addNat(suc(X1),X2)),
inference(paramodulation,[status(thm)],[f47,f58]) ).
fof(f100,plain,
! [X0] : shw(suc(X0)) = aux(X0,notb(evenNat(X0))),
inference(forward_demodulation,[status(thm)],[f41,f43]) ).
fof(f101,plain,
! [X0] : shw(suc(suc(X0))) = aux(suc(X0),notb(notb(evenNat(X0)))),
inference(paramodulation,[status(thm)],[f41,f100]) ).
fof(f102,plain,
shw(suc(zero)) = aux(zero,notb(btrue)),
inference(paramodulation,[status(thm)],[f40,f100]) ).
fof(f103,plain,
shw(suc(zero)) = aux(zero,bfalse),
inference(forward_demodulation,[status(thm)],[f35,f102]) ).
fof(f104,plain,
! [X0] : cons(i,append(nil,X0)) = append(aux(zero,bfalse),X0),
inference(paramodulation,[status(thm)],[f73,f45]) ).
fof(f106,plain,
! [X0,X1] : cons(o,append(shw(half(suc(X0))),X1)) = append(aux(X0,btrue),X1),
inference(paramodulation,[status(thm)],[f33,f45]) ).
fof(f107,plain,
! [X0] : cons(i,X0) = append(aux(zero,bfalse),X0),
inference(forward_demodulation,[status(thm)],[f44,f104]) ).
fof(f108,plain,
suc(double(rd(nil))) = rd(aux(zero,bfalse)),
inference(paramodulation,[status(thm)],[f73,f50]) ).
fof(f110,plain,
suc(double(zero)) = rd(aux(zero,bfalse)),
inference(forward_demodulation,[status(thm)],[f49,f108]) ).
fof(f111,plain,
suc(zero) = rd(aux(zero,bfalse)),
inference(forward_demodulation,[status(thm)],[f75,f110]) ).
fof(f126,plain,
! [X0] : x(zero,X0) = rd(append(nil,shw(X0))),
inference(paramodulation,[status(thm)],[f42,f52]) ).
fof(f128,plain,
! [X0] : x(zero,X0) = rd(shw(X0)),
inference(forward_demodulation,[status(thm)],[f44,f126]) ).
fof(f141,plain,
! [X0] : x(X0,suc(zero)) = rd(append(shw(X0),aux(zero,bfalse))),
inference(paramodulation,[status(thm)],[f103,f52]) ).
fof(f142,plain,
! [X0] : x(suc(zero),X0) = rd(append(aux(zero,bfalse),shw(X0))),
inference(paramodulation,[status(thm)],[f103,f52]) ).
fof(f144,plain,
suc(suc(suc(suc(zero)))) = double(suc(suc(zero))),
inference(paramodulation,[status(thm)],[f48,f89]) ).
fof(f165,plain,
aux(suc(zero),btrue) = cons(o,shw(suc(zero))),
inference(paramodulation,[status(thm)],[f37,f78]) ).
fof(f169,plain,
aux(suc(zero),btrue) = cons(o,aux(zero,bfalse)),
inference(forward_demodulation,[status(thm)],[f103,f165]) ).
fof(f304,plain,
! [X0,X1] : eq(addNat(X0,suc(X0)),X1) = eq(double(suc(X0)),suc(X1)),
inference(paramodulation,[status(thm)],[f48,f97]) ).
fof(f345,plain,
! [X0,X1] : eq(X0,addNat(X1,suc(X1))) = eq(suc(X0),double(suc(X1))),
inference(paramodulation,[status(thm)],[f48,f98]) ).
fof(f361,plain,
! [X0,X1] : double(rd(append(shw(half(suc(X0))),X1))) = rd(append(aux(X0,btrue),X1)),
inference(paramodulation,[status(thm)],[f106,f51]) ).
fof(f691,plain,
double(rd(aux(zero,bfalse))) = rd(aux(suc(zero),btrue)),
inference(paramodulation,[status(thm)],[f169,f51]) ).
fof(f693,plain,
double(suc(zero)) = rd(aux(suc(zero),btrue)),
inference(forward_demodulation,[status(thm)],[f111,f691]) ).
fof(f694,plain,
suc(suc(zero)) = rd(aux(suc(zero),btrue)),
inference(forward_demodulation,[status(thm)],[f88,f693]) ).
fof(f706,plain,
shw(suc(suc(zero))) = aux(suc(zero),notb(notb(btrue))),
inference(paramodulation,[status(thm)],[f40,f101]) ).
fof(f734,plain,
shw(suc(suc(zero))) = aux(suc(zero),notb(bfalse)),
inference(forward_demodulation,[status(thm)],[f35,f706]) ).
fof(f735,plain,
shw(suc(suc(zero))) = aux(suc(zero),btrue),
inference(forward_demodulation,[status(thm)],[f36,f734]) ).
fof(f762,plain,
x(zero,suc(suc(zero))) = rd(aux(suc(zero),btrue)),
inference(paramodulation,[status(thm)],[f735,f128]) ).
fof(f764,plain,
! [X0] : x(suc(suc(zero)),X0) = rd(append(aux(suc(zero),btrue),shw(X0))),
inference(paramodulation,[status(thm)],[f735,f52]) ).
fof(f1146,plain,
! [X0] : eq(double(suc(suc(zero))),suc(X0)) = eq(suc(suc(suc(zero))),X0),
inference(paramodulation,[status(thm)],[f79,f304]) ).
fof(f1296,plain,
! [X0] : eq(suc(X0),double(suc(suc(suc(zero))))) = eq(X0,suc(suc(suc(suc(suc(zero)))))),
inference(paramodulation,[status(thm)],[f89,f345]) ).
fof(f1297,plain,
! [X0] : eq(suc(X0),double(suc(suc(zero)))) = eq(X0,suc(suc(suc(zero)))),
inference(paramodulation,[status(thm)],[f79,f345]) ).
fof(f1328,plain,
! [X0] : eq(suc(X0),double(suc(suc(suc(zero))))) = eq(X0,suc(double(suc(suc(zero))))),
inference(forward_demodulation,[status(thm)],[f144,f1296]) ).
fof(f1946,plain,
! [X0,X1] : rd(append(aux(X0,btrue),shw(X1))) = double(x(half(suc(X0)),X1)),
inference(paramodulation,[status(thm)],[f52,f361]) ).
fof(f2007,plain,
x(suc(zero),suc(zero)) = rd(append(aux(zero,bfalse),aux(zero,bfalse))),
inference(paramodulation,[status(thm)],[f103,f141]) ).
fof(f2010,plain,
x(suc(zero),suc(zero)) = rd(cons(i,aux(zero,bfalse))),
inference(forward_demodulation,[status(thm)],[f107,f2007]) ).
fof(f2011,plain,
x(suc(zero),suc(zero)) = suc(double(rd(aux(zero,bfalse)))),
inference(forward_demodulation,[status(thm)],[f50,f2010]) ).
fof(f2012,plain,
x(suc(zero),suc(zero)) = suc(double(suc(zero))),
inference(forward_demodulation,[status(thm)],[f111,f2011]) ).
fof(f2013,plain,
x(suc(zero),suc(zero)) = suc(suc(suc(zero))),
inference(forward_demodulation,[status(thm)],[f88,f2012]) ).
fof(f2028,plain,
! [X0] : x(suc(zero),X0) = rd(cons(i,shw(X0))),
inference(forward_demodulation,[status(thm)],[f107,f142]) ).
fof(f2029,plain,
! [X0] : x(suc(zero),X0) = suc(double(rd(shw(X0)))),
inference(forward_demodulation,[status(thm)],[f50,f2028]) ).
fof(f2030,plain,
! [X0] : x(suc(zero),X0) = suc(double(x(zero,X0))),
inference(forward_demodulation,[status(thm)],[f128,f2029]) ).
fof(f9589,plain,
x(zero,suc(suc(zero))) = suc(suc(zero)),
inference(paramodulation,[status(thm)],[f694,f762]) ).
fof(f9652,plain,
x(suc(zero),suc(suc(zero))) = suc(double(suc(suc(zero)))),
inference(paramodulation,[status(thm)],[f9589,f2030]) ).
fof(f48575,plain,
sat_comm(suc(zero),suc(suc(zero))) = eq(suc(double(suc(suc(zero)))),x(suc(suc(zero)),suc(zero))),
inference(paramodulation,[status(thm)],[f9652,f53]) ).
fof(f250834,plain,
! [X0] : x(suc(suc(zero)),X0) = double(x(half(suc(suc(zero))),X0)),
inference(forward_demodulation,[status(thm)],[f1946,f764]) ).
fof(f250835,plain,
! [X0] : x(suc(suc(zero)),X0) = double(x(suc(half(zero)),X0)),
inference(forward_demodulation,[status(thm)],[f39,f250834]) ).
fof(f250859,plain,
! [X0] : x(suc(suc(zero)),X0) = double(x(suc(zero),X0)),
inference(forward_demodulation,[status(thm)],[f37,f250835]) ).
fof(f250865,plain,
x(suc(suc(zero)),suc(zero)) = double(suc(suc(suc(zero)))),
inference(paramodulation,[status(thm)],[f2013,f250859]) ).
fof(f260490,plain,
sat_comm(suc(zero),suc(suc(zero))) = eq(suc(double(suc(suc(zero)))),double(suc(suc(suc(zero))))),
inference(backward_demodulation,[status(thm)],[f250865,f48575]) ).
fof(f260508,plain,
sat_comm(suc(zero),suc(suc(zero))) = eq(double(suc(suc(zero))),suc(double(suc(suc(zero))))),
inference(forward_demodulation,[status(thm)],[f1328,f260490]) ).
fof(f260509,plain,
sat_comm(suc(zero),suc(suc(zero))) = eq(suc(suc(suc(zero))),double(suc(suc(zero)))),
inference(forward_demodulation,[status(thm)],[f1146,f260508]) ).
fof(f260510,plain,
sat_comm(suc(zero),suc(suc(zero))) = eq(suc(suc(zero)),suc(suc(suc(zero)))),
inference(forward_demodulation,[status(thm)],[f1297,f260509]) ).
fof(f260511,plain,
sat_comm(suc(zero),suc(suc(zero))) = eq(suc(zero),suc(suc(zero))),
inference(forward_demodulation,[status(thm)],[f58,f260510]) ).
fof(f260512,plain,
sat_comm(suc(zero),suc(suc(zero))) = eq(zero,suc(zero)),
inference(forward_demodulation,[status(thm)],[f58,f260511]) ).
fof(f260513,plain,
sat_comm(suc(zero),suc(suc(zero))) = bfalse,
inference(forward_demodulation,[status(thm)],[f59,f260512]) ).
fof(f260542,plain,
btrue != eq2(bfalse,bfalse),
inference(paramodulation,[status(thm)],[f260513,f64]) ).
fof(f260543,plain,
btrue != btrue,
inference(forward_demodulation,[status(thm)],[f62,f260542]) ).
fof(f260544,plain,
$false,
inference(equality_resolution,[status(thm)],[f260543]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX217-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n016.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 10:39:53 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 249.92/32.07 % Refutation found
% 249.92/32.07 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 249.92/32.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.93/32.89 % Elapsed time: 32.432596 seconds
% 14.93/32.89 % CPU time: 254.532229 seconds
% 14.93/32.89 % Total memory used: 5.384 GB
% 14.93/32.89 % Net memory used: 5.287 GB
%------------------------------------------------------------------------------