%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PRO010+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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:31:21 PM UTC 2026
% Result : Theorem 8.92s 1.66s
% Output : Proof 8.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 8
% Syntax : Number of formulae : 60 ( 10 unt; 0 def)
% Number of atoms : 181 ( 0 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 170 ( 49 ~; 64 |; 44 &)
% ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 95 ( 4 sgn 39 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X19,X20] :
( ( earlier(X20,X19)
& legal(X19) )
=> legal(X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_09) ).
fof(f9_nnf,plain,
! [X19,X20] :
( legal(X20)
| ~ earlier(X20,X19)
| ~ legal(X19) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X19,X20] :
( legal(X20)
| ~ earlier(X20,X19)
| ~ legal(X19) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c12,plain,
( legal(X1)
| ~ earlier(X1,X0)
| ~ legal(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f35,axiom,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(f35_nnf,plain,
! [X105] :
( ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp2)
| occurrence_of(X108,tptp1) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [X105] :
( ( leaf_occ(sk17(X105),X105)
& next_subocc(sk16(X105),sk17(X105),tptp0)
& ( occurrence_of(sk17(X105),tptp2)
| occurrence_of(sk17(X105),tptp1) )
& next_subocc(sk15(X105),sk16(X105),tptp0)
& occurrence_of(sk16(X105),tptp4)
& root_occ(sk15(X105),X105)
& occurrence_of(sk15(X105),tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16,sk17])],[f35_nnf]) ).
cnf(c72,plain,
( leaf_occ(sk17(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
fof(f48,conjecture,
! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( ( occurrence_of(X111,tptp2)
=> ~ ? [X113] :
( min_precedes(X110,X113,tptp0)
& occurrence_of(X113,tptp1) ) )
& ( occurrence_of(X111,tptp1)
=> ~ ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) ) )
& leaf_occ(X111,X109) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f48_neg,negated_conjecture,
~ ! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( ( occurrence_of(X111,tptp2)
=> ~ ? [X113] :
( min_precedes(X110,X113,tptp0)
& occurrence_of(X113,tptp1) ) )
& ( occurrence_of(X111,tptp1)
=> ~ ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) ) )
& leaf_occ(X111,X109) ) ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f48_nnf,plain,
? [X109] :
( ! [X110,X111] :
( ( ? [X113] :
( min_precedes(X110,X113,tptp0)
& occurrence_of(X113,tptp1) )
& occurrence_of(X111,tptp2) )
| ( ? [X112] :
( min_precedes(X110,X112,tptp0)
& occurrence_of(X112,tptp2) )
& occurrence_of(X111,tptp1) )
| ~ leaf_occ(X111,X109) )
& occurrence_of(X109,tptp0) ),
inference(nnf_transformation,[status(thm)],[f48_neg]) ).
fof(f48_sk,plain,
! [X111,X110] :
( ( ( min_precedes(X110,sk20(X110,X111),tptp0)
& occurrence_of(sk20(X110,X111),tptp1)
& occurrence_of(X111,tptp2) )
| ( min_precedes(X110,sk19(X110,X111),tptp0)
& occurrence_of(sk19(X110,X111),tptp2)
& occurrence_of(X111,tptp1) )
| ~ leaf_occ(X111,sk18) )
& occurrence_of(sk18,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk18,sk19,sk20])],[f48_nnf]) ).
cnf(c85,plain,
occurrence_of(sk18,tptp0),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p117,plain,
leaf_occ(sk17(sk18),sk18),
inference(resolution,[status(thm)],[c72,c85]) ).
cnf(c94,plain,
( min_precedes(X1,sk20(X1,X2),tptp0)
| min_precedes(X1,sk19(X1,X2),tptp0)
| ~ leaf_occ(X2,sk18) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p126,plain,
( min_precedes(X0,sk20(X0,sk17(sk18)),tptp0)
| min_precedes(X0,sk19(X0,sk17(sk18)),tptp0) ),
inference(resolution,[status(thm)],[p117,c94]) ).
fof(f15,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_15) ).
fof(f15_nnf,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c25,plain,
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p183,plain,
( precedes(X0,sk20(X0,sk17(sk18)))
| min_precedes(X0,sk19(X0,sk17(sk18)),tptp0) ),
inference(resolution,[status(thm)],[p126,c25]) ).
cnf(p185,plain,
( precedes(X0,sk19(X0,sk17(sk18)))
| precedes(X0,sk20(X0,sk17(sk18))) ),
inference(resolution,[status(thm)],[p183,c25]) ).
fof(f10,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( legal(X22)
& earlier(X21,X22) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(f10_nnf,plain,
! [X21,X22] :
( ( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X21,X22] :
( ( ~ legal(X22)
| ~ earlier(X21,X22)
| precedes(X21,X22) )
& ( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c14,plain,
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p186,plain,
( legal(sk20(X0,sk17(sk18)))
| precedes(X0,sk19(X0,sk17(sk18))) ),
inference(resolution,[status(thm)],[p185,c14]) ).
cnf(p188,plain,
( legal(sk19(X0,sk17(sk18)))
| legal(sk20(X0,sk17(sk18))) ),
inference(resolution,[status(thm)],[p186,c14]) ).
cnf(p239,plain,
( legal(sk19(X1,sk17(sk18)))
| legal(X0)
| ~ earlier(X0,sk20(X1,sk17(sk18))) ),
inference(resolution,[status(thm)],[c12,p188]) ).
cnf(c13,plain,
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p187,plain,
( earlier(X0,sk20(X0,sk17(sk18)))
| precedes(X0,sk19(X0,sk17(sk18))) ),
inference(resolution,[status(thm)],[p185,c13]) ).
cnf(p193,plain,
( legal(sk19(X0,sk17(sk18)))
| earlier(X0,sk20(X0,sk17(sk18))) ),
inference(resolution,[status(thm)],[p187,c14]) ).
cnf(p268,plain,
( legal(sk19(X0,sk17(sk18)))
| legal(sk19(X0,sk17(sk18)))
| legal(X0) ),
inference(resolution,[status(thm)],[p239,p193]) ).
cnf(p270,plain,
( legal(sk19(X0,sk17(sk18)))
| legal(X0) ),
inference(factoring,[status(thm)],[p268]) ).
cnf(p272,plain,
( legal(X1)
| ~ earlier(X1,sk19(X0,sk17(sk18)))
| legal(X0) ),
inference(resolution,[status(thm)],[p270,c12]) ).
cnf(p273,plain,
( ~ earlier(X0,sk19(X0,sk17(sk18)))
| legal(X0) ),
inference(factoring,[status(thm)],[p272]) ).
cnf(p189,plain,
( earlier(X0,sk19(X0,sk17(sk18)))
| legal(sk20(X0,sk17(sk18))) ),
inference(resolution,[status(thm)],[p186,c13]) ).
cnf(p277,plain,
( legal(sk20(X0,sk17(sk18)))
| legal(X0) ),
inference(resolution,[status(thm)],[p273,p189]) ).
cnf(p279,plain,
( legal(X1)
| ~ earlier(X1,sk20(X0,sk17(sk18)))
| legal(X0) ),
inference(resolution,[status(thm)],[p277,c12]) ).
cnf(p284,plain,
( ~ earlier(X0,sk20(X0,sk17(sk18)))
| legal(X0) ),
inference(factoring,[status(thm)],[p279]) ).
cnf(p194,plain,
( earlier(X0,sk19(X0,sk17(sk18)))
| earlier(X0,sk20(X0,sk17(sk18))) ),
inference(resolution,[status(thm)],[p187,c13]) ).
cnf(p288,plain,
( earlier(X0,sk19(X0,sk17(sk18)))
| legal(X0) ),
inference(resolution,[status(thm)],[p284,p194]) ).
cnf(p294,plain,
( legal(X0)
| legal(X0) ),
inference(resolution,[status(thm)],[p288,p273]) ).
cnf(p295,plain,
legal(X0),
inference(factoring,[status(thm)],[p294]) ).
fof(f8,axiom,
! [X18] :
( legal(X18)
=> arboreal(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f8_nnf,plain,
! [X18] :
( arboreal(X18)
| ~ legal(X18) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X18] :
( arboreal(X18)
| ~ legal(X18) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c11,plain,
( arboreal(X0)
| ~ legal(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p296,plain,
arboreal(X0),
inference(resolution,[status(thm)],[p295,c11]) ).
fof(f7,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f7_nnf,plain,
! [X16,X17] :
( ( ( ~ atomic(X17)
| arboreal(X16) )
& ( atomic(X17)
| ~ arboreal(X16) ) )
| ~ occurrence_of(X16,X17) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X16,X17] :
( ( ( ~ atomic(X17)
| arboreal(X16) )
& ( atomic(X17)
| ~ arboreal(X16) ) )
| ~ occurrence_of(X16,X17) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c9,plain,
( atomic(X1)
| ~ arboreal(X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p197,plain,
( atomic(tptp0)
| ~ arboreal(sk18) ),
inference(resolution,[status(thm)],[c9,c85]) ).
cnf(p297,plain,
atomic(tptp0),
inference(resolution,[status(thm)],[p296,p197]) ).
fof(f37,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_37) ).
fof(f37_nnf,plain,
~ atomic(tptp0),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
~ atomic(tptp0),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c74,plain,
~ atomic(tptp0),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p299,plain,
$false,
inference(resolution,[status(thm)],[p297,c74]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO010+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n008.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 06:28:40 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.92/1.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.92/1.66 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------