%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PLA031-1.002 : 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 : n026.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 0.18s 5.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA031-1.002 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.41 % Computer : n026.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Mon Sep 21 03:36:12 UTC 2026
% 0.14/5.42 % CPUTime :
% 0.14/5.43 % Drodi V4.1.1
% 0.18/5.91 % Refutation found
% 0.18/5.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.18/5.91 % SZS output start CNFRefutation for theBenchmark
% 0.18/5.91 fof(f3,axiom,(
% 0.18/5.91 (![L,O2,O3,D1,D2,T1]: (( ~ s(L,O2,O3,D1,D2,T1,L)| s(truck2,O2,O3,D1,D2,T1,L) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f4,axiom,(
% 0.18/5.91 (![L,O2,O3,D1,D2,T1]: (( s(L,O2,O3,D1,D2,T1,L)| ~ s(truck2,O2,O3,D1,D2,T1,L) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f7,axiom,(
% 0.18/5.91 (![O1,L,O3,D1,D2,T1]: (( ~ s(O1,L,O3,D1,D2,T1,L)| s(O1,truck2,O3,D1,D2,T1,L) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f8,axiom,(
% 0.18/5.91 (![O1,L,O3,D1,D2,T1]: (( s(O1,L,O3,D1,D2,T1,L)| ~ s(O1,truck2,O3,D1,D2,T1,L) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f11,axiom,(
% 0.18/5.91 (![O1,O2,L,D1,D2,T1]: (( ~ s(O1,O2,L,D1,D2,T1,L)| s(O1,O2,truck2,D1,D2,T1,L) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f12,axiom,(
% 0.18/5.91 (![O1,O2,L,D1,D2,T1]: (( s(O1,O2,L,D1,D2,T1,L)| ~ s(O1,O2,truck2,D1,D2,T1,L) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f19,axiom,(
% 0.18/5.91 (![O1,O2,O3,D1,L,T1]: (( ~ s(O1,O2,O3,D1,L,T1,L)| ~ neq(D1,truck2)| s(O1,O2,O3,D1,truck2,T1,L) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f24,axiom,(
% 0.18/5.91 (![O1,O2,O3,D1,T1,S,D]: (( ~ s(O1,O2,O3,D1,truck2,T1,S)| ~ link(S,D)| s(O1,O2,O3,D1,truck2,T1,D) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f25,axiom,(
% 0.18/5.91 (![O1,O2,O3,S,D2,T1,T2,D]: (( ~ s(O1,O2,O3,S,D2,T1,T2)| ~ path(S,D)| s(O1,O2,O3,D,D2,T1,T2) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f26,axiom,(
% 0.18/5.91 (![O1,O2,O3,D1,S,T1,T2,D]: (( ~ s(O1,O2,O3,D1,S,T1,T2)| ~ path(S,D)| s(O1,O2,O3,D1,D,T1,T2) ) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f56,axiom,(
% 0.18/5.91 neq(s2,truck2) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f76,axiom,(
% 0.18/5.91 path(s1,p1_0) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f79,axiom,(
% 0.18/5.91 path(p1_0,s0) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f81,axiom,(
% 0.18/5.91 path(p2_1,s2) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f82,axiom,(
% 0.18/5.91 path(s1,p2_1) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f84,axiom,(
% 0.18/5.91 link(s0,s1) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f85,axiom,(
% 0.18/5.91 link(s1,s0) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f86,axiom,(
% 0.18/5.91 link(s1,s2) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f87,axiom,(
% 0.18/5.91 link(s2,s1) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f90,axiom,(
% 0.18/5.91 s(s1,s1,s1,s1,s1,s2,s0) ),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f91,negated_conjecture,(
% 0.18/5.91 (![X5,X7]: (~ s(s0,s0,s2,s2,X5,s2,X7) ))),
% 0.18/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/5.91 fof(f94,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,X4,X5,X0)|s(truck2,X1,X2,X3,X4,X5,X0))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f3])).
% 0.18/5.91 fof(f95,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (s(X0,X1,X2,X3,X4,X5,X0)|~s(truck2,X1,X2,X3,X4,X5,X0))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f4])).
% 0.18/5.91 fof(f98,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,X4,X5,X1)|s(X0,truck2,X2,X3,X4,X5,X1))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f7])).
% 0.18/5.91 fof(f99,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (s(X0,X1,X2,X3,X4,X5,X1)|~s(X0,truck2,X2,X3,X4,X5,X1))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f8])).
% 0.18/5.91 fof(f102,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,X4,X5,X2)|s(X0,X1,truck2,X3,X4,X5,X2))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f11])).
% 0.18/5.91 fof(f103,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (s(X0,X1,X2,X3,X4,X5,X2)|~s(X0,X1,truck2,X3,X4,X5,X2))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f12])).
% 0.18/5.91 fof(f110,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,X4,X5,X4)|~neq(X3,truck2)|s(X0,X1,X2,X3,truck2,X5,X4))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f19])).
% 0.18/5.91 fof(f118,plain,(
% 0.18/5.91 ![O1,O2,O3,D1,T1,D]: ((![S]: (~s(O1,O2,O3,D1,truck2,T1,S)|~link(S,D)))|s(O1,O2,O3,D1,truck2,T1,D))),
% 0.18/5.91 inference(miniscoping,[status(thm)],[f24])).
% 0.18/5.91 fof(f119,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,truck2,X4,X5)|~link(X5,X6)|s(X0,X1,X2,X3,truck2,X4,X6))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f118])).
% 0.18/5.91 fof(f120,plain,(
% 0.18/5.91 ![O1,O2,O3,D2,T1,T2,D]: ((![S]: (~s(O1,O2,O3,S,D2,T1,T2)|~path(S,D)))|s(O1,O2,O3,D,D2,T1,T2))),
% 0.18/5.91 inference(miniscoping,[status(thm)],[f25])).
% 0.18/5.91 fof(f121,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~s(X0,X1,X2,X3,X4,X5,X6)|~path(X3,X7)|s(X0,X1,X2,X7,X4,X5,X6))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f120])).
% 0.18/5.91 fof(f122,plain,(
% 0.18/5.91 ![O1,O2,O3,D1,T1,T2,D]: ((![S]: (~s(O1,O2,O3,D1,S,T1,T2)|~path(S,D)))|s(O1,O2,O3,D1,D,T1,T2))),
% 0.18/5.91 inference(miniscoping,[status(thm)],[f26])).
% 0.18/5.91 fof(f123,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~s(X0,X1,X2,X3,X4,X5,X6)|~path(X4,X7)|s(X0,X1,X2,X3,X7,X5,X6))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f122])).
% 0.18/5.91 fof(f153,plain,(
% 0.18/5.91 neq(s2,truck2)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f56])).
% 0.18/5.91 fof(f173,plain,(
% 0.18/5.91 path(s1,p1_0)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f76])).
% 0.18/5.91 fof(f176,plain,(
% 0.18/5.91 path(p1_0,s0)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f79])).
% 0.18/5.91 fof(f178,plain,(
% 0.18/5.91 path(p2_1,s2)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f81])).
% 0.18/5.91 fof(f179,plain,(
% 0.18/5.91 path(s1,p2_1)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f82])).
% 0.18/5.91 fof(f181,plain,(
% 0.18/5.91 link(s0,s1)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f84])).
% 0.18/5.91 fof(f182,plain,(
% 0.18/5.91 link(s1,s0)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f85])).
% 0.18/5.91 fof(f183,plain,(
% 0.18/5.91 link(s1,s2)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f86])).
% 0.18/5.91 fof(f184,plain,(
% 0.18/5.91 link(s2,s1)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f87])).
% 0.18/5.91 fof(f187,plain,(
% 0.18/5.91 s(s1,s1,s1,s1,s1,s2,s0)),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f90])).
% 0.18/5.91 fof(f188,plain,(
% 0.18/5.91 ![X0,X1]: (~s(s0,s0,s2,s2,X0,s2,X1))),
% 0.18/5.91 inference(cnf_transformation,[status(thm)],[f91])).
% 0.18/5.91 fof(f195,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,p2_1,X3,X4,X5)|s(X0,X1,X2,s2,X3,X4,X5))),
% 0.18/5.91 inference(resolution,[status(thm)],[f121,f178])).
% 0.18/5.91 fof(f201,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,p1_0,X4,X5)|s(X0,X1,X2,X3,s0,X4,X5))),
% 0.18/5.91 inference(resolution,[status(thm)],[f123,f176])).
% 0.18/5.91 fof(f203,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,s2,X3,X4,X3)|s(X0,X1,X2,s2,truck2,X4,X3))),
% 0.18/5.91 inference(resolution,[status(thm)],[f110,f153])).
% 0.18/5.91 fof(f228,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,X3,truck2,X4,s2)|s(X0,X1,X2,X3,truck2,X4,s1))),
% 0.18/5.91 inference(resolution,[status(thm)],[f119,f184])).
% 0.18/5.91 fof(f229,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,X3,truck2,X4,s1)|s(X0,X1,X2,X3,truck2,X4,s2))),
% 0.18/5.91 inference(resolution,[status(thm)],[f119,f183])).
% 0.18/5.91 fof(f230,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,X3,truck2,X4,s1)|s(X0,X1,X2,X3,truck2,X4,s0))),
% 0.18/5.91 inference(resolution,[status(thm)],[f119,f182])).
% 0.18/5.91 fof(f232,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,X3,truck2,X4,s0)|s(X0,X1,X2,X3,truck2,X4,s1))),
% 0.18/5.91 inference(resolution,[status(thm)],[f119,f181])).
% 0.18/5.91 fof(f245,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,X3,s1,X4,X5)|s(X0,X1,X2,X3,p1_0,X4,X5))),
% 0.18/5.91 inference(resolution,[status(thm)],[f173,f123])).
% 0.18/5.91 fof(f247,plain,(
% 0.18/5.91 s(s1,s1,s1,s1,p1_0,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f245,f187])).
% 0.18/5.91 fof(f252,plain,(
% 0.18/5.91 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,s1,X3,X4,X5)|s(X0,X1,X2,p2_1,X3,X4,X5))),
% 0.18/5.91 inference(resolution,[status(thm)],[f179,f121])).
% 0.18/5.91 fof(f260,plain,(
% 0.18/5.91 s(s1,s1,s1,s1,s0,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f247,f201])).
% 0.18/5.91 fof(f261,plain,(
% 0.18/5.91 s(s1,s1,s1,p2_1,s0,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f260,f252])).
% 0.18/5.91 fof(f298,plain,(
% 0.18/5.91 s(s1,s1,s1,s2,s0,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f261,f195])).
% 0.18/5.91 fof(f300,plain,(
% 0.18/5.91 s(s1,s1,s1,s2,truck2,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f298,f203])).
% 0.18/5.91 fof(f305,plain,(
% 0.18/5.91 s(s1,s1,s1,s2,truck2,s2,s1)),
% 0.18/5.91 inference(resolution,[status(thm)],[f300,f232])).
% 0.18/5.91 fof(f571,plain,(
% 0.18/5.91 s(s1,s1,truck2,s2,truck2,s2,s1)),
% 0.18/5.91 inference(resolution,[status(thm)],[f305,f102])).
% 0.18/5.91 fof(f1109,plain,(
% 0.18/5.91 s(s1,s1,truck2,s2,truck2,s2,s2)),
% 0.18/5.91 inference(resolution,[status(thm)],[f571,f229])).
% 0.18/5.91 fof(f1120,plain,(
% 0.18/5.91 s(s1,s1,s2,s2,truck2,s2,s2)),
% 0.18/5.91 inference(resolution,[status(thm)],[f1109,f103])).
% 0.18/5.91 fof(f1138,plain,(
% 0.18/5.91 s(s1,s1,s2,s2,truck2,s2,s1)),
% 0.18/5.91 inference(resolution,[status(thm)],[f1120,f228])).
% 0.18/5.91 fof(f1204,plain,(
% 0.18/5.91 s(s1,truck2,s2,s2,truck2,s2,s1)),
% 0.18/5.91 inference(resolution,[status(thm)],[f1138,f98])).
% 0.18/5.91 fof(f1352,plain,(
% 0.18/5.91 s(truck2,truck2,s2,s2,truck2,s2,s1)),
% 0.18/5.91 inference(resolution,[status(thm)],[f1204,f94])).
% 0.18/5.91 fof(f1604,plain,(
% 0.18/5.91 s(truck2,truck2,s2,s2,truck2,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f1352,f230])).
% 0.18/5.91 fof(f2161,plain,(
% 0.18/5.91 s(s0,truck2,s2,s2,truck2,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f1604,f95])).
% 0.18/5.91 fof(f3312,plain,(
% 0.18/5.91 s(s0,s0,s2,s2,truck2,s2,s0)),
% 0.18/5.91 inference(resolution,[status(thm)],[f2161,f99])).
% 0.18/5.91 fof(f3320,plain,(
% 0.18/5.91 $false),
% 0.18/5.91 inference(forward_subsumption_resolution,[status(thm)],[f3312,f188])).
% 0.18/5.91 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/5.95 % Elapsed time: 0.519344 seconds
% 0.18/5.95 % CPU time: 3.678161 seconds
% 0.18/5.95 % Total memory used: 93.148 MB
% 0.18/5.95 % Net memory used: 91.319 MB
%------------------------------------------------------------------------------