%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : PLA031-1.002 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 : Sun Sep 27 08:20:08 AM UTC 2026
% Result : Unsatisfiable 26.47s 21.04s
% Output : CNFRefutation 26.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 20
% Syntax : Number of clauses : 62 ( 25 unt; 0 nHn; 62 RR)
% Number of literals : 107 ( 0 equ; 48 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-7 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 164 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(load1,axiom,
( s(truck1,X1,X2,X3,X4,X0,X5)
| ~ s(X0,X1,X2,X3,X4,X0,X5) ) ).
cnf(load2,axiom,
( ~ s(truck1,X1,X2,X3,X4,X0,X5)
| s(X0,X1,X2,X3,X4,X0,X5) ) ).
cnf(load3,axiom,
( s(truck2,X1,X2,X3,X4,X5,X0)
| ~ s(X0,X1,X2,X3,X4,X5,X0) ) ).
cnf(load4,axiom,
( ~ s(truck2,X1,X2,X3,X4,X5,X0)
| s(X0,X1,X2,X3,X4,X5,X0) ) ).
cnf(load5,axiom,
( s(X0,truck1,X2,X3,X4,X1,X5)
| ~ s(X0,X1,X2,X3,X4,X1,X5) ) ).
cnf(load6,axiom,
( ~ s(X0,truck1,X2,X3,X4,X1,X5)
| s(X0,X1,X2,X3,X4,X1,X5) ) ).
cnf(load9,axiom,
( s(X0,X1,truck1,X3,X4,X2,X5)
| ~ s(X0,X1,X2,X3,X4,X2,X5) ) ).
cnf(load10,axiom,
( ~ s(X0,X1,truck1,X3,X4,X2,X5)
| s(X0,X1,X2,X3,X4,X2,X5) ) ).
cnf(board1,axiom,
( s(X0,X1,X2,truck1,X4,X3,X5)
| ~ neq(X4,truck1)
| ~ s(X0,X1,X2,X3,X4,X3,X5) ) ).
cnf(board2,axiom,
( ~ s(X0,X1,X2,truck1,X4,X3,X5)
| s(X0,X1,X2,X3,X4,X3,X5) ) ).
cnf(drive1,axiom,
( s(X0,X1,X2,truck1,X3,X6,X5)
| ~ link(X4,X6)
| ~ s(X0,X1,X2,truck1,X3,X4,X5) ) ).
cnf(walk1,axiom,
( s(X0,X1,X2,X7,X4,X5,X6)
| ~ path(X3,X7)
| ~ s(X0,X1,X2,X3,X4,X5,X6) ) ).
cnf(neq22,axiom,
neq(s1,truck1) ).
cnf(map6,axiom,
path('p2$u1',s2) ).
cnf(map7,axiom,
path(s1,'p2$u1') ).
cnf(map10,axiom,
link(s1,s0) ).
cnf(map12,axiom,
link(s2,s1) ).
cnf(map14,axiom,
link(s0,s2) ).
cnf(init,axiom,
s(s1,s1,s1,s1,s1,s2,s0) ).
cnf(goal,negated_conjecture,
~ s(s0,s0,s2,s2,X0,s2,X1) ).
cnf(c0,plain,
( s(truck1,X1,X2,X3,X4,X0,X5)
| ~ s(X0,X1,X2,X3,X4,X0,X5) ),
inference(clausification,[status(esa)],[load1]) ).
cnf(c1,plain,
( ~ s(truck1,X1,X2,X3,X4,X0,X5)
| s(X0,X1,X2,X3,X4,X0,X5) ),
inference(clausification,[status(esa)],[load2]) ).
cnf(c2,plain,
( s(truck2,X1,X2,X3,X4,X5,X0)
| ~ s(X0,X1,X2,X3,X4,X5,X0) ),
inference(clausification,[status(esa)],[load3]) ).
cnf(c3,plain,
( ~ s(truck2,X1,X2,X3,X4,X5,X0)
| s(X0,X1,X2,X3,X4,X5,X0) ),
inference(clausification,[status(esa)],[load4]) ).
cnf(c4,plain,
( s(X0,truck1,X2,X3,X4,X1,X5)
| ~ s(X0,X1,X2,X3,X4,X1,X5) ),
inference(clausification,[status(esa)],[load5]) ).
cnf(c5,plain,
( ~ s(X0,truck1,X2,X3,X4,X1,X5)
| s(X0,X1,X2,X3,X4,X1,X5) ),
inference(clausification,[status(esa)],[load6]) ).
cnf(c8,plain,
( s(X0,X1,truck1,X3,X4,X2,X5)
| ~ s(X0,X1,X2,X3,X4,X2,X5) ),
inference(clausification,[status(esa)],[load9]) ).
cnf(c9,plain,
( ~ s(X0,X1,truck1,X3,X4,X2,X5)
| s(X0,X1,X2,X3,X4,X2,X5) ),
inference(clausification,[status(esa)],[load10]) ).
cnf(c12,plain,
( s(X1,X2,X3,truck1,X0,X4,X5)
| ~ s(X1,X2,X3,X4,X0,X4,X5)
| ~ neq(X0,truck1) ),
inference(clausification,[status(esa)],[board1]) ).
cnf(c13,plain,
( ~ s(X0,X1,X2,truck1,X4,X3,X5)
| s(X0,X1,X2,X3,X4,X3,X5) ),
inference(clausification,[status(esa)],[board2]) ).
cnf(c20,plain,
( s(X2,X3,X4,truck1,X5,X1,X6)
| ~ s(X2,X3,X4,truck1,X5,X0,X6)
| ~ link(X0,X1) ),
inference(clausification,[status(esa)],[drive1]) ).
cnf(c24,plain,
( s(X2,X3,X4,X1,X5,X6,X7)
| ~ s(X2,X3,X4,X0,X5,X6,X7)
| ~ path(X0,X1) ),
inference(clausification,[status(esa)],[walk1]) ).
cnf(c47,plain,
neq(s1,truck1),
inference(clausification,[status(esa)],[neq22]) ).
cnf(c80,plain,
path('p2$u1',s2),
inference(clausification,[status(esa)],[map6]) ).
cnf(c81,plain,
path(s1,'p2$u1'),
inference(clausification,[status(esa)],[map7]) ).
cnf(c84,plain,
link(s1,s0),
inference(clausification,[status(esa)],[map10]) ).
cnf(c86,plain,
link(s2,s1),
inference(clausification,[status(esa)],[map12]) ).
cnf(c88,plain,
link(s0,s2),
inference(clausification,[status(esa)],[map14]) ).
cnf(c89,plain,
s(s1,s1,s1,s1,s1,s2,s0),
inference(clausification,[status(esa)],[init]) ).
cnf(c90,plain,
~ s(s0,s0,s2,s2,X0,s2,X1),
inference(clausification,[status(esa)],[goal]) ).
cnf(d0,plain,
( ~ path(s1,X0)
| s(s1,s1,s1,X0,s1,s2,s0) ),
inference(resolution,[status(thm)],[c24,c89]) ).
cnf(d1,plain,
( ~ path(X0,X1)
| s(s1,s1,s1,X1,s1,s2,s0)
| ~ path(s1,X0) ),
inference(resolution,[status(thm)],[d0,c24]) ).
cnf(d2,plain,
( ~ path('p2$u1',X0)
| s(s1,s1,s1,X0,s1,s2,s0) ),
inference(resolution,[status(thm)],[d1,c81]) ).
cnf(d3,plain,
( ~ neq(s1,truck1)
| s(s1,s1,s1,truck1,s1,s2,s0)
| ~ path('p2$u1',s2) ),
inference(resolution,[status(thm)],[d2,c12]) ).
cnf(d4,plain,
( ~ path('p2$u1',s2)
| s(s1,s1,s1,truck1,s1,s2,s0) ),
inference(resolution,[status(thm)],[c47,d3]) ).
cnf(d5,plain,
s(s1,s1,s1,truck1,s1,s2,s0),
inference(resolution,[status(thm)],[c80,d4]) ).
cnf(d6,plain,
( ~ link(s2,X0)
| s(s1,s1,s1,truck1,s1,X0,s0) ),
inference(resolution,[status(thm)],[d5,c20]) ).
cnf(d7,plain,
( s(s1,s1,truck1,truck1,s1,s1,s0)
| ~ link(s2,s1) ),
inference(resolution,[status(thm)],[d6,c8]) ).
cnf(d8,plain,
s(s1,s1,truck1,truck1,s1,s1,s0),
inference(resolution,[status(thm)],[c86,d7]) ).
cnf(d9,plain,
s(s1,truck1,truck1,truck1,s1,s1,s0),
inference(resolution,[status(thm)],[d8,c4]) ).
cnf(d10,plain,
s(truck1,truck1,truck1,truck1,s1,s1,s0),
inference(resolution,[status(thm)],[d9,c0]) ).
cnf(d11,plain,
( ~ link(s1,X0)
| s(truck1,truck1,truck1,truck1,s1,X0,s0) ),
inference(resolution,[status(thm)],[d10,c20]) ).
cnf(d12,plain,
( s(X0,truck1,truck1,truck1,s1,X0,s0)
| ~ link(s1,X0) ),
inference(resolution,[status(thm)],[d11,c1]) ).
cnf(d13,plain,
( s(truck2,truck1,truck1,truck1,s1,s0,s0)
| ~ link(s1,s0) ),
inference(resolution,[status(thm)],[d12,c2]) ).
cnf(d14,plain,
s(truck2,truck1,truck1,truck1,s1,s0,s0),
inference(resolution,[status(thm)],[c84,d13]) ).
cnf(d15,plain,
s(s0,truck1,truck1,truck1,s1,s0,s0),
inference(resolution,[status(thm)],[d14,c3]) ).
cnf(d16,plain,
s(s0,s0,truck1,truck1,s1,s0,s0),
inference(resolution,[status(thm)],[d15,c5]) ).
cnf(d17,plain,
( ~ link(s0,X0)
| s(s0,s0,truck1,truck1,s1,X0,s0) ),
inference(resolution,[status(thm)],[d16,c20]) ).
cnf(d18,plain,
( s(s0,s0,X0,truck1,s1,X0,s0)
| ~ link(s0,X0) ),
inference(resolution,[status(thm)],[d17,c9]) ).
cnf(d19,plain,
( s(s0,s0,X0,X0,s1,X0,s0)
| ~ link(s0,X0) ),
inference(resolution,[status(thm)],[d18,c13]) ).
cnf(d20,plain,
~ link(s0,s2),
inference(resolution,[status(thm)],[d19,c90]) ).
cnf(d21,plain,
$false,
inference(resolution,[status(thm)],[c88,d20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PLA031-1.002 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 04:48:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.47/21.04 % SZS status Unsatisfiable for theBenchmark.p
% 26.47/21.04 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------