%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX239-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:52 PM UTC 2026
% Result : Unsatisfiable 0.91s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX239-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 10:37:19 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.91/0.67 % Refutation found
% 0.91/0.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.91/0.67 % SZS output start CNFRefutation for theBenchmark
% 0.91/0.67 fof(f1,axiom,(
% 0.91/0.67 (![Y,B]: (aux(Y,B,btrue) = eps ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f6,axiom,(
% 0.91/0.67 (![P2,X6,X7]: (aux3(P2,X6,X7,bfalse) = bfalse ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f72,axiom,(
% 0.91/0.67 notb(btrue) = bfalse ),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f74,axiom,(
% 0.91/0.67 (![Q]: (andb(btrue,Q) = Q ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f76,axiom,(
% 0.91/0.67 eps2(eps) = btrue ),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f78,axiom,(
% 0.91/0.67 (![R,Q2]: (eps2(y(R,Q2)) = andb(eps2(R),eps2(Q2)) ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f79,axiom,(
% 0.91/0.67 (![Y]: (eps2(star(Y)) = btrue ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f82,axiom,(
% 0.91/0.67 (![B,Y]: (step(atom(B),Y) = aux(Y,B,eq(B,Y)) ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f85,axiom,(
% 0.91/0.67 (![P2,Y]: (step(star(P2),Y) = y(step(P2,Y),star(P2)) ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f88,axiom,(
% 0.91/0.67 (![X]: (rec(X,nil2) = eps2(X) ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f89,axiom,(
% 0.91/0.67 (![X,Z,Xs]: (rec(X,cons2(Z,Xs)) = rec(step(X,Z),Xs) ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f101,axiom,(
% 0.91/0.67 (![P2,X6,X7]: (reck2(star(P2),cons2(X6,X7)) = aux3(P2,X6,X7,notb(eps2(P2))) ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f102,axiom,(
% 0.91/0.67 (![X,Y]: (prop_same(X,Y) = eq2(rec(X,Y),reck2(X,Y)) ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f110,axiom,(
% 0.91/0.67 eq2(btrue,bfalse) = bfalse ),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f111,axiom,(
% 0.91/0.67 (![X]: (eq(X,X) = btrue ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f112,axiom,(
% 0.91/0.67 (![X]: (eq2(X,X) = btrue ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f113,negated_conjecture,(
% 0.91/0.67 (![X,Y]: (eq2(prop_same(X,Y),bfalse) != btrue ))),
% 0.91/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.91/0.67 fof(f114,plain,(
% 0.91/0.67 ![X0,X1]: (aux(X0,X1,btrue)=eps)),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f1])).
% 0.91/0.67 fof(f119,plain,(
% 0.91/0.67 ![X0,X1,X2]: (aux3(X0,X1,X2,bfalse)=bfalse)),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.91/0.67 fof(f185,plain,(
% 0.91/0.67 notb(btrue)=bfalse),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f72])).
% 0.91/0.67 fof(f187,plain,(
% 0.91/0.67 ![X0]: (andb(btrue,X0)=X0)),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f74])).
% 0.91/0.67 fof(f189,plain,(
% 0.91/0.67 eps2(eps)=btrue),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f76])).
% 0.91/0.67 fof(f191,plain,(
% 0.91/0.67 ![X0,X1]: (eps2(y(X0,X1))=andb(eps2(X0),eps2(X1)))),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f78])).
% 0.91/0.67 fof(f192,plain,(
% 0.91/0.67 ![X0]: (eps2(star(X0))=btrue)),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f79])).
% 0.91/0.67 fof(f195,plain,(
% 0.91/0.67 ![X0,X1]: (step(atom(X0),X1)=aux(X1,X0,eq(X0,X1)))),
% 0.91/0.67 inference(cnf_transformation,[status(thm)],[f82])).
% 2.12/0.67 fof(f198,plain,(
% 2.12/0.67 ![X0,X1]: (step(star(X0),X1)=y(step(X0,X1),star(X0)))),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f85])).
% 2.12/0.67 fof(f201,plain,(
% 2.12/0.67 ![X0]: (rec(X0,nil2)=eps2(X0))),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f88])).
% 2.12/0.67 fof(f202,plain,(
% 2.12/0.67 ![X0,X1,X2]: (rec(X0,cons2(X1,X2))=rec(step(X0,X1),X2))),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f89])).
% 2.12/0.67 fof(f214,plain,(
% 2.12/0.67 ![X0,X1,X2]: (reck2(star(X0),cons2(X1,X2))=aux3(X0,X1,X2,notb(eps2(X0))))),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f101])).
% 2.12/0.67 fof(f215,plain,(
% 2.12/0.67 ![X0,X1]: (prop_same(X0,X1)=eq2(rec(X0,X1),reck2(X0,X1)))),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f102])).
% 2.12/0.67 fof(f223,plain,(
% 2.12/0.67 eq2(btrue,bfalse)=bfalse),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f110])).
% 2.12/0.67 fof(f224,plain,(
% 2.12/0.67 ![X0]: (eq(X0,X0)=btrue)),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f111])).
% 2.12/0.67 fof(f225,plain,(
% 2.12/0.67 ![X0]: (eq2(X0,X0)=btrue)),
% 2.12/0.67 inference(cnf_transformation,[status(thm)],[f112])).
% 2.12/0.67 fof(f226,plain,(
% 2.12/0.67 ![X0,X1]: (~eq2(prop_same(X0,X1),bfalse)=btrue)),
% 0.65/0.69 inference(cnf_transformation,[status(thm)],[f113])).
% 0.65/0.69 fof(f227,definition,(
% 0.65/0.69 ![X0,X1]: (sF0_fnc(X0,X1)=eq2(prop_same(X0,X1),bfalse))),
% 0.65/0.69 introduced(definition,[new_symbols(definition,[sF0_fnc(X0,X1)])],[function_definition])).
% 0.65/0.69 fof(f228,plain,(
% 0.65/0.69 ![X0,X1]: (~sF0_fnc(X0,X1)=btrue)),
% 0.65/0.69 inference(definition_folding,[],[f226,f227])).
% 0.65/0.69 fof(f394,plain,(
% 0.65/0.69 ![X0,X1]: (eps2(y(star(X0),X1))=andb(btrue,eps2(X1)))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f192,f191])).
% 0.65/0.69 fof(f396,plain,(
% 0.65/0.69 ![X0]: (eps2(y(eps,X0))=andb(btrue,eps2(X0)))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f189,f191])).
% 0.65/0.69 fof(f414,plain,(
% 0.65/0.69 ![X0,X1]: (eps2(y(star(X0),X1))=eps2(X1))),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f187,f394])).
% 0.65/0.69 fof(f416,plain,(
% 0.65/0.69 ![X0]: (eps2(y(eps,X0))=eps2(X0))),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f187,f396])).
% 0.65/0.69 fof(f434,plain,(
% 0.65/0.69 ![X0,X1]: (eps2(y(y(eps,X0),X1))=andb(eps2(X0),eps2(X1)))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f416,f191])).
% 0.65/0.69 fof(f439,plain,(
% 0.65/0.69 ![X0,X1]: (eps2(y(y(eps,X0),X1))=eps2(y(X0,X1)))),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f191,f434])).
% 0.65/0.69 fof(f547,plain,(
% 0.65/0.69 ![X0]: (step(atom(X0),X0)=aux(X0,X0,btrue))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f224,f195])).
% 0.65/0.69 fof(f554,plain,(
% 0.65/0.69 ![X0]: (step(atom(X0),X0)=eps)),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f114,f547])).
% 0.65/0.69 fof(f622,plain,(
% 0.65/0.69 ![X0,X1]: (rec(X0,cons2(X1,nil2))=eps2(step(X0,X1)))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f201,f202])).
% 0.65/0.69 fof(f971,plain,(
% 0.65/0.69 ![X0,X1]: (prop_same(X0,cons2(X1,nil2))=eq2(eps2(step(X0,X1)),reck2(X0,cons2(X1,nil2))))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f622,f215])).
% 0.65/0.69 fof(f1247,plain,(
% 0.65/0.69 ![X0]: (step(star(atom(X0)),X0)=y(eps,star(atom(X0))))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f554,f198])).
% 0.65/0.69 fof(f2553,plain,(
% 0.65/0.69 ![X0,X1,X2]: (reck2(star(star(X0)),cons2(X1,X2))=aux3(star(X0),X1,X2,notb(btrue)))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f192,f214])).
% 0.65/0.69 fof(f2580,plain,(
% 0.65/0.69 ![X0,X1,X2]: (reck2(star(star(X0)),cons2(X1,X2))=aux3(star(X0),X1,X2,bfalse))),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f185,f2553])).
% 0.65/0.69 fof(f2581,plain,(
% 0.65/0.69 ![X0,X1,X2]: (reck2(star(star(X0)),cons2(X1,X2))=bfalse)),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f119,f2580])).
% 0.65/0.69 fof(f2613,plain,(
% 0.65/0.69 ![X0,X1]: (prop_same(star(star(X0)),cons2(X1,nil2))=eq2(eps2(step(star(star(X0)),X1)),bfalse))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f2581,f971])).
% 0.65/0.69 fof(f7043,plain,(
% 0.65/0.69 ![X0,X1]: (eps2(y(step(star(atom(X0)),X0),X1))=eps2(y(star(atom(X0)),X1)))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f1247,f439])).
% 0.65/0.69 fof(f7085,plain,(
% 0.65/0.69 ![X0,X1]: (eps2(y(step(star(atom(X0)),X0),X1))=eps2(X1))),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f414,f7043])).
% 0.65/0.69 fof(f7455,plain,(
% 0.65/0.69 ![X0]: (eps2(step(star(star(atom(X0))),X0))=eps2(star(star(atom(X0)))))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f198,f7085])).
% 0.65/0.69 fof(f7500,plain,(
% 0.65/0.69 ![X0]: (eps2(step(star(star(atom(X0))),X0))=btrue)),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f192,f7455])).
% 0.65/0.69 fof(f7525,plain,(
% 0.65/0.69 ![X0]: (prop_same(star(star(atom(X0))),cons2(X0,nil2))=eq2(btrue,bfalse))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f7500,f2613])).
% 0.65/0.69 fof(f7549,plain,(
% 0.65/0.69 ![X0]: (prop_same(star(star(atom(X0))),cons2(X0,nil2))=bfalse)),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f223,f7525])).
% 0.65/0.69 fof(f7680,plain,(
% 0.65/0.69 ![X0]: (sF0_fnc(star(star(atom(X0))),cons2(X0,nil2))=eq2(bfalse,bfalse))),
% 0.65/0.69 inference(paramodulation,[status(thm)],[f7549,f227])).
% 0.65/0.69 fof(f7681,plain,(
% 0.65/0.69 ![X0]: (sF0_fnc(star(star(atom(X0))),cons2(X0,nil2))=btrue)),
% 0.65/0.69 inference(forward_demodulation,[status(thm)],[f225,f7680])).
% 0.65/0.69 fof(f7682,plain,(
% 0.65/0.69 $false),
% 0.65/0.69 inference(forward_subsumption_resolution,[status(thm)],[f7681,f228])).
% 0.65/0.69 % SZS output end CNFRefutation for theBenchmark.p
% 0.65/0.70 % Elapsed time: 0.334149 seconds
% 0.65/0.70 % CPU time: 2.389193 seconds
% 0.65/0.70 % Total memory used: 66.968 MB
% 0.65/0.70 % Net memory used: 66.517 MB
%------------------------------------------------------------------------------