%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 01:58:43 PM UTC 2026
% Result : Unsatisfiable 4.57s 1.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.47 % Computer : n014.cluster.edu
% 0.16/0.47 % Model : x86_64 x86_64
% 0.16/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.47 % Memory : 8046.5625MB
% 0.16/0.47 % OS : Linux 6.8.0-71-generic
% 0.16/0.47 % CPULimit : 300
% 0.16/0.47 % WCLimit : 300
% 0.16/0.47 % DateTime : Mon Sep 21 03:33:20 UTC 2026
% 0.16/0.48 % CPUTime :
% 0.16/0.51 % Drodi V4.1.1
% 4.57/1.62 % Refutation found
% 4.57/1.62 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.57/1.62 % SZS output start CNFRefutation for theBenchmark
% 4.57/1.62 fof(f7,axiom,(
% 4.57/1.62 (![O1,L,D1,D2,T1]: (( ~ s(O1,L,D1,D2,T1,L)| s(O1,truck2,D1,D2,T1,L) ) ))),
% 4.57/1.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.62 fof(f8,axiom,(
% 4.57/1.62 (![O1,L,D1,D2,T1]: (( s(O1,L,D1,D2,T1,L)| ~ s(O1,truck2,D1,D2,T1,L) ) ))),
% 4.57/1.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.62 fof(f13,axiom,(
% 4.57/1.62 (![O1,O2,D1,L,T2]: (( ~ s(O1,O2,D1,L,L,T2)| ~ neq(D1,truck1)| s(O1,O2,D1,truck1,L,T2) ) ))),
% 4.57/1.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.62 fof(f14,axiom,(
% 4.57/1.62 (![O1,O2,D1,L,T2]: (( s(O1,O2,D1,L,L,T2)| ~ s(O1,O2,D1,truck1,L,T2) ) ))),
% 4.57/1.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.62 fof(f15,axiom,(
% 4.57/1.62 (![O1,O2,D1,L,T1]: (( ~ s(O1,O2,D1,L,T1,L)| ~ neq(D1,truck2)| s(O1,O2,D1,truck2,T1,L) ) ))),
% 4.57/1.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.62 fof(f16,axiom,(
% 4.57/1.62 (![O1,O2,D1,L,T1]: (( s(O1,O2,D1,L,T1,L)| ~ s(O1,O2,D1,truck2,T1,L) ) ))),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f19,axiom,(
% 4.57/1.63 (![O1,O2,D1,S,T2,D]: (( ~ s(O1,O2,D1,truck1,S,T2)| ~ link(S,D)| s(O1,O2,D1,truck1,D,T2) ) ))),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f20,axiom,(
% 4.57/1.63 (![O1,O2,D1,T1,S,D]: (( ~ s(O1,O2,D1,truck2,T1,S)| ~ link(S,D)| s(O1,O2,D1,truck2,T1,D) ) ))),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f21,axiom,(
% 4.57/1.63 (![O1,O2,S,D2,T1,T2,D]: (( ~ s(O1,O2,S,D2,T1,T2)| ~ path(S,D)| s(O1,O2,D,D2,T1,T2) ) ))),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f22,axiom,(
% 4.57/1.63 (![O1,O2,D1,S,T1,T2,D]: (( ~ s(O1,O2,D1,S,T1,T2)| ~ path(S,D)| s(O1,O2,D1,D,T1,T2) ) ))),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f55,axiom,(
% 4.57/1.63 neq(s2,truck1) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f56,axiom,(
% 4.57/1.63 neq(s2,truck2) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f92,axiom,(
% 4.57/1.63 path(p2_0,s2) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f93,axiom,(
% 4.57/1.63 path(s0,p2_0) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f96,axiom,(
% 4.57/1.63 path(p2_1,s2) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f97,axiom,(
% 4.57/1.63 path(s1,p2_1) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f100,axiom,(
% 4.57/1.63 link(s1,s0) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f101,axiom,(
% 4.57/1.63 link(s0,s2) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f104,axiom,(
% 4.57/1.63 link(s2,s1) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f105,axiom,(
% 4.57/1.63 s(s2,s2,s0,s1,s0,s2) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f106,negated_conjecture,(
% 4.57/1.63 ~ s(s2,s1,s2,s2,s2,s0) ),
% 4.57/1.63 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.57/1.63 fof(f113,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,X3,X4,X1)|s(X0,truck2,X2,X3,X4,X1))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f7])).
% 4.57/1.63 fof(f114,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (s(X0,X1,X2,X3,X4,X1)|~s(X0,truck2,X2,X3,X4,X1))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f8])).
% 4.57/1.63 fof(f119,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,X3,X3,X4)|~neq(X2,truck1)|s(X0,X1,X2,truck1,X3,X4))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f13])).
% 4.57/1.63 fof(f120,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (s(X0,X1,X2,X3,X3,X4)|~s(X0,X1,X2,truck1,X3,X4))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f14])).
% 4.57/1.63 fof(f121,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,X3,X4,X3)|~neq(X2,truck2)|s(X0,X1,X2,truck2,X4,X3))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f15])).
% 4.57/1.63 fof(f122,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (s(X0,X1,X2,X3,X4,X3)|~s(X0,X1,X2,truck2,X4,X3))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f16])).
% 4.57/1.63 fof(f127,plain,(
% 4.57/1.63 ![O1,O2,D1,T2,D]: ((![S]: (~s(O1,O2,D1,truck1,S,T2)|~link(S,D)))|s(O1,O2,D1,truck1,D,T2))),
% 4.57/1.63 inference(miniscoping,[status(thm)],[f19])).
% 4.57/1.63 fof(f128,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,truck1,X3,X4)|~link(X3,X5)|s(X0,X1,X2,truck1,X5,X4))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f127])).
% 4.57/1.63 fof(f129,plain,(
% 4.57/1.63 ![O1,O2,D1,T1,D]: ((![S]: (~s(O1,O2,D1,truck2,T1,S)|~link(S,D)))|s(O1,O2,D1,truck2,T1,D))),
% 4.57/1.63 inference(miniscoping,[status(thm)],[f20])).
% 4.57/1.63 fof(f130,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4,X5]: (~s(X0,X1,X2,truck2,X3,X4)|~link(X4,X5)|s(X0,X1,X2,truck2,X3,X5))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f129])).
% 4.57/1.63 fof(f131,plain,(
% 4.57/1.63 ![O1,O2,D2,T1,T2,D]: ((![S]: (~s(O1,O2,S,D2,T1,T2)|~path(S,D)))|s(O1,O2,D,D2,T1,T2))),
% 4.57/1.63 inference(miniscoping,[status(thm)],[f21])).
% 4.57/1.63 fof(f132,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,X5)|~path(X2,X6)|s(X0,X1,X6,X3,X4,X5))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f131])).
% 4.57/1.63 fof(f133,plain,(
% 4.57/1.63 ![O1,O2,D1,T1,T2,D]: ((![S]: (~s(O1,O2,D1,S,T1,T2)|~path(S,D)))|s(O1,O2,D1,D,T1,T2))),
% 4.57/1.63 inference(miniscoping,[status(thm)],[f22])).
% 4.57/1.63 fof(f134,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4,X5,X6]: (~s(X0,X1,X2,X3,X4,X5)|~path(X3,X6)|s(X0,X1,X2,X6,X4,X5))),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f133])).
% 4.57/1.63 fof(f167,plain,(
% 4.57/1.63 neq(s2,truck1)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f55])).
% 4.57/1.63 fof(f168,plain,(
% 4.57/1.63 neq(s2,truck2)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f56])).
% 4.57/1.63 fof(f204,plain,(
% 4.57/1.63 path(p2_0,s2)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f92])).
% 4.57/1.63 fof(f205,plain,(
% 4.57/1.63 path(s0,p2_0)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f93])).
% 4.57/1.63 fof(f208,plain,(
% 4.57/1.63 path(p2_1,s2)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f96])).
% 4.57/1.63 fof(f209,plain,(
% 4.57/1.63 path(s1,p2_1)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f97])).
% 4.57/1.63 fof(f212,plain,(
% 4.57/1.63 link(s1,s0)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f100])).
% 4.57/1.63 fof(f213,plain,(
% 4.57/1.63 link(s0,s2)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f101])).
% 4.57/1.63 fof(f216,plain,(
% 4.57/1.63 link(s2,s1)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f104])).
% 4.57/1.63 fof(f217,plain,(
% 4.57/1.63 s(s2,s2,s0,s1,s0,s2)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f105])).
% 4.57/1.63 fof(f218,plain,(
% 4.57/1.63 ~s(s2,s1,s2,s2,s2,s0)),
% 4.57/1.63 inference(cnf_transformation,[status(thm)],[f106])).
% 4.57/1.63 fof(f224,plain,(
% 4.57/1.63 s(s2,truck2,s0,s1,s0,s2)),
% 4.57/1.63 inference(resolution,[status(thm)],[f217,f113])).
% 4.57/1.63 fof(f255,plain,(
% 4.57/1.63 ![X0,X1,X2,X3]: (~s(X0,X1,s2,X2,X2,X3)|s(X0,X1,s2,truck1,X2,X3))),
% 4.57/1.63 inference(resolution,[status(thm)],[f167,f119])).
% 4.57/1.63 fof(f257,plain,(
% 4.57/1.63 ![X0,X1,X2,X3]: (~s(X0,X1,s2,X2,X3,X2)|s(X0,X1,s2,truck2,X3,X2))),
% 4.57/1.63 inference(resolution,[status(thm)],[f168,f121])).
% 4.57/1.63 fof(f282,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (~s(X0,X1,p2_0,X2,X3,X4)|s(X0,X1,s2,X2,X3,X4))),
% 4.57/1.63 inference(resolution,[status(thm)],[f204,f132])).
% 4.57/1.63 fof(f284,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (~s(X0,X1,s0,X2,X3,X4)|s(X0,X1,p2_0,X2,X3,X4))),
% 4.57/1.63 inference(resolution,[status(thm)],[f205,f132])).
% 4.57/1.63 fof(f289,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,p2_1,X3,X4)|s(X0,X1,X2,s2,X3,X4))),
% 4.57/1.63 inference(resolution,[status(thm)],[f208,f134])).
% 4.57/1.63 fof(f291,plain,(
% 4.57/1.63 ![X0,X1,X2,X3,X4]: (~s(X0,X1,X2,s1,X3,X4)|s(X0,X1,X2,p2_1,X3,X4))),
% 4.57/1.63 inference(resolution,[status(thm)],[f209,f134])).
% 4.57/1.63 fof(f299,plain,(
% 4.57/1.63 ![X0,X1,X2,X3]: (~s(X0,X1,X2,truck2,X3,s1)|s(X0,X1,X2,truck2,X3,s0))),
% 4.57/1.63 inference(resolution,[status(thm)],[f212,f130])).
% 4.57/1.63 fof(f304,plain,(
% 4.57/1.63 ![X0,X1,X2,X3]: (~s(X0,X1,X2,truck1,s0,X3)|s(X0,X1,X2,truck1,s2,X3))),
% 4.57/1.63 inference(resolution,[status(thm)],[f213,f128])).
% 4.57/1.63 fof(f315,plain,(
% 4.57/1.63 ![X0,X1,X2,X3]: (~s(X0,X1,X2,truck2,X3,s2)|s(X0,X1,X2,truck2,X3,s1))),
% 4.57/1.63 inference(resolution,[status(thm)],[f216,f130])).
% 4.57/1.63 fof(f437,plain,(
% 4.57/1.63 s(s2,truck2,p2_0,s1,s0,s2)),
% 4.57/1.63 inference(resolution,[status(thm)],[f284,f224])).
% 4.57/1.63 fof(f449,plain,(
% 4.57/1.63 s(s2,truck2,s2,s1,s0,s2)),
% 4.57/1.63 inference(resolution,[status(thm)],[f437,f282])).
% 4.57/1.63 fof(f652,plain,(
% 4.57/1.63 s(s2,truck2,s2,p2_1,s0,s2)),
% 4.57/1.63 inference(resolution,[status(thm)],[f449,f291])).
% 4.57/1.63 fof(f1068,plain,(
% 4.57/1.63 s(s2,truck2,s2,s2,s0,s2)),
% 4.57/1.63 inference(resolution,[status(thm)],[f652,f289])).
% 4.57/1.63 fof(f1920,plain,(
% 4.57/1.63 s(s2,truck2,s2,truck2,s0,s2)),
% 4.57/1.63 inference(resolution,[status(thm)],[f1068,f257])).
% 4.57/1.63 fof(f3337,plain,(
% 4.57/1.63 s(s2,truck2,s2,truck2,s0,s1)),
% 4.57/1.63 inference(resolution,[status(thm)],[f1920,f315])).
% 4.57/1.63 fof(f5991,plain,(
% 4.57/1.63 s(s2,s1,s2,truck2,s0,s1)),
% 4.57/1.63 inference(resolution,[status(thm)],[f3337,f114])).
% 4.57/1.63 fof(f10903,plain,(
% 4.57/1.63 s(s2,s1,s2,truck2,s0,s0)),
% 4.57/1.63 inference(resolution,[status(thm)],[f5991,f299])).
% 3.62/1.70 fof(f19373,plain,(
% 3.62/1.70 s(s2,s1,s2,s0,s0,s0)),
% 3.62/1.70 inference(resolution,[status(thm)],[f10903,f122])).
% 3.62/1.70 fof(f32332,plain,(
% 3.62/1.70 s(s2,s1,s2,truck1,s0,s0)),
% 3.62/1.70 inference(resolution,[status(thm)],[f19373,f255])).
% 3.62/1.70 fof(f48548,plain,(
% 3.62/1.70 s(s2,s1,s2,truck1,s2,s0)),
% 3.62/1.70 inference(resolution,[status(thm)],[f32332,f304])).
% 3.62/1.70 fof(f64530,plain,(
% 3.62/1.70 s(s2,s1,s2,s2,s2,s0)),
% 3.62/1.70 inference(resolution,[status(thm)],[f48548,f120])).
% 3.62/1.70 fof(f64532,plain,(
% 3.62/1.70 $false),
% 3.62/1.70 inference(forward_subsumption_resolution,[status(thm)],[f64530,f218])).
% 3.62/1.70 % SZS output end CNFRefutation for theBenchmark.p
% 3.62/1.71 % Elapsed time: 1.205829 seconds
% 3.62/1.71 % CPU time: 8.976699 seconds
% 3.62/1.71 % Total memory used: 157.614 MB
% 3.62/1.71 % Net memory used: 149.407 MB
%------------------------------------------------------------------------------