%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ039-1 : TPTP v9.3.1. Bugfixed v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 02:00:20 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ039-1 : TPTP v9.3.1. Bugfixed v2.6.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n009.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 03:46:28 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.41 fof(f7,axiom,(
% 0.14/0.41 (![B,V1,V2,V3,V4,H,S1,X,Y,S3,S4,E2]: (( ~ state(B,V1,V2,V3,V4,H,S1,s2(X,Y),S3,S4,e1(s(X),Y),E2)| state(B,V1,V2,V3,V4,H,S1,s2(s(X),Y),S3,S4,e1(X,Y),E2) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f13,axiom,(
% 0.14/0.41 (![B,V1,V2,V3,V4,H,S1,S2,S3,X,Y,E2]: (( ~ state(B,V1,V2,V3,V4,H,S1,S2,S3,s4(X,Y),e1(X,s(Y)),E2)| state(B,V1,V2,V3,V4,H,S1,S2,S3,s4(X,s(Y)),e1(X,Y),E2) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f27,axiom,(
% 0.14/0.41 (![B,V1,V2,X,Y,V4,H,S1,S2,S3,S4,E2]: (( ~ state(B,V1,V2,v3(X,Y),V4,H,S1,S2,S3,S4,e1(s(s(X)),Y),E2)| state(B,V1,V2,v3(s(X),Y),V4,H,S1,S2,S3,S4,e1(X,Y),E2) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f30,axiom,(
% 0.14/0.41 (![B,V1,V2,V3,X,Y,H,S1,S2,S3,S4]: (( ~ state(B,V1,V2,V3,v4(X,s(Y)),H,S1,S2,S3,S4,e1(X,Y),e2(s(X),Y))| state(B,V1,V2,V3,v4(X,Y),H,S1,S2,S3,S4,e1(X,s(Y)),e2(s(X),s(Y))) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f34,axiom,(
% 0.14/0.41 (![B,V1,V2,V3,V4,X,Y,S1,S2,S3,S4,E2]: (( ~ state(B,V1,V2,V3,V4,h(X,s(Y)),S1,S2,S3,S4,e1(X,Y),E2)| state(B,V1,V2,V3,V4,h(X,Y),S1,S2,S3,S4,e1(X,s(s(Y))),E2) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f41,axiom,(
% 0.14/0.41 (![B,V1,V2,V3,V4,H,S1,S2,S3,S4,X,Y,Q,W]: (( ~ state(B,V1,V2,V3,V4,H,S1,S2,S3,S4,e1(X,Y),e2(Q,W))| state(B,V1,V2,V3,V4,H,S1,S2,S3,S4,e1(Q,W),e2(X,Y)) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f42,hypothesis,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))) ),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f43,negated_conjecture,(
% 0.14/0.41 (![B,V1,V2,V3,H,S1,S2,S3,S4,E1,E2]: (~ state(B,V1,V2,V3,v4(s(s(o)),s(s(o))),H,S1,S2,S3,S4,E1,E2) ))),
% 0.14/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f50,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11)|state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.41 fof(f56,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11)|state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f13])).
% 0.14/0.41 fof(f70,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11)|state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f27])).
% 0.14/0.41 fof(f73,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5))|state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f30])).
% 0.14/0.41 fof(f77,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11)|state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f34])).
% 0.14/0.41 fof(f84,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(X12,X13))|state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X12,X13),e2(X10,X11)))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f41])).
% 0.14/0.41 fof(f85,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o)))))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f42])).
% 0.14/0.41 fof(f86,plain,(
% 0.14/0.41 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~state(X0,X1,X2,X3,v4(s(s(o)),s(s(o))),X4,X5,X6,X7,X8,X9,X10))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f43])).
% 0.14/0.41 fof(f87,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(s(o)))),s(s(s(o)))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f85,f70])).
% 0.14/0.41 fof(f92,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),s(s(o))),e2(s(s(s(s(o)))),s(s(s(o)))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f87,f77])).
% 0.14/0.41 fof(f105,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(s(s(o)))),e2(s(s(o)),s(s(o))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f92,f84])).
% 0.14/0.41 fof(f143,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(s(s(o)))),s(s(o))),e2(s(s(o)),s(s(o))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f105,f56])).
% 0.14/0.41 fof(f230,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(s(o))),s(s(o))),e2(s(s(o)),s(s(o))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f143,f50])).
% 0.14/0.41 fof(f399,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(o)),s(s(o))),e2(s(s(s(o))),s(s(o))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f230,f84])).
% 0.14/0.41 fof(f673,plain,(
% 0.14/0.41 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(o))),h(s(s(o)),o),s1(s(s(s(o))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(o)),s(s(s(o)))),e2(s(s(s(o))),s(s(s(o)))))),
% 0.14/0.41 inference(resolution,[status(thm)],[f399,f73])).
% 0.14/0.41 fof(f676,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f673,f86])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.44 % Elapsed time: 0.072919 seconds
% 0.14/0.44 % CPU time: 0.345823 seconds
% 0.14/0.44 % Total memory used: 52.953 MB
% 0.14/0.44 % Net memory used: 52.776 MB
%------------------------------------------------------------------------------