%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:30:42 PM UTC 2026
% Result : Unsatisfiable 19.53s 8.07s
% Output : Proof 19.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 29
% Syntax : Number of formulae : 145 ( 105 unt; 0 def)
% Number of atoms : 209 ( 38 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 166 ( 102 ~; 64 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-6 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-4 aty)
% Number of variables : 280 ( 0 sgn 112 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f21,axiom,
( s(O1,O2,D1,D,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,D1,S,T1,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk2) ).
fof(f21_nnf,plain,
! [O1,O2,D1,S,T1,T2,D] :
( s(O1,O2,D1,D,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,D1,S,T1,T2) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [O1,O2,D1,S,T1,T2,D] :
( s(O1,O2,D1,D,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,D1,S,T1,T2) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( s(X0,X1,X2,X6,X4,X5)
| ~ path(X3,X6)
| ~ s(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(hi21,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5),true,ifeq(path(X3,X6),true,s(X0,X1,X2,X6,X4,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(f104,axiom,
s(s2,s2,s0,s1,s0,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',init) ).
fof(f104_nnf,plain,
s(s2,s2,s0,s1,s0,s2),
inference(nnf_transformation,[status(thm)],[f104]) ).
cnf(c104,plain,
s(s2,s2,s0,s1,s0,s2),
inference(cnf_transformation,[status(esa)],[f104_nnf]) ).
cnf(hi96,axiom,
s(s2,s2,s0,s1,s0,s2) = true,
inference(equality_encoding,[status(esa)],[c104]) ).
cnf(f96,axiom,
path(s1,p2_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map11) ).
fof(f96_nnf,plain,
path(s1,p2_1),
inference(nnf_transformation,[status(thm)],[f96]) ).
cnf(c96,plain,
path(s1,p2_1),
inference(cnf_transformation,[status(esa)],[f96_nnf]) ).
cnf(hi88,axiom,
path(s1,p2_1) = true,
inference(equality_encoding,[status(esa)],[c96]) ).
cnf(h0,plain,
s(s2,s2,s0,p2_1,s0,s2) = true,
inference(hyper_resolution,[status(thm)],[hi21,hi96,hi88]) ).
cnf(f95,axiom,
path(p2_1,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map10) ).
fof(f95_nnf,plain,
path(p2_1,s2),
inference(nnf_transformation,[status(thm)],[f95]) ).
cnf(c95,plain,
path(p2_1,s2),
inference(cnf_transformation,[status(esa)],[f95_nnf]) ).
cnf(hi87,axiom,
path(p2_1,s2) = true,
inference(equality_encoding,[status(esa)],[c95]) ).
cnf(h7,plain,
s(s2,s2,s0,s2,s0,s2) = true,
inference(hyper_resolution,[status(thm)],[hi21,h0,hi87]) ).
cnf(f20,axiom,
( s(O1,O2,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,S,D2,T1,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk1) ).
fof(f20_nnf,plain,
! [O1,O2,S,D2,T1,T2,D] :
( s(O1,O2,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,S,D2,T1,T2) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [O1,O2,S,D2,T1,T2,D] :
( s(O1,O2,D,D2,T1,T2)
| ~ path(S,D)
| ~ s(O1,O2,S,D2,T1,T2) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( s(X0,X1,X6,X3,X4,X5)
| ~ path(X2,X6)
| ~ s(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi20,axiom,
ifeq(s(X0,X1,X2,X3,X4,X5),true,ifeq(path(X2,X6),true,s(X0,X1,X6,X3,X4,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(f92,axiom,
path(s0,p2_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map7) ).
fof(f92_nnf,plain,
path(s0,p2_0),
inference(nnf_transformation,[status(thm)],[f92]) ).
cnf(c92,plain,
path(s0,p2_0),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(hi84,axiom,
path(s0,p2_0) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(h31,plain,
s(s2,s2,p2_0,s2,s0,s2) = true,
inference(hyper_resolution,[status(thm)],[hi20,h7,hi84]) ).
cnf(f91,axiom,
path(p2_0,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map6) ).
fof(f91_nnf,plain,
path(p2_0,s2),
inference(nnf_transformation,[status(thm)],[f91]) ).
cnf(c91,plain,
path(p2_0,s2),
inference(cnf_transformation,[status(esa)],[f91_nnf]) ).
cnf(hi83,axiom,
path(p2_0,s2) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(h87,plain,
s(s2,s2,s2,s2,s0,s2) = true,
inference(hyper_resolution,[status(thm)],[hi20,h31,hi83]) ).
cnf(f14,axiom,
( s(O1,O2,D1,truck2,T1,L)
| ~ neq(D1,truck2)
| ~ s(O1,O2,D1,L,T1,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board7) ).
fof(f14_nnf,plain,
! [O1,O2,D1,L,T1] :
( s(O1,O2,D1,truck2,T1,L)
| ~ neq(D1,truck2)
| ~ s(O1,O2,D1,L,T1,L) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [O1,O2,D1,L,T1] :
( s(O1,O2,D1,truck2,T1,L)
| ~ neq(D1,truck2)
| ~ s(O1,O2,D1,L,T1,L) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( s(X0,X1,X2,truck2,X4,X3)
| ~ neq(X2,truck2)
| ~ s(X0,X1,X2,X3,X4,X3) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi14,axiom,
ifeq(s(X0,X1,X2,X3,X4,X3),true,ifeq(neq(X2,truck2),true,s(X0,X1,X2,truck2,X4,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(f55,axiom,
neq(s2,truck2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq34) ).
fof(f55_nnf,plain,
neq(s2,truck2),
inference(nnf_transformation,[status(thm)],[f55]) ).
cnf(c55,plain,
neq(s2,truck2),
inference(cnf_transformation,[status(esa)],[f55_nnf]) ).
cnf(hi51,axiom,
neq(s2,truck2) = true,
inference(equality_encoding,[status(esa)],[c55]) ).
cnf(h197,plain,
s(s2,s2,s2,truck2,s0,s2) = true,
inference(hyper_resolution,[status(thm)],[hi14,h87,hi51]) ).
cnf(f6,axiom,
( s(O1,truck2,D1,D2,T1,L)
| ~ s(O1,L,D1,D2,T1,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load7) ).
fof(f6_nnf,plain,
! [O1,L,D1,D2,T1] :
( s(O1,truck2,D1,D2,T1,L)
| ~ s(O1,L,D1,D2,T1,L) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [O1,L,D1,D2,T1] :
( s(O1,truck2,D1,D2,T1,L)
| ~ s(O1,L,D1,D2,T1,L) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( s(X0,truck2,X2,X3,X4,X1)
| ~ s(X0,X1,X2,X3,X4,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi6,axiom,
ifeq(s(X0,X1,X2,X3,X4,X1),true,s(X0,truck2,X2,X3,X4,X1),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(h402,plain,
s(s2,truck2,s2,truck2,s0,s2) = true,
inference(hyper_resolution,[status(thm)],[hi6,h197]) ).
cnf(f19,axiom,
( s(O1,O2,D1,truck2,T1,D)
| ~ link(S,D)
| ~ s(O1,O2,D1,truck2,T1,S) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive4) ).
fof(f19_nnf,plain,
! [O1,O2,D1,T1,S,D] :
( s(O1,O2,D1,truck2,T1,D)
| ~ link(S,D)
| ~ s(O1,O2,D1,truck2,T1,S) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [O1,O2,D1,T1,S,D] :
( s(O1,O2,D1,truck2,T1,D)
| ~ link(S,D)
| ~ s(O1,O2,D1,truck2,T1,S) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( s(X0,X1,X2,truck2,X3,X5)
| ~ link(X4,X5)
| ~ s(X0,X1,X2,truck2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(hi19,axiom,
ifeq(s(X0,X1,X2,truck2,X3,X4),true,ifeq(link(X4,X5),true,s(X0,X1,X2,truck2,X3,X5),true),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(f103,axiom,
link(s2,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map18) ).
fof(f103_nnf,plain,
link(s2,s1),
inference(nnf_transformation,[status(thm)],[f103]) ).
cnf(c103,plain,
link(s2,s1),
inference(cnf_transformation,[status(esa)],[f103_nnf]) ).
cnf(hi95,axiom,
link(s2,s1) = true,
inference(equality_encoding,[status(esa)],[c103]) ).
cnf(h778,plain,
s(s2,truck2,s2,truck2,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi19,h402,hi95]) ).
cnf(f7,axiom,
( ~ s(O1,truck2,D1,D2,T1,L)
| s(O1,L,D1,D2,T1,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',load8) ).
fof(f7_nnf,plain,
! [O1,L,D1,D2,T1] :
( ~ s(O1,truck2,D1,D2,T1,L)
| s(O1,L,D1,D2,T1,L) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [O1,L,D1,D2,T1] :
( ~ s(O1,truck2,D1,D2,T1,L)
| s(O1,L,D1,D2,T1,L) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ~ s(X0,truck2,X2,X3,X4,X1)
| s(X0,X1,X2,X3,X4,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi7,axiom,
ifeq(s(X0,truck2,X1,X2,X3,X4),true,s(X0,X4,X1,X2,X3,X4),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(h1454,plain,
s(s2,s1,s2,truck2,s0,s1) = true,
inference(hyper_resolution,[status(thm)],[hi7,h778]) ).
cnf(f99,axiom,
link(s1,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map14) ).
fof(f99_nnf,plain,
link(s1,s0),
inference(nnf_transformation,[status(thm)],[f99]) ).
cnf(c99,plain,
link(s1,s0),
inference(cnf_transformation,[status(esa)],[f99_nnf]) ).
cnf(hi91,axiom,
link(s1,s0) = true,
inference(equality_encoding,[status(esa)],[c99]) ).
cnf(h2572,plain,
s(s2,s1,s2,truck2,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi19,h1454,hi91]) ).
cnf(f15,axiom,
( ~ s(O1,O2,D1,truck2,T1,L)
| s(O1,O2,D1,L,T1,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board8) ).
fof(f15_nnf,plain,
! [O1,O2,D1,L,T1] :
( ~ s(O1,O2,D1,truck2,T1,L)
| s(O1,O2,D1,L,T1,L) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [O1,O2,D1,L,T1] :
( ~ s(O1,O2,D1,truck2,T1,L)
| s(O1,O2,D1,L,T1,L) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( ~ s(X0,X1,X2,truck2,X4,X3)
| s(X0,X1,X2,X3,X4,X3) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi15,axiom,
ifeq(s(X0,X1,X2,truck2,X3,X4),true,s(X0,X1,X2,X4,X3,X4),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(h4233,plain,
s(s2,s1,s2,s0,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi15,h2572]) ).
cnf(f12,axiom,
( s(O1,O2,D1,truck1,L,T2)
| ~ neq(D1,truck1)
| ~ s(O1,O2,D1,L,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board5) ).
fof(f12_nnf,plain,
! [O1,O2,D1,L,T2] :
( s(O1,O2,D1,truck1,L,T2)
| ~ neq(D1,truck1)
| ~ s(O1,O2,D1,L,L,T2) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [O1,O2,D1,L,T2] :
( s(O1,O2,D1,truck1,L,T2)
| ~ neq(D1,truck1)
| ~ s(O1,O2,D1,L,L,T2) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( s(X0,X1,X2,truck1,X3,X4)
| ~ neq(X2,truck1)
| ~ s(X0,X1,X2,X3,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi12,axiom,
ifeq(s(X0,X1,X2,X3,X3,X4),true,ifeq(neq(X2,truck1),true,s(X0,X1,X2,truck1,X3,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(f54,axiom,
neq(s2,truck1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq33) ).
fof(f54_nnf,plain,
neq(s2,truck1),
inference(nnf_transformation,[status(thm)],[f54]) ).
cnf(c54,plain,
neq(s2,truck1),
inference(cnf_transformation,[status(esa)],[f54_nnf]) ).
cnf(hi50,axiom,
neq(s2,truck1) = true,
inference(equality_encoding,[status(esa)],[c54]) ).
cnf(h6403,plain,
s(s2,s1,s2,truck1,s0,s0) = true,
inference(hyper_resolution,[status(thm)],[hi12,h4233,hi50]) ).
cnf(f18,axiom,
( s(O1,O2,D1,truck1,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,D1,truck1,S,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive3) ).
fof(f18_nnf,plain,
! [O1,O2,D1,S,T2,D] :
( s(O1,O2,D1,truck1,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,D1,truck1,S,T2) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [O1,O2,D1,S,T2,D] :
( s(O1,O2,D1,truck1,D,T2)
| ~ link(S,D)
| ~ s(O1,O2,D1,truck1,S,T2) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
( s(X0,X1,X2,truck1,X5,X4)
| ~ link(X3,X5)
| ~ s(X0,X1,X2,truck1,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(hi18,axiom,
ifeq(s(X0,X1,X2,truck1,X3,X4),true,ifeq(link(X3,X5),true,s(X0,X1,X2,truck1,X5,X4),true),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(f100,axiom,
link(s0,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',map15) ).
fof(f100_nnf,plain,
link(s0,s2),
inference(nnf_transformation,[status(thm)],[f100]) ).
cnf(c100,plain,
link(s0,s2),
inference(cnf_transformation,[status(esa)],[f100_nnf]) ).
cnf(hi92,axiom,
link(s0,s2) = true,
inference(equality_encoding,[status(esa)],[c100]) ).
cnf(h8754,plain,
s(s2,s1,s2,truck1,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi18,h6403,hi92]) ).
cnf(f13,axiom,
( ~ s(O1,O2,D1,truck1,L,T2)
| s(O1,O2,D1,L,L,T2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',board6) ).
fof(f13_nnf,plain,
! [O1,O2,D1,L,T2] :
( ~ s(O1,O2,D1,truck1,L,T2)
| s(O1,O2,D1,L,L,T2) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [O1,O2,D1,L,T2] :
( ~ s(O1,O2,D1,truck1,L,T2)
| s(O1,O2,D1,L,L,T2) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( ~ s(X0,X1,X2,truck1,X3,X4)
| s(X0,X1,X2,X3,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi13,axiom,
ifeq(s(X0,X1,X2,truck1,X3,X4),true,s(X0,X1,X2,X3,X3,X4),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(h10851,plain,
s(s2,s1,s2,s2,s2,s0) = true,
inference(hyper_resolution,[status(thm)],[hi13,h8754]) ).
cnf(f105,negated_conjecture,
~ s(s2,s1,s2,s2,s2,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f105_nnf,plain,
~ s(s2,s1,s2,s2,s2,s0),
inference(nnf_transformation,[status(thm)],[f105]) ).
fof(f105_sk,plain,
~ s(s2,s1,s2,s2,s2,s0),
inference(skolemisation,[status(esa)],[f105_nnf]) ).
cnf(c105,plain,
~ s(s2,s1,s2,s2,s2,s0),
inference(cnf_transformation,[status(esa)],[f105_sk]) ).
cnf(hi105,negated_conjecture,
ifeq(s(s2,s1,s2,s2,s2,s0),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c105]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi105,h10851]) ).
cnf(t2127,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
cnf(f22,axiom,
~ neq(truck1,truck1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq1) ).
fof(f22_nnf,plain,
~ neq(truck1,truck1),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
~ neq(truck1,truck1),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
~ neq(truck1,truck1),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(f31,axiom,
~ neq(truck2,truck2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq10) ).
fof(f31_nnf,plain,
~ neq(truck2,truck2),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
~ neq(truck2,truck2),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
~ neq(truck2,truck2),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(f40,axiom,
~ neq(s0,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq19) ).
fof(f40_nnf,plain,
~ neq(s0,s0),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
~ neq(s0,s0),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
~ neq(s0,s0),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(f49,axiom,
~ neq(s1,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq28) ).
fof(f49_nnf,plain,
~ neq(s1,s1),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
~ neq(s1,s1),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
~ neq(s1,s1),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(f58,axiom,
~ neq(s2,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq37) ).
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(f67,axiom,
~ neq(p1_0,p1_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq46) ).
fof(f67_nnf,plain,
~ neq(p1_0,p1_0),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
~ neq(p1_0,p1_0),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c67,plain,
~ neq(p1_0,p1_0),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(f76,axiom,
~ neq(p2_0,p2_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq55) ).
fof(f76_nnf,plain,
~ neq(p2_0,p2_0),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
~ neq(p2_0,p2_0),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c76,plain,
~ neq(p2_0,p2_0),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(f85,axiom,
~ neq(p2_1,p2_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq64) ).
fof(f85_nnf,plain,
~ neq(p2_1,p2_1),
inference(nnf_transformation,[status(thm)],[f85]) ).
fof(f85_sk,plain,
~ neq(p2_1,p2_1),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c85,plain,
~ neq(p2_1,p2_1),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c22,c31,c40,c49,c58,c67,c76,c85,c105]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2127]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA031-1.001 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n014.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Thu Sep 24 06:14:38 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.53/8.07 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.53/8.07 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------