%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX239-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 : n001.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:31 PM UTC 2026
% Result : Unsatisfiable 2.24s 0.77s
% Output : CNFRefutation 2.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 17
% Syntax : Number of formulae : 58 ( 58 unt; 0 def)
% Number of atoms : 58 ( 57 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-4 aty)
% Number of variables : 89 ( 89 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Y,B] : aux(Y,B,btrue) = eps,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [P2,X6,X7] : aux3(P2,X6,X7,bfalse) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
notb(btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [Q] : andb(btrue,Q) = Q,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
eps2(eps) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [R,Q2] : eps2(y(R,Q2)) = andb(eps2(R),eps2(Q2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [Y] : eps2(star(Y)) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [B,Y] : step(atom(B),Y) = aux(Y,B,eq(B,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [P2,Y] : step(star(P2),Y) = y(step(P2,Y),star(P2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [X] : rec(X,nil2) = eps2(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [X,Z,Xs] : rec(X,cons2(Z,Xs)) = rec(step(X,Z),Xs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [P2,X6,X7] : reck2(star(P2),cons2(X6,X7)) = aux3(P2,X6,X7,notb(eps2(P2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [X,Y] : prop_same(X,Y) = eq2(rec(X,Y),reck2(X,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,axiom,
eq2(btrue,bfalse) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,axiom,
! [X] : eq(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,axiom,
! [X] : eq2(X,X) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,negated_conjecture,
! [X,Y] : eq2(prop_same(X,Y),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,plain,
! [X0,X1] : aux(X0,X1,btrue) = eps,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f119,plain,
! [X0,X1,X2] : aux3(X0,X1,X2,bfalse) = bfalse,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f185,plain,
notb(btrue) = bfalse,
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f187,plain,
! [X0] : andb(btrue,X0) = X0,
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f189,plain,
eps2(eps) = btrue,
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f191,plain,
! [X0,X1] : eps2(y(X0,X1)) = andb(eps2(X0),eps2(X1)),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f192,plain,
! [X0] : eps2(star(X0)) = btrue,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f195,plain,
! [X0,X1] : step(atom(X0),X1) = aux(X1,X0,eq(X0,X1)),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f198,plain,
! [X0,X1] : step(star(X0),X1) = y(step(X0,X1),star(X0)),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f201,plain,
! [X0] : rec(X0,nil2) = eps2(X0),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f202,plain,
! [X0,X1,X2] : rec(X0,cons2(X1,X2)) = rec(step(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f214,plain,
! [X0,X1,X2] : reck2(star(X0),cons2(X1,X2)) = aux3(X0,X1,X2,notb(eps2(X0))),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f215,plain,
! [X0,X1] : prop_same(X0,X1) = eq2(rec(X0,X1),reck2(X0,X1)),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f223,plain,
eq2(btrue,bfalse) = bfalse,
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f224,plain,
! [X0] : eq(X0,X0) = btrue,
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f225,plain,
! [X0] : eq2(X0,X0) = btrue,
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f226,plain,
! [X0,X1] : eq2(prop_same(X0,X1),bfalse) != btrue,
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f418,plain,
! [X0,X1] : eps2(y(star(X0),X1)) = andb(btrue,eps2(X1)),
inference(paramodulation,[status(thm)],[f192,f191]) ).
fof(f420,plain,
! [X0] : eps2(y(eps,X0)) = andb(btrue,eps2(X0)),
inference(paramodulation,[status(thm)],[f189,f191]) ).
fof(f438,plain,
! [X0,X1] : eps2(y(star(X0),X1)) = eps2(X1),
inference(forward_demodulation,[status(thm)],[f187,f418]) ).
fof(f440,plain,
! [X0] : eps2(y(eps,X0)) = eps2(X0),
inference(forward_demodulation,[status(thm)],[f187,f420]) ).
fof(f492,plain,
! [X0,X1] : eps2(y(y(eps,X0),X1)) = andb(eps2(X0),eps2(X1)),
inference(paramodulation,[status(thm)],[f440,f191]) ).
fof(f499,plain,
! [X0,X1] : eps2(y(y(eps,X0),X1)) = eps2(y(X0,X1)),
inference(forward_demodulation,[status(thm)],[f191,f492]) ).
fof(f621,plain,
! [X0] : step(atom(X0),X0) = aux(X0,X0,btrue),
inference(paramodulation,[status(thm)],[f224,f195]) ).
fof(f628,plain,
! [X0] : step(atom(X0),X0) = eps,
inference(forward_demodulation,[status(thm)],[f114,f621]) ).
fof(f676,plain,
! [X0,X1,X2] : prop_same(X0,cons2(X1,X2)) = eq2(rec(step(X0,X1),X2),reck2(X0,cons2(X1,X2))),
inference(paramodulation,[status(thm)],[f202,f215]) ).
fof(f697,plain,
! [X0,X1] : prop_same(X0,cons2(X1,nil2)) = eq2(eps2(step(X0,X1)),reck2(X0,cons2(X1,nil2))),
inference(paramodulation,[status(thm)],[f201,f676]) ).
fof(f1297,plain,
! [X0] : step(star(atom(X0)),X0) = y(eps,star(atom(X0))),
inference(paramodulation,[status(thm)],[f628,f198]) ).
fof(f1611,plain,
! [X0,X1,X2] : reck2(star(star(X0)),cons2(X1,X2)) = aux3(star(X0),X1,X2,notb(btrue)),
inference(paramodulation,[status(thm)],[f192,f214]) ).
fof(f1627,plain,
! [X0,X1,X2] : reck2(star(star(X0)),cons2(X1,X2)) = aux3(star(X0),X1,X2,bfalse),
inference(forward_demodulation,[status(thm)],[f185,f1611]) ).
fof(f1628,plain,
! [X0,X1,X2] : reck2(star(star(X0)),cons2(X1,X2)) = bfalse,
inference(forward_demodulation,[status(thm)],[f119,f1627]) ).
fof(f1749,plain,
! [X0,X1] : prop_same(star(star(X0)),cons2(X1,nil2)) = eq2(eps2(step(star(star(X0)),X1)),bfalse),
inference(paramodulation,[status(thm)],[f1628,f697]) ).
fof(f8742,plain,
! [X0,X1] : eps2(y(step(star(atom(X0)),X0),X1)) = eps2(y(star(atom(X0)),X1)),
inference(paramodulation,[status(thm)],[f1297,f499]) ).
fof(f8809,plain,
! [X0,X1] : eps2(y(step(star(atom(X0)),X0),X1)) = eps2(X1),
inference(forward_demodulation,[status(thm)],[f438,f8742]) ).
fof(f9043,plain,
! [X0] : eps2(step(star(star(atom(X0))),X0)) = eps2(star(star(atom(X0)))),
inference(paramodulation,[status(thm)],[f198,f8809]) ).
fof(f9082,plain,
! [X0] : eps2(step(star(star(atom(X0))),X0)) = btrue,
inference(forward_demodulation,[status(thm)],[f192,f9043]) ).
fof(f9196,plain,
! [X0] : prop_same(star(star(atom(X0))),cons2(X0,nil2)) = eq2(btrue,bfalse),
inference(paramodulation,[status(thm)],[f9082,f1749]) ).
fof(f9213,plain,
! [X0] : prop_same(star(star(atom(X0))),cons2(X0,nil2)) = bfalse,
inference(forward_demodulation,[status(thm)],[f223,f9196]) ).
fof(f9318,plain,
eq2(bfalse,bfalse) != btrue,
inference(paramodulation,[status(thm)],[f9213,f226]) ).
fof(f9319,plain,
btrue != btrue,
inference(forward_demodulation,[status(thm)],[f225,f9318]) ).
fof(f9320,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f9319]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX239-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 10:42:59 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 2.24/0.77 % Refutation found
% 2.24/0.77 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.24/0.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.37/0.83 % Elapsed time: 0.460902 seconds
% 2.37/0.83 % CPU time: 3.164312 seconds
% 2.37/0.83 % Total memory used: 134.793 MB
% 2.37/0.83 % Net memory used: 133.019 MB
%------------------------------------------------------------------------------