%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PLA031-1.002 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:30:43 PM UTC 2026
% Result : Unsatisfiable 9.96s 2.01s
% Output : Proof 9.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 25
% Syntax : Number of formulae : 129 ( 89 unt; 0 def)
% Number of atoms : 181 ( 35 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 138 ( 86 ~; 52 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-7 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-4 aty)
% Number of variables : 325 ( 6 sgn 130 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f24,axiom,
( s(O1,O2,O3,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,S,D2,T1,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk1) ).
fof(f24_nnf,plain,
! [O1,O2,O3,S,D2,T1,T2,D] :
( s(O1,O2,O3,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,S,D2,T1,T2) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [O1,O2,O3,S,D2,T1,T2,D] :
( s(O1,O2,O3,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,O3,S,D2,T1,T2) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( s(X0,X1,X2,X7,X4,X5,X6)
| ~ path(X3,X7)
| ~ s(X0,X1,X2,X3,X4,X5,X6) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi24,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5,X6),true,ifeq(path(X3,X7),true,s(X0,X1,X2,X7,X4,X5,X6),true),true) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(f89,axiom,
s(s1,s1,s1,s1,s1,s2,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',init) ).
fof(f89_nnf,plain,
s(s1,s1,s1,s1,s1,s2,s0),
inference(nnf_transformation,[status(thm)],[f89]) ).
cnf(c89,plain,
s(s1,s1,s1,s1,s1,s2,s0),
inference(cnf_transformation,[status(esa)],[f89_nnf]) ).
cnf(hi82,axiom,
s(s1,s1,s1,s1,s1,s2,s0) = true,
inference(equality_encoding,[status(esa)],[c89]) ).
cnf(f81,axiom,
path(s1,p2_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map7) ).
fof(f81_nnf,plain,
path(s1,p2_1),
inference(nnf_transformation,[status(thm)],[f81]) ).
cnf(c81,plain,
path(s1,p2_1),
inference(cnf_transformation,[status(esa)],[f81_nnf]) ).
cnf(hi74,axiom,
path(s1,p2_1) = true,
inference(equality_encoding,[status(esa)],[c81]) ).
cnf(h2,plain,
s(s1,s1,s1,p2_1,s1,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi24,hi82,hi74]) ).
cnf(f80,axiom,
path(p2_1,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map6) ).
fof(f80_nnf,plain,
path(p2_1,s2),
inference(nnf_transformation,[status(thm)],[f80]) ).
cnf(c80,plain,
path(p2_1,s2),
inference(cnf_transformation,[status(esa)],[f80_nnf]) ).
cnf(hi73,axiom,
path(p2_1,s2) = true,
inference(equality_encoding,[status(esa)],[c80]) ).
cnf(h10,plain,
s(s1,s1,s1,s2,s1,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi24,h2,hi73]) ).
cnf(f12,axiom,
( s(O1,O2,O3,truck1,D2,L,T2)
| ~ neq(D2,truck1)
| ~ s(O1,O2,O3,L,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board1) ).
fof(f12_nnf,plain,
! [O1,O2,O3,L,D2,T2] :
( s(O1,O2,O3,truck1,D2,L,T2)
| ~ neq(D2,truck1)
| ~ s(O1,O2,O3,L,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [O1,O2,O3,L,D2,T2] :
( s(O1,O2,O3,truck1,D2,L,T2)
| ~ neq(D2,truck1)
| ~ s(O1,O2,O3,L,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( s(X0,X1,X2,truck1,X4,X3,X5)
| ~ neq(X4,truck1)
| ~ s(X0,X1,X2,X3,X4,X3,X5) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi12,axiom,
ifeq(s(X0,X1,X2,X3,X4,X3,X5),true,ifeq(neq(X4,truck1),true,s(X0,X1,X2,truck1,X4,X3,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(f47,axiom,
neq(s1,truck1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq22) ).
fof(f47_nnf,plain,
neq(s1,truck1),
inference(nnf_transformation,[status(thm)],[f47]) ).
cnf(c47,plain,
neq(s1,truck1),
inference(cnf_transformation,[status(esa)],[f47_nnf]) ).
cnf(hi44,axiom,
neq(s1,truck1) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(h22,plain,
s(s1,s1,s1,truck1,s1,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi12,h10,hi44]) ).
cnf(f20,axiom,
( s(O1,O2,O3,truck1,D2,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,O3,truck1,D2,S,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive1) ).
fof(f20_nnf,plain,
! [O1,O2,O3,D2,S,T2,D] :
( s(O1,O2,O3,truck1,D2,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,O3,truck1,D2,S,T2) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [O1,O2,O3,D2,S,T2,D] :
( s(O1,O2,O3,truck1,D2,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,O3,truck1,D2,S,T2) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( s(X0,X1,X2,truck1,X3,X6,X5)
| ~ link(X4,X6)
| ~ s(X0,X1,X2,truck1,X3,X4,X5) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi20,axiom,
ifeq(s(X0,X1,X2,truck1,X3,X4,X5),true,ifeq(link(X4,X6),true,s(X0,X1,X2,truck1,X3,X6,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(f86,axiom,
link(s2,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map12) ).
fof(f86_nnf,plain,
link(s2,s1),
inference(nnf_transformation,[status(thm)],[f86]) ).
cnf(c86,plain,
link(s2,s1),
inference(cnf_transformation,[status(esa)],[f86_nnf]) ).
cnf(hi79,axiom,
link(s2,s1) = true,
inference(equality_encoding,[status(esa)],[c86]) ).
cnf(h41,plain,
s(s1,s1,s1,truck1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi20,h22,hi79]) ).
cnf(f8,axiom,
( s(O1,O2,truck1,D1,D2,L,T2)
| ~ s(O1,O2,L,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load9) ).
fof(f8_nnf,plain,
! [O1,O2,L,D1,D2,T2] :
( s(O1,O2,truck1,D1,D2,L,T2)
| ~ s(O1,O2,L,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [O1,O2,L,D1,D2,T2] :
( s(O1,O2,truck1,D1,D2,L,T2)
| ~ s(O1,O2,L,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( s(X0,X1,truck1,X3,X4,X2,X5)
| ~ s(X0,X1,X2,X3,X4,X2,X5) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi8,axiom,
ifeq(s(X0,X1,X2,X3,X4,X2,X5),true,s(X0,X1,truck1,X3,X4,X2,X5),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h79,plain,
s(s1,s1,truck1,truck1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi8,h41]) ).
cnf(f4,axiom,
( s(O1,truck1,O3,D1,D2,L,T2)
| ~ s(O1,L,O3,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load5) ).
fof(f4_nnf,plain,
! [O1,L,O3,D1,D2,T2] :
( s(O1,truck1,O3,D1,D2,L,T2)
| ~ s(O1,L,O3,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [O1,L,O3,D1,D2,T2] :
( s(O1,truck1,O3,D1,D2,L,T2)
| ~ s(O1,L,O3,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( s(X0,truck1,X2,X3,X4,X1,X5)
| ~ s(X0,X1,X2,X3,X4,X1,X5) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,axiom,
ifeq(s(X0,X1,X2,X3,X4,X1,X5),true,s(X0,truck1,X2,X3,X4,X1,X5),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h176,plain,
s(s1,truck1,truck1,truck1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi4,h79]) ).
cnf(f0,axiom,
( s(truck1,O2,O3,D1,D2,L,T2)
| ~ s(L,O2,O3,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load1) ).
fof(f0_nnf,plain,
! [L,O2,O3,D1,D2,T2] :
( s(truck1,O2,O3,D1,D2,L,T2)
| ~ s(L,O2,O3,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [L,O2,O3,D1,D2,T2] :
( s(truck1,O2,O3,D1,D2,L,T2)
| ~ s(L,O2,O3,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( s(truck1,X1,X2,X3,X4,X0,X5)
| ~ s(X0,X1,X2,X3,X4,X0,X5) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
ifeq(s(X0,X1,X2,X3,X4,X0,X5),true,s(truck1,X1,X2,X3,X4,X0,X5),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(h416,plain,
s(truck1,truck1,truck1,truck1,s1,s1,s0) = true,
inference(hyper_resolution,[status(thm)],[hi0,h176]) ).
cnf(f84,axiom,
link(s1,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map10) ).
fof(f84_nnf,plain,
link(s1,s0),
inference(nnf_transformation,[status(thm)],[f84]) ).
cnf(c84,plain,
link(s1,s0),
inference(cnf_transformation,[status(esa)],[f84_nnf]) ).
cnf(hi77,axiom,
link(s1,s0) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
cnf(h951,plain,
s(truck1,truck1,truck1,truck1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi20,h416,hi77]) ).
cnf(f5,axiom,
( ~ s(O1,truck1,O3,D1,D2,L,T2)
| s(O1,L,O3,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load6) ).
fof(f5_nnf,plain,
! [O1,L,O3,D1,D2,T2] :
( ~ s(O1,truck1,O3,D1,D2,L,T2)
| s(O1,L,O3,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [O1,L,O3,D1,D2,T2] :
( ~ s(O1,truck1,O3,D1,D2,L,T2)
| s(O1,L,O3,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ s(X0,truck1,X2,X3,X4,X1,X5)
| s(X0,X1,X2,X3,X4,X1,X5) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi5,axiom,
ifeq(s(X0,truck1,X1,X2,X3,X4,X5),true,s(X0,X4,X1,X2,X3,X4,X5),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h2115,plain,
s(truck1,s0,truck1,truck1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi5,h951]) ).
cnf(f1,axiom,
( ~ s(truck1,O2,O3,D1,D2,L,T2)
| s(L,O2,O3,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load2) ).
fof(f1_nnf,plain,
! [L,O2,O3,D1,D2,T2] :
( ~ s(truck1,O2,O3,D1,D2,L,T2)
| s(L,O2,O3,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [L,O2,O3,D1,D2,T2] :
( ~ s(truck1,O2,O3,D1,D2,L,T2)
| s(L,O2,O3,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ s(truck1,X1,X2,X3,X4,X0,X5)
| s(X0,X1,X2,X3,X4,X0,X5) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi1,axiom,
ifeq(s(truck1,X0,X1,X2,X3,X4,X5),true,s(X4,X0,X1,X2,X3,X4,X5),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h4392,plain,
s(s0,s0,truck1,truck1,s1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi1,h2115]) ).
cnf(f88,axiom,
link(s0,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map14) ).
fof(f88_nnf,plain,
link(s0,s2),
inference(nnf_transformation,[status(thm)],[f88]) ).
cnf(c88,plain,
link(s0,s2),
inference(cnf_transformation,[status(esa)],[f88_nnf]) ).
cnf(hi81,axiom,
link(s0,s2) = true,
inference(equality_encoding,[status(esa)],[c88]) ).
cnf(h8185,plain,
s(s0,s0,truck1,truck1,s1,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi20,h4392,hi81]) ).
cnf(f13,axiom,
( ~ s(O1,O2,O3,truck1,D2,L,T2)
| s(O1,O2,O3,L,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board2) ).
fof(f13_nnf,plain,
! [O1,O2,O3,L,D2,T2] :
( ~ s(O1,O2,O3,truck1,D2,L,T2)
| s(O1,O2,O3,L,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [O1,O2,O3,L,D2,T2] :
( ~ s(O1,O2,O3,truck1,D2,L,T2)
| s(O1,O2,O3,L,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ s(X0,X1,X2,truck1,X4,X3,X5)
| s(X0,X1,X2,X3,X4,X3,X5) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi13,axiom,
ifeq(s(X0,X1,X2,truck1,X3,X4,X5),true,s(X0,X1,X2,X4,X3,X4,X5),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(h14117,plain,
s(s0,s0,truck1,s2,s1,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi13,h8185]) ).
cnf(f9,axiom,
( ~ s(O1,O2,truck1,D1,D2,L,T2)
| s(O1,O2,L,D1,D2,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load10) ).
fof(f9_nnf,plain,
! [O1,O2,L,D1,D2,T2] :
( ~ s(O1,O2,truck1,D1,D2,L,T2)
| s(O1,O2,L,D1,D2,L,T2) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [O1,O2,L,D1,D2,T2] :
( ~ s(O1,O2,truck1,D1,D2,L,T2)
| s(O1,O2,L,D1,D2,L,T2) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ s(X0,X1,truck1,X3,X4,X2,X5)
| s(X0,X1,X2,X3,X4,X2,X5) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(hi9,axiom,
ifeq(s(X0,X1,truck1,X2,X3,X4,X5),true,s(X0,X1,X4,X2,X3,X4,X5),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h21675,plain,
s(s0,s0,s2,s2,s1,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi9,h14117]) ).
cnf(f90,negated_conjecture,
~ s(s0,s0,s2,s2,X5,s2,X7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f90_nnf,plain,
! [X5,X7] : ~ s(s0,s0,s2,s2,X5,s2,X7),
inference(nnf_transformation,[status(thm)],[f90]) ).
fof(f90_sk,plain,
! [X5,X7] : ~ s(s0,s0,s2,s2,X5,s2,X7),
inference(skolemisation,[status(esa)],[f90_nnf]) ).
cnf(c90,plain,
~ s(s0,s0,s2,s2,X0,s2,X1),
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
cnf(hi90,negated_conjecture,
ifeq(s(s0,s0,s2,s2,X0,s2,X1),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi90,h21675]) ).
cnf(t2239,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
cnf(f26,axiom,
~ neq(truck1,truck1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq1) ).
fof(f26_nnf,plain,
~ neq(truck1,truck1),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
~ neq(truck1,truck1),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
~ neq(truck1,truck1),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(f34,axiom,
~ neq(truck2,truck2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq9) ).
fof(f34_nnf,plain,
~ neq(truck2,truck2),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
~ neq(truck2,truck2),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
~ neq(truck2,truck2),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(f42,axiom,
~ neq(s0,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq17) ).
fof(f42_nnf,plain,
~ neq(s0,s0),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
~ neq(s0,s0),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
~ neq(s0,s0),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(f50,axiom,
~ neq(s1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq25) ).
fof(f50_nnf,plain,
~ neq(s1,s1),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
~ neq(s1,s1),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
~ neq(s1,s1),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(f58,axiom,
~ neq(s2,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq33) ).
fof(f58_nnf,plain,
~ neq(s2,s2),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
~ neq(s2,s2),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
~ neq(s2,s2),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f66,axiom,
~ neq(p1_0,p1_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq41) ).
fof(f66_nnf,plain,
~ neq(p1_0,p1_0),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
~ neq(p1_0,p1_0),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c66,plain,
~ neq(p1_0,p1_0),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(f74,axiom,
~ neq(p2_1,p2_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq49) ).
fof(f74_nnf,plain,
~ neq(p2_1,p2_1),
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
~ neq(p2_1,p2_1),
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c74,plain,
~ neq(p2_1,p2_1),
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c26,c34,c42,c50,c58,c66,c74,c90]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2239]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA031-1.002 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 06:20:23 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.96/2.01 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.96/2.01 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------