%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PLA031-1.003 : 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 : n009.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:26 AM UTC 2026
% Result : Unsatisfiable 14.80s 2.36s
% Output : CNFRefutation 14.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 20
% Syntax : Number of formulae : 64 ( 36 unt; 0 def)
% Number of atoms : 100 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 80 ( 44 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-8 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 213 ( 9 sgn 77 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(board5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,truck1,VAR_5,VAR_6)
| ~ neq(VAR_4,truck1)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_5,VAR_6) ),
file('theBenchmark.p',board5) ).
cnf(c_4,plain,
( s(A,B,C,D,E,truck1,F,V6)
| ~ neq(E,truck1)
| ~ s(A,B,C,D,E,F,F,V6) ),
inference(clausify,[status(thm)],[board5]) ).
fof(neq33,axiom,
neq(s2,truck1),
file('theBenchmark.p',neq33) ).
cnf(c_37,plain,
neq(s2,truck1),
inference(clausify,[status(thm)],[neq33]) ).
fof(map13,axiom,
link(s1,s2),
file('theBenchmark.p',map13) ).
cnf(c_70,plain,
link(s1,s2),
inference(clausify,[status(thm)],[map13]) ).
fof(map15,axiom,
link(s2,s0),
file('theBenchmark.p',map15) ).
cnf(c_72,plain,
link(s2,s0),
inference(clausify,[status(thm)],[map15]) ).
fof(map16,axiom,
link(s0,s2),
file('theBenchmark.p',map16) ).
cnf(c_73,plain,
link(s0,s2),
inference(clausify,[status(thm)],[map16]) ).
fof(drive3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,truck1,VAR_7,VAR_6)
| ~ link(VAR_5,VAR_7)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,truck1,VAR_5,VAR_6) ),
file('theBenchmark.p',drive3) ).
cnf(c_74,plain,
( s(A,B,C,D,E,truck1,V7,V6)
| ~ link(F,V7)
| ~ s(A,B,C,D,E,truck1,F,V6) ),
inference(clausify,[status(thm)],[drive3]) ).
fof(map1,axiom,
path(s0,p0_1),
file('theBenchmark.p',map1) ).
cnf(c_77,plain,
path(s0,p0_1),
inference(clausify,[status(thm)],[map1]) ).
fof(walk2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] :
( s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_8,VAR_6,VAR_7)
| ~ path(VAR_5,VAR_8)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7) ),
file('theBenchmark.p',walk2) ).
cnf(c_78,plain,
( s(A,B,C,D,E,V8,V6,V7)
| ~ path(F,V8)
| ~ s(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[walk2]) ).
fof(walk1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] :
( s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_8,VAR_5,VAR_6,VAR_7)
| ~ path(VAR_4,VAR_8)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7) ),
file('theBenchmark.p',walk1) ).
cnf(c_79,plain,
( s(A,B,C,D,V8,F,V6,V7)
| ~ path(E,V8)
| ~ s(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[walk1]) ).
fof(map4,axiom,
path(p0_1,s1),
file('theBenchmark.p',map4) ).
cnf(c_82,plain,
path(p0_1,s1),
inference(clausify,[status(thm)],[map4]) ).
fof(map6,axiom,
path(p1_2,s1),
file('theBenchmark.p',map6) ).
cnf(c_84,plain,
path(p1_2,s1),
inference(clausify,[status(thm)],[map6]) ).
fof(map7,axiom,
path(s2,p1_2),
file('theBenchmark.p',map7) ).
cnf(c_85,plain,
path(s2,p1_2),
inference(clausify,[status(thm)],[map7]) ).
cnf(c_101,plain,
( s(A,B,C,D,p1_2,E,F,V6)
| ~ s(A,B,C,D,s2,E,F,V6) ),
inference(resolve,[status(thm)],[c_85,c_79]) ).
cnf(c_103,plain,
( s(A,B,C,D,s1,E,F,V6)
| ~ s(A,B,C,D,p1_2,E,F,V6) ),
inference(resolve,[status(thm)],[c_84,c_79]) ).
cnf(c_108,plain,
( s(A,B,C,D,E,s1,F,V6)
| ~ s(A,B,C,D,E,p0_1,F,V6) ),
inference(resolve,[status(thm)],[c_82,c_78]) ).
cnf(c_114,plain,
( s(A,B,C,D,E,p0_1,F,V6)
| ~ s(A,B,C,D,E,s0,F,V6) ),
inference(resolve,[status(thm)],[c_77,c_78]) ).
cnf(c_130,plain,
( s(A,B,C,D,s2,truck1,E,F)
| ~ s(A,B,C,D,s2,E,E,F) ),
inference(resolve,[status(thm)],[c_37,c_4]) ).
fof(goal,axiom,
! [VAR_0,VAR_1] : ~ s(s2,s2,s0,s2,s1,VAR_0,s0,VAR_1),
file('theBenchmark.p',goal) ).
cnf(c_143,plain,
~ s(s2,s2,s0,s2,s1,A,s0,B),
inference(clausify,[status(thm)],[goal]) ).
fof(init,axiom,
s(s1,s2,s2,s0,s2,s0,s1,s1),
file('theBenchmark.p',init) ).
cnf(c_144,plain,
s(s1,s2,s2,s0,s2,s0,s1,s1),
inference(clausify,[status(thm)],[init]) ).
fof(load14,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ s(VAR_0,VAR_1,VAR_2,truck1,VAR_4,VAR_5,VAR_3,VAR_6)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_3,VAR_6) ),
file('theBenchmark.p',load14) ).
cnf(c_151,plain,
( ~ s(A,B,C,truck1,E,F,D,V6)
| s(A,B,C,D,E,F,D,V6) ),
inference(clausify,[status(thm)],[load14]) ).
fof(load13,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_0,VAR_1,VAR_2,truck1,VAR_4,VAR_5,VAR_3,VAR_6)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_3,VAR_6) ),
file('theBenchmark.p',load13) ).
cnf(c_152,plain,
( s(A,B,C,truck1,E,F,D,V6)
| ~ s(A,B,C,D,E,F,D,V6) ),
inference(clausify,[status(thm)],[load13]) ).
fof(load10,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ s(VAR_0,VAR_1,truck1,VAR_3,VAR_4,VAR_5,VAR_2,VAR_6)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_2,VAR_6) ),
file('theBenchmark.p',load10) ).
cnf(c_155,plain,
( ~ s(A,B,truck1,D,E,F,C,V6)
| s(A,B,C,D,E,F,C,V6) ),
inference(clausify,[status(thm)],[load10]) ).
fof(load9,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(VAR_0,VAR_1,truck1,VAR_3,VAR_4,VAR_5,VAR_2,VAR_6)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_2,VAR_6) ),
file('theBenchmark.p',load9) ).
cnf(c_156,plain,
( s(A,B,truck1,D,E,F,C,V6)
| ~ s(A,B,C,D,E,F,C,V6) ),
inference(clausify,[status(thm)],[load9]) ).
fof(load2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( ~ s(truck1,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_0,VAR_6)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_0,VAR_6) ),
file('theBenchmark.p',load2) ).
cnf(c_163,plain,
( ~ s(truck1,B,C,D,E,F,A,V6)
| s(A,B,C,D,E,F,A,V6) ),
inference(clausify,[status(thm)],[load2]) ).
fof(load1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( s(truck1,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_0,VAR_6)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_0,VAR_6) ),
file('theBenchmark.p',load1) ).
cnf(c_164,plain,
( s(truck1,B,C,D,E,F,A,V6)
| ~ s(A,B,C,D,E,F,A,V6) ),
inference(clausify,[status(thm)],[load1]) ).
cnf(c_169,plain,
( s(A,B,C,D,E,truck1,s2,F)
| ~ s(A,B,C,D,E,truck1,s1,F) ),
inference(resolve,[status(thm)],[c_74,c_70]) ).
cnf(c_171,plain,
( s(A,B,C,D,E,truck1,s0,F)
| ~ s(A,B,C,D,E,truck1,s2,F) ),
inference(resolve,[status(thm)],[c_74,c_72]) ).
cnf(c_172,plain,
( s(A,B,C,D,E,truck1,s2,F)
| ~ s(A,B,C,D,E,truck1,s0,F) ),
inference(resolve,[status(thm)],[c_74,c_73]) ).
cnf(c_182,plain,
~ s(s2,s2,s0,s2,p1_2,A,s0,B),
inference(resolve,[status(thm)],[c_143,c_103]) ).
cnf(c_183,plain,
s(s1,s2,s2,s0,s2,p0_1,s1,s1),
inference(resolve,[status(thm)],[c_144,c_114]) ).
cnf(c_204,plain,
~ s(s2,s2,s0,s2,p1_2,truck1,s2,A),
inference(resolve,[status(thm)],[c_182,c_171]) ).
cnf(c_223,plain,
s(truck1,s2,s2,s0,s2,p0_1,s1,s1),
inference(resolve,[status(thm)],[c_183,c_164]) ).
cnf(c_279,plain,
s(truck1,s2,s2,s0,s2,s1,s1,s1),
inference(resolve,[status(thm)],[c_223,c_108]) ).
cnf(c_304,plain,
~ s(s2,s2,s0,truck1,p1_2,truck1,s2,A),
inference(resolve,[status(thm)],[c_204,c_151]) ).
cnf(c_414,plain,
s(truck1,s2,s2,s0,s2,truck1,s1,s1),
inference(resolve,[status(thm)],[c_279,c_130]) ).
cnf(c_691,plain,
~ s(s2,s2,s0,truck1,p1_2,truck1,s0,A),
inference(resolve,[status(thm)],[c_304,c_172]) ).
cnf(c_698,plain,
s(truck1,s2,s2,s0,s2,truck1,s2,s1),
inference(resolve,[status(thm)],[c_414,c_169]) ).
cnf(c_1054,plain,
s(s2,s2,s2,s0,s2,truck1,s2,s1),
inference(resolve,[status(thm)],[c_698,c_163]) ).
cnf(c_1653,plain,
s(s2,s2,truck1,s0,s2,truck1,s2,s1),
inference(resolve,[status(thm)],[c_1054,c_156]) ).
cnf(c_2126,plain,
~ s(s2,s2,truck1,truck1,p1_2,truck1,s0,A),
inference(resolve,[status(thm)],[c_691,c_155]) ).
cnf(c_3007,plain,
s(s2,s2,truck1,s0,s2,truck1,s0,s1),
inference(resolve,[status(thm)],[c_1653,c_171]) ).
cnf(c_6080,plain,
s(s2,s2,truck1,s0,p1_2,truck1,s0,s1),
inference(resolve,[status(thm)],[c_3007,c_101]) ).
cnf(c_6307,plain,
~ s(s2,s2,truck1,s0,p1_2,truck1,s0,A),
inference(resolve,[status(thm)],[c_2126,c_152]) ).
cnf(c_6308,plain,
$false,
inference(resolve,[status(thm)],[c_6307,c_6080]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PLA031-1.003 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n009.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.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sat Sep 26 04:45:44 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 3379077 was started by sandbox2 on n009,
% 0.18/0.45 % Sat Sep 26 04:45:44 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.46
% 0.18/0.46 % From the command line: assign(max_seconds, 300).
% 14.80/2.36
% 14.80/2.36 % given #500 (F,wt=14): 520 -s(s2,truck2,s0,truck1,p0_1,truck1,s2,s2). [resolve(260,a,151,a)].
% 14.80/2.36
% 14.80/2.36 % given #1000 (T,wt=14): 1590 s(s1,truck2,s2,s0,truck2,s0,s1,s0). [resolve(963,a,175,a)].
% 14.80/2.36
% 14.80/2.36 % given #1500 (F,wt=14): 1339 -s(truck1,s2,s0,s2,s0,truck2,s2,truck1). [resolve(501,a,113,b)].
% 14.80/2.36
% 14.80/2.36 % given #2000 (T,wt=14): 2745 s(truck2,s2,truck2,s0,s2,s0,s1,s2). [resolve(1509,a,147,b)].
% 14.80/2.36
% 14.80/2.36 % SZS status Unsatisfiable for theBenchmark
% 14.80/2.36
% 14.80/2.36 % Proof 1 at 1.24 (+ 0.64) seconds.
% 14.80/2.36 % Length of proof is 44.
% 14.80/2.36 % Level of proof is 11.
% 14.80/2.36 % Maximum clause weight is 23.000.
% 14.80/2.36 % Given clauses 2339.
% 14.80/2.36
% 14.80/2.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------