%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PRO005+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n019.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:33 PM UTC 2026
% Result : Theorem 86.05s 13.50s
% Output : CNFRefutation 53.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 21
% Syntax : Number of formulae : 191 ( 23 unt; 0 def)
% Number of atoms : 644 ( 44 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 790 ( 337 ~; 353 |; 82 &)
% ( 7 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 3 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 375 ( 0 sgn 342 !; 33 ?; 150 :)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2,X3] :
( ( leaf_occ(X1,X2)
& leaf_occ(X0,X2)
& ~ atomic(X3)
& occurrence_of(X2,X3) )
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
fof(f5,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( ~ ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
& min_precedes(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f6,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
=> ( arboreal(X1)
& arboreal(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_05) ).
fof(f11,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( root(X0,X2)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(f14,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(f15,axiom,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ~ ? [X3] : min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
fof(f21,axiom,
! [X0,X1,X2] :
( ( root_occ(X1,X0)
& occurrence_of(X0,X2) )
=> ~ ? [X3] : min_precedes(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_20) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( leaf_occ(X1,X0)
& occurrence_of(X0,X2) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& occurrence_of(X0,X1) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f24,axiom,
! [X0,X1] :
( ( ~ atomic(X1)
& leaf(X0,X1) )
=> ? [X2] :
( leaf_occ(X0,X2)
& occurrence_of(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_23) ).
fof(f25,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( subactivity_occurrence(X2,X3)
& subactivity_occurrence(X1,X3)
& occurrence_of(X3,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
fof(f33,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( next_subocc(X1,X2,tptp0)
& leaf_occ(X2,X0)
& ( occurrence_of(X2,tptp2)
| occurrence_of(X2,tptp3) )
& root_occ(X1,X0)
& occurrence_of(X1,tptp4) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
fof(f39,axiom,
atomic(tptp1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
fof(f43,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(f44,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f46,axiom,
! [X0,X1] :
( ( ~ leaf_occ(X0,X1)
& arboreal(X0)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,tptp0) )
=> root_occ(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_45) ).
fof(f47,axiom,
! [X0,X1] :
( ( ~ leaf_occ(X0,X1)
& arboreal(X0)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,tptp0) )
=> ? [X2] :
( next_subocc(X0,X2,tptp0)
& occurrence_of(X2,tptp1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_46) ).
fof(f48,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f49,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f50,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f49]) ).
fof(f58,plain,
! [X0,X1,X2,X3] :
( ~ leaf_occ(X1,X2)
| ~ leaf_occ(X0,X2)
| atomic(X3)
| ~ occurrence_of(X2,X3)
| X0 = X1 ),
inference(ennf_transformation,[],[f4]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( ~ leaf_occ(X1,X2)
| ~ leaf_occ(X0,X2)
| atomic(X3)
| ~ occurrence_of(X2,X3)
| X0 = X1 ),
inference(flattening,[],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( ! [X3] :
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) )
& min_precedes(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f61,plain,
! [X0,X1,X2] :
( ~ next_subocc(X0,X1,X2)
| ( arboreal(X1)
& arboreal(X0) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f67,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ( arboreal(X0)
<=> atomic(X1) ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f68,plain,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ! [X3] : ~ min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ~ root_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ! [X3] : ~ min_precedes(X3,X1,X2) ),
inference(ennf_transformation,[],[f21]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ~ root_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ! [X3] : ~ min_precedes(X3,X1,X2) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ! [X3] : ~ min_precedes(X1,X3,X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ! [X3] : ~ min_precedes(X1,X3,X2) ),
inference(flattening,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(ennf_transformation,[],[f23]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(flattening,[],[f78]) ).
fof(f80,plain,
! [X0,X1] :
( atomic(X1)
| ~ leaf(X0,X1)
| ? [X2] :
( leaf_occ(X0,X2)
& occurrence_of(X2,X1) ) ),
inference(ennf_transformation,[],[f24]) ).
fof(f81,plain,
! [X0,X1] :
( atomic(X1)
| ~ leaf(X0,X1)
| ? [X2] :
( leaf_occ(X0,X2)
& occurrence_of(X2,X1) ) ),
inference(flattening,[],[f80]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X2,X0)
| ? [X3] :
( subactivity_occurrence(X2,X3)
& subactivity_occurrence(X1,X3)
& occurrence_of(X3,X0) ) ),
inference(ennf_transformation,[],[f25]) ).
fof(f93,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ? [X1,X2] :
( next_subocc(X1,X2,tptp0)
& leaf_occ(X2,X0)
& ( occurrence_of(X2,tptp2)
| occurrence_of(X2,tptp3) )
& root_occ(X1,X0)
& occurrence_of(X1,tptp4) ) ),
inference(ennf_transformation,[],[f33]) ).
fof(f94,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| root_occ(X0,X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f95,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| root_occ(X0,X1) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ? [X2] :
( next_subocc(X0,X2,tptp0)
& occurrence_of(X2,tptp1) ) ),
inference(ennf_transformation,[],[f47]) ).
fof(f97,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ? [X2] :
( next_subocc(X0,X2,tptp0)
& occurrence_of(X2,tptp1) ) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ( ~ next_subocc(X0,X1,X2)
| ( ! [X3] :
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) )
& min_precedes(X0,X1,X2) ) )
& ( ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f60]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ( ~ next_subocc(X0,X1,X2)
| ( ! [X3] :
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) )
& min_precedes(X0,X1,X2) ) )
& ( ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ( ~ next_subocc(X0,X1,X2)
| ( ! [X4] :
( ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) )
& min_precedes(X0,X1,X2) ) )
& ( ? [X3] :
( min_precedes(X3,X1,X2)
& min_precedes(X0,X3,X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(rectify,[],[f99]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ( ~ next_subocc(X0,X1,X2)
| ( ! [X4] :
( ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) )
& min_precedes(X0,X1,X2) ) )
& ( ( min_precedes(sK0(X0,X1,X2),X1,X2)
& min_precedes(X0,sK0(X0,X1,X2),X2) )
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[f100]) ).
fof(f102,plain,
! [X0,X1] :
( ( ~ root_occ(X0,X1)
| ? [X2] :
( root(X0,X2)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X2) ) )
& ( ! [X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f103,plain,
! [X0,X1] :
( ( ~ root_occ(X0,X1)
| ? [X3] :
( root(X0,X3)
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,X3) ) )
& ( ! [X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| root_occ(X0,X1) ) ),
inference(rectify,[],[f102]) ).
fof(f104,plain,
! [X0,X1] :
( ( ~ root_occ(X0,X1)
| ( root(X0,sK1(X0,X1))
& subactivity_occurrence(X0,X1)
& occurrence_of(X1,sK1(X0,X1)) ) )
& ( ! [X2] :
( ~ root(X0,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2) )
| root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1))],[f103]) ).
fof(f108,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ( ( ~ arboreal(X0)
| atomic(X1) )
& ( ~ atomic(X1)
| arboreal(X0) ) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f109,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X3] : ~ min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) )
& ( ? [X3] : min_precedes(X0,X3,X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f110,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X3] : ~ min_precedes(X0,X3,X1)
& ( ? [X2] : min_precedes(X2,X0,X1)
| root(X0,X1) ) ) )
& ( ? [X3] : min_precedes(X0,X3,X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X5] : ~ min_precedes(X0,X5,X1)
& ( ? [X4] : min_precedes(X4,X0,X1)
| root(X0,X1) ) ) )
& ( ? [X3] : min_precedes(X0,X3,X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(rectify,[],[f110]) ).
fof(f112,plain,
! [X0,X1] :
( ( ~ leaf(X0,X1)
| ( ! [X5] : ~ min_precedes(X0,X5,X1)
& ( min_precedes(sK4(X0,X1),X0,X1)
| root(X0,X1) ) ) )
& ( min_precedes(X0,sK3(X0,X1),X1)
| ( ! [X2] : ~ min_precedes(X2,X0,X1)
& ~ root(X0,X1) )
| leaf(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X3,sK3(X0,X1)),skolemize(X4,sK4(X0,X1))],[f111]) ).
fof(f117,plain,
! [X0,X1] :
( atomic(X1)
| ~ leaf(X0,X1)
| ( leaf_occ(X0,sK7(X0,X1))
& occurrence_of(sK7(X0,X1),X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f81]) ).
fof(f118,plain,
! [X0,X1,X2] :
( ~ min_precedes(X1,X2,X0)
| ( subactivity_occurrence(X2,sK8(X0,X1,X2))
& subactivity_occurrence(X1,sK8(X0,X1,X2))
& occurrence_of(sK8(X0,X1,X2),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f82]) ).
fof(f123,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ( next_subocc(sK14(X0),sK15(X0),tptp0)
& leaf_occ(sK15(X0),X0)
& ( occurrence_of(sK15(X0),tptp2)
| occurrence_of(sK15(X0),tptp3) )
& root_occ(sK14(X0),X0)
& occurrence_of(sK14(X0),tptp4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15]),skolemize(X1,sK14(X0)),skolemize(X2,sK15(X0))],[f93]) ).
fof(f124,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ( next_subocc(X0,sK16(X0),tptp0)
& occurrence_of(sK16(X0),tptp1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X2,sK16(X0))],[f97]) ).
fof(f125,plain,
occurrence_of(sK17,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X0,sK17)],[f50]) ).
fof(f129,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X2)
| ~ leaf_occ(X0,X2)
| atomic(X3)
| ~ occurrence_of(X2,X3)
| X0 = X1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f131,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f101]) ).
fof(f135,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| arboreal(X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f142,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
fof(f151,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f154,plain,
! [X2,X0,X1] :
( min_precedes(X0,sK3(X0,X1),X1)
| ~ min_precedes(X2,X0,X1)
| leaf(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
fof(f166,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ min_precedes(X3,X1,X2) ),
inference(cnf_transformation,[],[f75]) ).
fof(f167,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(cnf_transformation,[],[f77]) ).
fof(f168,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f79]) ).
fof(f169,plain,
! [X0,X1] :
( atomic(X1)
| ~ leaf(X0,X1)
| leaf_occ(X0,sK7(X0,X1)) ),
inference(cnf_transformation,[],[f117]) ).
fof(f170,plain,
! [X0,X1] :
( atomic(X1)
| ~ leaf(X0,X1)
| occurrence_of(sK7(X0,X1),X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f171,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| subactivity_occurrence(X2,sK8(X0,X1,X2)) ),
inference(cnf_transformation,[],[f118]) ).
fof(f173,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK8(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f118]) ).
fof(f188,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| next_subocc(sK14(X0),sK15(X0),tptp0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f189,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK15(X0),X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f190,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| occurrence_of(sK15(X0),tptp2)
| occurrence_of(sK15(X0),tptp3) ),
inference(cnf_transformation,[],[f123]) ).
fof(f191,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| root_occ(sK14(X0),X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f194,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f35]) ).
fof(f198,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f39]) ).
fof(f202,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f43]) ).
fof(f203,plain,
tptp2 != tptp1,
inference(cnf_transformation,[],[f44]) ).
fof(f205,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| root_occ(X0,X1) ),
inference(cnf_transformation,[],[f95]) ).
fof(f206,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK16(X0),tptp0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f207,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16(X0),tptp1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f208,plain,
occurrence_of(sK17,tptp0),
inference(cnf_transformation,[],[f125]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( atomic(X1)
| ( X2 = X3 )
| ~ leaf_occ(X3,X0)
| ~ leaf_occ(X2,X0)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( arboreal(X0)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] :
( subactivity_occurrence(X0,X1)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( arboreal(X0)
| ~ atomic(X1)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i,X2: $i] :
( leaf(X1,X2)
| min_precedes(X1,sK3(X1,X2),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ root_occ(X1,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ leaf_occ(X0,X3)
| ~ occurrence_of(X3,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f167]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( atomic(X1)
| occurrence_of(sK7(X0,X1),X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( atomic(X1)
| leaf_occ(X0,sK7(X0,X1))
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( occurrence_of(sK8(X2,X0,X1),X2)
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] :
( subactivity_occurrence(X1,sK8(X2,X0,X1))
| ~ min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_112,plain,
! [X0: $i] :
( root_occ(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_113,plain,
! [X0: $i] :
( occurrence_of(sK15(X0),tptp2)
| occurrence_of(sK15(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_114,plain,
! [X0: $i] :
( leaf_occ(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_115,plain,
! [X0: $i] :
( next_subocc(sK14(X0),sK15(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_117,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f194]) ).
tcf(c_121,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f198]) ).
tcf(c_125,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f202]) ).
tcf(c_126,plain,
tptp2 != tptp1,
inference(cnf_transformation,[],[f203]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| root_occ(X0,X1)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| occurrence_of(sK16(X0),tptp1)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] :
( leaf_occ(X0,X1)
| next_subocc(X0,sK16(X0),tptp0)
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_131,negated_conjecture,
occurrence_of(sK17,tptp0),
inference(cnf_transformation,[],[f208]) ).
tcf(c_210,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1)
| next_subocc(X0_iProver_occurrence_of_1,sK16(X0_iProver_occurrence_of_1),tptp0)
| ~ arboreal(X0_iProver_occurrence_of_1)
| ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ subactivity_occurrence(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1) ),
inference(subtyping,[status(esa)],[c_130]) ).
tcf(c_211,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1)
| occurrence_of(sK16(X0_iProver_occurrence_of_1),tptp1)
| ~ arboreal(X0_iProver_occurrence_of_1)
| ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ subactivity_occurrence(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1) ),
inference(subtyping,[status(esa)],[c_129]) ).
tcf(c_212,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1)
| root_occ(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1)
| ~ arboreal(X0_iProver_occurrence_of_1)
| ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ subactivity_occurrence(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1) ),
inference(subtyping,[status(esa)],[c_128]) ).
tcf(c_214,plain,
tptp2 != tptp1,
inference(subtyping,[status(esa)],[c_126]) ).
tcf(c_215,plain,
tptp3 != tptp1,
inference(subtyping,[status(esa)],[c_125]) ).
tcf(c_225,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( next_subocc(sK14(X0_iProver_occurrence_of_1),sK15(X0_iProver_occurrence_of_1),tptp0)
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp0) ),
inference(subtyping,[status(esa)],[c_115]) ).
tcf(c_226,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(sK15(X0_iProver_occurrence_of_1),X0_iProver_occurrence_of_1)
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp0) ),
inference(subtyping,[status(esa)],[c_114]) ).
tcf(c_227,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(sK15(X0_iProver_occurrence_of_1),tptp2)
| occurrence_of(sK15(X0_iProver_occurrence_of_1),tptp3)
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp0) ),
inference(subtyping,[status(esa)],[c_113]) ).
tcf(c_228,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( root_occ(sK14(X0_iProver_occurrence_of_1),X0_iProver_occurrence_of_1)
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp0) ),
inference(subtyping,[status(esa)],[c_112]) ).
tcf(c_244,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( subactivity_occurrence(X1_iProver_occurrence_of_1,sK8(X0_iProver_tptp3_0,X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1))
| ~ min_precedes(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_96]) ).
tcf(c_246,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(sK8(X0_iProver_tptp3_0,X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1),X0_iProver_tptp3_0)
| ~ min_precedes(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_94]) ).
tcf(c_247,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0] :
( atomic(X0_iProver_tptp3_0)
| leaf_occ(X0_iProver_occurrence_of_1,sK7(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0))
| ~ leaf(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_93]) ).
tcf(c_248,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0] :
( atomic(X0_iProver_tptp3_0)
| occurrence_of(sK7(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0),X0_iProver_tptp3_0)
| ~ leaf(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_92]) ).
tcf(c_249,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_tptp3_0: iProver_tptp3_0] :
( ( X0_iProver_tptp3_0 = X1_iProver_tptp3_0 )
| ~ occurrence_of(X0_iProver_occurrence_of_1,X1_iProver_tptp3_0)
| ~ occurrence_of(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_91]) ).
tcf(c_250,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1,X2_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ~ leaf_occ(X0_iProver_occurrence_of_1,X2_iProver_occurrence_of_1)
| ~ occurrence_of(X2_iProver_occurrence_of_1,X0_iProver_tptp3_0)
| ~ min_precedes(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_90]) ).
tcf(c_251,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1,X2_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ~ root_occ(X1_iProver_occurrence_of_1,X2_iProver_occurrence_of_1)
| ~ occurrence_of(X2_iProver_occurrence_of_1,X0_iProver_tptp3_0)
| ~ min_precedes(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_89]) ).
tcf(c_264,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf(X1_iProver_occurrence_of_1,X0_iProver_tptp3_0)
| min_precedes(X1_iProver_occurrence_of_1,sK3(X1_iProver_occurrence_of_1,X0_iProver_tptp3_0),X0_iProver_tptp3_0)
| ~ min_precedes(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_76]) ).
tcf(c_267,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0] :
( arboreal(X0_iProver_occurrence_of_1)
| ~ atomic(X0_iProver_tptp3_0)
| ~ occurrence_of(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_73]) ).
tcf(c_274,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( subactivity_occurrence(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1)
| ~ root_occ(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1) ),
inference(subtyping,[status(esa)],[c_66]) ).
tcf(c_283,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( arboreal(X0_iProver_occurrence_of_1)
| ~ next_subocc(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_57]) ).
tcf(c_285,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( min_precedes(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0)
| ~ next_subocc(X0_iProver_occurrence_of_1,X1_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_55]) ).
tcf(c_288,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1,X2_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( atomic(X0_iProver_tptp3_0)
| ( X1_iProver_occurrence_of_1 = X2_iProver_occurrence_of_1 )
| ~ leaf_occ(X2_iProver_occurrence_of_1,X0_iProver_occurrence_of_1)
| ~ leaf_occ(X1_iProver_occurrence_of_1,X0_iProver_occurrence_of_1)
| ~ occurrence_of(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0) ),
inference(subtyping,[status(esa)],[c_52]) ).
tcf(c_294,plain,
! [X0_iProver_tptp3_0: iProver_tptp3_0] : X0_iProver_tptp3_0 = X0_iProver_tptp3_0,
theory(equality) ).
tcf(c_298,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_tptp3_0: iProver_tptp3_0] :
( occurrence_of(X0_iProver_occurrence_of_1,X0_iProver_tptp3_0)
| ~ occurrence_of(X1_iProver_occurrence_of_1,X1_iProver_tptp3_0)
| ( X0_iProver_tptp3_0 != X1_iProver_tptp3_0 )
| ( X0_iProver_occurrence_of_1 != X1_iProver_occurrence_of_1 ) ),
theory(equality) ).
tcf(c_315,plain,
( next_subocc(sK14(sK17),sK15(sK17),tptp0)
| ~ occurrence_of(sK17,tptp0) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_318,plain,
( root_occ(sK14(sK17),sK17)
| ~ occurrence_of(sK17,tptp0) ),
inference(instantiation,[status(thm)],[c_228]) ).
tcf(c_388,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ( tptp2 = tptp1 )
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp1)
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp2) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_390,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ( tptp3 = tptp1 )
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp1)
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp3) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_416,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( arboreal(X0_iProver_occurrence_of_1)
| ~ atomic(tptp1)
| ~ occurrence_of(X0_iProver_occurrence_of_1,tptp1) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_464,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( subactivity_occurrence(sK14(X0_iProver_occurrence_of_1),X0_iProver_occurrence_of_1)
| ~ root_occ(sK14(X0_iProver_occurrence_of_1),X0_iProver_occurrence_of_1) ),
inference(instantiation,[status(thm)],[c_274]) ).
tcf(c_465,plain,
( subactivity_occurrence(sK14(sK17),sK17)
| ~ root_occ(sK14(sK17),sK17) ),
inference(instantiation,[status(thm)],[c_464]) ).
tcf(c_468,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( arboreal(sK14(X0_iProver_occurrence_of_1))
| ~ next_subocc(sK14(X0_iProver_occurrence_of_1),sK15(X0_iProver_occurrence_of_1),tptp0) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_469,plain,
( arboreal(sK14(sK17))
| ~ next_subocc(sK14(sK17),sK15(sK17),tptp0) ),
inference(instantiation,[status(thm)],[c_468]) ).
tcf(c_500,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( min_precedes(sK14(X0_iProver_occurrence_of_1),sK15(X0_iProver_occurrence_of_1),tptp0)
| ~ next_subocc(sK14(X0_iProver_occurrence_of_1),sK15(X0_iProver_occurrence_of_1),tptp0) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_501,plain,
( min_precedes(sK14(sK17),sK15(sK17),tptp0)
| ~ next_subocc(sK14(sK17),sK15(sK17),tptp0) ),
inference(instantiation,[status(thm)],[c_500]) ).
tcf(c_556,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(X0_iProver_occurrence_of_1,tptp1)
| ~ occurrence_of(X1_iProver_occurrence_of_1,X0_iProver_tptp3_0)
| ( tptp1 != X0_iProver_tptp3_0 )
| ( X0_iProver_occurrence_of_1 != X1_iProver_occurrence_of_1 ) ),
inference(instantiation,[status(thm)],[c_298]) ).
tcf(c_623,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(sK14(X0_iProver_occurrence_of_1),X1_iProver_occurrence_of_1)
| next_subocc(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)
| ~ arboreal(sK14(X0_iProver_occurrence_of_1))
| ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ subactivity_occurrence(sK14(X0_iProver_occurrence_of_1),X1_iProver_occurrence_of_1) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_624,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(sK14(X0_iProver_occurrence_of_1),X1_iProver_occurrence_of_1)
| occurrence_of(sK16(sK14(X0_iProver_occurrence_of_1)),tptp1)
| ~ arboreal(sK14(X0_iProver_occurrence_of_1))
| ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ subactivity_occurrence(sK14(X0_iProver_occurrence_of_1),X1_iProver_occurrence_of_1) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_627,plain,
( leaf_occ(sK14(sK17),sK17)
| occurrence_of(sK16(sK14(sK17)),tptp1)
| ~ arboreal(sK14(sK17))
| ~ occurrence_of(sK17,tptp0)
| ~ subactivity_occurrence(sK14(sK17),sK17) ),
inference(instantiation,[status(thm)],[c_624]) ).
tcf(c_628,plain,
( leaf_occ(sK14(sK17),sK17)
| next_subocc(sK14(sK17),sK16(sK14(sK17)),tptp0)
| ~ arboreal(sK14(sK17))
| ~ occurrence_of(sK17,tptp0)
| ~ subactivity_occurrence(sK14(sK17),sK17) ),
inference(instantiation,[status(thm)],[c_623]) ).
tcf(c_653,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ leaf_occ(sK14(X0_iProver_occurrence_of_1),X1_iProver_occurrence_of_1)
| ~ min_precedes(sK14(X0_iProver_occurrence_of_1),sK15(X0_iProver_occurrence_of_1),tptp0) ),
inference(instantiation,[status(thm)],[c_250]) ).
tcf(c_656,plain,
( ~ occurrence_of(sK17,tptp0)
| ~ leaf_occ(sK14(sK17),sK17)
| ~ min_precedes(sK14(sK17),sK15(sK17),tptp0) ),
inference(instantiation,[status(thm)],[c_653]) ).
tcf(c_1309,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(X0_iProver_occurrence_of_1,tptp1)
| ~ occurrence_of(X1_iProver_occurrence_of_1,tptp1)
| ( tptp1 != tptp1 )
| ( X0_iProver_occurrence_of_1 != X1_iProver_occurrence_of_1 ) ),
inference(instantiation,[status(thm)],[c_556]) ).
tcf(c_1310,plain,
tptp1 = tptp1,
inference(instantiation,[status(thm)],[c_294]) ).
tcf(c_1350,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( arboreal(sK16(sK14(X0_iProver_occurrence_of_1)))
| ~ atomic(tptp1)
| ~ occurrence_of(sK16(sK14(X0_iProver_occurrence_of_1)),tptp1) ),
inference(instantiation,[status(thm)],[c_416]) ).
tcf(c_1357,plain,
( arboreal(sK16(sK14(sK17)))
| ~ atomic(tptp1)
| ~ occurrence_of(sK16(sK14(sK17)),tptp1) ),
inference(instantiation,[status(thm)],[c_1350]) ).
tcf(c_1411,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( min_precedes(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)
| ~ next_subocc(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_1416,plain,
( min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| ~ next_subocc(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
inference(instantiation,[status(thm)],[c_1411]) ).
tcf(c_1621,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1,X2_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( atomic(X0_iProver_tptp3_0)
| ( sK15(X0_iProver_occurrence_of_1) = X2_iProver_occurrence_of_1 )
| ~ leaf_occ(X2_iProver_occurrence_of_1,X1_iProver_occurrence_of_1)
| ~ occurrence_of(X1_iProver_occurrence_of_1,X0_iProver_tptp3_0)
| ~ leaf_occ(sK15(X0_iProver_occurrence_of_1),X1_iProver_occurrence_of_1) ),
inference(instantiation,[status(thm)],[c_288]) ).
tcf(c_2003,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(sK16(sK14(X0_iProver_occurrence_of_1)),X1_iProver_occurrence_of_1)
| root_occ(sK16(sK14(X0_iProver_occurrence_of_1)),X1_iProver_occurrence_of_1)
| ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ arboreal(sK16(sK14(X0_iProver_occurrence_of_1)))
| ~ subactivity_occurrence(sK16(sK14(X0_iProver_occurrence_of_1)),X1_iProver_occurrence_of_1) ),
inference(instantiation,[status(thm)],[c_212]) ).
tcf(c_2157,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(X0_iProver_occurrence_of_1,tptp1)
| ~ occurrence_of(sK16(sK14(X1_iProver_occurrence_of_1)),tptp1)
| ( tptp1 != tptp1 )
| ( X0_iProver_occurrence_of_1 != sK16(sK14(X1_iProver_occurrence_of_1)) ) ),
inference(instantiation,[status(thm)],[c_1309]) ).
tcf(c_2303,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)
| min_precedes(sK16(sK14(X0_iProver_occurrence_of_1)),sK3(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),tptp0)
| ~ min_precedes(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_264]) ).
tcf(c_2305,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( subactivity_occurrence(sK16(sK14(X0_iProver_occurrence_of_1)),sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1))))
| ~ min_precedes(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_244]) ).
tcf(c_2312,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ root_occ(sK16(sK14(X0_iProver_occurrence_of_1)),X1_iProver_occurrence_of_1)
| ~ min_precedes(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_251]) ).
tcf(c_2314,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1))),tptp0)
| ~ min_precedes(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_246]) ).
tcf(c_2315,plain,
( occurrence_of(sK8(tptp0,sK14(sK17),sK16(sK14(sK17))),tptp0)
| ~ min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
inference(instantiation,[status(thm)],[c_2314]) ).
tcf(c_2324,plain,
( subactivity_occurrence(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| ~ min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
inference(instantiation,[status(thm)],[c_2305]) ).
tcf(c_2326,plain,
( leaf(sK16(sK14(sK17)),tptp0)
| min_precedes(sK16(sK14(sK17)),sK3(sK16(sK14(sK17)),tptp0),tptp0)
| ~ min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
inference(instantiation,[status(thm)],[c_2303]) ).
tcf(c_5298,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ~ occurrence_of(X1_iProver_occurrence_of_1,tptp0)
| ~ leaf_occ(sK16(sK14(X0_iProver_occurrence_of_1)),X1_iProver_occurrence_of_1)
| ~ min_precedes(sK16(sK14(X0_iProver_occurrence_of_1)),sK3(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),tptp0) ),
inference(instantiation,[status(thm)],[c_250]) ).
tcf(c_6109,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(sK16(sK14(X0_iProver_occurrence_of_1)),sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1))))
| root_occ(sK16(sK14(X0_iProver_occurrence_of_1)),sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1))))
| ~ arboreal(sK16(sK14(X0_iProver_occurrence_of_1)))
| ~ occurrence_of(sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1))),tptp0)
| ~ subactivity_occurrence(sK16(sK14(X0_iProver_occurrence_of_1)),sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)))) ),
inference(instantiation,[status(thm)],[c_2003]) ).
tcf(c_6110,plain,
( leaf_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| ~ arboreal(sK16(sK14(sK17)))
| ~ occurrence_of(sK8(tptp0,sK14(sK17),sK16(sK14(sK17))),tptp0)
| ~ subactivity_occurrence(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17)))) ),
inference(instantiation,[status(thm)],[c_6109]) ).
tcf(c_11423,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( atomic(tptp0)
| leaf_occ(sK16(sK14(X0_iProver_occurrence_of_1)),sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0))
| ~ leaf(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_11426,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( atomic(tptp0)
| occurrence_of(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),tptp0)
| ~ leaf(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0) ),
inference(instantiation,[status(thm)],[c_248]) ).
tcf(c_11429,plain,
( atomic(tptp0)
| occurrence_of(sK7(sK16(sK14(sK17)),tptp0),tptp0)
| ~ leaf(sK16(sK14(sK17)),tptp0) ),
inference(instantiation,[status(thm)],[c_11426]) ).
tcf(c_11432,plain,
( atomic(tptp0)
| leaf_occ(sK16(sK14(sK17)),sK7(sK16(sK14(sK17)),tptp0))
| ~ leaf(sK16(sK14(sK17)),tptp0) ),
inference(instantiation,[status(thm)],[c_11423]) ).
tcf(c_15516,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ~ min_precedes(sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)
| ~ occurrence_of(sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1))),tptp0)
| ~ root_occ(sK16(sK14(X0_iProver_occurrence_of_1)),sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)))) ),
inference(instantiation,[status(thm)],[c_2312]) ).
tcf(c_15517,plain,
( ~ min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| ~ occurrence_of(sK8(tptp0,sK14(sK17),sK16(sK14(sK17))),tptp0)
| ~ root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17)))) ),
inference(instantiation,[status(thm)],[c_15516]) ).
tcf(c_20300,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0,X1_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( atomic(X0_iProver_tptp3_0)
| ( sK15(X1_iProver_occurrence_of_1) = sK16(sK14(X0_iProver_occurrence_of_1)) )
| ~ occurrence_of(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),X0_iProver_tptp3_0)
| ~ leaf_occ(sK15(X1_iProver_occurrence_of_1),sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0))
| ~ leaf_occ(sK16(sK14(X0_iProver_occurrence_of_1)),sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)) ),
inference(instantiation,[status(thm)],[c_1621]) ).
tcf(c_22789,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ~ occurrence_of(sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1))),tptp0)
| ~ min_precedes(sK16(sK14(X0_iProver_occurrence_of_1)),sK3(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),tptp0)
| ~ leaf_occ(sK16(sK14(X0_iProver_occurrence_of_1)),sK8(tptp0,sK14(X0_iProver_occurrence_of_1),sK16(sK14(X0_iProver_occurrence_of_1)))) ),
inference(instantiation,[status(thm)],[c_5298]) ).
tcf(c_22792,plain,
( ~ occurrence_of(sK8(tptp0,sK14(sK17),sK16(sK14(sK17))),tptp0)
| ~ min_precedes(sK16(sK14(sK17)),sK3(sK16(sK14(sK17)),tptp0),tptp0)
| ~ leaf_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17)))) ),
inference(instantiation,[status(thm)],[c_22789]) ).
tcf(c_28448,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1,X0_iProver_tptp3_0: iProver_tptp3_0] :
( atomic(X0_iProver_tptp3_0)
| ( sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)) = sK16(sK14(X0_iProver_occurrence_of_1)) )
| ~ occurrence_of(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),X0_iProver_tptp3_0)
| ~ leaf_occ(sK16(sK14(X0_iProver_occurrence_of_1)),sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0))
| ~ leaf_occ(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)) ),
inference(instantiation,[status(thm)],[c_20300]) ).
tcf(c_28449,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( leaf_occ(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0))
| ~ occurrence_of(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),tptp0) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_28450,plain,
( atomic(tptp0)
| ( sK15(sK7(sK16(sK14(sK17)),tptp0)) = sK16(sK14(sK17)) )
| ~ occurrence_of(sK7(sK16(sK14(sK17)),tptp0),tptp0)
| ~ leaf_occ(sK16(sK14(sK17)),sK7(sK16(sK14(sK17)),tptp0))
| ~ leaf_occ(sK15(sK7(sK16(sK14(sK17)),tptp0)),sK7(sK16(sK14(sK17)),tptp0)) ),
inference(instantiation,[status(thm)],[c_28448]) ).
tcf(c_28451,plain,
( leaf_occ(sK15(sK7(sK16(sK14(sK17)),tptp0)),sK7(sK16(sK14(sK17)),tptp0))
| ~ occurrence_of(sK7(sK16(sK14(sK17)),tptp0),tptp0) ),
inference(instantiation,[status(thm)],[c_28449]) ).
tcf(c_33914,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),tptp1)
| ~ occurrence_of(sK16(sK14(X0_iProver_occurrence_of_1)),tptp1)
| ( tptp1 != tptp1 )
| ( sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)) != sK16(sK14(X0_iProver_occurrence_of_1)) ) ),
inference(instantiation,[status(thm)],[c_2157]) ).
tcf(c_33915,plain,
( occurrence_of(sK15(sK7(sK16(sK14(sK17)),tptp0)),tptp1)
| ~ occurrence_of(sK16(sK14(sK17)),tptp1)
| ( tptp1 != tptp1 )
| ( sK15(sK7(sK16(sK14(sK17)),tptp0)) != sK16(sK14(sK17)) ) ),
inference(instantiation,[status(thm)],[c_33914]) ).
tcf(c_35683,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ( tptp3 = tptp1 )
| ~ occurrence_of(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),tptp1)
| ~ occurrence_of(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),tptp3) ),
inference(instantiation,[status(thm)],[c_390]) ).
tcf(c_35684,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( ( tptp2 = tptp1 )
| ~ occurrence_of(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),tptp1)
| ~ occurrence_of(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),tptp2) ),
inference(instantiation,[status(thm)],[c_388]) ).
tcf(c_35685,plain,
( ( tptp2 = tptp1 )
| ~ occurrence_of(sK15(sK7(sK16(sK14(sK17)),tptp0)),tptp1)
| ~ occurrence_of(sK15(sK7(sK16(sK14(sK17)),tptp0)),tptp2) ),
inference(instantiation,[status(thm)],[c_35684]) ).
tcf(c_35686,plain,
( ( tptp3 = tptp1 )
| ~ occurrence_of(sK15(sK7(sK16(sK14(sK17)),tptp0)),tptp1)
| ~ occurrence_of(sK15(sK7(sK16(sK14(sK17)),tptp0)),tptp3) ),
inference(instantiation,[status(thm)],[c_35683]) ).
tcf(c_60088,plain,
! [X0_iProver_occurrence_of_1: iProver_occurrence_of_1] :
( occurrence_of(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),tptp2)
| occurrence_of(sK15(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0)),tptp3)
| ~ occurrence_of(sK7(sK16(sK14(X0_iProver_occurrence_of_1)),tptp0),tptp0) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_60089,plain,
( occurrence_of(sK15(sK7(sK16(sK14(sK17)),tptp0)),tptp2)
| occurrence_of(sK15(sK7(sK16(sK14(sK17)),tptp0)),tptp3)
| ~ occurrence_of(sK7(sK16(sK14(sK17)),tptp0),tptp0) ),
inference(instantiation,[status(thm)],[c_60088]) ).
tcf(c_60090,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_60089,c_35686,c_35685,c_33915,c_28451,c_28450,c_22792,c_15517,c_11432,c_11429,c_6110,c_2326,c_2324,c_2315,c_1416,c_1357,c_1310,c_656,c_628,c_627,c_501,c_469,c_465,c_318,c_315,c_215,c_214,c_117,c_131,c_121]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO005+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 % Computer : n019.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Thu Sep 24 06:24:34 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.46
% 0.12/0.46 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.46
% 0.12/0.46 % Detected problem language: tptp
% 0.19/0.49 % Proving...
% 86.05/13.50 % SZS status Started for theBenchmark.p
% 86.05/13.50 % SZS status Theorem for theBenchmark.p
% 86.05/13.50
% 86.05/13.50 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 86.05/13.50
% 86.05/13.50 % ------ iProver source info
% 86.05/13.50
% 86.05/13.50 % git: date: 2026-07-19 20:42:38 +0200
% 86.05/13.50 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 86.05/13.50 % git: non_committed_changes: false
% 86.05/13.50
% 86.05/13.50 % ------ Parsing...
% 86.05/13.50 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 86.05/13.50
% 86.05/13.50 % ------ Preprocessing... sf_s rm: 1 0s sf_e %
% 86.05/13.50
% 86.05/13.50 % ------ Preprocessing...%
% 86.05/13.50
% 86.05/13.50 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 86.05/13.50 % ------ Proving...
% 86.05/13.50 % ------ Problem Properties
% 86.05/13.50
% 86.05/13.50 %
% 86.05/13.50 % clauses 83
% 86.05/13.50 % conjectures 1
% 86.05/13.50 % EPR 47
% 86.05/13.50 % Horn 66
% 86.05/13.50 % unary 13
% 86.05/13.50 % binary 40
% 86.05/13.50 % lits 200
% 86.05/13.50 % lits eq 10
% 86.05/13.50 % fd_pure 0
% 86.05/13.50 % fd_pseudo 0
% 86.05/13.50 % fd_cond 0
% 86.05/13.50 % fd_pseudo_cond 4
% 86.05/13.50 % AC symbols 0
% 86.05/13.50
% 86.05/13.50 % ------ Input Options Time Limit: Unbounded
% 86.05/13.50
% 86.05/13.50
% 86.05/13.50 % ------
% 86.05/13.50 % Current options:
% 86.05/13.50 % ------
% 86.05/13.50
% 86.05/13.50
% 86.05/13.50 %
% 86.05/13.50
% 86.05/13.50 % ------ Proving...
% 86.05/13.50 %
% 86.05/13.50
% 86.05/13.50 % SZS status Theorem for theBenchmark.p
% 86.05/13.50
% 86.05/13.50 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 53.53/13.51
%------------------------------------------------------------------------------