%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 08:20:25 AM UTC 2026
% Result : Unsatisfiable 0.93s 0.60s
% Output : CNFRefutation 0.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 20
% Syntax : Number of formulae : 63 ( 36 unt; 0 def)
% Number of atoms : 100 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 83 ( 46 ~; 37 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-6 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 138 ( 0 sgn 49 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(neq2,axiom,
neq(truck1,truck2),
file('theBenchmark.p',neq2) ).
cnf(c_1,plain,
neq(truck1,truck2),
inference(clausify,[status(thm)],[neq2]) ).
fof(board7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( s(VAR_0,VAR_1,VAR_2,truck2,VAR_4,VAR_3)
| ~ neq(VAR_2,truck2)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_3) ),
file('theBenchmark.p',board7) ).
cnf(c_3,plain,
( s(A,B,C,truck2,E,D)
| ~ neq(C,truck2)
| ~ s(A,B,C,D,E,D) ),
inference(clausify,[status(thm)],[board7]) ).
fof(board1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( s(VAR_0,VAR_1,truck1,VAR_3,VAR_2,VAR_4)
| ~ neq(VAR_3,truck1)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_2,VAR_4) ),
file('theBenchmark.p',board1) ).
cnf(c_6,plain,
( s(A,B,truck1,D,C,E)
| ~ neq(D,truck1)
| ~ s(A,B,C,D,C,E) ),
inference(clausify,[status(thm)],[board1]) ).
fof(neq25,axiom,
neq(s1,truck1),
file('theBenchmark.p',neq25) ).
cnf(c_29,plain,
neq(s1,truck1),
inference(clausify,[status(thm)],[neq25]) ).
fof(drive4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( s(VAR_0,VAR_1,VAR_2,truck2,VAR_3,VAR_5)
| ~ link(VAR_4,VAR_5)
| ~ s(VAR_0,VAR_1,VAR_2,truck2,VAR_3,VAR_4) ),
file('theBenchmark.p',drive4) ).
cnf(c_69,plain,
( s(A,B,C,truck2,D,F)
| ~ link(E,F)
| ~ s(A,B,C,truck2,D,E) ),
inference(clausify,[status(thm)],[drive4]) ).
fof(map14,axiom,
link(s1,s0),
file('theBenchmark.p',map14) ).
cnf(c_71,plain,
link(s1,s0),
inference(clausify,[status(thm)],[map14]) ).
fof(map15,axiom,
link(s0,s2),
file('theBenchmark.p',map15) ).
cnf(c_72,plain,
link(s0,s2),
inference(clausify,[status(thm)],[map15]) ).
fof(map18,axiom,
link(s2,s1),
file('theBenchmark.p',map18) ).
cnf(c_75,plain,
link(s2,s1),
inference(clausify,[status(thm)],[map18]) ).
fof(drive1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( s(VAR_0,VAR_1,truck1,VAR_2,VAR_5,VAR_4)
| ~ link(VAR_3,VAR_5)
| ~ s(VAR_0,VAR_1,truck1,VAR_2,VAR_3,VAR_4) ),
file('theBenchmark.p',drive1) ).
cnf(c_78,plain,
( s(A,B,truck1,C,F,E)
| ~ link(D,F)
| ~ s(A,B,truck1,C,D,E) ),
inference(clausify,[status(thm)],[drive1]) ).
fof(walk2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_0,VAR_1,VAR_2,VAR_6,VAR_4,VAR_5)
| ~ path(VAR_3,VAR_6)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5) ),
file('theBenchmark.p',walk2) ).
cnf(c_80,plain,
( s(A,B,C,V6,E,F)
| ~ path(D,V6)
| ~ s(A,B,C,D,E,F) ),
inference(clausify,[status(thm)],[walk2]) ).
fof(map6,axiom,
path(p2_0,s2),
file('theBenchmark.p',map6) ).
cnf(c_86,plain,
path(p2_0,s2),
inference(clausify,[status(thm)],[map6]) ).
fof(map7,axiom,
path(s0,p2_0),
file('theBenchmark.p',map7) ).
cnf(c_87,plain,
path(s0,p2_0),
inference(clausify,[status(thm)],[map7]) ).
fof(map10,axiom,
path(p2_1,s2),
file('theBenchmark.p',map10) ).
cnf(c_90,plain,
path(p2_1,s2),
inference(clausify,[status(thm)],[map10]) ).
fof(map11,axiom,
path(s1,p2_1),
file('theBenchmark.p',map11) ).
cnf(c_91,plain,
path(s1,p2_1),
inference(clausify,[status(thm)],[map11]) ).
cnf(c_96,plain,
( s(A,B,C,p2_1,D,E)
| ~ s(A,B,C,s1,D,E) ),
inference(resolve,[status(thm)],[c_91,c_80]) ).
cnf(c_98,plain,
( s(A,B,C,s2,D,E)
| ~ s(A,B,C,p2_1,D,E) ),
inference(resolve,[status(thm)],[c_90,c_80]) ).
cnf(c_104,plain,
( s(A,B,C,p2_0,D,E)
| ~ s(A,B,C,s0,D,E) ),
inference(resolve,[status(thm)],[c_87,c_80]) ).
cnf(c_106,plain,
( s(A,B,C,s2,D,E)
| ~ s(A,B,C,p2_0,D,E) ),
inference(resolve,[status(thm)],[c_86,c_80]) ).
cnf(c_135,plain,
( s(A,B,truck1,s1,C,D)
| ~ s(A,B,C,s1,C,D) ),
inference(resolve,[status(thm)],[c_29,c_6]) ).
cnf(c_144,plain,
( s(A,B,truck1,truck2,D,C)
| ~ s(A,B,truck1,C,D,C) ),
inference(resolve,[status(thm)],[c_1,c_3]) ).
fof(goal,axiom,
~ s(s2,s1,s2,s2,s2,s0),
file('theBenchmark.p',goal) ).
cnf(c_145,plain,
~ s(s2,s1,s2,s2,s2,s0),
inference(clausify,[status(thm)],[goal]) ).
fof(init,axiom,
s(s2,s2,s0,s1,s0,s2),
file('theBenchmark.p',init) ).
cnf(c_146,plain,
s(s2,s2,s0,s1,s0,s2),
inference(clausify,[status(thm)],[init]) ).
fof(board8,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ s(VAR_0,VAR_1,VAR_2,truck2,VAR_4,VAR_3)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_3) ),
file('theBenchmark.p',board8) ).
cnf(c_147,plain,
( ~ s(A,B,C,truck2,E,D)
| s(A,B,C,D,E,D) ),
inference(clausify,[status(thm)],[board8]) ).
fof(board2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ s(VAR_0,VAR_1,truck1,VAR_3,VAR_2,VAR_4)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_2,VAR_4) ),
file('theBenchmark.p',board2) ).
cnf(c_150,plain,
( ~ s(A,B,truck1,D,C,E)
| s(A,B,C,D,C,E) ),
inference(clausify,[status(thm)],[board2]) ).
fof(load8,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ s(VAR_0,truck2,VAR_2,VAR_3,VAR_4,VAR_1)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_1) ),
file('theBenchmark.p',load8) ).
cnf(c_151,plain,
( ~ s(A,truck2,C,D,E,B)
| s(A,B,C,D,E,B) ),
inference(clausify,[status(thm)],[load8]) ).
fof(load7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( s(VAR_0,truck2,VAR_2,VAR_3,VAR_4,VAR_1)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_1) ),
file('theBenchmark.p',load7) ).
cnf(c_152,plain,
( s(A,truck2,C,D,E,B)
| ~ s(A,B,C,D,E,B) ),
inference(clausify,[status(thm)],[load7]) ).
cnf(c_160,plain,
( s(A,B,C,truck2,D,s0)
| ~ s(A,B,C,truck2,D,s1) ),
inference(resolve,[status(thm)],[c_69,c_71]) ).
cnf(c_164,plain,
( s(A,B,C,truck2,D,s1)
| ~ s(A,B,C,truck2,D,s2) ),
inference(resolve,[status(thm)],[c_69,c_75]) ).
cnf(c_179,plain,
( s(A,B,truck1,C,s2,D)
| ~ s(A,B,truck1,C,s0,D) ),
inference(resolve,[status(thm)],[c_78,c_72]) ).
cnf(c_183,plain,
~ s(s2,s1,s2,p2_0,s2,s0),
inference(resolve,[status(thm)],[c_145,c_106]) ).
cnf(c_187,plain,
s(s2,s2,truck1,s1,s0,s2),
inference(resolve,[status(thm)],[c_146,c_135]) ).
cnf(c_198,plain,
~ s(s2,s1,truck1,p2_0,s2,s0),
inference(resolve,[status(thm)],[c_183,c_150]) ).
cnf(c_223,plain,
s(s2,truck2,truck1,s1,s0,s2),
inference(resolve,[status(thm)],[c_187,c_152]) ).
cnf(c_248,plain,
~ s(s2,s1,truck1,p2_0,s0,s0),
inference(resolve,[status(thm)],[c_198,c_179]) ).
cnf(c_275,plain,
s(s2,truck2,truck1,p2_1,s0,s2),
inference(resolve,[status(thm)],[c_223,c_96]) ).
cnf(c_357,plain,
~ s(s2,s1,truck1,s0,s0,s0),
inference(resolve,[status(thm)],[c_248,c_104]) ).
cnf(c_438,plain,
s(s2,truck2,truck1,s2,s0,s2),
inference(resolve,[status(thm)],[c_275,c_98]) ).
cnf(c_570,plain,
~ s(s2,s1,truck1,truck2,s0,s0),
inference(resolve,[status(thm)],[c_357,c_147]) ).
cnf(c_753,plain,
s(s2,truck2,truck1,truck2,s0,s2),
inference(resolve,[status(thm)],[c_438,c_144]) ).
cnf(c_986,plain,
~ s(s2,s1,truck1,truck2,s0,s1),
inference(resolve,[status(thm)],[c_570,c_160]) ).
cnf(c_1363,plain,
s(s2,truck2,truck1,truck2,s0,s1),
inference(resolve,[status(thm)],[c_753,c_164]) ).
cnf(c_1754,plain,
~ s(s2,truck2,truck1,truck2,s0,s1),
inference(resolve,[status(thm)],[c_986,c_151]) ).
cnf(c_1753,plain,
$false,
inference(resolve,[status(thm)],[c_1363,c_1754]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.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:45:16 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 2163816 was started by sandbox2 on n014,
% 0.13/0.36 % Sat Sep 26 04:45:16 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 0.93/0.60
% 0.93/0.60 % given #500 (F,wt=12): 598 -s(s2,s1,truck2,p2_0,s2,s1). [resolve(363,a,172,b)].
% 0.93/0.60
% 0.93/0.60 % SZS status Unsatisfiable for theBenchmark
% 0.93/0.60
% 0.93/0.60 % Proof 1 at 0.15 (+ 0.07) seconds.
% 0.93/0.60 % Length of proof is 42.
% 0.93/0.60 % Level of proof is 8.
% 0.93/0.60 % Maximum clause weight is 19.000.
% 0.93/0.60 % Given clauses 890.
% 0.93/0.60
% 0.93/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------