%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO008+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:30:23 PM UTC 2026
% Result : Theorem 11.03s 2.46s
% Output : Refutation 11.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 66
% Syntax : Number of formulae : 545 ( 59 unt; 36 def)
% Number of atoms : 2020 ( 187 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 2585 (1110 ~;1265 |; 144 &)
% ( 41 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 36 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 510 ( 0 sgn 473 !; 37 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos) ).
fof(f2,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(f20,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ atomic(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_19) ).
fof(f23,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(f25,axiom,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
=> ( activity_occurrence(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(f26,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_25) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& arboreal(X2)
& arboreal(X3)
& subactivity_occurrence(X2,X1)
& subactivity_occurrence(X3,X1) )
=> ( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
fof(f30,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X2)
& occurrence_of(X3,X2)
& subactivity_occurrence(X1,X3) )
=> subactivity_occurrence(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_29) ).
fof(f34,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_33) ).
fof(f35,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(f37,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X2,X3)
& ~ atomic(X3)
& leaf_occ(X0,X2)
& leaf_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_36) ).
fof(f38,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(f41,axiom,
! [X0,X1,X2,X3] :
( ( next_subocc(X1,X0,X3)
& next_subocc(X2,X0,X3) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_40) ).
fof(f42,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X0,X3)
& leaf_occ(X1,X0)
& root_occ(X2,X0)
& X1 != X2 )
=> min_precedes(X2,X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_41) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& subactivity_occurrence(X2,X1)
& root_occ(X3,X1)
& arboreal(X2)
& ~ min_precedes(X3,X2,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_42) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& subactivity_occurrence(X2,X1)
& leaf_occ(X3,X1)
& arboreal(X2)
& ~ min_precedes(X2,X3,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_43) ).
fof(f45,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
=> ( arboreal(X0)
& arboreal(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_44) ).
fof(f47,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> arboreal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_46) ).
fof(f50,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2,X3] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& occurrence_of(X2,tptp4)
& next_subocc(X1,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& next_subocc(X2,X3,tptp0)
& leaf_occ(X3,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f53,axiom,
atomic(tptp4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_52) ).
fof(f54,axiom,
atomic(tptp1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_53) ).
fof(f55,axiom,
atomic(tptp2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_54) ).
fof(f56,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_55) ).
fof(f58,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_57) ).
fof(f59,axiom,
tptp4 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_58) ).
fof(f62,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_61) ).
fof(f63,conjecture,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp1)
| occurrence_of(X2,tptp2) )
& min_precedes(X1,X2,tptp0)
& leaf_occ(X2,X0)
& ( occurrence_of(X2,tptp1)
=> ~ ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) ) )
& ( occurrence_of(X2,tptp2)
=> ~ ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f64,negated_conjecture,
~ ! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp1)
| occurrence_of(X2,tptp2) )
& min_precedes(X1,X2,tptp0)
& leaf_occ(X2,X0)
& ( occurrence_of(X2,tptp1)
=> ~ ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) ) )
& ( occurrence_of(X2,tptp2)
=> ~ ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f63]) ).
fof(f65,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f66,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f67,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f68,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f67]) ).
fof(f75,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f89,plain,
! [X0,X1,X2] :
( ~ atomic(X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f20]) ).
fof(f93,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f94,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f95,plain,
! [X0,X1,X2] :
( ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(flattening,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(ennf_transformation,[],[f30]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f102]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(ennf_transformation,[],[f37]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f114]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( X1 = X2
| ~ next_subocc(X1,X0,X3)
| ~ next_subocc(X2,X0,X3) ),
inference(ennf_transformation,[],[f41]) ).
fof(f121,plain,
! [X0,X1,X2,X3] :
( X1 = X2
| ~ next_subocc(X1,X0,X3)
| ~ next_subocc(X2,X0,X3) ),
inference(flattening,[],[f120]) ).
fof(f122,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X1,X3)
| ~ occurrence_of(X0,X3)
| ~ leaf_occ(X1,X0)
| ~ root_occ(X2,X0)
| X1 = X2 ),
inference(ennf_transformation,[],[f42]) ).
fof(f123,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X1,X3)
| ~ occurrence_of(X0,X3)
| ~ leaf_occ(X1,X0)
| ~ root_occ(X2,X0)
| X1 = X2 ),
inference(flattening,[],[f122]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ root_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X3,X2,X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f125,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ root_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X3,X2,X0) ),
inference(flattening,[],[f124]) ).
fof(f126,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ leaf_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f127,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ leaf_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(flattening,[],[f126]) ).
fof(f128,plain,
! [X0,X1,X2] :
( ( arboreal(X0)
& arboreal(X1) )
| ~ next_subocc(X0,X1,X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f131,plain,
! [X0,X1,X2] :
( arboreal(X0)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f47]) ).
fof(f136,plain,
! [X0] :
( ? [X1,X2,X3] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& occurrence_of(X2,tptp4)
& next_subocc(X1,X2,tptp0)
& ( occurrence_of(X3,tptp1)
| occurrence_of(X3,tptp2) )
& next_subocc(X2,X3,tptp0)
& leaf_occ(X3,X0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f137,plain,
? [X0] :
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,X0)
| ( ~ occurrence_of(X2,tptp1)
& ~ occurrence_of(X2,tptp2) )
| ~ min_precedes(X1,X2,tptp0)
| ~ leaf_occ(X2,X0)
| ( ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) )
& occurrence_of(X2,tptp1) )
| ( ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) )
& occurrence_of(X2,tptp2) ) )
& occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f138,definition,
! [X0,X1,X2] :
( ( ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) )
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f139,plain,
? [X0] :
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,X0)
| ( ~ occurrence_of(X2,tptp1)
& ~ occurrence_of(X2,tptp2) )
| ~ min_precedes(X1,X2,tptp0)
| ~ leaf_occ(X2,X0)
| ( ? [X3] :
( occurrence_of(X3,tptp2)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) )
& occurrence_of(X2,tptp1) )
| sP0(X0,X1,X2) )
& occurrence_of(X0,tptp0) ),
inference(definition_folding,[],[f137,f138]) ).
fof(f140,plain,
! [X0] :
( ( activity(sK1(X0))
& occurrence_of(X0,sK1(X0)) )
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X1,sK1(X0))],[f66]) ).
fof(f141,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f75]) ).
fof(f151,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f152,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(flattening,[],[f151]) ).
fof(f153,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(rectify,[],[f152]) ).
fof(f154,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK8(X0,X1,X2),X2)
& min_precedes(sK8(X0,X1,X2),X1,X2) ) )
& ( ( min_precedes(X0,X1,X2)
& ! [X4] :
( ~ min_precedes(X0,X4,X2)
| ~ min_precedes(X4,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f153]) ).
fof(f158,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK10(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK10(X0,X1,X2))
& subactivity_occurrence(X2,sK10(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X3,sK10(X0,X1,X2))],[f95]) ).
fof(f162,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) )
| ~ root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f163,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& root(X0,X3) )
| ~ root_occ(X0,X1) ) ),
inference(rectify,[],[f162]) ).
fof(f164,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK14(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK14(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X3,sK14(X0,X1))],[f163]) ).
fof(f165,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f166,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& leaf(X0,X3) )
| ~ leaf_occ(X0,X1) ) ),
inference(rectify,[],[f165]) ).
fof(f167,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ( occurrence_of(X1,sK15(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK15(X0,X1)) )
| ~ leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X3,sK15(X0,X1))],[f166]) ).
fof(f169,plain,
! [X0] :
( ( occurrence_of(sK17(X0),tptp3)
& root_occ(sK17(X0),X0)
& occurrence_of(sK18(X0),tptp4)
& next_subocc(sK17(X0),sK18(X0),tptp0)
& ( occurrence_of(sK19(X0),tptp1)
| occurrence_of(sK19(X0),tptp2) )
& next_subocc(sK18(X0),sK19(X0),tptp0)
& leaf_occ(sK19(X0),X0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X1,sK17(X0)),skolemize(X2,sK18(X0)),skolemize(X3,sK19(X0))],[f136]) ).
fof(f170,plain,
! [X0,X1,X2] :
( ( ? [X4] :
( occurrence_of(X4,tptp1)
& subactivity_occurrence(X4,X0)
& min_precedes(X1,X4,tptp0) )
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
inference(nnf_transformation,[],[f138]) ).
fof(f171,plain,
! [X0,X1,X2] :
( ( ? [X3] :
( occurrence_of(X3,tptp1)
& subactivity_occurrence(X3,X0)
& min_precedes(X1,X3,tptp0) )
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
inference(rectify,[],[f170]) ).
fof(f172,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK20(X0,X1),tptp1)
& subactivity_occurrence(sK20(X0,X1),X0)
& min_precedes(X1,sK20(X0,X1),tptp0)
& occurrence_of(X2,tptp2) )
| ~ sP0(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X3,sK20(X0,X1))],[f171]) ).
fof(f173,plain,
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,sK21)
| ( ~ occurrence_of(X2,tptp1)
& ~ occurrence_of(X2,tptp2) )
| ~ min_precedes(X1,X2,tptp0)
| ~ leaf_occ(X2,sK21)
| ( occurrence_of(sK22(X1),tptp2)
& subactivity_occurrence(sK22(X1),sK21)
& min_precedes(X1,sK22(X1),tptp0)
& occurrence_of(X2,tptp1) )
| sP0(sK21,X1,X2) )
& occurrence_of(sK21,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22]),skolemize(X0,sK21),skolemize(X3,sK22(X1))],[f139]) ).
fof(f174,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f65]) ).
fof(f176,plain,
! [X0] :
( occurrence_of(X0,sK1(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f178,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f68]) ).
fof(f184,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f82]) ).
fof(f203,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ atomic(X2) ),
inference(cnf_transformation,[],[f89]) ).
fof(f209,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f154]) ).
fof(f210,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f154]) ).
fof(f218,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[],[f94]) ).
fof(f219,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK10(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f220,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK10(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f221,plain,
! [X2,X0,X1] :
( occurrence_of(sK10(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f226,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f227,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(cnf_transformation,[],[f103]) ).
fof(f232,plain,
! [X0,X1] :
( root(X0,sK14(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
fof(f233,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
fof(f234,plain,
! [X0,X1] :
( occurrence_of(X1,sK14(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
fof(f236,plain,
! [X0,X1] :
( leaf(X0,sK15(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f237,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f238,plain,
! [X0,X1] :
( occurrence_of(X1,sK15(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f239,plain,
! [X2,X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,X2)
| leaf_occ(X0,X1)
| ~ leaf(X0,X2) ),
inference(cnf_transformation,[],[f167]) ).
fof(f241,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f113]) ).
fof(f242,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f245,plain,
! [X2,X3,X0,X1] :
( ~ next_subocc(X2,X0,X3)
| ~ next_subocc(X1,X0,X3)
| X1 = X2 ),
inference(cnf_transformation,[],[f121]) ).
fof(f246,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X3)
| min_precedes(X2,X1,X3)
| ~ root_occ(X2,X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f123]) ).
fof(f247,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X3,X1)
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| X2 = X3
| ~ arboreal(X2)
| min_precedes(X3,X2,X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f248,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X3,X1)
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| X2 = X3
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f249,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| arboreal(X1) ),
inference(cnf_transformation,[],[f128]) ).
fof(f253,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| arboreal(X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f256,plain,
! [X0] :
( leaf_occ(sK19(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f257,plain,
! [X0] :
( next_subocc(sK18(X0),sK19(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f258,plain,
! [X0] :
( occurrence_of(sK19(X0),tptp2)
| occurrence_of(sK19(X0),tptp1)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f259,plain,
! [X0] :
( next_subocc(sK17(X0),sK18(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f260,plain,
! [X0] :
( occurrence_of(sK18(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f261,plain,
! [X0] :
( root_occ(sK17(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f262,plain,
! [X0] :
( occurrence_of(sK17(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f265,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f53]) ).
fof(f266,plain,
atomic(tptp1),
inference(cnf_transformation,[],[f54]) ).
fof(f267,plain,
atomic(tptp2),
inference(cnf_transformation,[],[f55]) ).
fof(f268,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f56]) ).
fof(f270,plain,
tptp4 != tptp1,
inference(cnf_transformation,[],[f58]) ).
fof(f271,plain,
tptp4 != tptp2,
inference(cnf_transformation,[],[f59]) ).
fof(f274,plain,
tptp1 != tptp2,
inference(cnf_transformation,[],[f62]) ).
fof(f275,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| occurrence_of(X2,tptp2) ),
inference(cnf_transformation,[],[f172]) ).
fof(f276,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| min_precedes(X1,sK20(X0,X1),tptp0) ),
inference(cnf_transformation,[],[f172]) ).
fof(f277,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| subactivity_occurrence(sK20(X0,X1),X0) ),
inference(cnf_transformation,[],[f172]) ).
fof(f278,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| occurrence_of(sK20(X0,X1),tptp1) ),
inference(cnf_transformation,[],[f172]) ).
fof(f279,plain,
occurrence_of(sK21,tptp0),
inference(cnf_transformation,[],[f173]) ).
fof(f280,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK21)
| ~ occurrence_of(X2,tptp2)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK21)
| occurrence_of(X2,tptp1)
| sP0(sK21,X1,X2) ),
inference(cnf_transformation,[],[f173]) ).
fof(f285,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK21)
| ~ occurrence_of(X2,tptp1)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK21)
| min_precedes(X1,sK22(X1),tptp0)
| sP0(sK21,X1,X2) ),
inference(cnf_transformation,[],[f173]) ).
fof(f286,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK21)
| ~ occurrence_of(X2,tptp1)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK21)
| subactivity_occurrence(sK22(X1),sK21)
| sP0(sK21,X1,X2) ),
inference(cnf_transformation,[],[f173]) ).
fof(f287,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK21)
| ~ occurrence_of(X2,tptp1)
| ~ occurrence_of(X1,tptp3)
| ~ leaf_occ(X2,sK21)
| occurrence_of(sK22(X1),tptp2)
| sP0(sK21,X1,X2) ),
inference(cnf_transformation,[],[f173]) ).
fof(f288,plain,
! [X0] :
( ~ occurrence_of(sK21,X0)
| tptp0 = X0 ),
inference(resolution,[],[f178,f279]) ).
fof(f291,plain,
! [X2,X0,X1] :
( min_precedes(X2,sK19(X0),X1)
| ~ occurrence_of(X0,X1)
| ~ root_occ(X2,X0)
| sK19(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f246,f256]) ).
fof(f295,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X1,sK10(X3,X4,X0))
| X0 = X1
| ~ occurrence_of(sK10(X3,X4,X0),X2)
| ~ arboreal(X1)
| ~ arboreal(X0)
| min_precedes(X0,X1,X2)
| min_precedes(X1,X0,X2)
| ~ min_precedes(X4,X0,X3) ),
inference(resolution,[],[f226,f219]) ).
fof(f296,plain,
! [X2,X3,X0,X1,X4] :
( min_precedes(X0,X1,X2)
| X0 = X1
| ~ occurrence_of(sK10(X3,X0,X4),X2)
| ~ arboreal(X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X1,sK10(X3,X0,X4))
| min_precedes(X1,X0,X2)
| ~ min_precedes(X0,X4,X3) ),
inference(resolution,[],[f226,f220]) ).
fof(f297,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X1,sK10(X3,X0,X4))
| X0 = X1
| ~ occurrence_of(sK10(X3,X0,X4),X2)
| ~ arboreal(X1)
| min_precedes(X0,X1,X2)
| min_precedes(X1,X0,X2)
| ~ min_precedes(X0,X4,X3) ),
inference(forward_subsumption_resolution,[],[f296,f253]) ).
fof(f303,plain,
! [X2,X0,X1] :
( min_precedes(X2,sK19(X0),X1)
| ~ subactivity_occurrence(X2,X0)
| sK19(X0) = X2
| ~ arboreal(X2)
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f248,f256]) ).
fof(f307,plain,
! [X2,X0,X1] :
( min_precedes(sK17(X0),X2,X1)
| ~ subactivity_occurrence(X2,X0)
| sK17(X0) = X2
| ~ arboreal(X2)
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f247,f261]) ).
fof(f308,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp3)
| arboreal(sK17(X0)) ),
inference(resolution,[],[f262,f184]) ).
fof(f310,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK17(X0)) ),
inference(forward_subsumption_resolution,[],[f308,f268]) ).
fof(f315,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK10(X2,X0,X1),X3)
| ~ min_precedes(X0,X1,X2)
| X2 = X3 ),
inference(resolution,[],[f221,f178]) ).
fof(f316,plain,
! [X0] :
( min_precedes(sK17(X0),sK18(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f259,f210]) ).
fof(f320,plain,
! [X0] :
( min_precedes(sK18(X0),sK19(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f257,f210]) ).
fof(f325,plain,
! [X0,X1] :
( ~ next_subocc(X0,sK19(X1),tptp0)
| sK18(X1) = X0
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f245,f257]) ).
fof(f326,plain,
! [X0,X1] :
( ~ min_precedes(sK17(X1),X0,tptp0)
| ~ min_precedes(X0,sK18(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f209,f259]) ).
fof(f327,plain,
! [X0,X1] :
( ~ min_precedes(sK18(X1),X0,tptp0)
| ~ min_precedes(X0,sK19(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f209,f257]) ).
fof(f328,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK18(X0)) ),
inference(resolution,[],[f260,f184]) ).
fof(f330,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK18(X0)) ),
inference(forward_subsumption_resolution,[],[f328,f265]) ).
fof(f340,plain,
! [X0] :
( subactivity_occurrence(sK19(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f237,f256]) ).
fof(f349,plain,
! [X2,X0,X1] :
( ~ leaf_occ(X2,X0)
| atomic(X1)
| ~ occurrence_of(X0,X1)
| sK19(X0) = X2
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f241,f256]) ).
fof(f360,definition,
( spl23_2
<=> sK17(sK21) = sK19(sK21) ),
introduced(definition,[new_symbols(definition,[spl23_2])],[avatar_definition]) ).
fof(f361,plain,
( sK17(sK21) != sK19(sK21)
| spl23_2 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f362,plain,
( sK17(sK21) = sK19(sK21)
| ~ spl23_2 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f364,plain,
( min_precedes(sK19(sK21),sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_2 ),
inference(superposition,[],[f316,f362]) ).
fof(f374,plain,
( min_precedes(sK19(sK21),sK18(sK21),tptp0)
| ~ spl23_2 ),
inference(forward_subsumption_resolution,[],[f364,f279]) ).
fof(f382,plain,
( ! [X0] :
( ~ leaf_occ(sK19(sK21),X0)
| ~ occurrence_of(X0,tptp0) )
| ~ spl23_2 ),
inference(resolution,[],[f374,f242]) ).
fof(f411,plain,
( ~ occurrence_of(sK21,tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_2 ),
inference(resolution,[],[f382,f256]) ).
fof(f412,plain,
( ~ occurrence_of(sK21,tptp0)
| ~ spl23_2 ),
inference(duplicate_literal_removal,[],[f411]) ).
fof(f413,plain,
( $false
| ~ spl23_2 ),
inference(forward_subsumption_resolution,[],[f412,f279]) ).
fof(f414,plain,
~ spl23_2,
inference(avatar_contradiction_clause,[],[f413]) ).
fof(f431,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK19(X0)) ),
inference(resolution,[],[f249,f257]) ).
fof(f433,plain,
arboreal(sK19(sK21)),
inference(resolution,[],[f431,f279]) ).
fof(f513,plain,
activity_occurrence(sK21),
inference(resolution,[],[f174,f279]) ).
fof(f515,plain,
! [X0,X1] :
( arboreal(sK17(sK10(tptp0,X0,X1)))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f310,f221]) ).
fof(f576,plain,
! [X0,X1] :
( ~ subactivity_occurrence(sK19(X0),X1)
| ~ occurrence_of(X1,tptp0)
| subactivity_occurrence(sK18(X0),X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f227,f320]) ).
fof(f656,plain,
arboreal(sK18(sK21)),
inference(resolution,[],[f330,f279]) ).
fof(f681,plain,
! [X0,X1] :
( ~ activity_occurrence(X0)
| ~ occurrence_of(X0,X1)
| sK1(X0) = X1 ),
inference(resolution,[],[f176,f178]) ).
fof(f683,plain,
( ~ activity_occurrence(sK21)
| tptp0 = sK1(sK21) ),
inference(resolution,[],[f176,f288]) ).
fof(f686,plain,
tptp0 = sK1(sK21),
inference(forward_subsumption_resolution,[],[f683,f513]) ).
fof(f688,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK1(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f681,f174]) ).
fof(f691,plain,
! [X0,X1] :
( ~ leaf_occ(X1,X0)
| sK1(X0) = sK15(X1,X0) ),
inference(resolution,[],[f688,f238]) ).
fof(f694,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp3 = sK1(sK17(X0)) ),
inference(resolution,[],[f688,f262]) ).
fof(f774,plain,
! [X0,X1] :
( ~ min_precedes(X0,sK18(X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| sK17(X1) = X0
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f326,f307]) ).
fof(f781,plain,
! [X0,X1] :
( ~ min_precedes(X0,sK18(X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| sK17(X1) = X0
| ~ arboreal(X0) ),
inference(duplicate_literal_removal,[],[f774]) ).
fof(f786,plain,
! [X0,X1] :
( ~ min_precedes(X0,sK18(X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| sK17(X1) = X0 ),
inference(forward_subsumption_resolution,[],[f781,f253]) ).
fof(f803,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| sK1(X0) = sK15(sK19(X0),X0) ),
inference(resolution,[],[f691,f256]) ).
fof(f810,definition,
( spl23_11
<=> root_occ(sK17(sK21),sK21) ),
introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition]) ).
fof(f811,plain,
( root_occ(sK17(sK21),sK21)
| ~ spl23_11 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f812,plain,
( ~ root_occ(sK17(sK21),sK21)
| spl23_11 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f818,plain,
( ~ occurrence_of(sK21,tptp0)
| spl23_11 ),
inference(resolution,[],[f812,f261]) ).
fof(f819,plain,
( $false
| spl23_11 ),
inference(forward_subsumption_resolution,[],[f818,f279]) ).
fof(f820,plain,
spl23_11,
inference(avatar_contradiction_clause,[],[f819]) ).
fof(f825,plain,
( ! [X0,X1] :
( min_precedes(sK17(sK21),X1,X0)
| ~ subactivity_occurrence(X1,sK21)
| sK17(sK21) = X1
| ~ arboreal(X1)
| ~ occurrence_of(sK21,X0) )
| ~ spl23_11 ),
inference(resolution,[],[f811,f247]) ).
fof(f826,plain,
( subactivity_occurrence(sK17(sK21),sK21)
| ~ spl23_11 ),
inference(resolution,[],[f811,f233]) ).
fof(f898,definition,
( spl23_19
<=> occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition]) ).
fof(f899,plain,
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| spl23_19 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f900,plain,
( occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| ~ spl23_19 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f934,plain,
( activity_occurrence(sK17(sK21))
| ~ spl23_11 ),
inference(resolution,[],[f218,f826]) ).
fof(f943,plain,
sK1(sK21) = sK15(sK19(sK21),sK21),
inference(resolution,[],[f803,f279]) ).
fof(f944,plain,
tptp0 = sK15(sK19(sK21),sK21),
inference(forward_demodulation,[],[f943,f686]) ).
fof(f945,plain,
( leaf(sK19(sK21),tptp0)
| ~ leaf_occ(sK19(sK21),sK21) ),
inference(superposition,[],[f236,f944]) ).
fof(f948,definition,
( spl23_20
<=> leaf_occ(sK19(sK21),sK21) ),
introduced(definition,[new_symbols(definition,[spl23_20])],[avatar_definition]) ).
fof(f949,plain,
( leaf_occ(sK19(sK21),sK21)
| ~ spl23_20 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f950,plain,
( ~ leaf_occ(sK19(sK21),sK21)
| spl23_20 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f952,definition,
( spl23_21
<=> leaf(sK19(sK21),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_21])],[avatar_definition]) ).
fof(f954,plain,
( leaf(sK19(sK21),tptp0)
| ~ spl23_21 ),
inference(avatar_component_clause,[],[f952]) ).
fof(f955,plain,
( ~ spl23_20
| spl23_21 ),
inference(avatar_split_clause,[],[f945,f952,f948]) ).
fof(f956,plain,
( ~ occurrence_of(sK21,tptp0)
| spl23_20 ),
inference(resolution,[],[f950,f256]) ).
fof(f957,plain,
( $false
| spl23_20 ),
inference(forward_subsumption_resolution,[],[f956,f279]) ).
fof(f958,plain,
spl23_20,
inference(avatar_contradiction_clause,[],[f957]) ).
fof(f959,plain,
( subactivity_occurrence(sK19(sK21),sK21)
| ~ spl23_20 ),
inference(resolution,[],[f949,f237]) ).
fof(f961,plain,
( ! [X0,X1] :
( min_precedes(X1,sK19(sK21),X0)
| ~ occurrence_of(sK21,X0)
| ~ root_occ(X1,sK21)
| sK19(sK21) = X1 )
| ~ spl23_20 ),
inference(resolution,[],[f949,f246]) ).
fof(f1064,plain,
( ! [X0] :
( ~ occurrence_of(sK21,tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ root_occ(X0,sK21)
| ~ occurrence_of(sK19(sK21),tptp2)
| ~ occurrence_of(X0,tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(resolution,[],[f961,f280]) ).
fof(f1068,plain,
( ! [X0] :
( ~ occurrence_of(sK21,tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ root_occ(X0,sK21)
| ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(X0,tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| min_precedes(X0,sK22(X0),tptp0)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(resolution,[],[f961,f285]) ).
fof(f1075,plain,
( ! [X0] :
( ~ occurrence_of(sK21,tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(X0,tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| min_precedes(X0,sK22(X0),tptp0)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(duplicate_literal_removal,[],[f1068]) ).
fof(f1079,plain,
( ! [X0] :
( ~ occurrence_of(sK21,tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(sK19(sK21),tptp2)
| ~ occurrence_of(X0,tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(duplicate_literal_removal,[],[f1064]) ).
fof(f1082,plain,
( ! [X0] :
( ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(X0,tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| min_precedes(X0,sK22(X0),tptp0)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1075,f279]) ).
fof(f1095,plain,
( ! [X0] :
( ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(X0,tptp3)
| min_precedes(X0,sK22(X0),tptp0)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1082,f949]) ).
fof(f1100,definition,
( spl23_29
<=> occurrence_of(sK19(sK21),tptp1) ),
introduced(definition,[new_symbols(definition,[spl23_29])],[avatar_definition]) ).
fof(f1101,plain,
( occurrence_of(sK19(sK21),tptp1)
| ~ spl23_29 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1102,plain,
( ~ occurrence_of(sK19(sK21),tptp1)
| spl23_29 ),
inference(avatar_component_clause,[],[f1100]) ).
fof(f1112,definition,
( spl23_32
<=> ! [X0] :
( ~ root_occ(X0,sK21)
| sP0(sK21,X0,sK19(sK21))
| min_precedes(X0,sK22(X0),tptp0)
| ~ occurrence_of(X0,tptp3)
| sK19(sK21) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl23_32])],[avatar_definition]) ).
fof(f1113,plain,
( ! [X0] :
( sP0(sK21,X0,sK19(sK21))
| min_precedes(X0,sK22(X0),tptp0)
| ~ root_occ(X0,sK21)
| ~ occurrence_of(X0,tptp3)
| sK19(sK21) = X0 )
| ~ spl23_32 ),
inference(avatar_component_clause,[],[f1112]) ).
fof(f1114,plain,
( ~ spl23_29
| spl23_32
| ~ spl23_20 ),
inference(avatar_split_clause,[],[f1095,f948,f1112,f1100]) ).
fof(f1116,definition,
( spl23_33
<=> occurrence_of(sK19(sK21),tptp2) ),
introduced(definition,[new_symbols(definition,[spl23_33])],[avatar_definition]) ).
fof(f1117,plain,
( occurrence_of(sK19(sK21),tptp2)
| ~ spl23_33 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1118,plain,
( ~ occurrence_of(sK19(sK21),tptp2)
| spl23_33 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1128,plain,
( tptp1 = sK1(sK19(sK21))
| ~ spl23_29 ),
inference(resolution,[],[f1101,f688]) ).
fof(f1357,definition,
( spl23_40
<=> ! [X0] :
( ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3) ) ),
introduced(definition,[new_symbols(definition,[spl23_40])],[avatar_definition]) ).
fof(f1358,plain,
( ! [X0] :
( ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3) )
| ~ spl23_40 ),
inference(avatar_component_clause,[],[f1357]) ).
fof(f1373,plain,
( tptp2 = sK1(sK19(sK21))
| ~ spl23_33 ),
inference(resolution,[],[f1117,f688]) ).
fof(f1378,plain,
( tptp1 = tptp2
| ~ spl23_29
| ~ spl23_33 ),
inference(forward_demodulation,[],[f1373,f1128]) ).
fof(f1382,plain,
( $false
| ~ spl23_29
| ~ spl23_33 ),
inference(forward_subsumption_resolution,[],[f1378,f274]) ).
fof(f1383,plain,
( ~ spl23_29
| ~ spl23_33 ),
inference(avatar_contradiction_clause,[],[f1382]) ).
fof(f1420,plain,
( sK17(sK21) = sK19(sK21)
| ~ occurrence_of(sK17(sK21),tptp3)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_40 ),
inference(resolution,[],[f1358,f261]) ).
fof(f1421,plain,
( ~ occurrence_of(sK17(sK21),tptp3)
| ~ occurrence_of(sK21,tptp0)
| spl23_2
| ~ spl23_40 ),
inference(forward_subsumption_resolution,[],[f1420,f361]) ).
fof(f1423,plain,
( ~ occurrence_of(sK21,tptp0)
| spl23_2
| ~ spl23_40 ),
inference(forward_subsumption_resolution,[],[f1421,f262]) ).
fof(f1424,plain,
( $false
| spl23_2
| ~ spl23_40 ),
inference(forward_subsumption_resolution,[],[f1423,f279]) ).
fof(f1425,plain,
( spl23_2
| ~ spl23_40 ),
inference(avatar_contradiction_clause,[],[f1424]) ).
fof(f1467,plain,
( ~ occurrence_of(sK21,tptp0)
| subactivity_occurrence(sK18(sK21),sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_20 ),
inference(resolution,[],[f576,f959]) ).
fof(f1468,plain,
( ~ occurrence_of(sK21,tptp0)
| subactivity_occurrence(sK18(sK21),sK21)
| ~ spl23_20 ),
inference(duplicate_literal_removal,[],[f1467]) ).
fof(f1470,plain,
( subactivity_occurrence(sK18(sK21),sK21)
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1468,f279]) ).
fof(f1476,plain,
( ! [X0,X1] :
( min_precedes(sK18(sK21),X0,X1)
| sK18(sK21) = X0
| ~ occurrence_of(sK21,X1)
| ~ arboreal(X0)
| ~ arboreal(sK18(sK21))
| ~ subactivity_occurrence(X0,sK21)
| min_precedes(X0,sK18(sK21),X1) )
| ~ spl23_20 ),
inference(resolution,[],[f1470,f226]) ).
fof(f1501,plain,
( ! [X0,X1] :
( min_precedes(sK18(sK21),X0,X1)
| min_precedes(X0,sK18(sK21),X1)
| ~ occurrence_of(sK21,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0 )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1476,f656]) ).
fof(f1508,definition,
( spl23_46
<=> sK17(sK21) = sK18(sK21) ),
introduced(definition,[new_symbols(definition,[spl23_46])],[avatar_definition]) ).
fof(f1509,plain,
( sK17(sK21) != sK18(sK21)
| spl23_46 ),
inference(avatar_component_clause,[],[f1508]) ).
fof(f1510,plain,
( sK17(sK21) = sK18(sK21)
| ~ spl23_46 ),
inference(avatar_component_clause,[],[f1508]) ).
fof(f1556,plain,
( ! [X0] :
( min_precedes(X0,sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| ~ min_precedes(X0,sK19(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0) )
| ~ spl23_20 ),
inference(resolution,[],[f1501,f327]) ).
fof(f1599,plain,
( ! [X0] :
( min_precedes(X0,sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| ~ min_precedes(X0,sK19(sK21),tptp0) )
| ~ spl23_20 ),
inference(duplicate_literal_removal,[],[f1556]) ).
fof(f1606,plain,
( ! [X0] :
( min_precedes(X0,sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| ~ min_precedes(X0,sK19(sK21),tptp0) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1599,f253]) ).
fof(f1610,plain,
( ! [X0] :
( ~ min_precedes(X0,sK19(sK21),tptp0)
| ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| min_precedes(X0,sK18(sK21),tptp0) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1606,f279]) ).
fof(f1617,plain,
( ! [X0] :
( ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| min_precedes(X0,sK18(sK21),tptp0)
| ~ subactivity_occurrence(X0,sK21)
| sK19(sK21) = X0
| ~ arboreal(X0)
| ~ occurrence_of(sK21,tptp0)
| ~ occurrence_of(sK21,tptp0) )
| ~ spl23_20 ),
inference(resolution,[],[f1610,f303]) ).
fof(f1618,plain,
( ! [X0] :
( ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| min_precedes(X0,sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(sK21,tptp0) )
| ~ spl23_20 ),
inference(resolution,[],[f1610,f291]) ).
fof(f1623,plain,
( ! [X0] :
( ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| min_precedes(X0,sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0 )
| ~ spl23_20 ),
inference(duplicate_literal_removal,[],[f1618]) ).
fof(f1624,plain,
( ! [X0] :
( ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| min_precedes(X0,sK18(sK21),tptp0)
| sK19(sK21) = X0
| ~ arboreal(X0)
| ~ occurrence_of(sK21,tptp0) )
| ~ spl23_20 ),
inference(duplicate_literal_removal,[],[f1617]) ).
fof(f1628,plain,
( ! [X0] :
( ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| min_precedes(X0,sK18(sK21),tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0 )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1623,f279]) ).
fof(f1629,plain,
( ! [X0] :
( min_precedes(X0,sK18(sK21),tptp0)
| sK18(sK21) = X0
| ~ subactivity_occurrence(X0,sK21)
| sK19(sK21) = X0
| ~ arboreal(X0) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1624,f279]) ).
fof(f1633,plain,
( ! [X0] :
( min_precedes(X0,sK18(sK21),tptp0)
| sK18(sK21) = X0
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0 )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1628,f233]) ).
fof(f1648,plain,
( ! [X0] :
( sK18(sK21) = X0
| ~ subactivity_occurrence(X0,sK21)
| sK19(sK21) = X0
| ~ arboreal(X0)
| ~ occurrence_of(sK21,tptp0)
| ~ subactivity_occurrence(X0,sK21)
| sK17(sK21) = X0 )
| ~ spl23_20 ),
inference(resolution,[],[f1629,f786]) ).
fof(f1669,plain,
( ! [X0] :
( sK18(sK21) = X0
| ~ subactivity_occurrence(X0,sK21)
| sK19(sK21) = X0
| ~ arboreal(X0)
| ~ occurrence_of(sK21,tptp0)
| sK17(sK21) = X0 )
| ~ spl23_20 ),
inference(duplicate_literal_removal,[],[f1648]) ).
fof(f1689,plain,
( ! [X0] :
( ~ subactivity_occurrence(X0,sK21)
| sK18(sK21) = X0
| sK19(sK21) = X0
| ~ arboreal(X0)
| sK17(sK21) = X0 )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1669,f279]) ).
fof(f1746,plain,
( min_precedes(sK17(sK21),sK17(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_46 ),
inference(superposition,[],[f316,f1510]) ).
fof(f1761,plain,
( min_precedes(sK17(sK21),sK17(sK21),tptp0)
| ~ spl23_46 ),
inference(forward_subsumption_resolution,[],[f1746,f279]) ).
fof(f1778,plain,
( ~ min_precedes(sK17(sK21),sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_46 ),
inference(resolution,[],[f1761,f326]) ).
fof(f1806,plain,
( ~ occurrence_of(sK21,tptp0)
| ~ spl23_46 ),
inference(forward_subsumption_resolution,[],[f1778,f316]) ).
fof(f1812,definition,
( spl23_60
<=> occurrence_of(sK22(sK17(sK21)),tptp2) ),
introduced(definition,[new_symbols(definition,[spl23_60])],[avatar_definition]) ).
fof(f1814,plain,
( occurrence_of(sK22(sK17(sK21)),tptp2)
| ~ spl23_60 ),
inference(avatar_component_clause,[],[f1812]) ).
fof(f1820,definition,
( spl23_62
<=> occurrence_of(sK17(sK21),tptp3) ),
introduced(definition,[new_symbols(definition,[spl23_62])],[avatar_definition]) ).
fof(f1821,plain,
( occurrence_of(sK17(sK21),tptp3)
| ~ spl23_62 ),
inference(avatar_component_clause,[],[f1820]) ).
fof(f1829,definition,
( spl23_64
<=> subactivity_occurrence(sK22(sK17(sK21)),sK21) ),
introduced(definition,[new_symbols(definition,[spl23_64])],[avatar_definition]) ).
fof(f1831,plain,
( subactivity_occurrence(sK22(sK17(sK21)),sK21)
| ~ spl23_64 ),
inference(avatar_component_clause,[],[f1829]) ).
fof(f1846,plain,
( $false
| ~ spl23_46 ),
inference(forward_subsumption_resolution,[],[f1806,f279]) ).
fof(f1847,plain,
~ spl23_46,
inference(avatar_contradiction_clause,[],[f1846]) ).
fof(f2232,plain,
tptp3 = sK1(sK17(sK21)),
inference(resolution,[],[f694,f279]) ).
fof(f2233,plain,
( occurrence_of(sK17(sK21),tptp3)
| ~ activity_occurrence(sK17(sK21)) ),
inference(superposition,[],[f176,f2232]) ).
fof(f2234,plain,
( occurrence_of(sK17(sK21),tptp3)
| ~ spl23_11 ),
inference(forward_subsumption_resolution,[],[f2233,f934]) ).
fof(f2235,plain,
( spl23_62
| ~ spl23_11 ),
inference(avatar_split_clause,[],[f2234,f810,f1820]) ).
fof(f2488,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X3,sK10(X2,X0,X1))
| sK14(X3,sK10(X2,X0,X1)) = X2
| ~ min_precedes(X0,X1,X2) ),
inference(resolution,[],[f315,f234]) ).
fof(f2492,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK10(X0,X1,X2),tptp0)
| ~ min_precedes(X1,X2,X0)
| sK14(sK17(sK10(X0,X1,X2)),sK10(X0,X1,X2)) = X0 ),
inference(resolution,[],[f2488,f261]) ).
fof(f2493,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK14(sK17(sK10(tptp0,X0,X1)),sK10(tptp0,X0,X1))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f2492,f221]) ).
fof(f2494,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK14(sK17(sK10(tptp0,X0,X1)),sK10(tptp0,X0,X1)) ),
inference(duplicate_literal_removal,[],[f2493]) ).
fof(f2518,plain,
! [X0,X1] :
( tptp0 = sK14(sK17(sK10(tptp0,X0,sK19(X1))),sK10(tptp0,X0,sK19(X1)))
| ~ subactivity_occurrence(X0,X1)
| sK19(X1) = X0
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f2494,f303]) ).
fof(f2527,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| tptp0 = sK14(sK17(sK10(tptp0,X0,sK19(X1))),sK10(tptp0,X0,sK19(X1)))
| sK19(X1) = X0
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0) ),
inference(duplicate_literal_removal,[],[f2518]) ).
fof(f2539,plain,
( tptp0 = sK14(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| sK17(sK21) = sK19(sK21)
| ~ arboreal(sK17(sK21))
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11 ),
inference(resolution,[],[f2527,f826]) ).
fof(f2549,plain,
( tptp0 = sK14(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| sK17(sK21) = sK19(sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11 ),
inference(forward_subsumption_resolution,[],[f2539,f310]) ).
fof(f2553,plain,
( tptp0 = sK14(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK21,tptp0)
| spl23_2
| ~ spl23_11 ),
inference(forward_subsumption_resolution,[],[f2549,f361]) ).
fof(f2554,plain,
( tptp0 = sK14(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| spl23_2
| ~ spl23_11 ),
inference(forward_subsumption_resolution,[],[f2553,f279]) ).
fof(f2555,plain,
( root(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ root_occ(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| spl23_2
| ~ spl23_11 ),
inference(superposition,[],[f232,f2554]) ).
fof(f2558,definition,
( spl23_92
<=> root_occ(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21))) ),
introduced(definition,[new_symbols(definition,[spl23_92])],[avatar_definition]) ).
fof(f2559,plain,
( root_occ(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_92 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2560,plain,
( ~ root_occ(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| spl23_92 ),
inference(avatar_component_clause,[],[f2558]) ).
fof(f2563,definition,
( spl23_93
<=> root(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_93])],[avatar_definition]) ).
fof(f2565,plain,
( root(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ spl23_93 ),
inference(avatar_component_clause,[],[f2563]) ).
fof(f2566,plain,
( ~ spl23_92
| spl23_93
| spl23_2
| ~ spl23_11 ),
inference(avatar_split_clause,[],[f2555,f810,f360,f2563,f2558]) ).
fof(f2567,plain,
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| spl23_92 ),
inference(resolution,[],[f2560,f261]) ).
fof(f2568,plain,
( ~ spl23_19
| spl23_92 ),
inference(avatar_split_clause,[],[f2567,f2558,f898]) ).
fof(f2569,plain,
( ~ min_precedes(sK17(sK21),sK19(sK21),tptp0)
| spl23_19 ),
inference(resolution,[],[f899,f221]) ).
fof(f2570,plain,
( ~ subactivity_occurrence(sK19(sK21),sK21)
| sK17(sK21) = sK19(sK21)
| ~ arboreal(sK19(sK21))
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11
| spl23_19 ),
inference(resolution,[],[f2569,f825]) ).
fof(f2587,plain,
( sK17(sK21) = sK19(sK21)
| ~ arboreal(sK19(sK21))
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11
| spl23_19 ),
inference(forward_subsumption_resolution,[],[f2570,f340]) ).
fof(f2594,plain,
( sK17(sK21) = sK19(sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11
| spl23_19 ),
inference(forward_subsumption_resolution,[],[f2587,f431]) ).
fof(f2603,plain,
( ~ occurrence_of(sK21,tptp0)
| spl23_2
| ~ spl23_11
| spl23_19 ),
inference(forward_subsumption_resolution,[],[f2594,f361]) ).
fof(f2611,plain,
( $false
| spl23_2
| ~ spl23_11
| spl23_19 ),
inference(forward_subsumption_resolution,[],[f2603,f279]) ).
fof(f2612,plain,
( spl23_2
| ~ spl23_11
| spl23_19 ),
inference(avatar_contradiction_clause,[],[f2611]) ).
fof(f2615,plain,
( subactivity_occurrence(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_92 ),
inference(resolution,[],[f2559,f233]) ).
fof(f2631,definition,
( spl23_95
<=> ! [X0] : ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0) ),
introduced(definition,[new_symbols(definition,[spl23_95])],[avatar_definition]) ).
fof(f2632,plain,
( ! [X0] : ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ spl23_95 ),
inference(avatar_component_clause,[],[f2631]) ).
fof(f2634,plain,
( ! [X0] :
( sK17(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ arboreal(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))))
| min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0)
| min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK17(sK21),X0)
| ~ min_precedes(sK17(sK21),sK19(sK21),tptp0) )
| ~ spl23_92 ),
inference(resolution,[],[f2615,f297]) ).
fof(f2635,plain,
( ! [X0] :
( sK19(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ arboreal(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))))
| ~ arboreal(sK19(sK21))
| min_precedes(sK19(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0)
| min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK19(sK21),X0)
| ~ min_precedes(sK17(sK21),sK19(sK21),tptp0) )
| ~ spl23_92 ),
inference(resolution,[],[f2615,f295]) ).
fof(f2655,plain,
( ! [X0] :
( sK19(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ arboreal(sK19(sK21))
| min_precedes(sK19(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0)
| min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK19(sK21),X0)
| ~ min_precedes(sK17(sK21),sK19(sK21),tptp0) )
| ~ spl23_92 ),
inference(forward_subsumption_resolution,[],[f2635,f515]) ).
fof(f2656,plain,
( ! [X0] :
( sK17(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0)
| min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK17(sK21),X0)
| ~ min_precedes(sK17(sK21),sK19(sK21),tptp0) )
| ~ spl23_92 ),
inference(forward_subsumption_resolution,[],[f2634,f515]) ).
fof(f2657,plain,
( ! [X0] :
( sK19(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| min_precedes(sK19(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0)
| min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK19(sK21),X0)
| ~ min_precedes(sK17(sK21),sK19(sK21),tptp0) )
| ~ spl23_92 ),
inference(forward_subsumption_resolution,[],[f2655,f433]) ).
fof(f2659,definition,
( spl23_98
<=> min_precedes(sK17(sK21),sK19(sK21),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_98])],[avatar_definition]) ).
fof(f2660,plain,
( min_precedes(sK17(sK21),sK19(sK21),tptp0)
| ~ spl23_98 ),
inference(avatar_component_clause,[],[f2659]) ).
fof(f2661,plain,
( ~ min_precedes(sK17(sK21),sK19(sK21),tptp0)
| spl23_98 ),
inference(avatar_component_clause,[],[f2659]) ).
fof(f2663,definition,
( spl23_99
<=> ! [X0] :
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK17(sK21),X0)
| min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl23_99])],[avatar_definition]) ).
fof(f2664,plain,
( ! [X0] :
( min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK17(sK21),X0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0) )
| ~ spl23_99 ),
inference(avatar_component_clause,[],[f2663]) ).
fof(f2666,definition,
( spl23_100
<=> sK17(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21))) ),
introduced(definition,[new_symbols(definition,[spl23_100])],[avatar_definition]) ).
fof(f2668,plain,
( sK17(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_100 ),
inference(avatar_component_clause,[],[f2666]) ).
fof(f2669,plain,
( ~ spl23_98
| spl23_99
| spl23_100
| ~ spl23_92 ),
inference(avatar_split_clause,[],[f2656,f2558,f2666,f2663,f2659]) ).
fof(f2671,definition,
( spl23_101
<=> ! [X0] :
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK19(sK21),X0)
| min_precedes(sK19(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl23_101])],[avatar_definition]) ).
fof(f2672,plain,
( ! [X0] :
( min_precedes(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),sK19(sK21),X0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| min_precedes(sK19(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0) )
| ~ spl23_101 ),
inference(avatar_component_clause,[],[f2671]) ).
fof(f2674,definition,
( spl23_102
<=> sK19(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21))) ),
introduced(definition,[new_symbols(definition,[spl23_102])],[avatar_definition]) ).
fof(f2676,plain,
( sK19(sK21) = sK17(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_102 ),
inference(avatar_component_clause,[],[f2674]) ).
fof(f2677,plain,
( ~ spl23_98
| spl23_101
| spl23_102
| ~ spl23_92 ),
inference(avatar_split_clause,[],[f2657,f2558,f2674,f2671,f2659]) ).
fof(f2678,plain,
( ~ subactivity_occurrence(sK19(sK21),sK21)
| sK17(sK21) = sK19(sK21)
| ~ arboreal(sK19(sK21))
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11
| spl23_98 ),
inference(resolution,[],[f2661,f825]) ).
fof(f2695,plain,
( sK17(sK21) = sK19(sK21)
| ~ arboreal(sK19(sK21))
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11
| spl23_98 ),
inference(forward_subsumption_resolution,[],[f2678,f340]) ).
fof(f2702,plain,
( sK17(sK21) = sK19(sK21)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_11
| spl23_98 ),
inference(forward_subsumption_resolution,[],[f2695,f431]) ).
fof(f2711,plain,
( ~ occurrence_of(sK21,tptp0)
| spl23_2
| ~ spl23_11
| spl23_98 ),
inference(forward_subsumption_resolution,[],[f2702,f361]) ).
fof(f2719,plain,
( $false
| spl23_2
| ~ spl23_11
| spl23_98 ),
inference(forward_subsumption_resolution,[],[f2711,f279]) ).
fof(f2720,plain,
( spl23_2
| ~ spl23_11
| spl23_98 ),
inference(avatar_contradiction_clause,[],[f2719]) ).
fof(f2723,plain,
( ~ subactivity_occurrence(sK17(sK21),sK21)
| sK17(sK21) = sK18(sK21)
| min_precedes(sK17(sK21),sK18(sK21),tptp0)
| ~ spl23_20
| ~ spl23_98 ),
inference(resolution,[],[f2660,f1610]) ).
fof(f2725,plain,
( ~ root_occ(sK17(sK21),sK21)
| ~ occurrence_of(sK19(sK21),tptp2)
| ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_98 ),
inference(resolution,[],[f2660,f280]) ).
fof(f2730,plain,
( ~ root_occ(sK17(sK21),sK21)
| ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| subactivity_occurrence(sK22(sK17(sK21)),sK21)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_98 ),
inference(resolution,[],[f2660,f286]) ).
fof(f2731,plain,
( ~ root_occ(sK17(sK21),sK21)
| ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK22(sK17(sK21)),tptp2)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_98 ),
inference(resolution,[],[f2660,f287]) ).
fof(f2734,plain,
( ~ root(sK19(sK21),tptp0)
| ~ spl23_98 ),
inference(resolution,[],[f2660,f198]) ).
fof(f2744,plain,
( ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK22(sK17(sK21)),tptp2)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2731,f811]) ).
fof(f2745,plain,
( ~ occurrence_of(sK19(sK21),tptp1)
| ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| subactivity_occurrence(sK22(sK17(sK21)),sK21)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2730,f811]) ).
fof(f2748,plain,
( sK17(sK21) = sK18(sK21)
| min_precedes(sK17(sK21),sK18(sK21),tptp0)
| ~ spl23_11
| ~ spl23_20
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2723,f826]) ).
fof(f2749,plain,
( ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK22(sK17(sK21)),tptp2)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_29
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2744,f1101]) ).
fof(f2750,plain,
( ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| subactivity_occurrence(sK22(sK17(sK21)),sK21)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_29
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2745,f1101]) ).
fof(f2752,plain,
( min_precedes(sK17(sK21),sK18(sK21),tptp0)
| ~ spl23_11
| ~ spl23_20
| spl23_46
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2748,f1509]) ).
fof(f2753,plain,
( ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK22(sK17(sK21)),tptp2)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_29
| ~ spl23_62
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2749,f1821]) ).
fof(f2754,plain,
( ~ leaf_occ(sK19(sK21),sK21)
| subactivity_occurrence(sK22(sK17(sK21)),sK21)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_29
| ~ spl23_62
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2750,f1821]) ).
fof(f2756,plain,
( occurrence_of(sK22(sK17(sK21)),tptp2)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_20
| ~ spl23_29
| ~ spl23_62
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2753,f949]) ).
fof(f2757,plain,
( subactivity_occurrence(sK22(sK17(sK21)),sK21)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_20
| ~ spl23_29
| ~ spl23_62
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2754,f949]) ).
fof(f2760,definition,
( spl23_103
<=> sP0(sK21,sK17(sK21),sK19(sK21)) ),
introduced(definition,[new_symbols(definition,[spl23_103])],[avatar_definition]) ).
fof(f2761,plain,
( ~ sP0(sK21,sK17(sK21),sK19(sK21))
| spl23_103 ),
inference(avatar_component_clause,[],[f2760]) ).
fof(f2762,plain,
( sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_103 ),
inference(avatar_component_clause,[],[f2760]) ).
fof(f2763,plain,
( spl23_103
| spl23_60
| ~ spl23_11
| ~ spl23_20
| ~ spl23_29
| ~ spl23_62
| ~ spl23_98 ),
inference(avatar_split_clause,[],[f2756,f2659,f1820,f1100,f948,f810,f1812,f2760]) ).
fof(f2764,plain,
( spl23_103
| spl23_64
| ~ spl23_11
| ~ spl23_20
| ~ spl23_29
| ~ spl23_62
| ~ spl23_98 ),
inference(avatar_split_clause,[],[f2757,f2659,f1820,f1100,f948,f810,f1829,f2760]) ).
fof(f2792,plain,
( ! [X0] :
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| min_precedes(sK19(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),X0)
| ~ atomic(X0) )
| ~ spl23_101 ),
inference(resolution,[],[f2672,f203]) ).
fof(f2824,plain,
( ! [X0] :
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ atomic(X0) )
| ~ spl23_101 ),
inference(forward_subsumption_resolution,[],[f2792,f203]) ).
fof(f2890,plain,
( root(sK19(sK21),tptp0)
| ~ spl23_93
| ~ spl23_102 ),
inference(superposition,[],[f2565,f2676]) ).
fof(f2922,plain,
( $false
| ~ spl23_93
| ~ spl23_98
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f2890,f2734]) ).
fof(f2923,plain,
( ~ spl23_93
| ~ spl23_98
| ~ spl23_102 ),
inference(avatar_contradiction_clause,[],[f2922]) ).
fof(f2925,definition,
( spl23_118
<=> leaf_occ(sK19(sK21),sK10(tptp0,sK17(sK21),sK19(sK21))) ),
introduced(definition,[new_symbols(definition,[spl23_118])],[avatar_definition]) ).
fof(f2926,plain,
( ~ leaf_occ(sK19(sK21),sK10(tptp0,sK17(sK21),sK19(sK21)))
| spl23_118 ),
inference(avatar_component_clause,[],[f2925]) ).
fof(f2927,plain,
( leaf_occ(sK19(sK21),sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_118 ),
inference(avatar_component_clause,[],[f2925]) ).
fof(f2929,definition,
( spl23_119
<=> ! [X0] :
( ~ leaf(sK19(sK21),X0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl23_119])],[avatar_definition]) ).
fof(f2930,plain,
( ! [X0] :
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ leaf(sK19(sK21),X0) )
| ~ spl23_119 ),
inference(avatar_component_clause,[],[f2929]) ).
fof(f3008,plain,
( ~ atomic(tptp2)
| arboreal(sK22(sK17(sK21)))
| ~ spl23_60 ),
inference(resolution,[],[f1814,f184]) ).
fof(f3010,plain,
( arboreal(sK22(sK17(sK21)))
| ~ spl23_60 ),
inference(forward_subsumption_resolution,[],[f3008,f267]) ).
fof(f3022,plain,
( sK18(sK21) = sK22(sK17(sK21))
| sK19(sK21) = sK22(sK17(sK21))
| ~ arboreal(sK22(sK17(sK21)))
| sK17(sK21) = sK22(sK17(sK21))
| ~ spl23_20
| ~ spl23_64 ),
inference(resolution,[],[f1831,f1689]) ).
fof(f3047,plain,
( sK18(sK21) = sK22(sK17(sK21))
| sK19(sK21) = sK22(sK17(sK21))
| sK17(sK21) = sK22(sK17(sK21))
| ~ spl23_20
| ~ spl23_60
| ~ spl23_64 ),
inference(forward_subsumption_resolution,[],[f3022,f3010]) ).
fof(f3053,definition,
( spl23_126
<=> sK17(sK21) = sK22(sK17(sK21)) ),
introduced(definition,[new_symbols(definition,[spl23_126])],[avatar_definition]) ).
fof(f3055,plain,
( sK17(sK21) = sK22(sK17(sK21))
| ~ spl23_126 ),
inference(avatar_component_clause,[],[f3053]) ).
fof(f3061,definition,
( spl23_128
<=> sK19(sK21) = sK22(sK17(sK21)) ),
introduced(definition,[new_symbols(definition,[spl23_128])],[avatar_definition]) ).
fof(f3063,plain,
( sK19(sK21) = sK22(sK17(sK21))
| ~ spl23_128 ),
inference(avatar_component_clause,[],[f3061]) ).
fof(f3066,definition,
( spl23_129
<=> sK18(sK21) = sK22(sK17(sK21)) ),
introduced(definition,[new_symbols(definition,[spl23_129])],[avatar_definition]) ).
fof(f3068,plain,
( sK18(sK21) = sK22(sK17(sK21))
| ~ spl23_129 ),
inference(avatar_component_clause,[],[f3066]) ).
fof(f3069,plain,
( spl23_126
| spl23_128
| spl23_129
| ~ spl23_20
| ~ spl23_60
| ~ spl23_64 ),
inference(avatar_split_clause,[],[f3047,f1829,f1812,f948,f3066,f3061,f3053]) ).
fof(f3075,plain,
( occurrence_of(sK19(sK21),tptp2)
| ~ spl23_103 ),
inference(resolution,[],[f2762,f275]) ).
fof(f3076,plain,
( subactivity_occurrence(sK20(sK21,sK17(sK21)),sK21)
| ~ spl23_103 ),
inference(resolution,[],[f2762,f277]) ).
fof(f3077,plain,
( occurrence_of(sK20(sK21,sK17(sK21)),tptp1)
| ~ spl23_103 ),
inference(resolution,[],[f2762,f278]) ).
fof(f3078,plain,
( min_precedes(sK17(sK21),sK20(sK21,sK17(sK21)),tptp0)
| ~ spl23_103 ),
inference(resolution,[],[f2762,f276]) ).
fof(f3079,plain,
( $false
| spl23_33
| ~ spl23_103 ),
inference(forward_subsumption_resolution,[],[f3075,f1118]) ).
fof(f3080,plain,
( spl23_33
| ~ spl23_103 ),
inference(avatar_contradiction_clause,[],[f3079]) ).
fof(f3090,plain,
( ! [X0] :
( ~ occurrence_of(sK21,tptp0)
| ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f1079,f258]) ).
fof(f3091,plain,
( ! [X0] :
( ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f3090,f279]) ).
fof(f3092,plain,
( ! [X0] :
( ~ root_occ(X0,sK21)
| sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,X0,sK19(sK21)) )
| ~ spl23_20 ),
inference(forward_subsumption_resolution,[],[f3091,f949]) ).
fof(f3093,plain,
( ! [X0] :
( sP0(sK21,X0,sK19(sK21))
| sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3)
| ~ root_occ(X0,sK21) )
| ~ spl23_20
| spl23_29 ),
inference(forward_subsumption_resolution,[],[f3092,f1102]) ).
fof(f3101,plain,
( ~ min_precedes(sK20(sK21,sK17(sK21)),sK18(sK21),tptp0)
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_103 ),
inference(resolution,[],[f3078,f326]) ).
fof(f3124,plain,
( ~ min_precedes(sK20(sK21,sK17(sK21)),sK18(sK21),tptp0)
| ~ spl23_103 ),
inference(forward_subsumption_resolution,[],[f3101,f279]) ).
fof(f3149,plain,
( sK18(sK21) = sK20(sK21,sK17(sK21))
| sK19(sK21) = sK20(sK21,sK17(sK21))
| ~ arboreal(sK20(sK21,sK17(sK21)))
| sK17(sK21) = sK20(sK21,sK17(sK21))
| ~ spl23_20
| ~ spl23_103 ),
inference(resolution,[],[f3076,f1689]) ).
fof(f3172,definition,
( spl23_136
<=> arboreal(sK20(sK21,sK17(sK21))) ),
introduced(definition,[new_symbols(definition,[spl23_136])],[avatar_definition]) ).
fof(f3174,plain,
( ~ arboreal(sK20(sK21,sK17(sK21)))
| spl23_136 ),
inference(avatar_component_clause,[],[f3172]) ).
fof(f3183,definition,
( spl23_139
<=> sK17(sK21) = sK20(sK21,sK17(sK21)) ),
introduced(definition,[new_symbols(definition,[spl23_139])],[avatar_definition]) ).
fof(f3185,plain,
( sK17(sK21) = sK20(sK21,sK17(sK21))
| ~ spl23_139 ),
inference(avatar_component_clause,[],[f3183]) ).
fof(f3191,definition,
( spl23_141
<=> sK19(sK21) = sK20(sK21,sK17(sK21)) ),
introduced(definition,[new_symbols(definition,[spl23_141])],[avatar_definition]) ).
fof(f3192,plain,
( sK19(sK21) != sK20(sK21,sK17(sK21))
| spl23_141 ),
inference(avatar_component_clause,[],[f3191]) ).
fof(f3193,plain,
( sK19(sK21) = sK20(sK21,sK17(sK21))
| ~ spl23_141 ),
inference(avatar_component_clause,[],[f3191]) ).
fof(f3196,definition,
( spl23_142
<=> sK18(sK21) = sK20(sK21,sK17(sK21)) ),
introduced(definition,[new_symbols(definition,[spl23_142])],[avatar_definition]) ).
fof(f3198,plain,
( sK18(sK21) = sK20(sK21,sK17(sK21))
| ~ spl23_142 ),
inference(avatar_component_clause,[],[f3196]) ).
fof(f3199,plain,
( spl23_139
| ~ spl23_136
| spl23_141
| spl23_142
| ~ spl23_20
| ~ spl23_103 ),
inference(avatar_split_clause,[],[f3149,f2760,f948,f3196,f3191,f3172,f3183]) ).
fof(f3209,plain,
( ~ atomic(tptp1)
| arboreal(sK20(sK21,sK17(sK21)))
| ~ spl23_103 ),
inference(resolution,[],[f3077,f184]) ).
fof(f3211,plain,
( arboreal(sK20(sK21,sK17(sK21)))
| ~ spl23_103 ),
inference(forward_subsumption_resolution,[],[f3209,f266]) ).
fof(f3212,plain,
( $false
| ~ spl23_103
| spl23_136 ),
inference(forward_subsumption_resolution,[],[f3211,f3174]) ).
fof(f3213,plain,
( ~ spl23_103
| spl23_136 ),
inference(avatar_contradiction_clause,[],[f3212]) ).
fof(f3214,plain,
( occurrence_of(sK19(sK21),tptp1)
| ~ spl23_103
| ~ spl23_141 ),
inference(superposition,[],[f3077,f3193]) ).
fof(f3221,plain,
( $false
| spl23_29
| ~ spl23_103
| ~ spl23_141 ),
inference(forward_subsumption_resolution,[],[f3214,f1102]) ).
fof(f3222,plain,
( spl23_29
| ~ spl23_103
| ~ spl23_141 ),
inference(avatar_contradiction_clause,[],[f3221]) ).
fof(f3224,plain,
( occurrence_of(sK18(sK21),tptp1)
| ~ spl23_103
| ~ spl23_142 ),
inference(superposition,[],[f3077,f3198]) ).
fof(f3233,plain,
( tptp1 = sK1(sK18(sK21))
| ~ spl23_103
| ~ spl23_142 ),
inference(resolution,[],[f3224,f688]) ).
fof(f3242,plain,
( sK18(sK21) = sK20(sK21,sK17(sK21))
| ~ root_occ(sK20(sK21,sK17(sK21)),sK21)
| sK19(sK21) = sK20(sK21,sK17(sK21))
| ~ spl23_20
| ~ spl23_103 ),
inference(resolution,[],[f3124,f1633]) ).
fof(f3247,plain,
( ! [X0] :
( sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3)
| ~ root_occ(X0,sK21)
| occurrence_of(sK19(sK21),tptp2) )
| ~ spl23_20
| spl23_29 ),
inference(resolution,[],[f3093,f275]) ).
fof(f3532,plain,
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ min_precedes(sK17(sK21),sK18(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| ~ spl23_99 ),
inference(resolution,[],[f2664,f326]) ).
fof(f3552,plain,
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ min_precedes(sK17(sK21),sK18(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ spl23_99 ),
inference(duplicate_literal_removal,[],[f3532]) ).
fof(f3556,plain,
( min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ min_precedes(sK17(sK21),sK18(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ spl23_19
| ~ spl23_99 ),
inference(forward_subsumption_resolution,[],[f3552,f900]) ).
fof(f3562,definition,
( spl23_152
<=> min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_152])],[avatar_definition]) ).
fof(f3563,plain,
( ~ min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| spl23_152 ),
inference(avatar_component_clause,[],[f3562]) ).
fof(f3564,plain,
( min_precedes(sK17(sK21),sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ spl23_152 ),
inference(avatar_component_clause,[],[f3562]) ).
fof(f3567,definition,
( spl23_153
<=> min_precedes(sK17(sK21),sK18(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_153])],[avatar_definition]) ).
fof(f3569,plain,
( ~ min_precedes(sK17(sK21),sK18(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| spl23_153 ),
inference(avatar_component_clause,[],[f3567]) ).
fof(f3570,plain,
( ~ spl23_153
| spl23_152
| ~ spl23_19
| ~ spl23_99 ),
inference(avatar_split_clause,[],[f3556,f2663,f898,f3562,f3567]) ).
fof(f3738,definition,
( spl23_167
<=> sK19(sK21) = sK19(sK10(tptp0,sK17(sK21),sK19(sK21))) ),
introduced(definition,[new_symbols(definition,[spl23_167])],[avatar_definition]) ).
fof(f3739,plain,
( sK19(sK21) != sK19(sK10(tptp0,sK17(sK21),sK19(sK21)))
| spl23_167 ),
inference(avatar_component_clause,[],[f3738]) ).
fof(f3740,plain,
( sK19(sK21) = sK19(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_167 ),
inference(avatar_component_clause,[],[f3738]) ).
fof(f3921,plain,
( next_subocc(sK18(sK10(tptp0,sK17(sK21),sK19(sK21))),sK19(sK21),tptp0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| ~ spl23_167 ),
inference(superposition,[],[f257,f3740]) ).
fof(f3952,plain,
( next_subocc(sK18(sK10(tptp0,sK17(sK21),sK19(sK21))),sK19(sK21),tptp0)
| ~ spl23_19
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f3921,f900]) ).
fof(f4007,plain,
( sK18(sK21) = sK18(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK21,tptp0)
| ~ spl23_19
| ~ spl23_167 ),
inference(resolution,[],[f3952,f325]) ).
fof(f4014,plain,
( sK18(sK21) = sK18(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_19
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f4007,f279]) ).
fof(f4017,plain,
( ~ min_precedes(sK17(sK21),sK18(sK21),tptp0)
| ~ spl23_19
| spl23_153
| ~ spl23_167 ),
inference(superposition,[],[f3569,f4014]) ).
fof(f4022,plain,
( occurrence_of(sK18(sK21),tptp4)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0)
| ~ spl23_19
| ~ spl23_167 ),
inference(superposition,[],[f260,f4014]) ).
fof(f4047,plain,
( occurrence_of(sK18(sK21),tptp4)
| ~ spl23_19
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f4022,f900]) ).
fof(f4050,plain,
( $false
| ~ spl23_11
| ~ spl23_19
| ~ spl23_20
| spl23_46
| ~ spl23_98
| spl23_153
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f4017,f2752]) ).
fof(f4051,plain,
( ~ spl23_11
| ~ spl23_19
| ~ spl23_20
| spl23_46
| ~ spl23_98
| spl23_153
| ~ spl23_167 ),
inference(avatar_contradiction_clause,[],[f4050]) ).
fof(f4064,plain,
( tptp4 = sK1(sK18(sK21))
| ~ spl23_19
| ~ spl23_167 ),
inference(resolution,[],[f4047,f688]) ).
fof(f4069,plain,
( tptp4 = tptp1
| ~ spl23_19
| ~ spl23_103
| ~ spl23_142
| ~ spl23_167 ),
inference(forward_demodulation,[],[f4064,f3233]) ).
fof(f4070,plain,
( $false
| ~ spl23_19
| ~ spl23_103
| ~ spl23_142
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f4069,f270]) ).
fof(f4071,plain,
( ~ spl23_19
| ~ spl23_103
| ~ spl23_142
| ~ spl23_167 ),
inference(avatar_contradiction_clause,[],[f4070]) ).
fof(f4076,plain,
( sK18(sK21) = sK20(sK21,sK17(sK21))
| ~ root_occ(sK20(sK21,sK17(sK21)),sK21)
| ~ spl23_20
| ~ spl23_103
| spl23_141 ),
inference(forward_subsumption_resolution,[],[f3242,f3192]) ).
fof(f4116,plain,
( sK17(sK21) = sK18(sK21)
| ~ root_occ(sK20(sK21,sK17(sK21)),sK21)
| ~ spl23_20
| ~ spl23_103
| ~ spl23_139
| spl23_141 ),
inference(forward_demodulation,[],[f4076,f3185]) ).
fof(f4150,plain,
( ~ root_occ(sK20(sK21,sK17(sK21)),sK21)
| ~ spl23_20
| spl23_46
| ~ spl23_103
| ~ spl23_139
| spl23_141 ),
inference(forward_subsumption_resolution,[],[f4116,f1509]) ).
fof(f4184,plain,
( ~ root_occ(sK17(sK21),sK21)
| ~ spl23_20
| spl23_46
| ~ spl23_103
| ~ spl23_139
| spl23_141 ),
inference(forward_demodulation,[],[f4150,f3185]) ).
fof(f4194,plain,
( $false
| ~ spl23_11
| ~ spl23_20
| spl23_46
| ~ spl23_103
| ~ spl23_139
| spl23_141 ),
inference(forward_subsumption_resolution,[],[f4184,f811]) ).
fof(f4195,plain,
( ~ spl23_11
| ~ spl23_20
| spl23_46
| ~ spl23_103
| ~ spl23_139
| spl23_141 ),
inference(avatar_contradiction_clause,[],[f4194]) ).
fof(f4340,plain,
( ~ root(sK17(sK10(tptp0,sK17(sK21),sK19(sK21))),tptp0)
| ~ spl23_152 ),
inference(resolution,[],[f3564,f198]) ).
fof(f4350,plain,
( $false
| ~ spl23_93
| ~ spl23_152 ),
inference(forward_subsumption_resolution,[],[f4340,f2565]) ).
fof(f4351,plain,
( ~ spl23_93
| ~ spl23_152 ),
inference(avatar_contradiction_clause,[],[f4350]) ).
fof(f4717,plain,
( ! [X0] :
( atomic(X0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| sK19(sK21) = sK19(sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0) )
| ~ spl23_118 ),
inference(resolution,[],[f2927,f349]) ).
fof(f4724,plain,
( ! [X0] :
( atomic(X0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),tptp0) )
| ~ spl23_118
| spl23_167 ),
inference(forward_subsumption_resolution,[],[f4717,f3739]) ).
fof(f4729,plain,
( ! [X0] :
( atomic(X0)
| ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0) )
| ~ spl23_19
| ~ spl23_118
| spl23_167 ),
inference(forward_subsumption_resolution,[],[f4724,f900]) ).
fof(f4735,plain,
( ! [X0] : ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ spl23_19
| ~ spl23_101
| ~ spl23_118
| spl23_167 ),
inference(forward_subsumption_resolution,[],[f4729,f2824]) ).
fof(f4744,plain,
( spl23_95
| ~ spl23_19
| ~ spl23_101
| ~ spl23_118
| spl23_167 ),
inference(avatar_split_clause,[],[f4735,f3738,f2925,f2671,f898,f2631]) ).
fof(f4765,definition,
( spl23_213
<=> subactivity_occurrence(sK19(sK21),sK10(tptp0,sK17(sK21),sK19(sK21))) ),
introduced(definition,[new_symbols(definition,[spl23_213])],[avatar_definition]) ).
fof(f4766,plain,
( subactivity_occurrence(sK19(sK21),sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ spl23_213 ),
inference(avatar_component_clause,[],[f4765]) ).
fof(f4767,plain,
( ~ subactivity_occurrence(sK19(sK21),sK10(tptp0,sK17(sK21),sK19(sK21)))
| spl23_213 ),
inference(avatar_component_clause,[],[f4765]) ).
fof(f4772,plain,
( ~ min_precedes(sK17(sK21),sK19(sK21),tptp0)
| ~ spl23_95 ),
inference(resolution,[],[f2632,f221]) ).
fof(f4780,plain,
( $false
| ~ spl23_95
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f4772,f2660]) ).
fof(f4781,plain,
( ~ spl23_95
| ~ spl23_98 ),
inference(avatar_contradiction_clause,[],[f4780]) ).
fof(f5020,plain,
( ~ min_precedes(sK17(sK21),sK19(sK21),tptp0)
| spl23_213 ),
inference(resolution,[],[f4767,f219]) ).
fof(f5025,plain,
( $false
| ~ spl23_98
| spl23_213 ),
inference(forward_subsumption_resolution,[],[f5020,f2660]) ).
fof(f5026,plain,
( ~ spl23_98
| spl23_213 ),
inference(avatar_contradiction_clause,[],[f5025]) ).
fof(f5039,plain,
( ! [X0] :
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| leaf_occ(sK19(sK21),sK10(tptp0,sK17(sK21),sK19(sK21)))
| ~ leaf(sK19(sK21),X0) )
| ~ spl23_213 ),
inference(resolution,[],[f4766,f239]) ).
fof(f5045,plain,
( ! [X0] :
( ~ occurrence_of(sK10(tptp0,sK17(sK21),sK19(sK21)),X0)
| ~ leaf(sK19(sK21),X0) )
| spl23_118
| ~ spl23_213 ),
inference(forward_subsumption_resolution,[],[f5039,f2926]) ).
fof(f5059,plain,
( spl23_119
| spl23_118
| ~ spl23_213 ),
inference(avatar_split_clause,[],[f5045,f4765,f2925,f2929]) ).
fof(f5241,plain,
( ~ leaf(sK19(sK21),tptp0)
| ~ min_precedes(sK17(sK21),sK19(sK21),tptp0)
| ~ spl23_119 ),
inference(resolution,[],[f2930,f221]) ).
fof(f5249,plain,
( ~ min_precedes(sK17(sK21),sK19(sK21),tptp0)
| ~ spl23_21
| ~ spl23_119 ),
inference(forward_subsumption_resolution,[],[f5241,f954]) ).
fof(f5251,plain,
( $false
| ~ spl23_21
| ~ spl23_98
| ~ spl23_119 ),
inference(forward_subsumption_resolution,[],[f5249,f2660]) ).
fof(f5252,plain,
( ~ spl23_21
| ~ spl23_98
| ~ spl23_119 ),
inference(avatar_contradiction_clause,[],[f5251]) ).
fof(f5294,plain,
( ~ occurrence_of(sK19(sK21),tptp2)
| ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f2725,f811]) ).
fof(f5327,plain,
( ~ occurrence_of(sK17(sK21),tptp3)
| ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_33
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f5294,f1117]) ).
fof(f5338,plain,
( ~ leaf_occ(sK19(sK21),sK21)
| occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_33
| ~ spl23_62
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f5327,f1821]) ).
fof(f5349,plain,
( occurrence_of(sK19(sK21),tptp1)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_20
| ~ spl23_33
| ~ spl23_62
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f5338,f949]) ).
fof(f5353,plain,
( sP0(sK21,sK17(sK21),sK19(sK21))
| ~ spl23_11
| ~ spl23_20
| spl23_29
| ~ spl23_33
| ~ spl23_62
| ~ spl23_98 ),
inference(forward_subsumption_resolution,[],[f5349,f1102]) ).
fof(f5359,plain,
( $false
| ~ spl23_11
| ~ spl23_20
| spl23_29
| ~ spl23_33
| ~ spl23_62
| ~ spl23_98
| spl23_103 ),
inference(forward_subsumption_resolution,[],[f5353,f2761]) ).
fof(f5360,plain,
( ~ spl23_11
| ~ spl23_20
| spl23_29
| ~ spl23_33
| ~ spl23_62
| ~ spl23_98
| spl23_103 ),
inference(avatar_contradiction_clause,[],[f5359]) ).
fof(f5374,plain,
( ! [X0] :
( sK19(sK21) = X0
| ~ occurrence_of(X0,tptp3)
| ~ root_occ(X0,sK21) )
| ~ spl23_20
| spl23_29
| spl23_33 ),
inference(forward_subsumption_resolution,[],[f3247,f1118]) ).
fof(f5384,plain,
( spl23_40
| ~ spl23_20
| spl23_29
| spl23_33 ),
inference(avatar_split_clause,[],[f5374,f1116,f1100,f948,f1357]) ).
fof(f5521,plain,
( ~ min_precedes(sK17(sK21),sK17(sK21),tptp0)
| ~ spl23_100
| spl23_152 ),
inference(superposition,[],[f3563,f2668]) ).
fof(f5805,plain,
( occurrence_of(sK19(sK21),tptp2)
| ~ spl23_60
| ~ spl23_128 ),
inference(superposition,[],[f1814,f3063]) ).
fof(f5810,plain,
( $false
| spl23_33
| ~ spl23_60
| ~ spl23_128 ),
inference(forward_subsumption_resolution,[],[f5805,f1118]) ).
fof(f5811,plain,
( spl23_33
| ~ spl23_60
| ~ spl23_128 ),
inference(avatar_contradiction_clause,[],[f5810]) ).
fof(f5835,plain,
( min_precedes(sK17(sK21),sK17(sK21),tptp0)
| sP0(sK21,sK17(sK21),sK19(sK21))
| ~ root_occ(sK17(sK21),sK21)
| ~ occurrence_of(sK17(sK21),tptp3)
| sK17(sK21) = sK19(sK21)
| ~ spl23_32
| ~ spl23_126 ),
inference(superposition,[],[f1113,f3055]) ).
fof(f5836,plain,
( sP0(sK21,sK17(sK21),sK19(sK21))
| ~ root_occ(sK17(sK21),sK21)
| ~ occurrence_of(sK17(sK21),tptp3)
| sK17(sK21) = sK19(sK21)
| ~ spl23_32
| ~ spl23_100
| ~ spl23_126
| spl23_152 ),
inference(forward_subsumption_resolution,[],[f5835,f5521]) ).
fof(f5844,plain,
( ~ root_occ(sK17(sK21),sK21)
| ~ occurrence_of(sK17(sK21),tptp3)
| sK17(sK21) = sK19(sK21)
| ~ spl23_32
| ~ spl23_100
| spl23_103
| ~ spl23_126
| spl23_152 ),
inference(forward_subsumption_resolution,[],[f5836,f2761]) ).
fof(f5847,plain,
( ~ occurrence_of(sK17(sK21),tptp3)
| sK17(sK21) = sK19(sK21)
| ~ spl23_11
| ~ spl23_32
| ~ spl23_100
| spl23_103
| ~ spl23_126
| spl23_152 ),
inference(forward_subsumption_resolution,[],[f5844,f811]) ).
fof(f5850,plain,
( sK17(sK21) = sK19(sK21)
| ~ spl23_11
| ~ spl23_32
| ~ spl23_62
| ~ spl23_100
| spl23_103
| ~ spl23_126
| spl23_152 ),
inference(forward_subsumption_resolution,[],[f5847,f1821]) ).
fof(f5853,plain,
( $false
| spl23_2
| ~ spl23_11
| ~ spl23_32
| ~ spl23_62
| ~ spl23_100
| spl23_103
| ~ spl23_126
| spl23_152 ),
inference(forward_subsumption_resolution,[],[f5850,f361]) ).
fof(f5854,plain,
( spl23_2
| ~ spl23_11
| ~ spl23_32
| ~ spl23_62
| ~ spl23_100
| spl23_103
| ~ spl23_126
| spl23_152 ),
inference(avatar_contradiction_clause,[],[f5853]) ).
fof(f5872,plain,
( occurrence_of(sK18(sK21),tptp2)
| ~ spl23_60
| ~ spl23_129 ),
inference(superposition,[],[f1814,f3068]) ).
fof(f6758,plain,
( tptp2 = sK1(sK18(sK21))
| ~ spl23_60
| ~ spl23_129 ),
inference(resolution,[],[f5872,f688]) ).
fof(f6763,plain,
( tptp4 = tptp2
| ~ spl23_19
| ~ spl23_60
| ~ spl23_129
| ~ spl23_167 ),
inference(forward_demodulation,[],[f6758,f4064]) ).
fof(f6766,plain,
( $false
| ~ spl23_19
| ~ spl23_60
| ~ spl23_129
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f6763,f271]) ).
fof(f6767,plain,
( ~ spl23_19
| ~ spl23_60
| ~ spl23_129
| ~ spl23_167 ),
inference(avatar_contradiction_clause,[],[f6766]) ).
cnf(s4,plain,
~ spl23_2,
inference(sat_conversion,[],[f414]) ).
cnf(s13,plain,
spl23_11,
inference(sat_conversion,[],[f820]) ).
cnf(s19,plain,
( ~ spl23_20
| spl23_21 ),
inference(sat_conversion,[],[f955]) ).
cnf(s20,plain,
spl23_20,
inference(sat_conversion,[],[f958]) ).
cnf(s37,plain,
( ~ spl23_20
| ~ spl23_29
| spl23_32 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s52,plain,
( ~ spl23_29
| ~ spl23_33 ),
inference(sat_conversion,[],[f1383]) ).
cnf(s54,plain,
( spl23_2
| ~ spl23_40 ),
inference(sat_conversion,[],[f1425]) ).
cnf(s82,plain,
~ spl23_46,
inference(sat_conversion,[],[f1847]) ).
cnf(s96,plain,
( ~ spl23_11
| spl23_62 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s108,plain,
( spl23_2
| ~ spl23_11
| ~ spl23_92
| spl23_93 ),
inference(sat_conversion,[],[f2566]) ).
cnf(s109,plain,
( ~ spl23_19
| spl23_92 ),
inference(sat_conversion,[],[f2568]) ).
cnf(s115,plain,
( spl23_2
| ~ spl23_11
| spl23_19 ),
inference(sat_conversion,[],[f2612]) ).
cnf(s119,plain,
( ~ spl23_92
| ~ spl23_98
| spl23_99
| spl23_100 ),
inference(sat_conversion,[],[f2669]) ).
cnf(s120,plain,
( ~ spl23_92
| ~ spl23_98
| spl23_101
| spl23_102 ),
inference(sat_conversion,[],[f2677]) ).
cnf(s126,plain,
( spl23_2
| ~ spl23_11
| spl23_98 ),
inference(sat_conversion,[],[f2720]) ).
cnf(s127,plain,
( ~ spl23_11
| ~ spl23_20
| ~ spl23_29
| spl23_60
| ~ spl23_62
| ~ spl23_98
| spl23_103 ),
inference(sat_conversion,[],[f2763]) ).
cnf(s128,plain,
( ~ spl23_11
| ~ spl23_20
| ~ spl23_29
| ~ spl23_62
| spl23_64
| ~ spl23_98
| spl23_103 ),
inference(sat_conversion,[],[f2764]) ).
cnf(s138,plain,
( ~ spl23_93
| ~ spl23_98
| ~ spl23_102 ),
inference(sat_conversion,[],[f2923]) ).
cnf(s149,plain,
( ~ spl23_20
| ~ spl23_60
| ~ spl23_64
| spl23_126
| spl23_128
| spl23_129 ),
inference(sat_conversion,[],[f3069]) ).
cnf(s151,plain,
( spl23_33
| ~ spl23_103 ),
inference(sat_conversion,[],[f3080]) ).
cnf(s158,plain,
( ~ spl23_20
| ~ spl23_103
| ~ spl23_136
| spl23_139
| spl23_141
| spl23_142 ),
inference(sat_conversion,[],[f3199]) ).
cnf(s160,plain,
( ~ spl23_103
| spl23_136 ),
inference(sat_conversion,[],[f3213]) ).
cnf(s161,plain,
( spl23_29
| ~ spl23_103
| ~ spl23_141 ),
inference(sat_conversion,[],[f3222]) ).
cnf(s173,plain,
( ~ spl23_19
| ~ spl23_99
| spl23_152
| ~ spl23_153 ),
inference(sat_conversion,[],[f3570]) ).
cnf(s204,plain,
( ~ spl23_11
| ~ spl23_19
| ~ spl23_20
| spl23_46
| ~ spl23_98
| spl23_153
| ~ spl23_167 ),
inference(sat_conversion,[],[f4051]) ).
cnf(s207,plain,
( ~ spl23_19
| ~ spl23_103
| ~ spl23_142
| ~ spl23_167 ),
inference(sat_conversion,[],[f4071]) ).
cnf(s214,plain,
( ~ spl23_11
| ~ spl23_20
| spl23_46
| ~ spl23_103
| ~ spl23_139
| spl23_141 ),
inference(sat_conversion,[],[f4195]) ).
cnf(s220,plain,
( ~ spl23_93
| ~ spl23_152 ),
inference(sat_conversion,[],[f4351]) ).
cnf(s240,plain,
( ~ spl23_19
| spl23_95
| ~ spl23_101
| ~ spl23_118
| spl23_167 ),
inference(sat_conversion,[],[f4744]) ).
cnf(s245,plain,
( ~ spl23_95
| ~ spl23_98 ),
inference(sat_conversion,[],[f4781]) ).
cnf(s269,plain,
( ~ spl23_98
| spl23_213 ),
inference(sat_conversion,[],[f5026]) ).
cnf(s271,plain,
( spl23_118
| spl23_119
| ~ spl23_213 ),
inference(sat_conversion,[],[f5059]) ).
cnf(s281,plain,
( ~ spl23_21
| ~ spl23_98
| ~ spl23_119 ),
inference(sat_conversion,[],[f5252]) ).
cnf(s303,plain,
( ~ spl23_11
| ~ spl23_20
| spl23_29
| ~ spl23_33
| ~ spl23_62
| ~ spl23_98
| spl23_103 ),
inference(sat_conversion,[],[f5360]) ).
cnf(s307,plain,
( ~ spl23_20
| spl23_29
| spl23_33
| spl23_40 ),
inference(sat_conversion,[],[f5384]) ).
cnf(s319,plain,
( spl23_33
| ~ spl23_60
| ~ spl23_128 ),
inference(sat_conversion,[],[f5811]) ).
cnf(s325,plain,
( spl23_2
| ~ spl23_11
| ~ spl23_32
| ~ spl23_62
| ~ spl23_100
| spl23_103
| ~ spl23_126
| spl23_152 ),
inference(sat_conversion,[],[f5854]) ).
cnf(s383,plain,
( ~ spl23_19
| ~ spl23_60
| ~ spl23_129
| ~ spl23_167 ),
inference(sat_conversion,[],[f6767]) ).
cnf(s400,plain,
spl23_21,
inference(rat,[],[s19,s20]) ).
cnf(s403,plain,
spl23_62,
inference(rat,[],[s96,s13]) ).
cnf(s409,plain,
spl23_98,
inference(rat,[],[s126,s13,s4]) ).
cnf(s410,plain,
spl23_19,
inference(rat,[],[s115,s13,s4]) ).
cnf(s413,plain,
~ spl23_40,
inference(rat,[],[s54,s4]) ).
cnf(s417,plain,
~ spl23_119,
inference(rat,[],[s281,s400,s409]) ).
cnf(s418,plain,
spl23_213,
inference(rat,[],[s269,s409]) ).
cnf(s419,plain,
~ spl23_95,
inference(rat,[],[s245,s409]) ).
cnf(s430,plain,
spl23_92,
inference(rat,[],[s109,s410]) ).
cnf(s439,plain,
spl23_118,
inference(rat,[],[s271,s418,s417]) ).
cnf(s448,plain,
spl23_93,
inference(rat,[],[s108,s4,s13,s430]) ).
cnf(s452,plain,
~ spl23_152,
inference(rat,[],[s220,s448]) ).
cnf(s453,plain,
~ spl23_102,
inference(rat,[],[s138,s409,s448]) ).
cnf(s454,plain,
spl23_101,
inference(rat,[],[s120,s430,s409,s453]) ).
cnf(s459,plain,
spl23_167,
inference(rat,[],[s240,s419,s439,s410,s454]) ).
cnf(s465,plain,
spl23_153,
inference(rat,[],[s204,s410,s409,s13,s82,s20,s459]) ).
cnf(s469,plain,
~ spl23_99,
inference(rat,[],[s173,s452,s410,s465]) ).
cnf(s471,plain,
spl23_100,
inference(rat,[],[s119,s430,s409,s469]) ).
cnf(s485,plain,
( ~ spl23_33
| spl23_29 ),
inference(rat,[],[s158,s214,s160,s161,s207,s303,s409,s403,s459,s410,s13,s82,s20]) ).
cnf(s486,plain,
spl23_29,
inference(rat,[],[s485,s307,s20,s413]) ).
cnf(s487,plain,
~ spl23_33,
inference(rat,[],[s52,s486]) ).
cnf(s488,plain,
spl23_32,
inference(rat,[],[s37,s20,s486]) ).
cnf(s491,plain,
~ spl23_103,
inference(rat,[],[s151,s487]) ).
cnf(s492,plain,
~ spl23_126,
inference(rat,[],[s325,s452,s491,s471,s4,s403,s13,s488]) ).
cnf(s494,plain,
spl23_60,
inference(rat,[],[s127,s486,s409,s403,s13,s20,s491]) ).
cnf(s496,plain,
spl23_64,
inference(rat,[],[s128,s486,s409,s403,s13,s20,s491]) ).
cnf(s501,plain,
~ spl23_129,
inference(rat,[],[s383,s459,s410,s494]) ).
cnf(s502,plain,
~ spl23_128,
inference(rat,[],[s319,s487,s494]) ).
cnf(s503,plain,
$false,
inference(rat,[],[s149,s501,s502,s492,s20,s496,s494]) ).
fof(f6768,plain,
$false,
inference(avatar_sat_refutation,[],[s503]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO008+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n008.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 22:20:10 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.03/2.46 % (1659861)Detected formulas, will run a generic FOF schedule.
% 11.03/2.46 % (1659868)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3464915478:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.03/2.46 % (1659870)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2344888256:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.03/2.46 % (1659872)dis-21_1_sil=8000:lcm=predicate:random_seed=3482243646:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.03/2.46 % (1659867)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1083172605:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.03/2.46 % (1659866)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3465249672:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.03/2.46 % (1659869)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2321832631:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.03/2.46 % (1659871)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4078973310:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.03/2.46 % (1659869)Instruction limit reached!
% 11.03/2.46 % (1659869)------------------------------
% 11.03/2.46 % (1659869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659869)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659869)Termination reason: Instruction limit
% 11.03/2.46 % (1659869)Termination phase: Saturation
% 11.03/2.46 % (1659869)Time elapsed: 0.058 s
% 11.03/2.46 % (1659869)Peak memory usage: 88 MB
% 11.03/2.46 % (1659869)Instructions burned: 110 (million)
% 11.03/2.46 % (1659870)Instruction limit reached!
% 11.03/2.46 % (1659870)------------------------------
% 11.03/2.46 % (1659870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659870)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659870)Termination reason: Instruction limit
% 11.03/2.46 % (1659870)Termination phase: Saturation
% 11.03/2.46 % (1659870)Time elapsed: 0.069 s
% 11.03/2.46 % (1659870)Peak memory usage: 88 MB
% 11.03/2.46 % (1659870)Instructions burned: 120 (million)
% 11.03/2.46 % (1659872)Instruction limit reached!
% 11.03/2.46 % (1659872)------------------------------
% 11.03/2.46 % (1659872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659872)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659872)Termination reason: Instruction limit
% 11.03/2.46 % (1659872)Termination phase: Saturation
% 11.03/2.46 % (1659872)Time elapsed: 0.074 s
% 11.03/2.46 % (1659872)Peak memory usage: 89 MB
% 11.03/2.46 % (1659872)Instructions burned: 130 (million)
% 11.03/2.46 % (1659871)Instruction limit reached!
% 11.03/2.46 % (1659871)------------------------------
% 11.03/2.46 % (1659871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659871)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659871)Termination reason: Instruction limit
% 11.03/2.46 % (1659871)Termination phase: Saturation
% 11.03/2.46 % (1659871)Time elapsed: 0.100 s
% 11.03/2.46 % (1659871)Peak memory usage: 90 MB
% 11.03/2.46 % (1659871)Instructions burned: 140 (million)
% 11.03/2.46 % (1659880)lrs+10_1_sil=8000:sp=occurrence:random_seed=1191817079:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.03/2.46 % (1659882)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2253145499:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 11.03/2.46 % (1659881)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2596968548:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.03/2.46 % (1659881)Refutation not found, incomplete strategy
% 11.03/2.46 % (1659881)------------------------------
% 11.03/2.46 % (1659881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659881)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659881)Termination reason: Refutation not found, incomplete strategy
% 11.03/2.46 % (1659881)Time elapsed: 0.004 s
% 11.03/2.46 % (1659881)Peak memory usage: 88 MB
% 11.03/2.46 % (1659881)Instructions burned: 5 (million)
% 11.03/2.46 % (1659883)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1341307144:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 11.03/2.46 % (1659880)Instruction limit reached!
% 11.03/2.46 % (1659880)------------------------------
% 11.03/2.46 % (1659880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659880)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659880)Termination reason: Instruction limit
% 11.03/2.46 % (1659880)Termination phase: Saturation
% 11.03/2.46 % (1659880)Time elapsed: 0.167 s
% 11.03/2.46 % (1659880)Peak memory usage: 90 MB
% 11.03/2.46 % (1659880)Instructions burned: 286 (million)
% 11.03/2.46 % (1659883)Instruction limit reached!
% 11.03/2.46 % (1659883)------------------------------
% 11.03/2.46 % (1659883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659883)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659883)Termination reason: Instruction limit
% 11.03/2.46 % (1659883)Termination phase: Saturation
% 11.03/2.46 % (1659883)Time elapsed: 0.136 s
% 11.03/2.46 % (1659883)Peak memory usage: 90 MB
% 11.03/2.46 % (1659883)Instructions burned: 248 (million)
% 11.03/2.46 % (1659882)Instruction limit reached!
% 11.03/2.46 % (1659882)------------------------------
% 11.03/2.46 % (1659882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659882)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659882)Termination reason: Instruction limit
% 11.03/2.46 % (1659882)Termination phase: Saturation
% 11.03/2.46 % (1659882)Time elapsed: 0.213 s
% 11.03/2.46 % (1659882)Peak memory usage: 92 MB
% 11.03/2.46 % (1659882)Instructions burned: 326 (million)
% 11.03/2.46 % (1659881)------------------------------
% 11.03/2.46 % (1659881)------------------------------
% 11.03/2.46 % (1659888)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3682693533:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 11.03/2.46 % (1659889)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2696530041:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 11.03/2.46 % (1659890)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1352682624:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 11.03/2.46 % (1659891)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3032462766:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 11.03/2.46 % (1659890)Instruction limit reached!
% 11.03/2.46 % (1659890)------------------------------
% 11.03/2.46 % (1659890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659890)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659890)Termination reason: Instruction limit
% 11.03/2.46 % (1659890)Termination phase: Saturation
% 11.03/2.46 % (1659890)Time elapsed: 0.080 s
% 11.03/2.46 % (1659890)Peak memory usage: 90 MB
% 11.03/2.46 % (1659890)Instructions burned: 113 (million)
% 11.03/2.46 % (1659891)Instruction limit reached!
% 11.03/2.46 % (1659891)------------------------------
% 11.03/2.46 % (1659891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659891)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659891)Termination reason: Instruction limit
% 11.03/2.46 % (1659891)Termination phase: Saturation
% 11.03/2.46 % (1659891)Time elapsed: 0.066 s
% 11.03/2.46 % (1659891)Peak memory usage: 89 MB
% 11.03/2.46 % (1659891)Instructions burned: 127 (million)
% 11.03/2.46 % (1659888)Instruction limit reached!
% 11.03/2.46 % (1659888)------------------------------
% 11.03/2.46 % (1659888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659888)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659888)Termination reason: Instruction limit
% 11.03/2.46 % (1659888)Termination phase: Saturation
% 11.03/2.46 % (1659888)Time elapsed: 0.165 s
% 11.03/2.46 % (1659888)Peak memory usage: 88 MB
% 11.03/2.46 % (1659888)Instructions burned: 295 (million)
% 11.03/2.46 % (1659896)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2273632770:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 11.03/2.46 % (1659898)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4201045852:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 11.03/2.46 % (1659897)lrs+10_1_sil=8000:sp=occurrence:random_seed=3781632544:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 11.03/2.46 % (1659896)Instruction limit reached!
% 11.03/2.46 % (1659896)------------------------------
% 11.03/2.46 % (1659896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659896)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659896)Termination reason: Instruction limit
% 11.03/2.46 % (1659896)Termination phase: Saturation
% 11.03/2.46 % (1659896)Time elapsed: 0.068 s
% 11.03/2.46 % (1659896)Peak memory usage: 89 MB
% 11.03/2.46 % (1659896)Instructions burned: 116 (million)
% 11.03/2.46 % (1659902)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2847108621:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 11.03/2.46 % (1659898)Instruction limit reached!
% 11.03/2.46 % (1659898)------------------------------
% 11.03/2.46 % (1659898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659898)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659898)Termination reason: Instruction limit
% 11.03/2.46 % (1659898)Termination phase: Saturation
% 11.03/2.46 % (1659898)Time elapsed: 0.225 s
% 11.03/2.46 % (1659898)Peak memory usage: 89 MB
% 11.03/2.46 % (1659898)Instructions burned: 438 (million)
% 11.03/2.46 % (1659904)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=980374038:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 11.03/2.46 % (1659866)First to succeed.
% 11.03/2.46 % (1659904)Instruction limit reached!
% 11.03/2.46 % (1659904)------------------------------
% 11.03/2.46 % (1659904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659904)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659904)Termination reason: Instruction limit
% 11.03/2.46 % (1659904)Termination phase: Saturation
% 11.03/2.46 % (1659904)Time elapsed: 0.078 s
% 11.03/2.46 % (1659904)Peak memory usage: 90 MB
% 11.03/2.46 % (1659904)Instructions burned: 134 (million)
% 11.03/2.46 % (1659866)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1659861"
% 11.03/2.46 % (1659897)Instruction limit reached!
% 11.03/2.46 % (1659897)------------------------------
% 11.03/2.46 % (1659897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.03/2.46 % (1659897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.03/2.46 % (1659897)CaDiCaL version: 2.1.3
% 11.03/2.46 % (1659897)Termination reason: Instruction limit
% 11.03/2.46 % (1659897)Termination phase: Saturation
% 11.03/2.46 % (1659897)Time elapsed: 0.514 s
% 11.03/2.46 % (1659897)Peak memory usage: 94 MB
% 11.03/2.46 % (1659897)Instructions burned: 908 (million)
% 11.03/2.46 % (1659906)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2914493812:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 11.03/2.46 % (1659907)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3652875239:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 11.03/2.46 % (1659866)Refutation found. Thanks to Tanya!
% 11.03/2.46 % SZS status Theorem for theBenchmark
% 11.03/2.46 % SZS output start Proof for theBenchmark
% See solution above
% 11.89/2.66 % (1659866)------------------------------
% 11.89/2.66 % (1659866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.89/2.66 % (1659866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.89/2.66 % (1659866)CaDiCaL version: 2.1.3
% 11.89/2.66 % (1659866)Termination reason: Refutation
% 11.89/2.66 % (1659866)Time elapsed: 1.192 s
% 11.89/2.66 % (1659866)Peak memory usage: 136 MB
% 11.89/2.66 % (1659866)Instructions burned: 1776 (million)
% 11.89/2.66 % (1659866)------------------------------
% 11.89/2.66 % (1659866)------------------------------
% 11.89/2.66 % (1659861)Success in time 1.608 s
% 11.89/2.66 % Vampire exiting
%------------------------------------------------------------------------------