%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PRO009+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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:20 PM UTC 2026
% Result : Theorem 31.88s 9.56s
% Output : Proof 31.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 6
% Syntax : Number of formulae : 56 ( 12 unt; 0 def)
% Number of atoms : 199 ( 11 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 235 ( 92 ~; 87 |; 49 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 92 ( 1 sgn 49 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f49,axiom,
! [X161] :
( occurrence_of(X161,tptp0)
=> ? [X162,X163,X164] :
( leaf_occ(X164,X161)
& next_subocc(X163,X164,tptp0)
& ( occurrence_of(X164,tptp1)
| occurrence_of(X164,tptp2) )
& next_subocc(X162,X163,tptp0)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& occurrence_of(X162,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f49_nnf,plain,
! [X161] :
( ? [X162,X163,X164] :
( leaf_occ(X164,X161)
& next_subocc(X163,X164,tptp0)
& ( occurrence_of(X164,tptp1)
| occurrence_of(X164,tptp2) )
& next_subocc(X162,X163,tptp0)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& occurrence_of(X162,tptp3) )
| ~ occurrence_of(X161,tptp0) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [X161] :
( ( leaf_occ(sk18(X161),X161)
& next_subocc(sk17(X161),sk18(X161),tptp0)
& ( occurrence_of(sk18(X161),tptp1)
| occurrence_of(sk18(X161),tptp2) )
& next_subocc(sk16(X161),sk17(X161),tptp0)
& occurrence_of(sk17(X161),tptp4)
& root_occ(sk16(X161),X161)
& occurrence_of(sk16(X161),tptp3) )
| ~ occurrence_of(X161,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16,sk17,sk18])],[f49_nnf]) ).
cnf(c86,plain,
( occurrence_of(sk18(X0),tptp1)
| occurrence_of(sk18(X0),tptp2)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
fof(f62,conjecture,
! [X165] :
( occurrence_of(X165,tptp0)
=> ? [X166,X167] :
( leaf_occ(X167,X165)
& min_precedes(X166,X167,tptp0)
& ( occurrence_of(X167,tptp1)
| occurrence_of(X167,tptp2) )
& root_occ(X166,X165)
& occurrence_of(X166,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f62_neg,negated_conjecture,
~ ! [X165] :
( occurrence_of(X165,tptp0)
=> ? [X166,X167] :
( leaf_occ(X167,X165)
& min_precedes(X166,X167,tptp0)
& ( occurrence_of(X167,tptp1)
| occurrence_of(X167,tptp2) )
& root_occ(X166,X165)
& occurrence_of(X166,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f62]) ).
fof(f62_nnf,plain,
? [X165] :
( ! [X166,X167] :
( ~ leaf_occ(X167,X165)
| ~ min_precedes(X166,X167,tptp0)
| ( ~ occurrence_of(X167,tptp1)
& ~ occurrence_of(X167,tptp2) )
| ~ root_occ(X166,X165)
| ~ occurrence_of(X166,tptp3) )
& occurrence_of(X165,tptp0) ),
inference(nnf_transformation,[status(thm)],[f62_neg]) ).
fof(f62_sk,plain,
! [X166,X167] :
( ( ~ leaf_occ(X167,sk19)
| ~ min_precedes(X166,X167,tptp0)
| ( ~ occurrence_of(X167,tptp1)
& ~ occurrence_of(X167,tptp2) )
| ~ root_occ(X166,sk19)
| ~ occurrence_of(X166,tptp3) )
& occurrence_of(sk19,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19])],[f62_nnf]) ).
cnf(c101,plain,
occurrence_of(sk19,tptp0),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p620,plain,
( occurrence_of(sk18(sk19),tptp1)
| occurrence_of(sk18(sk19),tptp2) ),
inference(resolution,[status(thm)],[c86,c101]) ).
cnf(c83,plain,
( root_occ(sk16(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p136,plain,
root_occ(sk16(sk19),sk19),
inference(resolution,[status(thm)],[c83,c101]) ).
cnf(c82,plain,
( occurrence_of(sk16(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p117,plain,
occurrence_of(sk16(sk19),tptp3),
inference(resolution,[status(thm)],[c82,c101]) ).
cnf(c103,plain,
( ~ leaf_occ(X2,sk19)
| ~ min_precedes(X1,X2,tptp0)
| ~ occurrence_of(X2,tptp1)
| ~ root_occ(X1,sk19)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p119,plain,
( ~ leaf_occ(X0,sk19)
| ~ min_precedes(sk16(sk19),X0,tptp0)
| ~ occurrence_of(X0,tptp1)
| ~ root_occ(sk16(sk19),sk19) ),
inference(resolution,[status(thm)],[p117,c103]) ).
cnf(p139,plain,
( ~ leaf_occ(X0,sk19)
| ~ min_precedes(sk16(sk19),X0,tptp0)
| ~ occurrence_of(X0,tptp1) ),
inference(resolution,[status(thm)],[p136,p119]) ).
cnf(p799,plain,
( ~ leaf_occ(sk18(sk19),sk19)
| ~ min_precedes(sk16(sk19),sk18(sk19),tptp0)
| occurrence_of(sk18(sk19),tptp2) ),
inference(resolution,[status(thm)],[p620,p139]) ).
fof(f41,axiom,
! [X130,X131,X132,X133] :
( ( X131 != X132
& root_occ(X132,X130)
& leaf_occ(X131,X130)
& occurrence_of(X130,X133) )
=> min_precedes(X132,X131,X133) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_41) ).
fof(f41_nnf,plain,
! [X130,X131,X132,X133] :
( min_precedes(X132,X131,X133)
| X131 = X132
| ~ root_occ(X132,X130)
| ~ leaf_occ(X131,X130)
| ~ occurrence_of(X130,X133) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X130,X133,X131,X132] :
( min_precedes(X132,X131,X133)
| X131 = X132
| ~ root_occ(X132,X130)
| ~ leaf_occ(X131,X130)
| ~ occurrence_of(X130,X133) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c72,plain,
( min_precedes(X2,X1,X3)
| X1 = X2
| ~ root_occ(X2,X0)
| ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X3) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p451,plain,
( min_precedes(X1,X0,tptp0)
| X0 = X1
| ~ root_occ(X1,sk19)
| ~ leaf_occ(X0,sk19) ),
inference(resolution,[status(thm)],[c72,c101]) ).
cnf(c88,plain,
( leaf_occ(sk18(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p158,plain,
leaf_occ(sk18(sk19),sk19),
inference(resolution,[status(thm)],[c88,c101]) ).
cnf(p3140,plain,
( min_precedes(X0,sk18(sk19),tptp0)
| sk18(sk19) = X0
| ~ root_occ(X0,sk19) ),
inference(resolution,[status(thm)],[p451,p158]) ).
cnf(p4643,plain,
( min_precedes(sk16(sk19),sk18(sk19),tptp0)
| sk18(sk19) = sk16(sk19) ),
inference(resolution,[status(thm)],[p3140,p136]) ).
cnf(p8031,plain,
( sk18(sk19) = sk16(sk19)
| ~ leaf_occ(sk18(sk19),sk19)
| occurrence_of(sk18(sk19),tptp2) ),
inference(resolution,[status(thm)],[p799,p4643]) ).
cnf(p8186,plain,
( sk18(sk19) = sk16(sk19)
| occurrence_of(sk18(sk19),tptp2) ),
inference(resolution,[status(thm)],[p8031,p158]) ).
cnf(c87,plain,
( next_subocc(sk17(X0),sk18(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(p631,plain,
next_subocc(sk17(sk19),sk18(sk19),tptp0),
inference(resolution,[status(thm)],[c87,c101]) ).
fof(f22,axiom,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ~ ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(f22_nnf,plain,
! [X60,X61,X62] :
( ( ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X60,X61,X62,X63] :
( ( ( min_precedes(sk7(X60,X61,X62),X61,X62)
& min_precedes(X60,sk7(X60,X61,X62),X62) )
| ~ min_precedes(X60,X61,X62)
| next_subocc(X60,X61,X62) )
& ( ( ( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f22_nnf]) ).
cnf(c35,plain,
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p636,plain,
min_precedes(sk17(sk19),sk18(sk19),tptp0),
inference(resolution,[status(thm)],[p631,c35]) ).
fof(f14,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(f14_nnf,plain,
! [X35,X36,X37] :
( ~ root(X36,X37)
| ~ min_precedes(X35,X36,X37) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X35,X36,X37] :
( ~ root(X36,X37)
| ~ min_precedes(X35,X36,X37) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c24,plain,
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p642,plain,
~ root(sk18(sk19),tptp0),
inference(resolution,[status(thm)],[p636,c24]) ).
cnf(p8217,plain,
( ~ root(sk16(sk19),tptp0)
| occurrence_of(sk18(sk19),tptp2) ),
inference(superposition,[status(thm)],[p8186,p642]) ).
fof(f33,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_33) ).
fof(f33_nnf,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [X99,X100,X101] :
( ( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101)
| root_occ(X99,X100) )
& ( ( root(X99,sk13(X99,X100))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sk13(X99,X100)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13])],[f33_nnf]) ).
cnf(c60,plain,
( root(X0,sk13(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p179,plain,
root(sk16(sk19),tptp0),
inference(resolution,[status(thm)],[c60,p136]) ).
cnf(p8960,plain,
occurrence_of(sk18(sk19),tptp2),
inference(resolution,[status(thm)],[p8217,p179]) ).
cnf(c102,plain,
( ~ leaf_occ(X2,sk19)
| ~ min_precedes(X1,X2,tptp0)
| ~ occurrence_of(X2,tptp2)
| ~ root_occ(X1,sk19)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(p118,plain,
( ~ leaf_occ(X0,sk19)
| ~ min_precedes(sk16(sk19),X0,tptp0)
| ~ occurrence_of(X0,tptp2)
| ~ root_occ(sk16(sk19),sk19) ),
inference(resolution,[status(thm)],[p117,c102]) ).
cnf(p138,plain,
( ~ leaf_occ(X0,sk19)
| ~ min_precedes(sk16(sk19),X0,tptp0)
| ~ occurrence_of(X0,tptp2) ),
inference(resolution,[status(thm)],[p136,p118]) ).
cnf(p8963,plain,
( ~ leaf_occ(sk18(sk19),sk19)
| ~ min_precedes(sk16(sk19),sk18(sk19),tptp0) ),
inference(resolution,[status(thm)],[p8960,p138]) ).
cnf(p9415,plain,
( sk18(sk19) = sk16(sk19)
| ~ leaf_occ(sk18(sk19),sk19) ),
inference(resolution,[status(thm)],[p8963,p4643]) ).
cnf(p9416,plain,
sk18(sk19) = sk16(sk19),
inference(resolution,[status(thm)],[p9415,p158]) ).
cnf(p9503,plain,
~ root(sk16(sk19),tptp0),
inference(demodulation,[status(thm)],[p9416,p642]) ).
cnf(p12135,plain,
$false,
inference(resolution,[status(thm)],[p9503,p179]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO009+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n026.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:31:00 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 31.88/9.56 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 31.88/9.56 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------