%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PRO014+4 : 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:23 PM UTC 2026
% Result : Theorem 76.74s 11.94s
% Output : Proof 76.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 11
% Syntax : Number of formulae : 146 ( 6 unt; 0 def)
% Number of atoms : 568 ( 26 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 632 ( 210 ~; 329 |; 81 &)
% ( 3 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 197 ( 2 sgn 102 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f32,axiom,
! [X101,X102] :
( ( ~ leaf_occ(X101,X102)
& arboreal(X101)
& subactivity_occurrence(X101,X102)
& occurrence_of(X102,tptp0) )
=> ? [X103,X104,X105] :
( leaf(X105,tptp0)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
fof(f32_nnf,plain,
! [X101,X102] :
( ? [X103,X104,X105] :
( leaf(X105,tptp0)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [X102,X101] :
( ( leaf(sk14(X101,X102),tptp0)
& next_subocc(sk13(X101,X102),sk14(X101,X102),tptp0)
& ( occurrence_of(sk14(X101,X102),tptp1)
| occurrence_of(sk14(X101,X102),tptp2) )
& next_subocc(sk12(X101,X102),sk13(X101,X102),tptp0)
& occurrence_of(sk13(X101,X102),tptp4)
& next_subocc(X101,sk12(X101,X102),tptp0)
& occurrence_of(sk12(X101,X102),tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12,sk13,sk14])],[f32_nnf]) ).
cnf(c63,plain,
( next_subocc(sk12(X0,X1),sk13(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
fof(f45,conjecture,
! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( leaf(X109,tptp0)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f45_neg,negated_conjecture,
~ ! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( leaf(X109,tptp0)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f45_nnf,plain,
? [X106,X107] :
( ! [X108,X109] :
( ~ leaf(X109,tptp0)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp1)
& ~ occurrence_of(X109,tptp2) )
| ~ next_subocc(X106,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) ),
inference(nnf_transformation,[status(thm)],[f45_neg]) ).
fof(f45_sk,plain,
! [X108,X109] :
( ( ~ leaf(X109,tptp0)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp1)
& ~ occurrence_of(X109,tptp2) )
| ~ next_subocc(sk15,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(sk15,sk16)
& arboreal(sk15)
& subactivity_occurrence(sk15,sk16)
& occurrence_of(sk16,tptp0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk15,sk16])],[f45_nnf]) ).
cnf(c79,plain,
occurrence_of(sk16,tptp0),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p644,plain,
( next_subocc(sk12(X0,sk16),sk13(X0,sk16),tptp0)
| leaf_occ(X0,sk16)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sk16) ),
inference(resolution,[status(thm)],[c63,c79]) ).
cnf(c80,plain,
subactivity_occurrence(sk15,sk16),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p994,plain,
( next_subocc(sk12(sk15,sk16),sk13(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16)
| ~ arboreal(sk15) ),
inference(resolution,[status(thm)],[p644,c80]) ).
cnf(c81,plain,
arboreal(sk15),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p997,plain,
( next_subocc(sk12(sk15,sk16),sk13(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p994,c81]) ).
fof(f26,axiom,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ~ ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_26) ).
fof(f26_nnf,plain,
! [X78,X79,X80] :
( ( ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X78,X79,X80,X81] :
( ( ( min_precedes(sk11(X78,X79,X80),X79,X80)
& min_precedes(X78,sk11(X78,X79,X80),X80) )
| ~ min_precedes(X78,X79,X80)
| next_subocc(X78,X79,X80) )
& ( ( ( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11])],[f26_nnf]) ).
cnf(c51,plain,
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(p1010,plain,
( min_precedes(sk12(sk15,sk16),sk13(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p997,c51]) ).
fof(f27,axiom,
! [X82,X83,X84,X85] :
( ( subactivity_occurrence(X83,X85)
& occurrence_of(X85,X84)
& min_precedes(X82,X83,X84) )
=> subactivity_occurrence(X82,X85) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_27) ).
fof(f27_nnf,plain,
! [X82,X83,X84,X85] :
( subactivity_occurrence(X82,X85)
| ~ subactivity_occurrence(X83,X85)
| ~ occurrence_of(X85,X84)
| ~ min_precedes(X82,X83,X84) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X82,X83,X84,X85] :
( subactivity_occurrence(X82,X85)
| ~ subactivity_occurrence(X83,X85)
| ~ occurrence_of(X85,X84)
| ~ min_precedes(X82,X83,X84) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c55,plain,
( subactivity_occurrence(X0,X3)
| ~ subactivity_occurrence(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p1020,plain,
( subactivity_occurrence(sk12(sk15,sk16),X0)
| ~ subactivity_occurrence(sk13(sk15,sk16),X0)
| ~ occurrence_of(X0,tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1010,c55]) ).
cnf(c65,plain,
( next_subocc(sk13(X0,X1),sk14(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p659,plain,
( next_subocc(sk13(X0,sk16),sk14(X0,sk16),tptp0)
| leaf_occ(X0,sk16)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sk16) ),
inference(resolution,[status(thm)],[c65,c79]) ).
cnf(p1142,plain,
( next_subocc(sk13(sk15,sk16),sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16)
| ~ arboreal(sk15) ),
inference(resolution,[status(thm)],[p659,c80]) ).
cnf(p1145,plain,
( next_subocc(sk13(sk15,sk16),sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1142,c81]) ).
cnf(p1147,plain,
( min_precedes(sk13(sk15,sk16),sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1145,c51]) ).
fof(f6,axiom,
! [X21,X22,X23] :
( min_precedes(X22,X23,X21)
=> ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_06) ).
fof(f6_nnf,plain,
! [X21,X22,X23] :
( ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X22,X23,X21] :
( ( subactivity_occurrence(X23,sk2(X21,X22,X23))
& subactivity_occurrence(X22,sk2(X21,X22,X23))
& occurrence_of(sk2(X21,X22,X23),X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f6_nnf]) ).
cnf(c9,plain,
( occurrence_of(sk2(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p1160,plain,
( occurrence_of(sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1147,c9]) ).
cnf(p1363,plain,
( leaf_occ(sk15,sk16)
| subactivity_occurrence(sk12(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| ~ subactivity_occurrence(sk13(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1020,p1160]) ).
cnf(p17128,plain,
( subactivity_occurrence(sk12(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| ~ subactivity_occurrence(sk13(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p1363]) ).
cnf(c10,plain,
( subactivity_occurrence(X1,sk2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p1161,plain,
( subactivity_occurrence(sk13(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1147,c10]) ).
cnf(p17254,plain,
( leaf_occ(sk15,sk16)
| subactivity_occurrence(sk12(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p17128,p1161]) ).
cnf(p17255,plain,
( subactivity_occurrence(sk12(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p17254]) ).
cnf(c61,plain,
( next_subocc(X0,sk12(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p617,plain,
( next_subocc(X0,sk12(X0,sk16),tptp0)
| leaf_occ(X0,sk16)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sk16) ),
inference(resolution,[status(thm)],[c61,c79]) ).
cnf(p796,plain,
( next_subocc(sk15,sk12(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16)
| ~ arboreal(sk15) ),
inference(resolution,[status(thm)],[p617,c80]) ).
cnf(p799,plain,
( next_subocc(sk15,sk12(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p796,c81]) ).
cnf(p800,plain,
( min_precedes(sk15,sk12(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p799,c51]) ).
cnf(p810,plain,
( subactivity_occurrence(sk15,X0)
| ~ subactivity_occurrence(sk12(sk15,sk16),X0)
| ~ occurrence_of(X0,tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p800,c55]) ).
cnf(p1205,plain,
( subactivity_occurrence(sk15,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| ~ subactivity_occurrence(sk12(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1160,p810]) ).
cnf(p12858,plain,
( subactivity_occurrence(sk15,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| ~ subactivity_occurrence(sk12(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p1205]) ).
cnf(p17348,plain,
( subactivity_occurrence(sk15,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p17255,p12858]) ).
cnf(p17349,plain,
( subactivity_occurrence(sk15,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p17348]) ).
fof(f2,axiom,
! [X8,X9,X10,X11] :
( ( ~ min_precedes(X10,X11,X8)
& arboreal(X10)
& leaf_occ(X11,X9)
& subactivity_occurrence(X10,X9)
& occurrence_of(X9,X8) )
=> X11 = X10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f2_nnf,plain,
! [X8,X9,X10,X11] :
( X11 = X10
| min_precedes(X10,X11,X8)
| ~ arboreal(X10)
| ~ leaf_occ(X11,X9)
| ~ subactivity_occurrence(X10,X9)
| ~ occurrence_of(X9,X8) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X9,X8,X10,X11] :
( X11 = X10
| min_precedes(X10,X11,X8)
| ~ arboreal(X10)
| ~ leaf_occ(X11,X9)
| ~ subactivity_occurrence(X10,X9)
| ~ occurrence_of(X9,X8) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c3,plain,
( X3 = X2
| min_precedes(X2,X3,X0)
| ~ arboreal(X2)
| ~ leaf_occ(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ occurrence_of(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p1187,plain,
( X1 = X0
| min_precedes(X0,X1,tptp0)
| ~ arboreal(X0)
| ~ leaf_occ(X1,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| ~ subactivity_occurrence(X0,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1160,c3]) ).
cnf(p17351,plain,
( X0 = sk15
| min_precedes(sk15,X0,tptp0)
| ~ arboreal(sk15)
| ~ leaf_occ(X0,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p17349,p1187]) ).
cnf(p17366,plain,
( X0 = sk15
| min_precedes(sk15,X0,tptp0)
| ~ arboreal(sk15)
| ~ leaf_occ(X0,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p17351]) ).
fof(f18,axiom,
! [X55,X56] :
( leaf_occ(X55,X56)
<=> ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_18) ).
fof(f18_nnf,plain,
! [X55,X56] :
( ( ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) )
| leaf_occ(X55,X56) )
& ( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X55,X56,X57] :
( ( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57)
| leaf_occ(X55,X56) )
& ( ( leaf(X55,sk8(X55,X56))
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,sk8(X55,X56)) )
| ~ leaf_occ(X55,X56) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8])],[f18_nnf]) ).
cnf(c36,plain,
( ~ leaf(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| leaf_occ(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p1194,plain,
( ~ leaf(X0,tptp0)
| ~ subactivity_occurrence(X0,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(X0,sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1160,c36]) ).
cnf(c11,plain,
( subactivity_occurrence(X2,sk2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p1162,plain,
( subactivity_occurrence(sk14(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1147,c11]) ).
cnf(p11173,plain,
( leaf_occ(sk15,sk16)
| ~ leaf(sk14(sk15,sk16),tptp0)
| leaf_occ(sk14(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1194,p1162]) ).
cnf(p11215,plain,
( ~ leaf(sk14(sk15,sk16),tptp0)
| leaf_occ(sk14(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p11173]) ).
cnf(c66,plain,
( leaf(sk14(X0,X1),tptp0)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p678,plain,
( leaf(sk14(X0,sk16),tptp0)
| leaf_occ(X0,sk16)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sk16) ),
inference(resolution,[status(thm)],[c66,c79]) ).
cnf(p727,plain,
( leaf(sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16)
| ~ arboreal(sk15) ),
inference(resolution,[status(thm)],[p678,c80]) ).
cnf(p733,plain,
( leaf(sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p727,c81]) ).
cnf(p11216,plain,
( leaf_occ(sk15,sk16)
| leaf_occ(sk14(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p11215,p733]) ).
cnf(p11217,plain,
( leaf_occ(sk14(sk15,sk16),sk2(tptp0,sk13(sk15,sk16),sk14(sk15,sk16)))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p11216]) ).
cnf(p17367,plain,
( leaf_occ(sk15,sk16)
| sk14(sk15,sk16) = sk15
| min_precedes(sk15,sk14(sk15,sk16),tptp0)
| ~ arboreal(sk15)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p17366,p11217]) ).
cnf(p17368,plain,
( sk14(sk15,sk16) = sk15
| min_precedes(sk15,sk14(sk15,sk16),tptp0)
| ~ arboreal(sk15)
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p17367]) ).
cnf(p17369,plain,
( sk14(sk15,sk16) = sk15
| min_precedes(sk15,sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p17368,c81]) ).
fof(f31,axiom,
! [X97,X98,X99,X100] :
( ( precedes(X98,X99)
& min_precedes(X97,X99,X100)
& min_precedes(X97,X98,X100) )
=> min_precedes(X98,X99,X100) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_31) ).
fof(f31_nnf,plain,
! [X97,X98,X99,X100] :
( min_precedes(X98,X99,X100)
| ~ precedes(X98,X99)
| ~ min_precedes(X97,X99,X100)
| ~ min_precedes(X97,X98,X100) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [X97,X98,X100,X99] :
( min_precedes(X98,X99,X100)
| ~ precedes(X98,X99)
| ~ min_precedes(X97,X99,X100)
| ~ min_precedes(X97,X98,X100) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c59,plain,
( min_precedes(X1,X2,X3)
| ~ precedes(X1,X2)
| ~ min_precedes(X0,X2,X3)
| ~ min_precedes(X0,X1,X3) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p811,plain,
( min_precedes(sk12(sk15,sk16),X0,tptp0)
| ~ precedes(sk12(sk15,sk16),X0)
| ~ min_precedes(sk15,X0,tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p800,c59]) ).
cnf(p17380,plain,
( min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| ~ precedes(sk12(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p17369,p811]) ).
cnf(p18768,plain,
( min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| ~ precedes(sk12(sk15,sk16),sk14(sk15,sk16))
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p17380]) ).
fof(f24,axiom,
! [X72,X73,X74] :
( min_precedes(X72,X73,X74)
=> precedes(X72,X73) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(f24_nnf,plain,
! [X72,X73,X74] :
( precedes(X72,X73)
| ~ min_precedes(X72,X73,X74) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X72,X73,X74] :
( precedes(X72,X73)
| ~ min_precedes(X72,X73,X74) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c48,plain,
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(p1166,plain,
( precedes(sk13(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1147,c48]) ).
fof(f21,axiom,
! [X63,X64] :
( precedes(X63,X64)
<=> ( legal(X64)
& earlier(X63,X64) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
fof(f21_nnf,plain,
! [X63,X64] :
( ( ~ legal(X64)
| ~ earlier(X63,X64)
| precedes(X63,X64) )
& ( ( legal(X64)
& earlier(X63,X64) )
| ~ precedes(X63,X64) ) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X63,X64] :
( ( ~ legal(X64)
| ~ earlier(X63,X64)
| precedes(X63,X64) )
& ( ( legal(X64)
& earlier(X63,X64) )
| ~ precedes(X63,X64) ) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c42,plain,
( earlier(X0,X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p1169,plain,
( earlier(sk13(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1166,c42]) ).
cnf(p1019,plain,
( precedes(sk12(sk15,sk16),sk13(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1010,c48]) ).
cnf(p1022,plain,
( earlier(sk12(sk15,sk16),sk13(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1019,c42]) ).
fof(f30,axiom,
! [X94,X95,X96] :
( ( earlier(X95,X96)
& earlier(X94,X95) )
=> earlier(X94,X96) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_30) ).
fof(f30_nnf,plain,
! [X94,X95,X96] :
( earlier(X94,X96)
| ~ earlier(X95,X96)
| ~ earlier(X94,X95) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X94,X95,X96] :
( earlier(X94,X96)
| ~ earlier(X95,X96)
| ~ earlier(X94,X95) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c58,plain,
( earlier(X0,X2)
| ~ earlier(X1,X2)
| ~ earlier(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p1025,plain,
( earlier(sk12(sk15,sk16),X0)
| ~ earlier(sk13(sk15,sk16),X0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1022,c58]) ).
cnf(p1175,plain,
( earlier(sk12(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1169,p1025]) ).
cnf(p1241,plain,
( earlier(sk12(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p1175]) ).
cnf(c44,plain,
( ~ legal(X1)
| ~ earlier(X0,X1)
| precedes(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p1243,plain,
( ~ legal(sk14(sk15,sk16))
| precedes(sk12(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1241,c44]) ).
cnf(c43,plain,
( legal(X1)
| ~ precedes(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p1170,plain,
( legal(sk14(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1166,c43]) ).
cnf(p1282,plain,
( leaf_occ(sk15,sk16)
| precedes(sk12(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1243,p1170]) ).
cnf(p1283,plain,
( precedes(sk12(sk15,sk16),sk14(sk15,sk16))
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p1282]) ).
cnf(p18769,plain,
( leaf_occ(sk15,sk16)
| min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p18768,p1283]) ).
cnf(p18770,plain,
( min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p18769]) ).
cnf(c60,plain,
( occurrence_of(sk12(X0,X1),tptp3)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p594,plain,
( occurrence_of(sk12(X0,sk16),tptp3)
| leaf_occ(X0,sk16)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sk16) ),
inference(resolution,[status(thm)],[c60,c79]) ).
cnf(p598,plain,
( occurrence_of(sk12(sk15,sk16),tptp3)
| leaf_occ(sk15,sk16)
| ~ arboreal(sk15) ),
inference(resolution,[status(thm)],[p594,c80]) ).
cnf(p601,plain,
( occurrence_of(sk12(sk15,sk16),tptp3)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p598,c81]) ).
cnf(c84,plain,
( ~ leaf(X3,tptp0)
| ~ min_precedes(X2,X3,tptp0)
| ~ occurrence_of(X3,tptp1)
| ~ next_subocc(sk15,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p603,plain,
( ~ leaf(X0,tptp0)
| ~ min_precedes(sk12(sk15,sk16),X0,tptp0)
| ~ occurrence_of(X0,tptp1)
| ~ next_subocc(sk15,sk12(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p601,c84]) ).
cnf(p3927,plain,
( leaf_occ(sk15,sk16)
| ~ leaf(X0,tptp0)
| ~ min_precedes(sk12(sk15,sk16),X0,tptp0)
| ~ occurrence_of(X0,tptp1)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p603,p799]) ).
cnf(p4045,plain,
( ~ leaf(X0,tptp0)
| ~ min_precedes(sk12(sk15,sk16),X0,tptp0)
| ~ occurrence_of(X0,tptp1)
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p3927]) ).
cnf(c64,plain,
( occurrence_of(sk14(X0,X1),tptp1)
| occurrence_of(sk14(X0,X1),tptp2)
| leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p650,plain,
( occurrence_of(sk14(X0,sk16),tptp1)
| occurrence_of(sk14(X0,sk16),tptp2)
| leaf_occ(X0,sk16)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sk16) ),
inference(resolution,[status(thm)],[c64,c79]) ).
cnf(p1905,plain,
( occurrence_of(sk14(sk15,sk16),tptp1)
| occurrence_of(sk14(sk15,sk16),tptp2)
| leaf_occ(sk15,sk16)
| ~ arboreal(sk15) ),
inference(resolution,[status(thm)],[p650,c80]) ).
cnf(p1918,plain,
( occurrence_of(sk14(sk15,sk16),tptp1)
| occurrence_of(sk14(sk15,sk16),tptp2)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p1905,c81]) ).
cnf(p4046,plain,
( occurrence_of(sk14(sk15,sk16),tptp2)
| leaf_occ(sk15,sk16)
| ~ leaf(sk14(sk15,sk16),tptp0)
| ~ min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p4045,p1918]) ).
cnf(p9970,plain,
( occurrence_of(sk14(sk15,sk16),tptp2)
| ~ leaf(sk14(sk15,sk16),tptp0)
| ~ min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p4046]) ).
cnf(p18781,plain,
( occurrence_of(sk14(sk15,sk16),tptp2)
| ~ leaf(sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p18770,p9970]) ).
cnf(p20000,plain,
( occurrence_of(sk14(sk15,sk16),tptp2)
| ~ leaf(sk14(sk15,sk16),tptp0)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p18781]) ).
cnf(p20001,plain,
( leaf_occ(sk15,sk16)
| occurrence_of(sk14(sk15,sk16),tptp2)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p20000,p733]) ).
cnf(p20002,plain,
( occurrence_of(sk14(sk15,sk16),tptp2)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p20001]) ).
cnf(c83,plain,
( ~ leaf(X3,tptp0)
| ~ min_precedes(X2,X3,tptp0)
| ~ occurrence_of(X3,tptp2)
| ~ next_subocc(sk15,X2,tptp0)
| ~ occurrence_of(X2,tptp3) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p602,plain,
( ~ leaf(X0,tptp0)
| ~ min_precedes(sk12(sk15,sk16),X0,tptp0)
| ~ occurrence_of(X0,tptp2)
| ~ next_subocc(sk15,sk12(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p601,c83]) ).
cnf(p3912,plain,
( leaf_occ(sk15,sk16)
| ~ leaf(X0,tptp0)
| ~ min_precedes(sk12(sk15,sk16),X0,tptp0)
| ~ occurrence_of(X0,tptp2)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p602,p799]) ).
cnf(p4037,plain,
( ~ leaf(X0,tptp0)
| ~ min_precedes(sk12(sk15,sk16),X0,tptp0)
| ~ occurrence_of(X0,tptp2)
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p3912]) ).
cnf(p20104,plain,
( ~ leaf(sk14(sk15,sk16),tptp0)
| ~ min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| leaf_occ(sk15,sk16)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p20002,p4037]) ).
cnf(p21272,plain,
( ~ leaf(sk14(sk15,sk16),tptp0)
| ~ min_precedes(sk12(sk15,sk16),sk14(sk15,sk16),tptp0)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p20104]) ).
cnf(p21273,plain,
( sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16)
| ~ leaf(sk14(sk15,sk16),tptp0)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p21272,p18770]) ).
cnf(p21275,plain,
( leaf_occ(sk15,sk16)
| ~ leaf(sk14(sk15,sk16),tptp0)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p21273]) ).
cnf(p21276,plain,
( ~ leaf(sk14(sk15,sk16),tptp0)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p21275]) ).
cnf(p21279,plain,
( leaf_occ(sk15,sk16)
| sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p21276,p733]) ).
cnf(p21280,plain,
( sk14(sk15,sk16) = sk15
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p21279]) ).
cnf(p21281,plain,
( leaf(sk15,tptp0)
| leaf_occ(sk15,sk16)
| leaf_occ(sk15,sk16) ),
inference(superposition,[status(thm)],[p21280,p733]) ).
cnf(p21831,plain,
( leaf(sk15,tptp0)
| leaf_occ(sk15,sk16) ),
inference(factoring,[status(thm)],[p21281]) ).
cnf(p259,plain,
( ~ leaf(X0,tptp0)
| ~ subactivity_occurrence(X0,sk16)
| leaf_occ(X0,sk16) ),
inference(resolution,[status(thm)],[c36,c79]) ).
cnf(p266,plain,
( ~ leaf(sk15,tptp0)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p259,c80]) ).
cnf(p21836,plain,
( leaf_occ(sk15,sk16)
| leaf_occ(sk15,sk16) ),
inference(resolution,[status(thm)],[p21831,p266]) ).
cnf(p21839,plain,
leaf_occ(sk15,sk16),
inference(factoring,[status(thm)],[p21836]) ).
cnf(c82,plain,
~ leaf_occ(sk15,sk16),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p21840,plain,
$false,
inference(resolution,[status(thm)],[p21839,c82]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 06:33:53 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 76.74/11.94 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 76.74/11.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------