%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PLA031-1.003 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 01:58:43 PM UTC 2026
% Result : Unsatisfiable 55.61s 7.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PLA031-1.003 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n011.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 03:33:25 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 55.61/7.57 % Refutation found
% 55.61/7.57 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 55.61/7.57 % SZS output start CNFRefutation for theBenchmark
% 55.61/7.57 fof(f1,axiom,(
% 55.61/7.57 (![L,O2,O3,O4,D1,D2,T2]: (( ~ s(L,O2,O3,O4,D1,D2,L,T2)| s(truck1,O2,O3,O4,D1,D2,L,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f2,axiom,(
% 55.61/7.57 (![L,O2,O3,O4,D1,D2,T2]: (( s(L,O2,O3,O4,D1,D2,L,T2)| ~ s(truck1,O2,O3,O4,D1,D2,L,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f9,axiom,(
% 55.61/7.57 (![O1,O2,L,O4,D1,D2,T2]: (( ~ s(O1,O2,L,O4,D1,D2,L,T2)| s(O1,O2,truck1,O4,D1,D2,L,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f10,axiom,(
% 55.61/7.57 (![O1,O2,L,O4,D1,D2,T2]: (( s(O1,O2,L,O4,D1,D2,L,T2)| ~ s(O1,O2,truck1,O4,D1,D2,L,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f13,axiom,(
% 55.61/7.57 (![O1,O2,O3,L,D1,D2,T2]: (( ~ s(O1,O2,O3,L,D1,D2,L,T2)| s(O1,O2,O3,truck1,D1,D2,L,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f14,axiom,(
% 55.61/7.57 (![O1,O2,O3,L,D1,D2,T2]: (( s(O1,O2,O3,L,D1,D2,L,T2)| ~ s(O1,O2,O3,truck1,D1,D2,L,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f21,axiom,(
% 55.61/7.57 (![O1,O2,O3,O4,D1,L,T2]: (( ~ s(O1,O2,O3,O4,D1,L,L,T2)| ~ neq(D1,truck1)| s(O1,O2,O3,O4,D1,truck1,L,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f27,axiom,(
% 55.61/7.57 (![O1,O2,O3,O4,D1,S,T2,D]: (( ~ s(O1,O2,O3,O4,D1,truck1,S,T2)| ~ link(S,D)| s(O1,O2,O3,O4,D1,truck1,D,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f29,axiom,(
% 55.61/7.57 (![O1,O2,O3,O4,S,D2,T1,T2,D]: (( ~ s(O1,O2,O3,O4,S,D2,T1,T2)| ~ path(S,D)| s(O1,O2,O3,O4,D,D2,T1,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f30,axiom,(
% 55.61/7.57 (![O1,O2,O3,O4,D1,S,T1,T2,D]: (( ~ s(O1,O2,O3,O4,D1,S,T1,T2)| ~ path(S,D)| s(O1,O2,O3,O4,D1,D,T1,T2) ) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f63,axiom,(
% 55.61/7.57 neq(s2,truck1) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f95,axiom,(
% 55.61/7.57 path(s0,p0_1) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f98,axiom,(
% 55.61/7.57 path(p0_1,s1) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f100,axiom,(
% 55.61/7.57 path(p1_2,s1) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f101,axiom,(
% 55.61/7.57 path(s2,p1_2) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f107,axiom,(
% 55.61/7.57 link(s1,s2) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f109,axiom,(
% 55.61/7.57 link(s2,s0) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f110,axiom,(
% 55.61/7.57 link(s0,s2) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f111,axiom,(
% 55.61/7.57 s(s1,s2,s2,s0,s2,s0,s1,s1) ),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f112,negated_conjecture,(
% 55.61/7.57 (![X6,X8]: (~ s(s2,s2,s0,s2,s1,X6,s0,X8) ))),
% 55.61/7.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 55.61/7.57 fof(f113,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,X5,X0,X6)|s(truck1,X1,X2,X3,X4,X5,X0,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f1])).
% 55.61/7.57 fof(f114,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (s(X0,X1,X2,X3,X4,X5,X0,X6)|~s(truck1,X1,X2,X3,X4,X5,X0,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f2])).
% 55.61/7.57 fof(f121,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,X5,X2,X6)|s(X0,X1,truck1,X3,X4,X5,X2,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f9])).
% 55.61/7.57 fof(f122,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (s(X0,X1,X2,X3,X4,X5,X2,X6)|~s(X0,X1,truck1,X3,X4,X5,X2,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f10])).
% 55.61/7.57 fof(f125,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,X5,X3,X6)|s(X0,X1,X2,truck1,X4,X5,X3,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f13])).
% 55.61/7.57 fof(f126,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (s(X0,X1,X2,X3,X4,X5,X3,X6)|~s(X0,X1,X2,truck1,X4,X5,X3,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f14])).
% 55.61/7.57 fof(f133,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,X5,X5,X6)|~neq(X4,truck1)|s(X0,X1,X2,X3,X4,truck1,X5,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f21])).
% 55.61/7.57 fof(f141,plain,(
% 55.61/7.57 ![O1,O2,O3,O4,D1,T2,D]: ((![S]: (~s(O1,O2,O3,O4,D1,truck1,S,T2)|~link(S,D)))|s(O1,O2,O3,O4,D1,truck1,D,T2))),
% 55.61/7.57 inference(miniscoping,[status(thm)],[f27])).
% 55.61/7.57 fof(f142,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~s(X0,X1,X2,X3,X4,truck1,X5,X6)|~link(X5,X7)|s(X0,X1,X2,X3,X4,truck1,X7,X6))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f141])).
% 55.61/7.57 fof(f145,plain,(
% 55.61/7.57 ![O1,O2,O3,O4,D2,T1,T2,D]: ((![S]: (~s(O1,O2,O3,O4,S,D2,T1,T2)|~path(S,D)))|s(O1,O2,O3,O4,D,D2,T1,T2))),
% 55.61/7.57 inference(miniscoping,[status(thm)],[f29])).
% 55.61/7.57 fof(f146,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~s(X0,X1,X2,X3,X4,X5,X6,X7)|~path(X4,X8)|s(X0,X1,X2,X3,X8,X5,X6,X7))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f145])).
% 55.61/7.57 fof(f147,plain,(
% 55.61/7.57 ![O1,O2,O3,O4,D1,T1,T2,D]: ((![S]: (~s(O1,O2,O3,O4,D1,S,T1,T2)|~path(S,D)))|s(O1,O2,O3,O4,D1,D,T1,T2))),
% 55.61/7.57 inference(miniscoping,[status(thm)],[f30])).
% 55.61/7.57 fof(f148,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~s(X0,X1,X2,X3,X4,X5,X6,X7)|~path(X5,X8)|s(X0,X1,X2,X3,X4,X8,X6,X7))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f147])).
% 55.61/7.57 fof(f181,plain,(
% 55.61/7.57 neq(s2,truck1)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f63])).
% 55.61/7.57 fof(f213,plain,(
% 55.61/7.57 path(s0,p0_1)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f95])).
% 55.61/7.57 fof(f216,plain,(
% 55.61/7.57 path(p0_1,s1)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f98])).
% 55.61/7.57 fof(f218,plain,(
% 55.61/7.57 path(p1_2,s1)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f100])).
% 55.61/7.57 fof(f219,plain,(
% 55.61/7.57 path(s2,p1_2)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f101])).
% 55.61/7.57 fof(f225,plain,(
% 55.61/7.57 link(s1,s2)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f107])).
% 55.61/7.57 fof(f227,plain,(
% 55.61/7.57 link(s2,s0)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f109])).
% 55.61/7.57 fof(f228,plain,(
% 55.61/7.57 link(s0,s2)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f110])).
% 55.61/7.57 fof(f229,plain,(
% 55.61/7.57 s(s1,s2,s2,s0,s2,s0,s1,s1)),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f111])).
% 55.61/7.57 fof(f230,plain,(
% 55.61/7.57 ![X0,X1]: (~s(s2,s2,s0,s2,s1,X0,s0,X1))),
% 55.61/7.57 inference(cnf_transformation,[status(thm)],[f112])).
% 55.61/7.57 fof(f232,plain,(
% 55.61/7.57 s(truck1,s2,s2,s0,s2,s0,s1,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f229,f113])).
% 55.61/7.57 fof(f243,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,s2,X4,X4,X5)|s(X0,X1,X2,X3,s2,truck1,X4,X5))),
% 55.61/7.57 inference(resolution,[status(thm)],[f133,f181])).
% 55.61/7.57 fof(f263,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,s0,X5,X6)|s(X0,X1,X2,X3,X4,p0_1,X5,X6))),
% 55.61/7.57 inference(resolution,[status(thm)],[f213,f148])).
% 55.61/7.57 fof(f269,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,p0_1,X5,X6)|s(X0,X1,X2,X3,X4,s1,X5,X6))),
% 55.61/7.57 inference(resolution,[status(thm)],[f216,f148])).
% 55.61/7.57 fof(f274,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,p1_2,X4,X5,X6)|s(X0,X1,X2,X3,s1,X4,X5,X6))),
% 55.61/7.57 inference(resolution,[status(thm)],[f218,f146])).
% 55.61/7.57 fof(f276,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,s2,X4,X5,X6)|s(X0,X1,X2,X3,p1_2,X4,X5,X6))),
% 55.61/7.57 inference(resolution,[status(thm)],[f219,f146])).
% 55.61/7.57 fof(f288,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,X4,truck1,s1,X5)|s(X0,X1,X2,X3,X4,truck1,s2,X5))),
% 55.61/7.57 inference(resolution,[status(thm)],[f225,f142])).
% 55.61/7.57 fof(f296,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,X4,truck1,s2,X5)|s(X0,X1,X2,X3,X4,truck1,s0,X5))),
% 55.61/7.57 inference(resolution,[status(thm)],[f227,f142])).
% 55.61/7.57 fof(f300,plain,(
% 55.61/7.57 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,X4,truck1,s0,X5)|s(X0,X1,X2,X3,X4,truck1,s2,X5))),
% 55.61/7.57 inference(resolution,[status(thm)],[f228,f142])).
% 55.61/7.57 fof(f303,plain,(
% 55.61/7.57 s(truck1,s2,s2,s0,s2,p0_1,s1,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f263,f232])).
% 55.61/7.57 fof(f313,plain,(
% 55.61/7.57 s(truck1,s2,s2,s0,s2,s1,s1,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f269,f303])).
% 55.61/7.57 fof(f318,plain,(
% 55.61/7.57 s(truck1,s2,s2,s0,s2,truck1,s1,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f313,f243])).
% 55.61/7.57 fof(f354,plain,(
% 55.61/7.57 s(truck1,s2,s2,s0,p1_2,truck1,s1,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f276,f318])).
% 55.61/7.57 fof(f402,plain,(
% 55.61/7.57 s(truck1,s2,s2,s0,s1,truck1,s1,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f354,f274])).
% 55.61/7.57 fof(f658,plain,(
% 55.61/7.57 s(truck1,s2,s2,s0,s1,truck1,s2,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f402,f288])).
% 55.61/7.57 fof(f1180,plain,(
% 55.61/7.57 s(s2,s2,s2,s0,s1,truck1,s2,s1)),
% 55.61/7.57 inference(resolution,[status(thm)],[f658,f114])).
% 8.59/7.79 fof(f2415,plain,(
% 8.59/7.79 s(s2,s2,s2,s0,s1,truck1,s0,s1)),
% 8.59/7.79 inference(resolution,[status(thm)],[f1180,f296])).
% 8.59/7.79 fof(f5478,plain,(
% 8.59/7.79 s(s2,s2,s2,truck1,s1,truck1,s0,s1)),
% 8.59/7.79 inference(resolution,[status(thm)],[f2415,f125])).
% 8.59/7.79 fof(f13153,plain,(
% 8.59/7.79 s(s2,s2,s2,truck1,s1,truck1,s2,s1)),
% 8.59/7.79 inference(resolution,[status(thm)],[f5478,f300])).
% 8.59/7.79 fof(f29710,plain,(
% 8.59/7.79 s(s2,s2,s2,s2,s1,truck1,s2,s1)),
% 8.59/7.79 inference(resolution,[status(thm)],[f13153,f126])).
% 8.59/7.79 fof(f61888,plain,(
% 8.59/7.79 s(s2,s2,truck1,s2,s1,truck1,s2,s1)),
% 8.59/7.79 inference(resolution,[status(thm)],[f29710,f121])).
% 8.59/7.79 fof(f118762,plain,(
% 8.59/7.79 s(s2,s2,truck1,s2,s1,truck1,s0,s1)),
% 8.59/7.79 inference(resolution,[status(thm)],[f61888,f296])).
% 8.59/7.79 fof(f213680,plain,(
% 8.59/7.79 s(s2,s2,s0,s2,s1,truck1,s0,s1)),
% 8.59/7.79 inference(resolution,[status(thm)],[f118762,f122])).
% 8.59/7.79 fof(f213686,plain,(
% 8.59/7.79 $false),
% 8.59/7.79 inference(forward_subsumption_resolution,[status(thm)],[f213680,f230])).
% 8.59/7.79 % SZS output end CNFRefutation for theBenchmark.p
% 8.59/7.82 % Elapsed time: 7.320301 seconds
% 8.59/7.82 % CPU time: 56.671499 seconds
% 8.59/7.82 % Total memory used: 528.223 MB
% 8.59/7.82 % Net memory used: 479.081 MB
%------------------------------------------------------------------------------