%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PLA031-1.004 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 48.72s 15.11s
% Output : CNFRefutation 48.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 17
% Syntax : Number of formulae : 54 ( 25 unt; 0 def)
% Number of atoms : 97 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 93 ( 50 ~; 43 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-9 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 223 ( 7 sgn 92 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(map13,axiom,
link(s0,s2),
file('theBenchmark.p',map13) ).
cnf(c_1,plain,
link(s0,s2),
inference(clausify,[status(thm)],[map13]) ).
fof(drive4,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,truck2,VAR_5,VAR_6,VAR_8)
| ~ link(VAR_7,VAR_8)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,truck2,VAR_5,VAR_6,VAR_7) ),
file('theBenchmark.p',drive4) ).
cnf(c_4,plain,
( s(A,B,C,D,E,truck2,F,V6,V8)
| ~ link(V7,V8)
| ~ s(A,B,C,D,E,truck2,F,V6,V7) ),
inference(clausify,[status(thm)],[drive4]) ).
fof(drive2,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,truck2,VAR_4,VAR_5,VAR_6,VAR_8)
| ~ link(VAR_7,VAR_8)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,truck2,VAR_4,VAR_5,VAR_6,VAR_7) ),
file('theBenchmark.p',drive2) ).
cnf(c_6,plain,
( s(A,B,C,D,truck2,E,F,V6,V8)
| ~ link(V7,V8)
| ~ s(A,B,C,D,truck2,E,F,V6,V7) ),
inference(clausify,[status(thm)],[drive2]) ).
fof(map15,axiom,
link(s1,s0),
file('theBenchmark.p',map15) ).
cnf(c_9,plain,
link(s1,s0),
inference(clausify,[status(thm)],[map15]) ).
fof(map17,axiom,
link(s2,s1),
file('theBenchmark.p',map17) ).
cnf(c_11,plain,
link(s2,s1),
inference(clausify,[status(thm)],[map17]) ).
fof(load3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( s(truck2,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_0)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_0) ),
file('theBenchmark.p',load3) ).
cnf(c_66,plain,
( s(truck2,B,C,D,E,F,V6,V7,A)
| ~ s(A,B,C,D,E,F,V6,V7,A) ),
inference(clausify,[status(thm)],[load3]) ).
fof(load4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( ~ s(truck2,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_0)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_0) ),
file('theBenchmark.p',load4) ).
cnf(c_67,plain,
( ~ s(truck2,B,C,D,E,F,V6,V7,A)
| s(A,B,C,D,E,F,V6,V7,A) ),
inference(clausify,[status(thm)],[load4]) ).
fof(load11,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( s(VAR_0,VAR_1,truck2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_2)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_2) ),
file('theBenchmark.p',load11) ).
cnf(c_74,plain,
( s(A,B,truck2,D,E,F,V6,V7,C)
| ~ s(A,B,C,D,E,F,V6,V7,C) ),
inference(clausify,[status(thm)],[load11]) ).
fof(load12,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( ~ s(VAR_0,VAR_1,truck2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_2)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_2) ),
file('theBenchmark.p',load12) ).
cnf(c_75,plain,
( ~ s(A,B,truck2,D,E,F,V6,V7,C)
| s(A,B,C,D,E,F,V6,V7,C) ),
inference(clausify,[status(thm)],[load12]) ).
fof(load15,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( s(VAR_0,VAR_1,VAR_2,truck2,VAR_4,VAR_5,VAR_6,VAR_7,VAR_3)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_3) ),
file('theBenchmark.p',load15) ).
cnf(c_78,plain,
( s(A,B,C,truck2,E,F,V6,V7,D)
| ~ s(A,B,C,D,E,F,V6,V7,D) ),
inference(clausify,[status(thm)],[load15]) ).
fof(load16,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] :
( ~ s(VAR_0,VAR_1,VAR_2,truck2,VAR_4,VAR_5,VAR_6,VAR_7,VAR_3)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_3) ),
file('theBenchmark.p',load16) ).
cnf(c_79,plain,
( ~ s(A,B,C,truck2,E,F,V6,V7,D)
| s(A,B,C,D,E,F,V6,V7,D) ),
inference(clausify,[status(thm)],[load16]) ).
fof(board3,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,truck2,VAR_5,VAR_6,VAR_7,VAR_4)
| ~ neq(VAR_6,truck2)
| ~ neq(VAR_5,truck2)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_4) ),
file('theBenchmark.p',board3) ).
cnf(c_82,plain,
( s(A,B,C,D,truck2,F,V6,V7,E)
| ~ neq(V6,truck2)
| ~ neq(F,truck2)
| ~ s(A,B,C,D,E,F,V6,V7,E) ),
inference(clausify,[status(thm)],[board3]) ).
fof(board4,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,truck2,VAR_5,VAR_6,VAR_7,VAR_4)
| s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_4) ),
file('theBenchmark.p',board4) ).
cnf(c_83,plain,
( ~ s(A,B,C,D,truck2,F,V6,V7,E)
| s(A,B,C,D,E,F,V6,V7,E) ),
inference(clausify,[status(thm)],[board4]) ).
fof(board7,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,truck2,VAR_6,VAR_7,VAR_5)
| ~ neq(VAR_6,truck2)
| ~ neq(VAR_4,truck2)
| ~ s(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_5) ),
file('theBenchmark.p',board7) ).
cnf(c_86,plain,
( s(A,B,C,D,E,truck2,V6,V7,F)
| ~ neq(V6,truck2)
| ~ neq(E,truck2)
| ~ s(A,B,C,D,E,F,V6,V7,F) ),
inference(clausify,[status(thm)],[board7]) ).
fof(neq38,axiom,
neq(s2,truck2),
file('theBenchmark.p',neq38) ).
cnf(c_129,plain,
neq(s2,truck2),
inference(clausify,[status(thm)],[neq38]) ).
fof(init,axiom,
s(s1,s0,s2,s0,s1,s2,s2,s0,s1),
file('theBenchmark.p',init) ).
cnf(c_173,plain,
s(s1,s0,s2,s0,s1,s2,s2,s0,s1),
inference(clausify,[status(thm)],[init]) ).
fof(goal,axiom,
! [VAR_0,VAR_1] : ~ s(s0,s0,s1,s2,s2,VAR_0,VAR_1,s0,s1),
file('theBenchmark.p',goal) ).
cnf(c_174,plain,
~ s(s0,s0,s1,s2,s2,A,B,s0,s1),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_179,plain,
( s(A,B,C,D,truck2,E,F,V6,s2)
| ~ s(A,B,C,D,truck2,E,F,V6,s0) ),
inference(resolve,[status(thm)],[c_1,c_6]) ).
cnf(c_191,plain,
( s(A,B,C,D,truck2,E,F,V6,s0)
| ~ s(A,B,C,D,truck2,E,F,V6,s1) ),
inference(resolve,[status(thm)],[c_9,c_6]) ).
cnf(c_201,plain,
( s(A,B,C,D,E,truck2,F,V6,s1)
| ~ s(A,B,C,D,E,truck2,F,V6,s2) ),
inference(resolve,[status(thm)],[c_11,c_4]) ).
cnf(c_17461,plain,
( s(s1,s0,s2,s0,truck2,s2,s2,s0,s1)
| ~ neq(s2,truck2)
| ~ neq(s2,truck2) ),
inference(resolve,[status(thm)],[c_82,c_173]) ).
cnf(c_17462,plain,
( s(s1,s0,s2,s0,truck2,s2,s2,s0,s1)
| ~ neq(s2,truck2) ),
inference(resolve,[status(thm)],[c_17461,c_129]) ).
cnf(c_211,plain,
s(s1,s0,s2,s0,truck2,s2,s2,s0,s1),
inference(resolve,[status(thm)],[c_17462,c_129]) ).
cnf(c_221,plain,
~ s(s0,s0,truck2,s2,s2,A,B,s0,s1),
inference(resolve,[status(thm)],[c_174,c_75]) ).
cnf(c_238,plain,
s(truck2,s0,s2,s0,truck2,s2,s2,s0,s1),
inference(resolve,[status(thm)],[c_66,c_211]) ).
cnf(c_243,plain,
~ s(s0,s0,truck2,s2,s2,truck2,A,s0,s2),
inference(resolve,[status(thm)],[c_221,c_201]) ).
cnf(c_452,plain,
s(truck2,s0,s2,s0,truck2,s2,s2,s0,s0),
inference(resolve,[status(thm)],[c_191,c_238]) ).
cnf(c_461,plain,
~ s(s0,s0,truck2,truck2,s2,truck2,A,s0,s2),
inference(resolve,[status(thm)],[c_243,c_79]) ).
cnf(c_1444,plain,
s(truck2,s0,s2,truck2,truck2,s2,s2,s0,s0),
inference(resolve,[status(thm)],[c_78,c_452]) ).
cnf(c_1774,plain,
~ s(s0,s0,s2,truck2,s2,truck2,A,s0,s2),
inference(resolve,[status(thm)],[c_461,c_74]) ).
cnf(c_3918,plain,
s(s0,s0,s2,truck2,truck2,s2,s2,s0,s0),
inference(resolve,[status(thm)],[c_67,c_1444]) ).
cnf(c_17463,plain,
( s(A,B,C,D,s2,truck2,F,V6,E)
| ~ neq(F,truck2)
| ~ s(A,B,C,D,s2,E,F,V6,E) ),
inference(resolve,[status(thm)],[c_86,c_129]) ).
cnf(c_17464,plain,
( s(A,B,C,D,s2,truck2,s2,F,E)
| ~ s(A,B,C,D,s2,E,s2,F,E) ),
inference(resolve,[status(thm)],[c_17463,c_129]) ).
cnf(c_7658,plain,
~ s(s0,s0,s2,truck2,s2,s2,s2,s0,s2),
inference(resolve,[status(thm)],[c_17464,c_1774]) ).
cnf(c_8967,plain,
s(s0,s0,s2,truck2,truck2,s2,s2,s0,s2),
inference(resolve,[status(thm)],[c_179,c_3918]) ).
cnf(c_17459,plain,
s(s0,s0,s2,truck2,s2,s2,s2,s0,s2),
inference(resolve,[status(thm)],[c_83,c_8967]) ).
cnf(c_17460,plain,
$false,
inference(resolve,[status(thm)],[c_17459,c_7658]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PLA031-1.004 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43 % Computer : n001.cluster.edu
% 0.10/0.43 % Model : x86_64 x86_64
% 0.10/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.43 % Memory : 8046.5625MB
% 0.10/0.43 % OS : Linux 6.8.0-71-generic
% 0.10/0.43 % CPULimit : 300
% 0.10/0.43 % WCLimit : 300
% 0.10/0.43 % DateTime : Sat Sep 26 04:51:26 UTC 2026
% 0.10/0.44 % CPUTime :
% 0.10/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.44 % Process 937570 was started by sandbox on n001,
% 0.10/0.44 % Sat Sep 26 04:51:26 2026
% 0.10/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.45
% 0.10/0.45 % From the command line: assign(max_seconds, 300).
% 48.72/15.11
% 48.72/15.11 % given #500 (F,wt=10): 476 -s(s0,s0,truck2,s2,s2,truck1,truck2,s2,s2). [resolve(244,a,184,b)].
% 48.72/15.11
% 48.72/15.11 % given #1000 (T,wt=10): 1538 s(truck2,truck1,s2,truck1,p0_1,s2,s2,s0,s1). [ur(37,a,588,a)].
% 48.72/15.11
% 48.72/15.11 % given #1500 (F,wt=10): 1175 -s(s0,s0,s1,truck1,s2,s1,s2,s2,s1). [ur(88,b,128,a,c,119,a,d,329,a)].
% 48.72/15.11
% 48.72/15.11 % given #2000 (T,wt=10): 3194 s(s1,s0,truck2,truck2,truck2,s2,s2,s0,s2). [ur(74,a,1268,a)].
% 48.72/15.11
% 48.72/15.11 % given #2500 (F,wt=10): 2016 -s(s0,s0,truck2,s2,p2_0,truck1,s2,s0,s2). [ur(90,b,156,a,c,93,a,d,484,a)].
% 48.72/15.11
% 48.72/15.11 % given #3000 (T,wt=10): 4865 s(truck2,truck1,s2,s0,p0_1,p1_2,p1_2,s0,s1). [ur(37,a,1827,a)].
% 48.72/15.11
% 48.72/15.11 % given #3500 (F,wt=10): 2773 -s(truck1,s0,truck2,s2,s2,s1,s0,s1,s1). [ur(84,b,128,a,c,110,a,d,611,a)].
% 48.72/15.11
% 48.72/15.11 % given #4000 (A,wt=10): 3158 -s(truck1,truck1,s1,s2,s2,s0,p0_1,s0,s0). [ur(86,b,129,a,c,138,a,d,662,a)].
% 48.72/15.11
% 48.72/15.11 % given #4500 (T,wt=10): 6720 s(s1,s0,truck2,s0,truck2,truck1,s2,s0,s2). [ur(84,a,2919,a,b,101,a,c,128,a)].
% 48.72/15.11
% 48.72/15.11 % given #5000 (F,wt=10): 3958 -s(truck1,s0,s1,s2,s2,p2_0,s1,s0,s2). [resolve(778,a,42,b)].
% 48.72/15.11
% 48.72/15.11 % given #5500 (T,wt=10): 7751 s(s1,truck1,s2,s0,truck2,s0,p2_0,s0,s0). [ur(40,a,3397,a)].
% 48.72/15.11
% 48.72/15.11 % given #6000 (F,wt=10): 4686 -s(s0,s0,s1,s2,s1,s2,truck1,s0,s2). [ur(86,b,120,a,c,93,a,d,902,a)].
% 48.72/15.11
% 48.72/15.11 % SZS status Unsatisfiable for theBenchmark
% 48.72/15.11
% 48.72/15.11 % Proof 1 at 4.87 (+ 1.55) seconds.
% 48.72/15.11 % Length of proof is 33.
% 48.72/15.11 % Level of proof is 8.
% 48.72/15.11 % Maximum clause weight is 26.000.
% 48.72/15.11 % Given clauses 6382.
% 48.72/15.11
% 48.72/15.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------