%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PLA031-1.003 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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 : Fri Sep 25 02:30:43 PM UTC 2026
% Result : Unsatisfiable 21.18s 3.14s
% Output : Proof 21.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 28
% Syntax : Number of formulae : 143 ( 103 unt; 0 def)
% Number of atoms : 199 ( 39 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 150 ( 94 ~; 56 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-8 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-4 aty)
% Number of variables : 385 ( 6 sgn 154 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f29,axiom,
( s(O1,O2,O3,O4,D1,D,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,O4,D1,S,T1,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk2) ).
fof(f29_nnf,plain,
! [O1,O2,O3,O4,D1,S,T1,T2,D] :
( s(O1,O2,O3,O4,D1,D,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,O4,D1,S,T1,T2) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [O1,O2,O3,O4,D1,S,T1,T2,D] :
( s(O1,O2,O3,O4,D1,D,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,O4,D1,S,T1,T2) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( s(X0,X1,X2,X3,X4,X8,X6,X7)
| ~ path(X5,X8)
| ~ s(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(hi29,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5,X6,X7),true,ifeq(path(X5,X8),true,s(X0,X1,X2,X3,X4,X8,X6,X7),true),true) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(f110,axiom,
s(s1,s2,s2,s0,s2,s0,s1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',init) ).
fof(f110_nnf,plain,
s(s1,s2,s2,s0,s2,s0,s1,s1),
inference(nnf_transformation,[status(thm)],[f110]) ).
cnf(c110,plain,
s(s1,s2,s2,s0,s2,s0,s1,s1),
inference(cnf_transformation,[status(esa)],[f110_nnf]) ).
cnf(hi102,axiom,
s(s1,s2,s2,s0,s2,s0,s1,s1) = true,
inference(equality_encoding,[status(esa)],[c110]) ).
cnf(f94,axiom,
path(s0,p0_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map1) ).
fof(f94_nnf,plain,
path(s0,p0_1),
inference(nnf_transformation,[status(thm)],[f94]) ).
cnf(c94,plain,
path(s0,p0_1),
inference(cnf_transformation,[status(esa)],[f94_nnf]) ).
cnf(hi86,axiom,
path(s0,p0_1) = true,
inference(equality_encoding,[status(esa)],[c94]) ).
cnf(h1,plain,
s(s1,s2,s2,s0,s2,p0_1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi29,hi102,hi86]) ).
cnf(f97,axiom,
path(p0_1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map4) ).
fof(f97_nnf,plain,
path(p0_1,s1),
inference(nnf_transformation,[status(thm)],[f97]) ).
cnf(c97,plain,
path(p0_1,s1),
inference(cnf_transformation,[status(esa)],[f97_nnf]) ).
cnf(hi89,axiom,
path(p0_1,s1) = true,
inference(equality_encoding,[status(esa)],[c97]) ).
cnf(h11,plain,
s(s1,s2,s2,s0,s2,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi29,h1,hi89]) ).
cnf(f28,axiom,
( s(O1,O2,O3,O4,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,O4,S,D2,T1,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk1) ).
fof(f28_nnf,plain,
! [O1,O2,O3,O4,S,D2,T1,T2,D] :
( s(O1,O2,O3,O4,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,O4,S,D2,T1,T2) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [O1,O2,O3,O4,S,D2,T1,T2,D] :
( s(O1,O2,O3,O4,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,O4,S,D2,T1,T2) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( s(X0,X1,X2,X3,X8,X5,X6,X7)
| ~ path(X4,X8)
| ~ s(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(hi28,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5,X6,X7),true,ifeq(path(X4,X8),true,s(X0,X1,X2,X3,X8,X5,X6,X7),true),true) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(f100,axiom,
path(s2,p1_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map7) ).
fof(f100_nnf,plain,
path(s2,p1_2),
inference(nnf_transformation,[status(thm)],[f100]) ).
cnf(c100,plain,
path(s2,p1_2),
inference(cnf_transformation,[status(esa)],[f100_nnf]) ).
cnf(hi92,axiom,
path(s2,p1_2) = true,
inference(equality_encoding,[status(esa)],[c100]) ).
cnf(h34,plain,
s(s1,s2,s2,s0,p1_2,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi28,h11,hi92]) ).
cnf(f99,axiom,
path(p1_2,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map6) ).
fof(f99_nnf,plain,
path(p1_2,s1),
inference(nnf_transformation,[status(thm)],[f99]) ).
cnf(c99,plain,
path(p1_2,s1),
inference(cnf_transformation,[status(esa)],[f99_nnf]) ).
cnf(hi91,axiom,
path(p1_2,s1) = true,
inference(equality_encoding,[status(esa)],[c99]) ).
cnf(h74,plain,
s(s1,s2,s2,s0,s1,s1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi28,h34,hi91]) ).
cnf(f20,axiom,
( s(O1,O2,O3,O4,D1,truck1,L,T2)
| ~ neq(D1,truck1)
| ~ s(O1,O2,O3,O4,D1,L,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board5) ).
fof(f20_nnf,plain,
! [O1,O2,O3,O4,D1,L,T2] :
( s(O1,O2,O3,O4,D1,truck1,L,T2)
| ~ neq(D1,truck1)
| ~ s(O1,O2,O3,O4,D1,L,L,T2) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [O1,O2,O3,O4,D1,L,T2] :
( s(O1,O2,O3,O4,D1,truck1,L,T2)
| ~ neq(D1,truck1)
| ~ s(O1,O2,O3,O4,D1,L,L,T2) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( s(X0,X1,X2,X3,X4,truck1,X5,X6)
| ~ neq(X4,truck1)
| ~ s(X0,X1,X2,X3,X4,X5,X5,X6) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi20,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5,X5,X6),true,ifeq(neq(X4,truck1),true,s(X0,X1,X2,X3,X4,truck1,X5,X6),true),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(f54,axiom,
neq(s1,truck1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq25) ).
fof(f54_nnf,plain,
neq(s1,truck1),
inference(nnf_transformation,[status(thm)],[f54]) ).
cnf(c54,plain,
neq(s1,truck1),
inference(cnf_transformation,[status(esa)],[f54_nnf]) ).
cnf(hi51,axiom,
neq(s1,truck1) = true,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(h133,plain,
s(s1,s2,s2,s0,s1,truck1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi20,h74,hi51]) ).
cnf(f0,axiom,
( s(truck1,O2,O3,O4,D1,D2,L,T2)
| ~ s(L,O2,O3,O4,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load1) ).
fof(f0_nnf,plain,
! [L,O2,O3,O4,D1,D2,T2] :
( s(truck1,O2,O3,O4,D1,D2,L,T2)
| ~ s(L,O2,O3,O4,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [L,O2,O3,O4,D1,D2,T2] :
( s(truck1,O2,O3,O4,D1,D2,L,T2)
| ~ s(L,O2,O3,O4,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( s(truck1,X1,X2,X3,X4,X5,X0,X6)
| ~ s(X0,X1,X2,X3,X4,X5,X0,X6) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5,X0,X6),true,s(truck1,X1,X2,X3,X4,X5,X0,X6),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h232,plain,
s(truck1,s2,s2,s0,s1,truck1,s1,s1) = true,
inference(hyper_resolution,[status(thm)],[hi0,h133]) ).
cnf(f26,axiom,
( s(O1,O2,O3,O4,D1,truck1,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,O3,O4,D1,truck1,S,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive3) ).
fof(f26_nnf,plain,
! [O1,O2,O3,O4,D1,S,T2,D] :
( s(O1,O2,O3,O4,D1,truck1,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,O3,O4,D1,truck1,S,T2) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [O1,O2,O3,O4,D1,S,T2,D] :
( s(O1,O2,O3,O4,D1,truck1,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,O3,O4,D1,truck1,S,T2) ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
( s(X0,X1,X2,X3,X4,truck1,X7,X6)
| ~ link(X5,X7)
| ~ s(X0,X1,X2,X3,X4,truck1,X5,X6) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi26,axiom,
ifeq(s(X0,X1,X2,X3,X4,truck1,X5,X6),true,ifeq(link(X5,X7),true,s(X0,X1,X2,X3,X4,truck1,X7,X6),true),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(f106,axiom,
link(s1,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map13) ).
fof(f106_nnf,plain,
link(s1,s2),
inference(nnf_transformation,[status(thm)],[f106]) ).
cnf(c106,plain,
link(s1,s2),
inference(cnf_transformation,[status(esa)],[f106_nnf]) ).
cnf(hi98,axiom,
link(s1,s2) = true,
inference(equality_encoding,[status(esa)],[c106]) ).
cnf(h474,plain,
s(truck1,s2,s2,s0,s1,truck1,s2,s1) = true,
inference(hyper_resolution,[status(thm)],[hi26,h232,hi98]) ).
cnf(f108,axiom,
link(s2,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map15) ).
fof(f108_nnf,plain,
link(s2,s0),
inference(nnf_transformation,[status(thm)],[f108]) ).
cnf(c108,plain,
link(s2,s0),
inference(cnf_transformation,[status(esa)],[f108_nnf]) ).
cnf(hi100,axiom,
link(s2,s0) = true,
inference(equality_encoding,[status(esa)],[c108]) ).
cnf(h1092,plain,
s(truck1,s2,s2,s0,s1,truck1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi26,h474,hi100]) ).
cnf(f12,axiom,
( s(O1,O2,O3,truck1,D1,D2,L,T2)
| ~ s(O1,O2,O3,L,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load13) ).
fof(f12_nnf,plain,
! [O1,O2,O3,L,D1,D2,T2] :
( s(O1,O2,O3,truck1,D1,D2,L,T2)
| ~ s(O1,O2,O3,L,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [O1,O2,O3,L,D1,D2,T2] :
( s(O1,O2,O3,truck1,D1,D2,L,T2)
| ~ s(O1,O2,O3,L,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( s(X0,X1,X2,truck1,X4,X5,X3,X6)
| ~ s(X0,X1,X2,X3,X4,X5,X3,X6) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi12,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5,X3,X6),true,s(X0,X1,X2,truck1,X4,X5,X3,X6),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(h2488,plain,
s(truck1,s2,s2,truck1,s1,truck1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi12,h1092]) ).
cnf(f109,axiom,
link(s0,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map16) ).
fof(f109_nnf,plain,
link(s0,s2),
inference(nnf_transformation,[status(thm)],[f109]) ).
cnf(c109,plain,
link(s0,s2),
inference(cnf_transformation,[status(esa)],[f109_nnf]) ).
cnf(hi101,axiom,
link(s0,s2) = true,
inference(equality_encoding,[status(esa)],[c109]) ).
cnf(h5293,plain,
s(truck1,s2,s2,truck1,s1,truck1,s2,s1) = true,
inference(hyper_resolution,[status(thm)],[hi26,h2488,hi101]) ).
cnf(f13,axiom,
( ~ s(O1,O2,O3,truck1,D1,D2,L,T2)
| s(O1,O2,O3,L,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load14) ).
fof(f13_nnf,plain,
! [O1,O2,O3,L,D1,D2,T2] :
( ~ s(O1,O2,O3,truck1,D1,D2,L,T2)
| s(O1,O2,O3,L,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [O1,O2,O3,L,D1,D2,T2] :
( ~ s(O1,O2,O3,truck1,D1,D2,L,T2)
| s(O1,O2,O3,L,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ s(X0,X1,X2,truck1,X4,X5,X3,X6)
| s(X0,X1,X2,X3,X4,X5,X3,X6) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi13,axiom,
ifeq(s(X0,X1,X2,truck1,X3,X4,X5,X6),true,s(X0,X1,X2,X5,X3,X4,X5,X6),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(h10343,plain,
s(truck1,s2,s2,s2,s1,truck1,s2,s1) = true,
inference(hyper_resolution,[status(thm)],[hi13,h5293]) ).
cnf(f8,axiom,
( s(O1,O2,truck1,O4,D1,D2,L,T2)
| ~ s(O1,O2,L,O4,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load9) ).
fof(f8_nnf,plain,
! [O1,O2,L,O4,D1,D2,T2] :
( s(O1,O2,truck1,O4,D1,D2,L,T2)
| ~ s(O1,O2,L,O4,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [O1,O2,L,O4,D1,D2,T2] :
( s(O1,O2,truck1,O4,D1,D2,L,T2)
| ~ s(O1,O2,L,O4,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( s(X0,X1,truck1,X3,X4,X5,X2,X6)
| ~ s(X0,X1,X2,X3,X4,X5,X2,X6) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi8,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5,X2,X6),true,s(X0,X1,truck1,X3,X4,X5,X2,X6),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h18833,plain,
s(truck1,s2,truck1,s2,s1,truck1,s2,s1) = true,
inference(hyper_resolution,[status(thm)],[hi8,h10343]) ).
cnf(f1,axiom,
( ~ s(truck1,O2,O3,O4,D1,D2,L,T2)
| s(L,O2,O3,O4,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load2) ).
fof(f1_nnf,plain,
! [L,O2,O3,O4,D1,D2,T2] :
( ~ s(truck1,O2,O3,O4,D1,D2,L,T2)
| s(L,O2,O3,O4,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [L,O2,O3,O4,D1,D2,T2] :
( ~ s(truck1,O2,O3,O4,D1,D2,L,T2)
| s(L,O2,O3,O4,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ s(truck1,X1,X2,X3,X4,X5,X0,X6)
| s(X0,X1,X2,X3,X4,X5,X0,X6) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi1,axiom,
ifeq(s(truck1,X0,X1,X2,X3,X4,X5,X6),true,s(X5,X0,X1,X2,X3,X4,X5,X6),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h32477,plain,
s(s2,s2,truck1,s2,s1,truck1,s2,s1) = true,
inference(hyper_resolution,[status(thm)],[hi1,h18833]) ).
cnf(h53315,plain,
s(s2,s2,truck1,s2,s1,truck1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi26,h32477,hi100]) ).
cnf(f9,axiom,
( ~ s(O1,O2,truck1,O4,D1,D2,L,T2)
| s(O1,O2,L,O4,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load10) ).
fof(f9_nnf,plain,
! [O1,O2,L,O4,D1,D2,T2] :
( ~ s(O1,O2,truck1,O4,D1,D2,L,T2)
| s(O1,O2,L,O4,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [O1,O2,L,O4,D1,D2,T2] :
( ~ s(O1,O2,truck1,O4,D1,D2,L,T2)
| s(O1,O2,L,O4,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ s(X0,X1,truck1,X3,X4,X5,X2,X6)
| s(X0,X1,X2,X3,X4,X5,X2,X6) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(hi9,axiom,
ifeq(s(X0,X1,truck1,X2,X3,X4,X5,X6),true,s(X0,X1,X5,X2,X3,X4,X5,X6),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h82563,plain,
s(s2,s2,s0,s2,s1,truck1,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi9,h53315]) ).
cnf(f111,negated_conjecture,
~ s(s2,s2,s0,s2,s1,X6,s0,X8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f111_nnf,plain,
! [X6,X8] : ~ s(s2,s2,s0,s2,s1,X6,s0,X8),
inference(nnf_transformation,[status(thm)],[f111]) ).
fof(f111_sk,plain,
! [X6,X8] : ~ s(s2,s2,s0,s2,s1,X6,s0,X8),
inference(skolemisation,[status(esa)],[f111_nnf]) ).
cnf(c111,plain,
~ s(s2,s2,s0,s2,s1,X0,s0,X1),
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
cnf(hi111,negated_conjecture,
ifeq(s(s2,s2,s0,s2,s1,X0,s0,X1),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c111]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi111,h82563]) ).
cnf(t2293,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
cnf(f30,axiom,
~ neq(truck1,truck1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq1) ).
fof(f30_nnf,plain,
~ neq(truck1,truck1),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
~ neq(truck1,truck1),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
~ neq(truck1,truck1),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f39,axiom,
~ neq(truck2,truck2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq10) ).
fof(f39_nnf,plain,
~ neq(truck2,truck2),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
~ neq(truck2,truck2),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
~ neq(truck2,truck2),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(f48,axiom,
~ neq(s0,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq19) ).
fof(f48_nnf,plain,
~ neq(s0,s0),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
~ neq(s0,s0),
inference(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c48,plain,
~ neq(s0,s0),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(f57,axiom,
~ neq(s1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq28) ).
fof(f57_nnf,plain,
~ neq(s1,s1),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
~ neq(s1,s1),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c57,plain,
~ neq(s1,s1),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(f66,axiom,
~ neq(s2,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq37) ).
fof(f66_nnf,plain,
~ neq(s2,s2),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
~ neq(s2,s2),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c66,plain,
~ neq(s2,s2),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(f75,axiom,
~ neq(p0_1,p0_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq46) ).
fof(f75_nnf,plain,
~ neq(p0_1,p0_1),
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
~ neq(p0_1,p0_1),
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
~ neq(p0_1,p0_1),
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(f84,axiom,
~ neq(p1_2,p1_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq55) ).
fof(f84_nnf,plain,
~ neq(p1_2,p1_2),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
~ neq(p1_2,p1_2),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c84,plain,
~ neq(p1_2,p1_2),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(f93,axiom,
~ neq(p2_0,p2_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq64) ).
fof(f93_nnf,plain,
~ neq(p2_0,p2_0),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
~ neq(p2_0,p2_0),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c93,plain,
~ neq(p2_0,p2_0),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c30,c39,c48,c57,c66,c75,c84,c93,c111]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2293]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PLA031-1.003 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 06:14:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 21.18/3.14 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.18/3.14 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------