%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO001+1 : 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 : n001.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:19 PM UTC 2026
% Result : Theorem 14.04s 3.33s
% Output : Refutation 16.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 45
% Syntax : Number of formulae : 354 ( 42 unt; 22 def)
% Number of atoms : 1024 ( 84 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1179 ( 509 ~; 520 |; 103 &)
% ( 29 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 41 ( 39 usr; 23 prp; 0-5 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-5 aty)
% Number of variables : 452 ( 0 sgn 397 !; 55 ?)
% 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(f12,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3,X4] :
( subactivity(X3,X0)
& subactivity(X4,X0)
& atocc(X1,X3)
& atocc(X2,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(f22,axiom,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ~ ? [X3] : min_precedes(X0,X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
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(f24,axiom,
! [X0,X1] :
( atocc(X0,X1)
<=> ? [X2] :
( subactivity(X1,X2)
& atomic(X2)
& occurrence_of(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_23) ).
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(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(f36,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp3)
| occurrence_of(X2,tptp2) )
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
fof(f39,axiom,
atomic(tptp4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_38) ).
fof(f40,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_39) ).
fof(f41,axiom,
atomic(tptp2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_40) ).
fof(f50,axiom,
! [X0,X1,X2,X3,X4] :
( send_message(X0,X1,X2,X3,X4)
=> ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f51,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( send_message(X0,X1,X2,X3,X4)
& occurrence_of(X5,X0) )
=> min_precedes(X3,X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_50) ).
fof(f55,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( transmit_message(X0,X1,X2,X3,X4)
& occurrence_of(X5,X0) )
=> ? [X6,X7] :
( send_message(X6,X1,X2,X3,X4)
& occurrence_of(X7,X6)
& root_occ(X7,X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_54) ).
fof(f57,axiom,
! [X0,X1,X2,X3] :
( ( tptp1(X0,X1,X2)
& occurrence_of(X3,X0) )
=> ? [X4,X5,X6,X7] :
( transmit_message(X4,X5,X6,X2,X1)
& occurrence_of(X7,X4)
& subactivity_occurrence(X7,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_56) ).
fof(f59,conjecture,
~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f60,negated_conjecture,
~ ~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(negated_conjecture,[status(cth)],[f59]) ).
fof(f61,plain,
? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(flattening,[],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
inference(unused_predicate_definition_removal,[],[f35]) ).
fof(f63,plain,
! [X0,X1] :
( leaf(X0,X1)
=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ~ ? [X3] : min_precedes(X0,X3,X1) ) ),
inference(unused_predicate_definition_removal,[],[f22]) ).
fof(f64,plain,
! [X0,X1] :
( root_occ(X0,X1)
=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
inference(unused_predicate_definition_removal,[],[f34]) ).
fof(f65,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(unused_predicate_definition_removal,[],[f23]) ).
fof(f66,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f67,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f68,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f69,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f68]) ).
fof(f76,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f80,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( subactivity(X3,X0)
& subactivity(X4,X0)
& atocc(X1,X3)
& atocc(X2,X4) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f83,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f93,plain,
! [X0,X1] :
( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ),
inference(ennf_transformation,[],[f63]) ).
fof(f94,plain,
! [X0,X1,X2] :
( ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) )
| ~ next_subocc(X0,X1,X2) ),
inference(ennf_transformation,[],[f65]) ).
fof(f95,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f96,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(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(ennf_transformation,[],[f29]) ).
fof(f102,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,[],[f101]) ).
fof(f111,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) )
| ~ root_occ(X0,X1) ),
inference(ennf_transformation,[],[f64]) ).
fof(f112,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f62]) ).
fof(f113,plain,
! [X0] :
( ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp3)
| occurrence_of(X2,tptp2) )
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f115,plain,
! [X0,X1,X2,X3,X4] :
( ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 )
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f50]) ).
fof(f116,plain,
! [X0,X1,X2,X3,X4,X5] :
( min_precedes(X3,X5,X4)
| ~ send_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(ennf_transformation,[],[f51]) ).
fof(f117,plain,
! [X0,X1,X2,X3,X4,X5] :
( min_precedes(X3,X5,X4)
| ~ send_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(flattening,[],[f116]) ).
fof(f120,plain,
! [X0,X1,X2,X3,X4,X5] :
( ? [X6,X7] :
( send_message(X6,X1,X2,X3,X4)
& occurrence_of(X7,X6)
& root_occ(X7,X5) )
| ~ transmit_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f121,plain,
! [X0,X1,X2,X3,X4,X5] :
( ? [X6,X7] :
( send_message(X6,X1,X2,X3,X4)
& occurrence_of(X7,X6)
& root_occ(X7,X5) )
| ~ transmit_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(flattening,[],[f120]) ).
fof(f123,plain,
! [X0,X1,X2,X3] :
( ? [X4,X5,X6,X7] :
( transmit_message(X4,X5,X6,X2,X1)
& occurrence_of(X7,X4)
& subactivity_occurrence(X7,X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(ennf_transformation,[],[f57]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( ? [X4,X5,X6,X7] :
( transmit_message(X4,X5,X6,X2,X1)
& occurrence_of(X7,X4)
& subactivity_occurrence(X7,X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(flattening,[],[f123]) ).
fof(f125,plain,
! [X0] :
( ( activity(sK0(X0))
& occurrence_of(X0,sK0(X0)) )
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f67]) ).
fof(f126,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f76]) ).
fof(f129,plain,
! [X0,X1,X2] :
( ( subactivity(sK1(X0,X1,X2),X0)
& subactivity(sK2(X0,X1,X2),X0)
& atocc(X1,sK1(X0,X1,X2))
& atocc(X2,sK2(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X3,sK1(X0,X1,X2)),skolemize(X4,sK2(X0,X1,X2))],[f80]) ).
fof(f132,plain,
! [X0,X1] :
( ( ( root(X0,X1)
| min_precedes(sK5(X0,X1),X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0,X1))],[f93]) ).
fof(f133,plain,
! [X0,X1] :
( ( atocc(X0,X1)
| ! [X2] :
( ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X0,X2) ) )
& ( ? [X2] :
( subactivity(X1,X2)
& atomic(X2)
& occurrence_of(X0,X2) )
| ~ atocc(X0,X1) ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f134,plain,
! [X0,X1] :
( ( atocc(X0,X1)
| ! [X2] :
( ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X0,X2) ) )
& ( ? [X3] :
( subactivity(X1,X3)
& atomic(X3)
& occurrence_of(X0,X3) )
| ~ atocc(X0,X1) ) ),
inference(rectify,[],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( ( atocc(X0,X1)
| ! [X2] :
( ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X0,X2) ) )
& ( ( subactivity(X1,sK6(X0,X1))
& atomic(sK6(X0,X1))
& occurrence_of(X0,sK6(X0,X1)) )
| ~ atocc(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X3,sK6(X0,X1))],[f134]) ).
fof(f136,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK7(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK7(X0,X1,X2))
& subactivity_occurrence(X2,sK7(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f96]) ).
fof(f140,plain,
! [X0,X1] :
( ( occurrence_of(X1,sK11(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK11(X0,X1)) )
| ~ root_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f111]) ).
fof(f141,plain,
! [X0,X1] :
( ( occurrence_of(X1,sK12(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK12(X0,X1)) )
| ~ leaf_occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f112]) ).
fof(f142,plain,
! [X0] :
( ( occurrence_of(sK13(X0),tptp4)
& root_occ(sK13(X0),X0)
& ( occurrence_of(sK14(X0),tptp3)
| occurrence_of(sK14(X0),tptp2) )
& leaf_occ(sK14(X0),X0)
& next_subocc(sK13(X0),sK14(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14]),skolemize(X1,sK13(X0)),skolemize(X2,sK14(X0))],[f113]) ).
fof(f143,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( send_message(sK15(X1,X2,X3,X4,X5),X1,X2,X3,X4)
& occurrence_of(sK16(X1,X2,X3,X4,X5),sK15(X1,X2,X3,X4,X5))
& root_occ(sK16(X1,X2,X3,X4,X5),X5) )
| ~ transmit_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X6,sK15(X1,X2,X3,X4,X5)),skolemize(X7,sK16(X1,X2,X3,X4,X5))],[f121]) ).
fof(f144,plain,
! [X0,X1,X2,X3] :
( ( transmit_message(sK17(X1,X2,X3),sK18(X1,X2,X3),sK19(X1,X2,X3),X2,X1)
& occurrence_of(sK20(X1,X2,X3),sK17(X1,X2,X3))
& subactivity_occurrence(sK20(X1,X2,X3),X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19,sK20]),skolemize(X4,sK17(X1,X2,X3)),skolemize(X5,sK18(X1,X2,X3)),skolemize(X6,sK19(X1,X2,X3)),skolemize(X7,sK20(X1,X2,X3))],[f124]) ).
fof(f145,plain,
( tptp1(sK21,tptp0,sK22)
& occurrence_of(sK23,sK21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23]),skolemize(X0,sK21),skolemize(X1,sK22),skolemize(X2,sK23)],[f61]) ).
fof(f146,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f148,plain,
! [X0] :
( occurrence_of(X0,sK0(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f69]) ).
fof(f156,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f162,plain,
! [X2,X0,X1] :
( atocc(X2,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f170,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f83]) ).
fof(f177,plain,
! [X3,X0,X1] :
( ~ min_precedes(X0,X3,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f132]) ).
fof(f179,plain,
! [X2,X3,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2) ),
inference(cnf_transformation,[],[f94]) ).
fof(f181,plain,
! [X0,X1] :
( occurrence_of(X0,sK6(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f182,plain,
! [X0,X1] :
( atomic(sK6(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f186,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f187,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK7(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f189,plain,
! [X2,X0,X1] :
( occurrence_of(sK7(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f194,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,[],[f102]) ).
fof(f200,plain,
! [X0,X1] :
( root(X0,sK11(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f140]) ).
fof(f201,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f140]) ).
fof(f202,plain,
! [X0,X1] :
( occurrence_of(X1,sK11(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f140]) ).
fof(f203,plain,
! [X0,X1] :
( leaf(X0,sK12(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
fof(f204,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
fof(f205,plain,
! [X0,X1] :
( occurrence_of(X1,sK12(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
fof(f206,plain,
! [X0] :
( next_subocc(sK13(X0),sK14(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f207,plain,
! [X0] :
( leaf_occ(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f208,plain,
! [X0] :
( occurrence_of(sK14(X0),tptp2)
| occurrence_of(sK14(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f209,plain,
! [X0] :
( root_occ(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f210,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f213,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f39]) ).
fof(f214,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f40]) ).
fof(f215,plain,
atomic(tptp2),
inference(cnf_transformation,[],[f41]) ).
fof(f227,plain,
! [X2,X3,X0,X1,X4] :
( tptp2 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f115]) ).
fof(f228,plain,
! [X2,X3,X0,X1,X4] :
( tptp3 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f115]) ).
fof(f229,plain,
! [X2,X3,X0,X1,X4] :
( tptp4 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f115]) ).
fof(f230,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ send_message(X0,X1,X2,X3,X4)
| min_precedes(X3,X5,X4)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f237,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| root_occ(sK16(X1,X2,X3,X4,X5),X5)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f238,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| occurrence_of(sK16(X1,X2,X3,X4,X5),sK15(X1,X2,X3,X4,X5))
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f239,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| send_message(sK15(X1,X2,X3,X4,X5),X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f245,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| occurrence_of(sK20(X1,X2,X3),sK17(X1,X2,X3))
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f246,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| transmit_message(sK17(X1,X2,X3),sK18(X1,X2,X3),sK19(X1,X2,X3),X2,X1)
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f248,plain,
occurrence_of(sK23,sK21),
inference(cnf_transformation,[],[f145]) ).
fof(f249,plain,
tptp1(sK21,tptp0,sK22),
inference(cnf_transformation,[],[f145]) ).
fof(f250,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp4,X1,X2,X3,X4),
inference(equality_resolution,[],[f229]) ).
fof(f251,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp3,X1,X2,X3,X4),
inference(equality_resolution,[],[f228]) ).
fof(f252,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp2,X1,X2,X3,X4),
inference(equality_resolution,[],[f227]) ).
fof(f253,plain,
! [X0] :
( transmit_message(sK17(tptp0,sK22,X0),sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0)
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f246,f249]) ).
fof(f254,plain,
! [X0] :
( occurrence_of(sK20(tptp0,sK22,X0),sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f245,f249]) ).
fof(f256,plain,
! [X0,X1] :
( ~ occurrence_of(sK20(tptp0,sK22,X0),X1)
| sK17(tptp0,sK22,X0) = X1
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f150,f254]) ).
fof(f268,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X3,sK7(X2,X0,X1))
| min_precedes(X1,X3,X4)
| X1 = X3
| ~ occurrence_of(sK7(X2,X0,X1),X4)
| ~ arboreal(X3)
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,X2)
| min_precedes(X3,X1,X4) ),
inference(resolution,[],[f187,f194]) ).
fof(f287,plain,
! [X0,X1] :
( ~ occurrence_of(sK14(X0),X1)
| ~ occurrence_of(X0,tptp0)
| occurrence_of(sK14(X0),tptp3)
| tptp2 = X1 ),
inference(resolution,[],[f208,f150]) ).
fof(f290,plain,
! [X0,X1] :
( occurrence_of(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1),sK15(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1))
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f238,f253]) ).
fof(f293,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK7(X2,X0,X1),X3)
| ~ min_precedes(X0,X1,X2)
| X2 = X3 ),
inference(resolution,[],[f189,f150]) ).
fof(f297,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK13(X0)) ),
inference(resolution,[],[f210,f156]) ).
fof(f299,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f297,f213]) ).
fof(f302,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK16(sK18(tptp0,sK22,X1),sK19(tptp0,sK22,X1),sK22,tptp0,X0),X2)
| ~ occurrence_of(X1,sK21)
| ~ occurrence_of(X0,sK17(tptp0,sK22,X1))
| sK15(sK18(tptp0,sK22,X1),sK19(tptp0,sK22,X1),sK22,tptp0,X0) = X2 ),
inference(resolution,[],[f290,f150]) ).
fof(f311,plain,
! [X0,X1] :
( send_message(sK15(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1),sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0)
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f239,f253]) ).
fof(f312,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X2,sK15(sK18(tptp0,sK22,X1),sK19(tptp0,sK22,X1),sK22,tptp0,X0))
| ~ occurrence_of(X1,sK21)
| min_precedes(sK22,X2,tptp0)
| ~ occurrence_of(X0,sK17(tptp0,sK22,X1)) ),
inference(resolution,[],[f311,f230]) ).
fof(f313,plain,
! [X0,X1] :
( ~ min_precedes(sK13(X1),X0,tptp0)
| ~ min_precedes(X0,sK14(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f179,f206]) ).
fof(f319,plain,
! [X0,X1] :
( activity_occurrence(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1))
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f146,f290]) ).
fof(f320,plain,
! [X0] :
( activity_occurrence(sK20(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f146,f254]) ).
fof(f324,plain,
! [X0,X1] :
( root_occ(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1),X1)
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f237,f253]) ).
fof(f372,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK21)
| min_precedes(sK22,sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1),tptp0)
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f312,f290]) ).
fof(f373,plain,
! [X0,X1] :
( min_precedes(sK22,sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1),tptp0)
| ~ occurrence_of(X0,sK21)
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0)) ),
inference(duplicate_literal_removal,[],[f372]) ).
fof(f419,plain,
! [X0,X1] :
( ~ activity_occurrence(X0)
| ~ occurrence_of(X0,X1)
| sK0(X0) = X1 ),
inference(resolution,[],[f148,f150]) ).
fof(f420,plain,
! [X0,X1] :
( ~ activity_occurrence(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1))
| ~ occurrence_of(X0,sK21)
| ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| sK15(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1) = sK0(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1)) ),
inference(resolution,[],[f148,f302]) ).
fof(f421,plain,
! [X0] :
( ~ activity_occurrence(sK20(tptp0,sK22,X0))
| sK17(tptp0,sK22,X0) = sK0(sK20(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f148,f256]) ).
fof(f424,plain,
! [X0] :
( ~ occurrence_of(X0,sK21)
| sK17(tptp0,sK22,X0) = sK0(sK20(tptp0,sK22,X0)) ),
inference(forward_subsumption_resolution,[],[f421,f320]) ).
fof(f425,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21)
| sK15(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1) = sK0(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1)) ),
inference(forward_subsumption_resolution,[],[f420,f319]) ).
fof(f426,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK0(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f419,f146]) ).
fof(f428,plain,
! [X0,X1] :
( ~ root_occ(X1,X0)
| sK0(X0) = sK11(X1,X0) ),
inference(resolution,[],[f426,f202]) ).
fof(f430,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| sK0(sK7(X0,X1,X2)) = X0 ),
inference(resolution,[],[f426,f189]) ).
fof(f431,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp4 = sK0(sK13(X0)) ),
inference(resolution,[],[f426,f210]) ).
fof(f432,plain,
! [X0] :
( occurrence_of(sK14(X0),tptp3)
| tptp2 = sK0(sK14(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f426,f208]) ).
fof(f439,plain,
sK17(tptp0,sK22,sK23) = sK0(sK20(tptp0,sK22,sK23)),
inference(resolution,[],[f424,f248]) ).
fof(f446,definition,
( spl24_11
<=> occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23)) ),
introduced(definition,[new_symbols(definition,[spl24_11])],[avatar_definition]) ).
fof(f448,plain,
( occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| ~ spl24_11 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f451,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21)
| tptp0 = sK0(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1))) ),
inference(resolution,[],[f430,f373]) ).
fof(f453,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| sK0(X0) = sK11(sK13(X0),X0) ),
inference(resolution,[],[f428,f209]) ).
fof(f454,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK17(tptp0,sK22,X1))
| sK0(X0) = sK11(sK16(sK18(tptp0,sK22,X1),sK19(tptp0,sK22,X1),sK22,tptp0,X0),X0)
| ~ occurrence_of(X1,sK21) ),
inference(resolution,[],[f428,f324]) ).
fof(f458,plain,
! [X0] :
( ~ occurrence_of(X0,sK21)
| sK15(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,sK20(tptp0,sK22,X0)) = sK0(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,sK20(tptp0,sK22,X0)))
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f425,f254]) ).
fof(f459,plain,
! [X0] :
( ~ occurrence_of(X0,sK21)
| sK15(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,sK20(tptp0,sK22,X0)) = sK0(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,sK20(tptp0,sK22,X0))) ),
inference(duplicate_literal_removal,[],[f458]) ).
fof(f461,plain,
sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK0(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),
inference(resolution,[],[f459,f248]) ).
fof(f462,plain,
( occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))
| ~ activity_occurrence(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))) ),
inference(superposition,[],[f148,f461]) ).
fof(f464,definition,
( spl24_12
<=> activity_occurrence(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))) ),
introduced(definition,[new_symbols(definition,[spl24_12])],[avatar_definition]) ).
fof(f466,plain,
( ~ activity_occurrence(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))
| spl24_12 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f468,definition,
( spl24_13
<=> occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))) ),
introduced(definition,[new_symbols(definition,[spl24_13])],[avatar_definition]) ).
fof(f470,plain,
( occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))
| ~ spl24_13 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f471,plain,
( ~ spl24_12
| spl24_13 ),
inference(avatar_split_clause,[],[f462,f468,f464]) ).
fof(f499,plain,
! [X0] :
( sK0(sK20(tptp0,sK22,X0)) = sK11(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,sK20(tptp0,sK22,X0)),sK20(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21)
| ~ occurrence_of(X0,sK21) ),
inference(resolution,[],[f454,f254]) ).
fof(f500,plain,
! [X0] :
( ~ occurrence_of(X0,sK21)
| sK0(sK20(tptp0,sK22,X0)) = sK11(sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,sK20(tptp0,sK22,X0)),sK20(tptp0,sK22,X0)) ),
inference(duplicate_literal_removal,[],[f499]) ).
fof(f502,plain,
sK0(sK20(tptp0,sK22,sK23)) = sK11(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK20(tptp0,sK22,sK23)),
inference(resolution,[],[f500,f248]) ).
fof(f503,plain,
sK17(tptp0,sK22,sK23) = sK11(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK20(tptp0,sK22,sK23)),
inference(forward_demodulation,[],[f502,f439]) ).
fof(f505,plain,
( occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| ~ root_occ(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK20(tptp0,sK22,sK23)) ),
inference(superposition,[],[f202,f503]) ).
fof(f507,definition,
( spl24_14
<=> root_occ(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK20(tptp0,sK22,sK23)) ),
introduced(definition,[new_symbols(definition,[spl24_14])],[avatar_definition]) ).
fof(f508,plain,
( root_occ(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK20(tptp0,sK22,sK23))
| ~ spl24_14 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f509,plain,
( ~ root_occ(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK20(tptp0,sK22,sK23))
| spl24_14 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f510,plain,
( ~ spl24_14
| spl24_11 ),
inference(avatar_split_clause,[],[f505,f446,f507]) ).
fof(f516,plain,
( ~ occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| ~ occurrence_of(sK23,sK21)
| spl24_14 ),
inference(resolution,[],[f509,f324]) ).
fof(f517,plain,
( ~ occurrence_of(sK23,sK21)
| spl24_14 ),
inference(forward_subsumption_resolution,[],[f516,f254]) ).
fof(f518,plain,
( $false
| spl24_14 ),
inference(forward_subsumption_resolution,[],[f517,f248]) ).
fof(f519,plain,
spl24_14,
inference(avatar_contradiction_clause,[],[f518]) ).
fof(f522,plain,
( subactivity_occurrence(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK20(tptp0,sK22,sK23))
| ~ spl24_14 ),
inference(resolution,[],[f508,f201]) ).
fof(f580,plain,
( activity_occurrence(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))
| ~ spl24_14 ),
inference(resolution,[],[f186,f522]) ).
fof(f581,plain,
( $false
| spl24_12
| ~ spl24_14 ),
inference(forward_subsumption_resolution,[],[f580,f466]) ).
fof(f582,plain,
( spl24_12
| ~ spl24_14 ),
inference(avatar_contradiction_clause,[],[f581]) ).
fof(f590,plain,
( ! [X0] :
( ~ occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = X0 )
| ~ spl24_13 ),
inference(resolution,[],[f470,f150]) ).
fof(f599,plain,
( ~ occurrence_of(sK23,sK21)
| tptp0 = sK0(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_11 ),
inference(resolution,[],[f451,f448]) ).
fof(f601,plain,
( tptp0 = sK0(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_11 ),
inference(forward_subsumption_resolution,[],[f599,f248]) ).
fof(f608,definition,
( spl24_21
<=> occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl24_21])],[avatar_definition]) ).
fof(f609,plain,
( ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| spl24_21 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f610,plain,
( occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| ~ spl24_21 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f615,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X3,sK7(X2,X0,X1))
| sK12(X3,sK7(X2,X0,X1)) = X2
| ~ min_precedes(X0,X1,X2) ),
inference(resolution,[],[f293,f205]) ).
fof(f619,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK7(X0,X1,X2),tptp0)
| ~ min_precedes(X1,X2,X0)
| sK12(sK14(sK7(X0,X1,X2)),sK7(X0,X1,X2)) = X0 ),
inference(resolution,[],[f615,f207]) ).
fof(f620,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK12(sK14(sK7(tptp0,X0,X1)),sK7(tptp0,X0,X1))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f619,f189]) ).
fof(f621,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK12(sK14(sK7(tptp0,X0,X1)),sK7(tptp0,X0,X1)) ),
inference(duplicate_literal_removal,[],[f620]) ).
fof(f623,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK17(tptp0,sK22,X0))
| ~ occurrence_of(X0,sK21)
| tptp0 = sK12(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,X0),sK19(tptp0,sK22,X0),sK22,tptp0,X1))) ),
inference(resolution,[],[f621,f373]) ).
fof(f713,plain,
! [X0,X1] :
( arboreal(sK13(sK7(tptp0,X0,X1)))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f299,f189]) ).
fof(f729,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| ~ atomic(sK6(X0,X1))
| arboreal(X0) ),
inference(resolution,[],[f181,f156]) ).
fof(f739,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| arboreal(X0) ),
inference(forward_subsumption_resolution,[],[f729,f182]) ).
fof(f813,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| arboreal(X1) ),
inference(resolution,[],[f162,f739]) ).
fof(f837,plain,
( ~ occurrence_of(sK23,sK21)
| tptp0 = sK12(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_11 ),
inference(resolution,[],[f623,f448]) ).
fof(f839,plain,
( tptp0 = sK12(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_11 ),
inference(forward_subsumption_resolution,[],[f837,f248]) ).
fof(f840,plain,
( leaf(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ leaf_occ(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_11 ),
inference(superposition,[],[f203,f839]) ).
fof(f843,definition,
( spl24_24
<=> leaf_occ(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))) ),
introduced(definition,[new_symbols(definition,[spl24_24])],[avatar_definition]) ).
fof(f844,plain,
( leaf_occ(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_24 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f845,plain,
( ~ leaf_occ(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| spl24_24 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f848,definition,
( spl24_25
<=> leaf(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl24_25])],[avatar_definition]) ).
fof(f850,plain,
( leaf(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ spl24_25 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f851,plain,
( ~ spl24_24
| spl24_25
| ~ spl24_11 ),
inference(avatar_split_clause,[],[f840,f446,f848,f843]) ).
fof(f852,plain,
( ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| spl24_24 ),
inference(resolution,[],[f845,f207]) ).
fof(f853,plain,
( ~ spl24_21
| spl24_24 ),
inference(avatar_split_clause,[],[f852,f843,f608]) ).
fof(f854,plain,
( ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| spl24_21 ),
inference(resolution,[],[f609,f189]) ).
fof(f855,plain,
( ~ occurrence_of(sK23,sK21)
| ~ occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| spl24_21 ),
inference(resolution,[],[f854,f373]) ).
fof(f856,plain,
( ~ occurrence_of(sK23,sK21)
| spl24_21 ),
inference(forward_subsumption_resolution,[],[f855,f254]) ).
fof(f857,plain,
( $false
| spl24_21 ),
inference(forward_subsumption_resolution,[],[f856,f248]) ).
fof(f858,plain,
spl24_21,
inference(avatar_contradiction_clause,[],[f857]) ).
fof(f865,plain,
( tptp4 = sK0(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_21 ),
inference(resolution,[],[f610,f431]) ).
fof(f868,plain,
( sK0(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))) = sK11(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_21 ),
inference(resolution,[],[f610,f453]) ).
fof(f882,plain,
( tptp0 = sK11(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_11
| ~ spl24_21 ),
inference(forward_demodulation,[],[f868,f601]) ).
fof(f887,plain,
( subactivity_occurrence(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_24 ),
inference(resolution,[],[f844,f204]) ).
fof(f890,plain,
( root(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ root_occ(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_11
| ~ spl24_21 ),
inference(superposition,[],[f200,f882]) ).
fof(f893,definition,
( spl24_26
<=> root_occ(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))) ),
introduced(definition,[new_symbols(definition,[spl24_26])],[avatar_definition]) ).
fof(f894,plain,
( root_occ(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_26 ),
inference(avatar_component_clause,[],[f893]) ).
fof(f895,plain,
( ~ root_occ(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| spl24_26 ),
inference(avatar_component_clause,[],[f893]) ).
fof(f897,definition,
( spl24_27
<=> root(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition]) ).
fof(f899,plain,
( root(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ spl24_27 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f900,plain,
( ~ spl24_26
| spl24_27
| ~ spl24_11
| ~ spl24_21 ),
inference(avatar_split_clause,[],[f890,f608,f446,f897,f893]) ).
fof(f901,plain,
( ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| spl24_26 ),
inference(resolution,[],[f895,f209]) ).
fof(f902,plain,
( $false
| ~ spl24_21
| spl24_26 ),
inference(forward_subsumption_resolution,[],[f901,f610]) ).
fof(f903,plain,
( ~ spl24_21
| spl24_26 ),
inference(avatar_contradiction_clause,[],[f902]) ).
fof(f908,plain,
( subactivity_occurrence(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_26 ),
inference(resolution,[],[f894,f201]) ).
fof(f911,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| ~ arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ arboreal(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))
| ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_24 ),
inference(resolution,[],[f887,f268]) ).
fof(f912,plain,
( activity_occurrence(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_24 ),
inference(resolution,[],[f887,f186]) ).
fof(f917,definition,
( spl24_28
<=> arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))) ),
introduced(definition,[new_symbols(definition,[spl24_28])],[avatar_definition]) ).
fof(f918,plain,
( arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_28 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f919,plain,
( ~ arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| spl24_28 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f926,definition,
( spl24_30
<=> min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl24_30])],[avatar_definition]) ).
fof(f927,plain,
( min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| ~ spl24_30 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f928,plain,
( ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| spl24_30 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f956,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| ~ arboreal(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ arboreal(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))
| ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| min_precedes(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_26 ),
inference(resolution,[],[f908,f268]) ).
fof(f974,plain,
( ~ occurrence_of(sK23,sK21)
| ~ occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| spl24_30 ),
inference(resolution,[],[f928,f373]) ).
fof(f975,plain,
( ~ occurrence_of(sK23,sK21)
| spl24_30 ),
inference(forward_subsumption_resolution,[],[f974,f254]) ).
fof(f976,plain,
( $false
| spl24_30 ),
inference(forward_subsumption_resolution,[],[f975,f248]) ).
fof(f977,plain,
spl24_30,
inference(avatar_contradiction_clause,[],[f976]) ).
fof(f994,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| ~ arboreal(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| min_precedes(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_26 ),
inference(forward_subsumption_resolution,[],[f956,f813]) ).
fof(f995,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| min_precedes(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_26 ),
inference(forward_subsumption_resolution,[],[f994,f713]) ).
fof(f996,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| min_precedes(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_26
| ~ spl24_30 ),
inference(forward_subsumption_resolution,[],[f995,f927]) ).
fof(f1009,definition,
( spl24_39
<=> sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))) ),
introduced(definition,[new_symbols(definition,[spl24_39])],[avatar_definition]) ).
fof(f1011,plain,
( sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_39 ),
inference(avatar_component_clause,[],[f1009]) ).
fof(f1013,definition,
( spl24_40
<=> ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| min_precedes(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_40])],[avatar_definition]) ).
fof(f1014,plain,
( ! [X0] :
( min_precedes(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0) )
| ~ spl24_40 ),
inference(avatar_component_clause,[],[f1013]) ).
fof(f1015,plain,
( spl24_39
| spl24_40
| ~ spl24_26
| ~ spl24_30 ),
inference(avatar_split_clause,[],[f996,f926,f893,f1013,f1009]) ).
fof(f1017,plain,
( tptp4 = sK0(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))
| ~ spl24_21
| ~ spl24_39 ),
inference(superposition,[],[f865,f1011]) ).
fof(f1038,plain,
( tptp4 = sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))
| ~ spl24_21
| ~ spl24_39 ),
inference(forward_demodulation,[],[f1017,f461]) ).
fof(f1042,plain,
( send_message(tptp4,sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0)
| ~ occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| ~ occurrence_of(sK23,sK21)
| ~ spl24_21
| ~ spl24_39 ),
inference(superposition,[],[f311,f1038]) ).
fof(f1044,plain,
( send_message(tptp4,sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0)
| ~ occurrence_of(sK23,sK21)
| ~ spl24_21
| ~ spl24_39 ),
inference(forward_subsumption_resolution,[],[f1042,f254]) ).
fof(f1046,plain,
( ~ occurrence_of(sK23,sK21)
| ~ spl24_21
| ~ spl24_39 ),
inference(forward_subsumption_resolution,[],[f1044,f250]) ).
fof(f1048,plain,
( $false
| ~ spl24_21
| ~ spl24_39 ),
inference(forward_subsumption_resolution,[],[f1046,f248]) ).
fof(f1049,plain,
( ~ spl24_21
| ~ spl24_39 ),
inference(avatar_contradiction_clause,[],[f1048]) ).
fof(f1061,plain,
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| ~ min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| ~ spl24_40 ),
inference(resolution,[],[f1014,f313]) ).
fof(f1075,plain,
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| ~ min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ spl24_40 ),
inference(duplicate_literal_removal,[],[f1061]) ).
fof(f1080,plain,
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ spl24_21
| ~ spl24_40 ),
inference(forward_subsumption_resolution,[],[f1075,f610]) ).
fof(f1087,definition,
( spl24_42
<=> min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl24_42])],[avatar_definition]) ).
fof(f1089,plain,
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ spl24_42 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1097,definition,
( spl24_44
<=> min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl24_44])],[avatar_definition]) ).
fof(f1099,plain,
( ~ min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| spl24_44 ),
inference(avatar_component_clause,[],[f1097]) ).
fof(f1100,plain,
( ~ spl24_44
| spl24_42
| ~ spl24_21
| ~ spl24_40 ),
inference(avatar_split_clause,[],[f1080,f1013,f608,f1087,f1097]) ).
fof(f1108,plain,
( ~ root(sK13(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ spl24_42 ),
inference(resolution,[],[f1089,f170]) ).
fof(f1119,plain,
( $false
| ~ spl24_27
| ~ spl24_42 ),
inference(forward_subsumption_resolution,[],[f1108,f899]) ).
fof(f1120,plain,
( ~ spl24_27
| ~ spl24_42 ),
inference(avatar_contradiction_clause,[],[f1119]) ).
fof(f1512,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp2 = sK0(sK14(X0))
| tptp3 = sK0(sK14(X0)) ),
inference(resolution,[],[f432,f426]) ).
fof(f1519,plain,
( tptp2 = sK0(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| tptp3 = sK0(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_21 ),
inference(resolution,[],[f1512,f610]) ).
fof(f1542,definition,
( spl24_65
<=> tptp3 = sK0(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))) ),
introduced(definition,[new_symbols(definition,[spl24_65])],[avatar_definition]) ).
fof(f1544,plain,
( tptp3 = sK0(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_65 ),
inference(avatar_component_clause,[],[f1542]) ).
fof(f1546,definition,
( spl24_66
<=> tptp2 = sK0(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))) ),
introduced(definition,[new_symbols(definition,[spl24_66])],[avatar_definition]) ).
fof(f1548,plain,
( tptp2 = sK0(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_66 ),
inference(avatar_component_clause,[],[f1546]) ).
fof(f1549,plain,
( spl24_65
| spl24_66
| ~ spl24_21 ),
inference(avatar_split_clause,[],[f1519,f608,f1546,f1542]) ).
fof(f1563,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| ~ arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_24 ),
inference(forward_subsumption_resolution,[],[f911,f813]) ).
fof(f1571,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| ~ min_precedes(sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_24
| ~ spl24_28 ),
inference(forward_subsumption_resolution,[],[f1563,f918]) ).
fof(f1576,plain,
( ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0)
| min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0) )
| ~ spl24_24
| ~ spl24_28
| ~ spl24_30 ),
inference(forward_subsumption_resolution,[],[f1571,f927]) ).
fof(f1584,definition,
( spl24_67
<=> sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))) ),
introduced(definition,[new_symbols(definition,[spl24_67])],[avatar_definition]) ).
fof(f1586,plain,
( sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)) = sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))))
| ~ spl24_67 ),
inference(avatar_component_clause,[],[f1584]) ).
fof(f1588,definition,
( spl24_68
<=> ! [X0] :
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl24_68])],[avatar_definition]) ).
fof(f1589,plain,
( ! [X0] :
( min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),X0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),X0) )
| ~ spl24_68 ),
inference(avatar_component_clause,[],[f1588]) ).
fof(f1590,plain,
( spl24_67
| spl24_68
| ~ spl24_24
| ~ spl24_28
| ~ spl24_30 ),
inference(avatar_split_clause,[],[f1576,f926,f917,f843,f1588,f1584]) ).
fof(f1690,plain,
( occurrence_of(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp3)
| ~ activity_occurrence(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_65 ),
inference(superposition,[],[f148,f1544]) ).
fof(f1691,plain,
( occurrence_of(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp3)
| ~ spl24_24
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f1690,f912]) ).
fof(f1697,plain,
( ~ atomic(tptp3)
| arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_24
| ~ spl24_65 ),
inference(resolution,[],[f1691,f156]) ).
fof(f1699,plain,
( arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_24
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f1697,f214]) ).
fof(f1700,plain,
( $false
| ~ spl24_24
| spl24_28
| ~ spl24_65 ),
inference(forward_subsumption_resolution,[],[f1699,f919]) ).
fof(f1701,plain,
( ~ spl24_24
| spl24_28
| ~ spl24_65 ),
inference(avatar_contradiction_clause,[],[f1700]) ).
fof(f1702,plain,
( occurrence_of(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp2)
| ~ activity_occurrence(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_66 ),
inference(superposition,[],[f148,f1548]) ).
fof(f1703,plain,
( occurrence_of(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp2)
| ~ spl24_24
| ~ spl24_66 ),
inference(forward_subsumption_resolution,[],[f1702,f912]) ).
fof(f1709,plain,
( ~ atomic(tptp2)
| arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_24
| ~ spl24_66 ),
inference(resolution,[],[f1703,f156]) ).
fof(f1711,plain,
( arboreal(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))))
| ~ spl24_24
| ~ spl24_66 ),
inference(forward_subsumption_resolution,[],[f1709,f215]) ).
fof(f1712,plain,
( $false
| ~ spl24_24
| spl24_28
| ~ spl24_66 ),
inference(forward_subsumption_resolution,[],[f1711,f919]) ).
fof(f1713,plain,
( ~ spl24_24
| spl24_28
| ~ spl24_66 ),
inference(avatar_contradiction_clause,[],[f1712]) ).
fof(f1744,plain,
( ! [X0] :
( ~ occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp3)
| tptp2 = X0 )
| ~ spl24_67 ),
inference(superposition,[],[f287,f1586]) ).
fof(f1764,plain,
( ! [X0] :
( ~ occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp3)
| tptp2 = X0 )
| ~ spl24_21
| ~ spl24_67 ),
inference(forward_subsumption_resolution,[],[f1744,f610]) ).
fof(f1855,definition,
( spl24_80
<=> occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl24_80])],[avatar_definition]) ).
fof(f1857,plain,
( occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp3)
| ~ spl24_80 ),
inference(avatar_component_clause,[],[f1855]) ).
fof(f1859,definition,
( spl24_81
<=> ! [X0] :
( ~ occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| tptp2 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl24_81])],[avatar_definition]) ).
fof(f1860,plain,
( ! [X0] :
( ~ occurrence_of(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),X0)
| tptp2 = X0 )
| ~ spl24_81 ),
inference(avatar_component_clause,[],[f1859]) ).
fof(f1861,plain,
( spl24_80
| spl24_81
| ~ spl24_21
| ~ spl24_67 ),
inference(avatar_split_clause,[],[f1764,f1584,f608,f1859,f1855]) ).
fof(f1911,plain,
( tptp2 = sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))
| ~ spl24_13
| ~ spl24_81 ),
inference(resolution,[],[f1860,f470]) ).
fof(f1936,plain,
( send_message(tptp2,sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0)
| ~ occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| ~ occurrence_of(sK23,sK21)
| ~ spl24_13
| ~ spl24_81 ),
inference(superposition,[],[f311,f1911]) ).
fof(f1939,plain,
( send_message(tptp2,sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0)
| ~ occurrence_of(sK23,sK21)
| ~ spl24_13
| ~ spl24_81 ),
inference(forward_subsumption_resolution,[],[f1936,f254]) ).
fof(f1941,plain,
( ~ occurrence_of(sK23,sK21)
| ~ spl24_13
| ~ spl24_81 ),
inference(forward_subsumption_resolution,[],[f1939,f252]) ).
fof(f1943,plain,
( $false
| ~ spl24_13
| ~ spl24_81 ),
inference(forward_subsumption_resolution,[],[f1941,f248]) ).
fof(f1944,plain,
( ~ spl24_13
| ~ spl24_81 ),
inference(avatar_contradiction_clause,[],[f1943]) ).
fof(f2530,definition,
( spl24_112
<=> min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl24_112])],[avatar_definition]) ).
fof(f2531,plain,
( min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| ~ spl24_112 ),
inference(avatar_component_clause,[],[f2530]) ).
fof(f2532,plain,
( ~ min_precedes(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),tptp0)
| spl24_112 ),
inference(avatar_component_clause,[],[f2530]) ).
fof(f2732,plain,
( min_precedes(sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)),sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| ~ spl24_68
| spl24_112 ),
inference(resolution,[],[f2532,f1589]) ).
fof(f2737,plain,
( ~ occurrence_of(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))),tptp0)
| spl24_44
| ~ spl24_68
| spl24_112 ),
inference(forward_subsumption_resolution,[],[f2732,f1099]) ).
fof(f2739,plain,
( $false
| ~ spl24_21
| spl24_44
| ~ spl24_68
| spl24_112 ),
inference(forward_subsumption_resolution,[],[f2737,f610]) ).
fof(f2740,plain,
( ~ spl24_21
| spl24_44
| ~ spl24_68
| spl24_112 ),
inference(avatar_contradiction_clause,[],[f2739]) ).
fof(f2791,plain,
( ~ leaf(sK14(sK7(tptp0,sK22,sK16(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23)))),tptp0)
| ~ spl24_112 ),
inference(resolution,[],[f2531,f177]) ).
fof(f2798,plain,
( $false
| ~ spl24_25
| ~ spl24_112 ),
inference(forward_subsumption_resolution,[],[f2791,f850]) ).
fof(f2799,plain,
( ~ spl24_25
| ~ spl24_112 ),
inference(avatar_contradiction_clause,[],[f2798]) ).
fof(f2900,plain,
( tptp3 = sK15(sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0,sK20(tptp0,sK22,sK23))
| ~ spl24_13
| ~ spl24_80 ),
inference(resolution,[],[f1857,f590]) ).
fof(f2923,plain,
( send_message(tptp3,sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0)
| ~ occurrence_of(sK20(tptp0,sK22,sK23),sK17(tptp0,sK22,sK23))
| ~ occurrence_of(sK23,sK21)
| ~ spl24_13
| ~ spl24_80 ),
inference(superposition,[],[f311,f2900]) ).
fof(f2925,plain,
( send_message(tptp3,sK18(tptp0,sK22,sK23),sK19(tptp0,sK22,sK23),sK22,tptp0)
| ~ occurrence_of(sK23,sK21)
| ~ spl24_13
| ~ spl24_80 ),
inference(forward_subsumption_resolution,[],[f2923,f254]) ).
fof(f2927,plain,
( ~ occurrence_of(sK23,sK21)
| ~ spl24_13
| ~ spl24_80 ),
inference(forward_subsumption_resolution,[],[f2925,f251]) ).
fof(f2929,plain,
( $false
| ~ spl24_13
| ~ spl24_80 ),
inference(forward_subsumption_resolution,[],[f2927,f248]) ).
fof(f2930,plain,
( ~ spl24_13
| ~ spl24_80 ),
inference(avatar_contradiction_clause,[],[f2929]) ).
cnf(s8,plain,
( ~ spl24_12
| spl24_13 ),
inference(sat_conversion,[],[f471]) ).
cnf(s9,plain,
( spl24_11
| ~ spl24_14 ),
inference(sat_conversion,[],[f510]) ).
cnf(s11,plain,
spl24_14,
inference(sat_conversion,[],[f519]) ).
cnf(s16,plain,
( spl24_12
| ~ spl24_14 ),
inference(sat_conversion,[],[f582]) ).
cnf(s22,plain,
( ~ spl24_11
| ~ spl24_24
| spl24_25 ),
inference(sat_conversion,[],[f851]) ).
cnf(s23,plain,
( ~ spl24_21
| spl24_24 ),
inference(sat_conversion,[],[f853]) ).
cnf(s24,plain,
spl24_21,
inference(sat_conversion,[],[f858]) ).
cnf(s26,plain,
( ~ spl24_11
| ~ spl24_21
| ~ spl24_26
| spl24_27 ),
inference(sat_conversion,[],[f900]) ).
cnf(s27,plain,
( ~ spl24_21
| spl24_26 ),
inference(sat_conversion,[],[f903]) ).
cnf(s33,plain,
spl24_30,
inference(sat_conversion,[],[f977]) ).
cnf(s36,plain,
( ~ spl24_26
| ~ spl24_30
| spl24_39
| spl24_40 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s37,plain,
( ~ spl24_21
| ~ spl24_39 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s40,plain,
( ~ spl24_21
| ~ spl24_40
| spl24_42
| ~ spl24_44 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s42,plain,
( ~ spl24_27
| ~ spl24_42 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s69,plain,
( ~ spl24_21
| spl24_65
| spl24_66 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s74,plain,
( ~ spl24_24
| ~ spl24_28
| ~ spl24_30
| spl24_67
| spl24_68 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s82,plain,
( ~ spl24_24
| spl24_28
| ~ spl24_65 ),
inference(sat_conversion,[],[f1701]) ).
cnf(s83,plain,
( ~ spl24_24
| spl24_28
| ~ spl24_66 ),
inference(sat_conversion,[],[f1713]) ).
cnf(s94,plain,
( ~ spl24_21
| ~ spl24_67
| spl24_80
| spl24_81 ),
inference(sat_conversion,[],[f1861]) ).
cnf(s96,plain,
( ~ spl24_13
| ~ spl24_81 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s148,plain,
( ~ spl24_21
| spl24_44
| ~ spl24_68
| spl24_112 ),
inference(sat_conversion,[],[f2740]) ).
cnf(s150,plain,
( ~ spl24_25
| ~ spl24_112 ),
inference(sat_conversion,[],[f2799]) ).
cnf(s155,plain,
( ~ spl24_13
| ~ spl24_80 ),
inference(sat_conversion,[],[f2930]) ).
cnf(s159,plain,
~ spl24_39,
inference(rat,[],[s37,s24]) ).
cnf(s160,plain,
spl24_26,
inference(rat,[],[s27,s24]) ).
cnf(s162,plain,
spl24_40,
inference(rat,[],[s36,s159,s33,s160]) ).
cnf(s165,plain,
spl24_24,
inference(rat,[],[s23,s24]) ).
cnf(s166,plain,
( ~ spl24_11
| spl24_25 ),
inference(rat,[],[s22,s165]) ).
cnf(s168,plain,
spl24_12,
inference(rat,[],[s16,s11]) ).
cnf(s171,plain,
spl24_11,
inference(rat,[],[s9,s11]) ).
cnf(s172,plain,
spl24_27,
inference(rat,[],[s26,s24,s160,s171]) ).
cnf(s173,plain,
spl24_25,
inference(rat,[],[s166,s171]) ).
cnf(s177,plain,
~ spl24_42,
inference(rat,[],[s42,s172]) ).
cnf(s178,plain,
~ spl24_112,
inference(rat,[],[s150,s173]) ).
cnf(s183,plain,
~ spl24_44,
inference(rat,[],[s40,s162,s24,s177]) ).
cnf(s188,plain,
~ spl24_68,
inference(rat,[],[s148,s178,s24,s183]) ).
cnf(s191,plain,
spl24_13,
inference(rat,[],[s8,s168]) ).
cnf(s192,plain,
~ spl24_80,
inference(rat,[],[s155,s191]) ).
cnf(s193,plain,
~ spl24_81,
inference(rat,[],[s96,s191]) ).
cnf(s194,plain,
~ spl24_67,
inference(rat,[],[s94,s193,s24,s192]) ).
cnf(s195,plain,
~ spl24_28,
inference(rat,[],[s74,s188,s165,s33,s194]) ).
cnf(s196,plain,
~ spl24_66,
inference(rat,[],[s83,s165,s195]) ).
cnf(s197,plain,
~ spl24_65,
inference(rat,[],[s82,s165,s195]) ).
cnf(s200,plain,
$false,
inference(rat,[],[s69,s24,s196,s197]) ).
fof(f2931,plain,
$false,
inference(avatar_sat_refutation,[],[s200]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : PRO001+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.43 % Computer : n001.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Sun Sep 27 22:21:46 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 Running first-order theorem proving
% 0.22/0.49 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
% 14.04/3.32 % (4021503)Detected formulas, will run a generic FOF schedule.
% 14.04/3.32 % (4021513)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3910456553:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.04/3.32 % (4021510)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=1815525106:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.04/3.32 % (4021508)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=3338959750:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.04/3.32 % (4021511)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1370493757:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.04/3.32 % (4021509)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=4036436669:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.04/3.32 % (4021514)dis-21_1_sil=8000:lcm=predicate:random_seed=3862813750: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)
% 14.04/3.32 % (4021511)Refutation not found, incomplete strategy
% 14.04/3.32 % (4021511)------------------------------
% 14.04/3.32 % (4021511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021511)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021511)Termination reason: Refutation not found, incomplete strategy
% 14.04/3.32 % (4021511)Time elapsed: 0.002 s
% 14.04/3.32 % (4021511)Peak memory usage: 88 MB
% 14.04/3.32 % (4021511)Instructions burned: 1 (million)
% 14.04/3.32 % (4021513)Instruction limit reached!
% 14.04/3.32 % (4021513)------------------------------
% 14.04/3.32 % (4021513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021513)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021513)Termination reason: Instruction limit
% 14.04/3.32 % (4021513)Termination phase: Saturation
% 14.04/3.32 % (4021513)Time elapsed: 0.075 s
% 14.04/3.32 % (4021513)Peak memory usage: 89 MB
% 14.04/3.32 % (4021513)Instructions burned: 141 (million)
% 14.04/3.32 % (4021512)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=811025226:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.04/3.32 % (4021512)Refutation not found, incomplete strategy
% 14.04/3.32 % (4021512)------------------------------
% 14.04/3.32 % (4021512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021512)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021512)Termination reason: Refutation not found, incomplete strategy
% 14.04/3.32 % (4021512)Time elapsed: 0.003 s
% 14.04/3.32 % (4021512)Peak memory usage: 88 MB
% 14.04/3.32 % (4021512)Instructions burned: 1 (million)
% 14.04/3.32 % (4021514)Instruction limit reached!
% 14.04/3.32 % (4021514)------------------------------
% 14.04/3.32 % (4021514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021514)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021514)Termination reason: Instruction limit
% 14.04/3.32 % (4021514)Termination phase: Saturation
% 14.04/3.32 % (4021514)Time elapsed: 0.132 s
% 14.04/3.32 % (4021514)Peak memory usage: 89 MB
% 14.04/3.32 % (4021514)Instructions burned: 129 (million)
% 14.04/3.32 % (4021523)lrs+10_1_sil=8000:sp=occurrence:random_seed=4283781660:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 14.04/3.32 % (4021511)------------------------------
% 14.04/3.32 % (4021511)------------------------------
% 14.04/3.32 % (4021523)Instruction limit reached!
% 14.04/3.32 % (4021523)------------------------------
% 14.04/3.32 % (4021523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021523)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021523)Termination reason: Instruction limit
% 14.04/3.32 % (4021523)Termination phase: Saturation
% 14.04/3.32 % (4021523)Time elapsed: 0.143 s
% 14.04/3.32 % (4021523)Peak memory usage: 91 MB
% 14.04/3.32 % (4021523)Instructions burned: 286 (million)
% 14.04/3.32 % (4021525)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1386599103:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 14.04/3.32 % (4021525)Refutation not found, incomplete strategy
% 14.04/3.32 % (4021525)------------------------------
% 14.04/3.32 % (4021525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021525)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021525)Termination reason: Refutation not found, incomplete strategy
% 14.04/3.32 % (4021525)Time elapsed: 0.003 s
% 14.04/3.32 % (4021525)Peak memory usage: 88 MB
% 14.04/3.32 % (4021525)Instructions burned: 1 (million)
% 14.04/3.32 % (4021512)------------------------------
% 14.04/3.32 % (4021512)------------------------------
% 14.04/3.32 % (4021528)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=2895110043:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 14.04/3.32 % (4021527)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1556853912:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 14.04/3.32 % (4021528)Instruction limit reached!
% 14.04/3.32 % (4021528)------------------------------
% 14.04/3.32 % (4021528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021528)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021528)Termination reason: Instruction limit
% 14.04/3.32 % (4021528)Termination phase: Saturation
% 14.04/3.32 % (4021528)Time elapsed: 0.117 s
% 14.04/3.32 % (4021528)Peak memory usage: 90 MB
% 14.04/3.32 % (4021528)Instructions burned: 249 (million)
% 14.04/3.32 % (4021530)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3939454394:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 14.04/3.32 % (4021530)Refutation not found, incomplete strategy
% 14.04/3.32 % (4021530)------------------------------
% 14.04/3.32 % (4021530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021530)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021530)Termination reason: Refutation not found, incomplete strategy
% 14.04/3.32 % (4021530)Time elapsed: 0.008 s
% 14.04/3.32 % (4021530)Peak memory usage: 88 MB
% 14.04/3.32 % (4021530)Instructions burned: 5 (million)
% 14.04/3.32 % (4021525)------------------------------
% 14.04/3.32 % (4021525)------------------------------
% 14.04/3.32 % (4021533)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3324708531:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 14.04/3.32 % (4021527)Instruction limit reached!
% 14.04/3.32 % (4021527)------------------------------
% 14.04/3.32 % (4021527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.32 % (4021527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.32 % (4021527)CaDiCaL version: 2.1.3
% 14.04/3.32 % (4021527)Termination reason: Instruction limit
% 14.04/3.32 % (4021527)Termination phase: Saturation
% 14.04/3.32 % (4021527)Time elapsed: 0.365 s
% 14.04/3.32 % (4021527)Peak memory usage: 92 MB
% 14.04/3.32 % (4021527)Instructions burned: 325 (million)
% 14.04/3.33 % (4021535)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1347569346:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 14.04/3.33 % (4021530)------------------------------
% 14.04/3.33 % (4021530)------------------------------
% 14.04/3.33 % (4021535)Instruction limit reached!
% 14.04/3.33 % (4021535)------------------------------
% 14.04/3.33 % (4021535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.33 % (4021535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.33 % (4021535)CaDiCaL version: 2.1.3
% 14.04/3.33 % (4021535)Termination reason: Instruction limit
% 14.04/3.33 % (4021535)Termination phase: Saturation
% 14.04/3.33 % (4021535)Time elapsed: 0.140 s
% 14.04/3.33 % (4021535)Peak memory usage: 90 MB
% 14.04/3.33 % (4021535)Instructions burned: 113 (million)
% 14.04/3.33 % (4021537)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2603163832:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 14.04/3.33 % (4021539)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4288100148:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 14.04/3.33 % (4021537)Instruction limit reached!
% 14.04/3.33 % (4021537)------------------------------
% 14.04/3.33 % (4021537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.33 % (4021537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.33 % (4021537)CaDiCaL version: 2.1.3
% 14.04/3.33 % (4021537)Termination reason: Instruction limit
% 14.04/3.33 % (4021537)Termination phase: Saturation
% 14.04/3.33 % (4021537)Time elapsed: 0.120 s
% 14.04/3.33 % (4021537)Peak memory usage: 89 MB
% 14.04/3.33 % (4021537)Instructions burned: 128 (million)
% 14.04/3.33 % (4021540)lrs+10_1_sil=8000:sp=occurrence:random_seed=2115156147:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 14.04/3.33 % (4021539)Instruction limit reached!
% 14.04/3.33 % (4021539)------------------------------
% 14.04/3.33 % (4021539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.33 % (4021539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.33 % (4021539)CaDiCaL version: 2.1.3
% 14.04/3.33 % (4021539)Termination reason: Instruction limit
% 14.04/3.33 % (4021539)Termination phase: Saturation
% 14.04/3.33 % (4021539)Time elapsed: 0.072 s
% 14.04/3.33 % (4021539)Peak memory usage: 88 MB
% 14.04/3.33 % (4021539)Instructions burned: 115 (million)
% 14.04/3.33 % (4021508)First to succeed.
% 14.04/3.33 % (4021508)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4021503"
% 14.04/3.33 % (4021543)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1090988976:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 14.04/3.33 % (4021543)Refutation not found, incomplete strategy
% 14.04/3.33 % (4021543)------------------------------
% 14.04/3.33 % (4021543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.04/3.33 % (4021543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.04/3.33 % (4021543)CaDiCaL version: 2.1.3
% 14.04/3.33 % (4021543)Termination reason: Refutation not found, incomplete strategy
% 14.04/3.33 % (4021543)Time elapsed: 0.009 s
% 14.04/3.33 % (4021543)Peak memory usage: 88 MB
% 14.04/3.33 % (4021543)Instructions burned: 6 (million)
% 14.04/3.33 % (4021533)Also succeeded, but the first one will report.
% 14.04/3.33 % (4021545)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3836725492:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 14.04/3.33 % (4021508)Refutation found. Thanks to Tanya!
% 14.04/3.33 % SZS status Theorem for theBenchmark
% 14.04/3.33 % SZS output start Proof for theBenchmark
% See solution above
% 16.50/3.44 % (4021508)------------------------------
% 16.50/3.44 % (4021508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.50/3.44 % (4021508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.50/3.44 % (4021508)CaDiCaL version: 2.1.3
% 16.50/3.44 % (4021508)Termination reason: Refutation
% 16.50/3.44 % (4021508)Time elapsed: 1.583 s
% 16.50/3.44 % (4021508)Peak memory usage: 132 MB
% 16.50/3.44 % (4021508)Instructions burned: 1390 (million)
% 16.50/3.44 % (4021508)------------------------------
% 16.50/3.44 % (4021508)------------------------------
% 16.50/3.44 % (4021503)Success in time 2.218 s
% 16.50/3.44 % Vampire exiting
%------------------------------------------------------------------------------