%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PUZ042-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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.18s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PUZ042-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n019.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 03:47:05 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 0.18/0.52 % Refutation found
% 0.18/0.52 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.18/0.52 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.52 fof(f3,axiom,(
% 0.18/0.52 (![B,V1,V2,V3,V4,H,X,Y,S2,S3,S4,E2]: (( ~ state(B,V1,V2,V3,V4,H,s1(X,Y),S2,S3,S4,e1(s(X),Y),E2)| state(B,V1,V2,V3,V4,H,s1(s(X),Y),S2,S3,S4,e1(X,Y),E2) ) ))),
% 0.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f7,axiom,(
% 0.18/0.52 (![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.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f10,axiom,(
% 0.18/0.52 (![B,V1,V2,V3,V4,H,S1,S2,X,Y,S4,E2]: (( ~ state(B,V1,V2,V3,V4,H,S1,S2,s3(X,s(Y)),S4,e1(X,Y),E2)| state(B,V1,V2,V3,V4,H,S1,S2,s3(X,Y),S4,e1(X,s(Y)),E2) ) ))),
% 0.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f13,axiom,(
% 0.18/0.52 (![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.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f35,axiom,(
% 0.18/0.52 (![B,V1,V2,V3,V4,X,Y,S1,S2,S3,S4]: (( ~ state(B,V1,V2,V3,V4,h(X,Y),S1,S2,S3,S4,e1(s(X),Y),e2(s(X),s(Y)))| state(B,V1,V2,V3,V4,h(s(X),Y),S1,S2,S3,S4,e1(X,Y),e2(X,s(Y))) ) ))),
% 0.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f41,axiom,(
% 0.18/0.52 (![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.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f42,hypothesis,(
% 0.18/0.52 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.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f43,negated_conjecture,(
% 0.18/0.52 (![B,V1,V2,V3,V4,S1,S2,S3,S4,E1,E2]: (~ state(B,V1,V2,V3,V4,h(s(s(s(o))),s(o)),S1,S2,S3,S4,E1,E2) ))),
% 0.18/0.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.52 fof(f46,plain,(
% 0.18/0.52 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1,X2,X3,X4,X5,s1(X6,X7),X8,X9,X10,e1(s(X6),X7),X11)|state(X0,X1,X2,X3,X4,X5,s1(s(X6),X7),X8,X9,X10,e1(X6,X7),X11))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f3])).
% 0.18/0.52 fof(f50,plain,(
% 0.18/0.52 ![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.18/0.52 inference(cnf_transformation,[status(thm)],[f7])).
% 0.18/0.52 fof(f53,plain,(
% 0.18/0.52 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11)|state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f10])).
% 0.18/0.52 fof(f56,plain,(
% 0.18/0.52 ![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.18/0.52 inference(cnf_transformation,[status(thm)],[f13])).
% 0.18/0.52 fof(f78,plain,(
% 0.18/0.52 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(s(X5),X6),e2(s(X5),s(X6)))|state(X0,X1,X2,X3,X4,h(s(X5),X6),X7,X8,X9,X10,e1(X5,X6),e2(X5,s(X6))))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f35])).
% 0.18/0.52 fof(f84,plain,(
% 0.18/0.52 ![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.18/0.52 inference(cnf_transformation,[status(thm)],[f41])).
% 0.18/0.52 fof(f85,plain,(
% 0.18/0.52 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.18/0.52 inference(cnf_transformation,[status(thm)],[f42])).
% 0.18/0.52 fof(f86,plain,(
% 0.18/0.52 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~state(X0,X1,X2,X3,X4,h(s(s(s(o))),s(o)),X5,X6,X7,X8,X9,X10))),
% 0.18/0.52 inference(cnf_transformation,[status(thm)],[f43])).
% 0.18/0.52 fof(f88,plain,(
% 0.18/0.52 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)))),o),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(o)),e2(s(s(s(s(o)))),s(s(s(o)))))),
% 0.18/0.52 inference(resolution,[status(thm)],[f85,f53])).
% 0.18/0.52 fof(f94,plain,(
% 0.18/0.52 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(s(o)))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(o))),s(o)),e2(s(s(s(s(o)))),s(s(s(o)))))),
% 0.18/0.52 inference(resolution,[status(thm)],[f88,f46])).
% 0.18/0.52 fof(f114,plain,(
% 0.18/0.52 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(s(o)))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(s(s(o)))),e2(s(s(s(o))),s(o)))),
% 0.18/0.52 inference(resolution,[status(thm)],[f94,f84])).
% 0.18/0.52 fof(f163,plain,(
% 0.18/0.52 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(s(o)))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(s(s(o)))),s(s(o))),e2(s(s(s(o))),s(o)))),
% 0.18/0.52 inference(resolution,[status(thm)],[f114,f56])).
% 0.18/0.52 fof(f278,plain,(
% 0.18/0.52 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(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(s(o))),s(s(o))),e2(s(s(s(o))),s(o)))),
% 0.18/0.52 inference(resolution,[status(thm)],[f163,f50])).
% 0.18/0.52 fof(f490,plain,(
% 0.18/0.52 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(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(s(o))),s(o)),e2(s(s(s(o))),s(s(o))))),
% 0.18/0.52 inference(resolution,[status(thm)],[f278,f84])).
% 0.18/0.52 fof(f772,plain,(
% 0.18/0.52 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(s(o))),s(o)),s1(s(s(s(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(s(o)))),s(s(s(o)))),e1(s(s(o)),s(o)),e2(s(s(o)),s(s(o))))),
% 0.18/0.52 inference(resolution,[status(thm)],[f490,f78])).
% 0.18/0.52 fof(f775,plain,(
% 0.18/0.52 $false),
% 0.18/0.52 inference(forward_subsumption_resolution,[status(thm)],[f772,f86])).
% 0.18/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.38/0.55 % Elapsed time: 0.111489 seconds
% 0.38/0.55 % CPU time: 0.491032 seconds
% 0.38/0.55 % Total memory used: 70.510 MB
% 0.38/0.55 % Net memory used: 70.342 MB
%------------------------------------------------------------------------------