%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO001+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 12.49s 2.66s
% Output : Refutation 13.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 40
% Syntax : Number of formulae : 333 ( 37 unt; 18 def)
% Number of atoms : 1037 ( 104 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1248 ( 544 ~; 567 |; 93 &)
% ( 23 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 19 prp; 0-5 aty)
% Number of functors : 19 ( 19 usr; 7 con; 0-5 aty)
% Number of variables : 490 ( 0 sgn 446 !; 44 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,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/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(f4,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
fof(f5,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/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f7,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/sandbox/benchmark/theBenchmark.p',sos_06) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& root_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(f12,axiom,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
=> ( activity_occurrence(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
fof(f13,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_12) ).
fof(f14,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(f17,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_16) ).
fof(f18,axiom,
! [X0,X1] :
( root(X0,X1)
=> legal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_17) ).
fof(f20,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_19) ).
fof(f23,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f27,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/sandbox/benchmark/theBenchmark.p',sos_26) ).
fof(f33,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/sandbox/benchmark/theBenchmark.p',sos_32) ).
fof(f36,axiom,
atomic(tptp4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(f47,axiom,
! [X0,X1,X2,X3,X4] :
( send_message(X0,X1,X2,X3,X4)
=> ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_46) ).
fof(f48,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/sandbox/benchmark/theBenchmark.p',sos_47) ).
fof(f52,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/sandbox/benchmark/theBenchmark.p',sos_51) ).
fof(f53,axiom,
! [X0,X1,X2] :
( tptp1(X0,X1,X2)
=> ( activity(X0)
& ~ atomic(X0)
& ~ atomic(X1)
& root(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_52) ).
fof(f54,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/sandbox/benchmark/theBenchmark.p',sos_53) ).
fof(f56,conjecture,
~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f57,negated_conjecture,
~ ~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(negated_conjecture,[status(cth)],[f56]) ).
fof(f58,plain,
? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(flattening,[],[f57]) ).
fof(f62,plain,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] : occurrence_of(X0,X1) ),
inference(pure_predicate_removal,[],[f13]) ).
fof(f63,plain,
! [X0,X1,X2] :
( tptp1(X0,X1,X2)
=> ( ~ atomic(X0)
& ~ atomic(X1)
& root(X2,X1) ) ),
inference(pure_predicate_removal,[],[f53]) ).
fof(f64,plain,
! [X0,X1] :
( occurrence_of(X1,X0)
=> activity_occurrence(X1) ),
inference(pure_predicate_removal,[],[f4]) ).
fof(f72,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,[],[f3]) ).
fof(f73,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,[],[f72]) ).
fof(f74,plain,
! [X0,X1] :
( activity_occurrence(X1)
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f75,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,[],[f5]) ).
fof(f76,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,[],[f75]) ).
fof(f78,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,[],[f7]) ).
fof(f81,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f82,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f81]) ).
fof(f85,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f88,plain,
! [X0] :
( ? [X1] : occurrence_of(X0,X1)
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f89,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f92,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f93,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f95,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f99,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,[],[f27]) ).
fof(f110,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,[],[f33]) ).
fof(f112,plain,
! [X0,X1,X2,X3,X4] :
( ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 )
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f47]) ).
fof(f113,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,[],[f48]) ).
fof(f114,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,[],[f113]) ).
fof(f117,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,[],[f52]) ).
fof(f118,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,[],[f117]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ( ~ atomic(X0)
& ~ atomic(X1)
& root(X2,X1) )
| ~ tptp1(X0,X1,X2) ),
inference(ennf_transformation,[],[f63]) ).
fof(f120,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,[],[f54]) ).
fof(f121,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,[],[f120]) ).
fof(f124,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK2(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK2(X0,X1,X2))
& subactivity_occurrence(X2,sK2(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1,X2))],[f78]) ).
fof(f126,plain,
! [X0] :
( occurrence_of(X0,sK4(X0))
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f88]) ).
fof(f132,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f92]) ).
fof(f136,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,[],[f20]) ).
fof(f137,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,[],[f136]) ).
fof(f138,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK9(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK9(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1))],[f137]) ).
fof(f142,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,[],[f99]) ).
fof(f143,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,[],[f142]) ).
fof(f144,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,[],[f143]) ).
fof(f145,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK11(X0,X1,X2),X2)
& min_precedes(sK11(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,[sK11]),skolemize(X3,sK11(X0,X1,X2))],[f144]) ).
fof(f146,plain,
! [X0] :
( ( occurrence_of(sK12(X0),tptp4)
& root_occ(sK12(X0),X0)
& ( occurrence_of(sK13(X0),tptp3)
| occurrence_of(sK13(X0),tptp2) )
& leaf_occ(sK13(X0),X0)
& next_subocc(sK12(X0),sK13(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0))],[f110]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( send_message(sK14(X1,X2,X3,X4,X5),X1,X2,X3,X4)
& occurrence_of(sK15(X1,X2,X3,X4,X5),sK14(X1,X2,X3,X4,X5))
& root_occ(sK15(X1,X2,X3,X4,X5),X5) )
| ~ transmit_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15]),skolemize(X6,sK14(X1,X2,X3,X4,X5)),skolemize(X7,sK15(X1,X2,X3,X4,X5))],[f118]) ).
fof(f148,plain,
! [X0,X1,X2,X3] :
( ( transmit_message(sK16(X1,X2,X3),sK17(X1,X2,X3),sK18(X1,X2,X3),X2,X1)
& occurrence_of(sK19(X1,X2,X3),sK16(X1,X2,X3))
& subactivity_occurrence(sK19(X1,X2,X3),X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17,sK18,sK19]),skolemize(X4,sK16(X1,X2,X3)),skolemize(X5,sK17(X1,X2,X3)),skolemize(X6,sK18(X1,X2,X3)),skolemize(X7,sK19(X1,X2,X3))],[f121]) ).
fof(f149,plain,
( tptp1(sK20,tptp0,sK21)
& occurrence_of(sK22,sK20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22]),skolemize(X0,sK20),skolemize(X1,sK21),skolemize(X2,sK22)],[f58]) ).
fof(f153,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,[],[f73]) ).
fof(f154,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f155,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,[],[f76]) ).
fof(f157,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f158,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f159,plain,
! [X2,X0,X1] :
( occurrence_of(sK2(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f162,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f82]) ).
fof(f164,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f166,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f167,plain,
! [X0] :
( occurrence_of(X0,sK4(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f168,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f89]) ).
fof(f176,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f177,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f182,plain,
! [X0,X1] :
( root(X0,sK9(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
fof(f183,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
fof(f184,plain,
! [X0,X1] :
( occurrence_of(X1,sK9(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
fof(f190,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f196,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f145]) ).
fof(f197,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(cnf_transformation,[],[f145]) ).
fof(f205,plain,
! [X0] :
( next_subocc(sK12(X0),sK13(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f206,plain,
! [X0] :
( leaf_occ(sK13(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f207,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp2)
| occurrence_of(sK13(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f208,plain,
! [X0] :
( root_occ(sK12(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f209,plain,
! [X0] :
( occurrence_of(sK12(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f211,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f36]) ).
fof(f224,plain,
! [X2,X3,X0,X1,X4] :
( tptp2 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f112]) ).
fof(f225,plain,
! [X2,X3,X0,X1,X4] :
( tptp3 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f112]) ).
fof(f227,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,[],[f114]) ).
fof(f233,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| root_occ(sK15(X1,X2,X3,X4,X5),X5)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f234,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| occurrence_of(sK15(X1,X2,X3,X4,X5),sK14(X1,X2,X3,X4,X5))
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f235,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| send_message(sK14(X1,X2,X3,X4,X5),X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ~ tptp1(X0,X1,X2)
| root(X2,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f240,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| occurrence_of(sK19(X1,X2,X3),sK16(X1,X2,X3))
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f241,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| transmit_message(sK16(X1,X2,X3),sK17(X1,X2,X3),sK18(X1,X2,X3),X2,X1)
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f243,plain,
occurrence_of(sK22,sK20),
inference(cnf_transformation,[],[f149]) ).
fof(f244,plain,
tptp1(sK20,tptp0,sK21),
inference(cnf_transformation,[],[f149]) ).
fof(f246,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp3,X1,X2,X3,X4),
inference(equality_resolution,[],[f225]) ).
fof(f247,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp2,X1,X2,X3,X4),
inference(equality_resolution,[],[f224]) ).
fof(f249,plain,
! [X0] :
( transmit_message(sK16(tptp0,sK21,X0),sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0)
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f241,f244]) ).
fof(f250,plain,
! [X0] :
( occurrence_of(sK19(tptp0,sK21,X0),sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f240,f244]) ).
fof(f251,plain,
! [X0,X1] :
( ~ occurrence_of(sK19(tptp0,sK21,X0),X1)
| ~ occurrence_of(X0,sK20)
| sK16(tptp0,sK21,X0) = X1 ),
inference(resolution,[],[f250,f162]) ).
fof(f256,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X2,X0,X1),X3)
| ~ min_precedes(X0,X1,X2)
| X2 = X3 ),
inference(resolution,[],[f159,f162]) ).
fof(f257,plain,
root(sK21,tptp0),
inference(resolution,[],[f236,f244]) ).
fof(f263,plain,
! [X0,X1] :
( occurrence_of(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1),sK14(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1))
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f234,f249]) ).
fof(f265,plain,
! [X0,X1] :
( send_message(sK14(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1),sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0)
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f235,f249]) ).
fof(f266,plain,
! [X0] :
( min_precedes(sK12(X0),sK13(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f205,f197]) ).
fof(f269,plain,
! [X0] :
( ~ root(sK13(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f190,f266]) ).
fof(f271,plain,
! [X0] :
( activity_occurrence(sK19(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f154,f250]) ).
fof(f272,plain,
! [X2,X0,X1] :
( activity_occurrence(sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(resolution,[],[f154,f159]) ).
fof(f273,plain,
! [X0,X1] :
( root_occ(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1),X1)
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f233,f249]) ).
fof(f274,plain,
! [X0,X1] :
( ~ min_precedes(sK12(X1),X0,tptp0)
| ~ min_precedes(X0,sK13(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f196,f205]) ).
fof(f278,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp3)
| ~ occurrence_of(X0,tptp0)
| activity_occurrence(sK13(X0)) ),
inference(resolution,[],[f207,f154]) ).
fof(f280,plain,
! [X0,X1] :
( ~ occurrence_of(sK13(X0),X1)
| ~ occurrence_of(X0,tptp0)
| occurrence_of(sK13(X0),tptp3)
| tptp2 = X1 ),
inference(resolution,[],[f207,f162]) ).
fof(f282,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| activity_occurrence(sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f278,f154]) ).
fof(f284,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK12(X0)) ),
inference(resolution,[],[f209,f176]) ).
fof(f286,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK12(X0)) ),
inference(forward_subsumption_resolution,[],[f284,f211]) ).
fof(f288,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK16(tptp0,sK21,X1))
| ~ occurrence_of(X1,sK20)
| activity_occurrence(sK15(sK17(tptp0,sK21,X1),sK18(tptp0,sK21,X1),sK21,tptp0,X0)) ),
inference(resolution,[],[f263,f154]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK15(sK17(tptp0,sK21,X1),sK18(tptp0,sK21,X1),sK21,tptp0,X0),X2)
| ~ occurrence_of(X1,sK20)
| ~ occurrence_of(X0,sK16(tptp0,sK21,X1))
| sK14(sK17(tptp0,sK21,X1),sK18(tptp0,sK21,X1),sK21,tptp0,X0) = X2 ),
inference(resolution,[],[f263,f162]) ).
fof(f302,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,sK14(sK17(tptp0,sK21,X1),sK18(tptp0,sK21,X1),sK21,tptp0,X2))
| min_precedes(sK21,X0,tptp0)
| ~ occurrence_of(X2,sK16(tptp0,sK21,X1))
| ~ occurrence_of(X1,sK20) ),
inference(resolution,[],[f227,f265]) ).
fof(f312,plain,
! [X2,X0,X1] :
( min_precedes(X2,sK13(X0),X1)
| ~ subactivity_occurrence(X2,X0)
| sK13(X0) = X2
| ~ arboreal(X2)
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f153,f206]) ).
fof(f334,plain,
! [X0] :
( subactivity_occurrence(sK12(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f183,f208]) ).
fof(f337,plain,
! [X0,X1] :
( min_precedes(sK21,sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1),tptp0)
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20)
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f302,f263]) ).
fof(f338,plain,
! [X0,X1] :
( min_precedes(sK21,sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1),tptp0)
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(duplicate_literal_removal,[],[f337]) ).
fof(f340,plain,
! [X0,X1] :
( ~ root(sK15(sK17(tptp0,sK21,X1),sK18(tptp0,sK21,X1),sK21,tptp0,X0),tptp0)
| ~ occurrence_of(X1,sK20)
| ~ occurrence_of(X0,sK16(tptp0,sK21,X1)) ),
inference(resolution,[],[f338,f190]) ).
fof(f370,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X1,sK2(X3,X4,X0))
| X0 = X1
| ~ occurrence_of(sK2(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,[],[f155,f157]) ).
fof(f371,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X1,sK2(X3,X0,X4))
| X0 = X1
| ~ occurrence_of(sK2(X3,X0,X4),X2)
| ~ arboreal(X1)
| ~ arboreal(X0)
| min_precedes(X0,X1,X2)
| min_precedes(X1,X0,X2)
| ~ min_precedes(X0,X4,X3) ),
inference(resolution,[],[f155,f158]) ).
fof(f396,plain,
! [X2,X3,X0,X1] :
( sK12(sK2(X1,X2,X0)) = X0
| ~ occurrence_of(sK2(X1,X2,X0),X3)
| ~ arboreal(sK12(sK2(X1,X2,X0)))
| ~ arboreal(X0)
| min_precedes(X0,sK12(sK2(X1,X2,X0)),X3)
| min_precedes(sK12(sK2(X1,X2,X0)),X0,X3)
| ~ min_precedes(X2,X0,X1)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0) ),
inference(resolution,[],[f370,f334]) ).
fof(f402,plain,
! [X2,X3,X0,X1] :
( min_precedes(sK12(sK2(X1,X2,X0)),X0,X3)
| ~ occurrence_of(sK2(X1,X2,X0),X3)
| ~ arboreal(X0)
| min_precedes(X0,sK12(sK2(X1,X2,X0)),X3)
| sK12(sK2(X1,X2,X0)) = X0
| ~ min_precedes(X2,X0,X1)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0) ),
inference(forward_subsumption_resolution,[],[f396,f286]) ).
fof(f425,plain,
! [X0,X1] :
( ~ activity_occurrence(X0)
| ~ occurrence_of(X0,X1)
| sK4(X0) = X1 ),
inference(resolution,[],[f167,f162]) ).
fof(f426,plain,
! [X2,X0,X1] :
( ~ activity_occurrence(sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0)
| sK4(sK2(X0,X1,X2)) = X0 ),
inference(resolution,[],[f167,f256]) ).
fof(f428,plain,
! [X0] :
( ~ activity_occurrence(sK13(X0))
| ~ occurrence_of(X0,tptp0)
| occurrence_of(sK13(X0),tptp3)
| tptp2 = sK4(sK13(X0)) ),
inference(resolution,[],[f167,f280]) ).
fof(f429,plain,
! [X0,X1] :
( ~ activity_occurrence(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1))
| ~ occurrence_of(X0,sK20)
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| sK14(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1) = sK4(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1)) ),
inference(resolution,[],[f167,f290]) ).
fof(f430,plain,
! [X0] :
( ~ activity_occurrence(sK19(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20)
| sK16(tptp0,sK21,X0) = sK4(sK19(tptp0,sK21,X0)) ),
inference(resolution,[],[f167,f251]) ).
fof(f433,plain,
! [X0] :
( ~ occurrence_of(X0,sK20)
| sK16(tptp0,sK21,X0) = sK4(sK19(tptp0,sK21,X0)) ),
inference(forward_subsumption_resolution,[],[f430,f271]) ).
fof(f434,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20)
| sK14(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1) = sK4(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1)) ),
inference(forward_subsumption_resolution,[],[f429,f288]) ).
fof(f435,plain,
! [X0] :
( occurrence_of(sK13(X0),tptp3)
| ~ occurrence_of(X0,tptp0)
| tptp2 = sK4(sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f428,f282]) ).
fof(f437,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| sK4(sK2(X0,X1,X2)) = X0 ),
inference(forward_subsumption_resolution,[],[f426,f272]) ).
fof(f438,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK4(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f425,f154]) ).
fof(f439,plain,
! [X0,X1] :
( ~ root_occ(X1,X0)
| sK4(X0) = sK9(X1,X0) ),
inference(resolution,[],[f438,f184]) ).
fof(f449,plain,
sK16(tptp0,sK21,sK22) = sK4(sK19(tptp0,sK21,sK22)),
inference(resolution,[],[f433,f243]) ).
fof(f456,definition,
( spl23_5
<=> occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22)) ),
introduced(definition,[new_symbols(definition,[spl23_5])],[avatar_definition]) ).
fof(f458,plain,
( occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ spl23_5 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f464,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| sK4(X0) = sK9(sK12(X0),X0) ),
inference(resolution,[],[f439,f208]) ).
fof(f465,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK16(tptp0,sK21,X1))
| sK4(X0) = sK9(sK15(sK17(tptp0,sK21,X1),sK18(tptp0,sK21,X1),sK21,tptp0,X0),X0)
| ~ occurrence_of(X1,sK20) ),
inference(resolution,[],[f439,f273]) ).
fof(f471,plain,
! [X0] :
( sK4(sK19(tptp0,sK21,X0)) = sK9(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,sK19(tptp0,sK21,X0)),sK19(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20)
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f465,f250]) ).
fof(f472,plain,
! [X0] :
( ~ occurrence_of(X0,sK20)
| sK4(sK19(tptp0,sK21,X0)) = sK9(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,sK19(tptp0,sK21,X0)),sK19(tptp0,sK21,X0)) ),
inference(duplicate_literal_removal,[],[f471]) ).
fof(f474,plain,
sK4(sK19(tptp0,sK21,sK22)) = sK9(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK19(tptp0,sK21,sK22)),
inference(resolution,[],[f472,f243]) ).
fof(f475,plain,
sK16(tptp0,sK21,sK22) = sK9(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK19(tptp0,sK21,sK22)),
inference(forward_demodulation,[],[f474,f449]) ).
fof(f477,plain,
( occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ root_occ(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK19(tptp0,sK21,sK22)) ),
inference(superposition,[],[f184,f475]) ).
fof(f479,definition,
( spl23_6
<=> root_occ(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK19(tptp0,sK21,sK22)) ),
introduced(definition,[new_symbols(definition,[spl23_6])],[avatar_definition]) ).
fof(f480,plain,
( root_occ(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK19(tptp0,sK21,sK22))
| ~ spl23_6 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f481,plain,
( ~ root_occ(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK19(tptp0,sK21,sK22))
| spl23_6 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,plain,
( ~ spl23_6
| spl23_5 ),
inference(avatar_split_clause,[],[f477,f456,f479]) ).
fof(f488,plain,
( ~ occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ occurrence_of(sK22,sK20)
| spl23_6 ),
inference(resolution,[],[f481,f273]) ).
fof(f489,plain,
( ~ occurrence_of(sK22,sK20)
| spl23_6 ),
inference(forward_subsumption_resolution,[],[f488,f250]) ).
fof(f490,plain,
( $false
| spl23_6 ),
inference(forward_subsumption_resolution,[],[f489,f243]) ).
fof(f491,plain,
spl23_6,
inference(avatar_contradiction_clause,[],[f490]) ).
fof(f516,plain,
( subactivity_occurrence(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK19(tptp0,sK21,sK22))
| ~ spl23_6 ),
inference(resolution,[],[f480,f183]) ).
fof(f550,plain,
! [X0,X1] :
( arboreal(sK12(sK2(tptp0,X0,X1)))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f286,f159]) ).
fof(f556,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| tptp0 = sK4(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1)))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f437,f338]) ).
fof(f577,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| legal(X0) ),
inference(resolution,[],[f177,f182]) ).
fof(f580,plain,
legal(sK21),
inference(resolution,[],[f177,f257]) ).
fof(f581,plain,
arboreal(sK21),
inference(resolution,[],[f580,f168]) ).
fof(f585,plain,
( ~ occurrence_of(sK22,sK20)
| sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK4(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ spl23_5 ),
inference(resolution,[],[f434,f458]) ).
fof(f587,plain,
( sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK4(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ spl23_5 ),
inference(forward_subsumption_resolution,[],[f585,f243]) ).
fof(f588,plain,
( occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ activity_occurrence(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ spl23_5 ),
inference(superposition,[],[f167,f587]) ).
fof(f590,definition,
( spl23_16
<=> activity_occurrence(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))) ),
introduced(definition,[new_symbols(definition,[spl23_16])],[avatar_definition]) ).
fof(f592,plain,
( ~ activity_occurrence(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| spl23_16 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f594,definition,
( spl23_17
<=> occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))) ),
introduced(definition,[new_symbols(definition,[spl23_17])],[avatar_definition]) ).
fof(f596,plain,
( occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ spl23_17 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f597,plain,
( ~ spl23_16
| spl23_17
| ~ spl23_5 ),
inference(avatar_split_clause,[],[f588,f456,f594,f590]) ).
fof(f605,plain,
( activity_occurrence(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ spl23_6 ),
inference(resolution,[],[f166,f516]) ).
fof(f607,plain,
( $false
| ~ spl23_6
| spl23_16 ),
inference(forward_subsumption_resolution,[],[f605,f592]) ).
fof(f608,plain,
( ~ spl23_6
| spl23_16 ),
inference(avatar_contradiction_clause,[],[f607]) ).
fof(f615,plain,
( ! [X0] :
( ~ occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),X0)
| sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = X0 )
| ~ spl23_17 ),
inference(resolution,[],[f596,f162]) ).
fof(f891,plain,
( tptp0 = sK4(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ occurrence_of(sK22,sK20)
| ~ spl23_5 ),
inference(resolution,[],[f556,f458]) ).
fof(f893,plain,
( tptp0 = sK4(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_5 ),
inference(forward_subsumption_resolution,[],[f891,f243]) ).
fof(f894,plain,
( occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| ~ activity_occurrence(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_5 ),
inference(superposition,[],[f167,f893]) ).
fof(f896,definition,
( spl23_21
<=> activity_occurrence(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))) ),
introduced(definition,[new_symbols(definition,[spl23_21])],[avatar_definition]) ).
fof(f898,plain,
( ~ activity_occurrence(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| spl23_21 ),
inference(avatar_component_clause,[],[f896]) ).
fof(f900,definition,
( spl23_22
<=> occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_22])],[avatar_definition]) ).
fof(f902,plain,
( occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| ~ spl23_22 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f903,plain,
( ~ spl23_21
| spl23_22
| ~ spl23_5 ),
inference(avatar_split_clause,[],[f894,f456,f900,f896]) ).
fof(f906,plain,
( ~ min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0)
| spl23_21 ),
inference(resolution,[],[f898,f272]) ).
fof(f907,plain,
( ~ occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ occurrence_of(sK22,sK20)
| spl23_21 ),
inference(resolution,[],[f906,f338]) ).
fof(f908,plain,
( ~ occurrence_of(sK22,sK20)
| spl23_21 ),
inference(forward_subsumption_resolution,[],[f907,f250]) ).
fof(f909,plain,
( $false
| spl23_21 ),
inference(forward_subsumption_resolution,[],[f908,f243]) ).
fof(f910,plain,
spl23_21,
inference(avatar_contradiction_clause,[],[f909]) ).
fof(f921,plain,
( sK4(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))) = sK9(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_22 ),
inference(resolution,[],[f902,f464]) ).
fof(f939,plain,
( tptp0 = sK9(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_5
| ~ spl23_22 ),
inference(forward_demodulation,[],[f921,f893]) ).
fof(f946,plain,
( root(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ root_occ(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_5
| ~ spl23_22 ),
inference(superposition,[],[f182,f939]) ).
fof(f949,definition,
( spl23_25
<=> root_occ(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))) ),
introduced(definition,[new_symbols(definition,[spl23_25])],[avatar_definition]) ).
fof(f950,plain,
( root_occ(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_25 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f951,plain,
( ~ root_occ(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| spl23_25 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f953,definition,
( spl23_26
<=> root(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_26])],[avatar_definition]) ).
fof(f955,plain,
( root(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ spl23_26 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f956,plain,
( ~ spl23_25
| spl23_26
| ~ spl23_5
| ~ spl23_22 ),
inference(avatar_split_clause,[],[f946,f900,f456,f953,f949]) ).
fof(f957,plain,
( ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| spl23_25 ),
inference(resolution,[],[f951,f208]) ).
fof(f958,plain,
( $false
| ~ spl23_22
| spl23_25 ),
inference(forward_subsumption_resolution,[],[f957,f902]) ).
fof(f959,plain,
( ~ spl23_22
| spl23_25 ),
inference(avatar_contradiction_clause,[],[f958]) ).
fof(f969,plain,
( subactivity_occurrence(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_25 ),
inference(resolution,[],[f950,f183]) ).
fof(f1039,definition,
( spl23_36
<=> min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_36])],[avatar_definition]) ).
fof(f1040,plain,
( min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0)
| ~ spl23_36 ),
inference(avatar_component_clause,[],[f1039]) ).
fof(f1041,plain,
( ~ min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0)
| spl23_36 ),
inference(avatar_component_clause,[],[f1039]) ).
fof(f1046,definition,
( spl23_38
<=> sK21 = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))) ),
introduced(definition,[new_symbols(definition,[spl23_38])],[avatar_definition]) ).
fof(f1047,plain,
( sK21 != sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| spl23_38 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1048,plain,
( sK21 = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_38 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1050,plain,
( ~ occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ occurrence_of(sK22,sK20)
| spl23_36 ),
inference(resolution,[],[f1041,f338]) ).
fof(f1051,plain,
( ~ occurrence_of(sK22,sK20)
| spl23_36 ),
inference(forward_subsumption_resolution,[],[f1050,f250]) ).
fof(f1052,plain,
( $false
| spl23_36 ),
inference(forward_subsumption_resolution,[],[f1051,f243]) ).
fof(f1053,plain,
spl23_36,
inference(avatar_contradiction_clause,[],[f1052]) ).
fof(f1110,plain,
( ~ root(sK21,tptp0)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| ~ spl23_38 ),
inference(superposition,[],[f269,f1048]) ).
fof(f1145,plain,
( ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| ~ spl23_38 ),
inference(forward_subsumption_resolution,[],[f1110,f257]) ).
fof(f1178,plain,
( $false
| ~ spl23_22
| ~ spl23_38 ),
inference(forward_subsumption_resolution,[],[f1145,f902]) ).
fof(f1179,plain,
( ~ spl23_22
| ~ spl23_38 ),
inference(avatar_contradiction_clause,[],[f1178]) ).
fof(f1202,plain,
( ! [X0] :
( sK21 = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),X0)
| ~ arboreal(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))))
| ~ arboreal(sK21)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),X0)
| min_precedes(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK21,X0)
| ~ min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0) )
| ~ spl23_25 ),
inference(resolution,[],[f969,f371]) ).
fof(f1209,plain,
( ! [X0] :
( sK21 = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),X0)
| ~ arboreal(sK21)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),X0)
| min_precedes(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK21,X0)
| ~ min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0) )
| ~ spl23_25 ),
inference(forward_subsumption_resolution,[],[f1202,f550]) ).
fof(f1210,plain,
( ! [X0] :
( sK21 = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),X0)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),X0)
| min_precedes(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK21,X0)
| ~ min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0) )
| ~ spl23_25 ),
inference(forward_subsumption_resolution,[],[f1209,f581]) ).
fof(f1211,plain,
( ! [X0] :
( sK21 = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),X0)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),X0)
| min_precedes(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK21,X0) )
| ~ spl23_25
| ~ spl23_36 ),
inference(forward_subsumption_resolution,[],[f1210,f1040]) ).
fof(f1213,definition,
( spl23_50
<=> ! [X0] :
( ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),X0)
| min_precedes(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK21,X0)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl23_50])],[avatar_definition]) ).
fof(f1214,plain,
( ! [X0] :
( min_precedes(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),sK21,X0)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),X0)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),X0) )
| ~ spl23_50 ),
inference(avatar_component_clause,[],[f1213]) ).
fof(f1216,definition,
( spl23_51
<=> sK21 = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))) ),
introduced(definition,[new_symbols(definition,[spl23_51])],[avatar_definition]) ).
fof(f1218,plain,
( sK21 = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_51 ),
inference(avatar_component_clause,[],[f1216]) ).
fof(f1219,plain,
( spl23_50
| spl23_51
| ~ spl23_25
| ~ spl23_36 ),
inference(avatar_split_clause,[],[f1211,f1039,f949,f1216,f1213]) ).
fof(f1221,plain,
( ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ min_precedes(sK21,sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| ~ spl23_50 ),
inference(resolution,[],[f1214,f274]) ).
fof(f1236,plain,
( ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ min_precedes(sK21,sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ spl23_50 ),
inference(duplicate_literal_removal,[],[f1221]) ).
fof(f1247,plain,
( min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ min_precedes(sK21,sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ spl23_22
| ~ spl23_50 ),
inference(forward_subsumption_resolution,[],[f1236,f902]) ).
fof(f1250,definition,
( spl23_54
<=> min_precedes(sK21,sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_54])],[avatar_definition]) ).
fof(f1252,plain,
( ~ min_precedes(sK21,sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| spl23_54 ),
inference(avatar_component_clause,[],[f1250]) ).
fof(f1254,definition,
( spl23_55
<=> min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl23_55])],[avatar_definition]) ).
fof(f1256,plain,
( min_precedes(sK21,sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ spl23_55 ),
inference(avatar_component_clause,[],[f1254]) ).
fof(f1303,plain,
( ~ spl23_54
| spl23_55
| ~ spl23_22
| ~ spl23_50 ),
inference(avatar_split_clause,[],[f1247,f1213,f900,f1254,f1250]) ).
fof(f1305,plain,
( ~ subactivity_occurrence(sK21,sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| sK21 = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ arboreal(sK21)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| spl23_54 ),
inference(resolution,[],[f1252,f312]) ).
fof(f1306,plain,
( ~ subactivity_occurrence(sK21,sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| sK21 = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ arboreal(sK21)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| spl23_54 ),
inference(duplicate_literal_removal,[],[f1305]) ).
fof(f1307,plain,
( ~ subactivity_occurrence(sK21,sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ arboreal(sK21)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| spl23_38
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f1306,f1047]) ).
fof(f1308,plain,
( ~ subactivity_occurrence(sK21,sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| spl23_38
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f1307,f581]) ).
fof(f1309,plain,
( ~ subactivity_occurrence(sK21,sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_22
| spl23_38
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f1308,f902]) ).
fof(f1328,plain,
( ~ min_precedes(sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp0)
| ~ spl23_22
| spl23_38
| spl23_54 ),
inference(resolution,[],[f1309,f158]) ).
fof(f1329,plain,
( $false
| ~ spl23_22
| ~ spl23_36
| spl23_38
| spl23_54 ),
inference(forward_subsumption_resolution,[],[f1328,f1040]) ).
fof(f1330,plain,
( ~ spl23_22
| ~ spl23_36
| spl23_38
| spl23_54 ),
inference(avatar_contradiction_clause,[],[f1329]) ).
fof(f1336,plain,
( ~ root(sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))),tptp0)
| ~ spl23_55 ),
inference(resolution,[],[f1256,f190]) ).
fof(f1345,plain,
( $false
| ~ spl23_26
| ~ spl23_55 ),
inference(forward_subsumption_resolution,[],[f1336,f955]) ).
fof(f1346,plain,
( ~ spl23_26
| ~ spl23_55 ),
inference(avatar_contradiction_clause,[],[f1345]) ).
fof(f1446,plain,
! [X0,X1] :
( legal(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1))
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f577,f273]) ).
fof(f1449,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK16(tptp0,sK21,X1))
| ~ occurrence_of(X1,sK20)
| arboreal(sK15(sK17(tptp0,sK21,X1),sK18(tptp0,sK21,X1),sK21,tptp0,X0)) ),
inference(resolution,[],[f1446,f168]) ).
fof(f1876,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK2(X0,X1,X2),tptp0)
| ~ arboreal(X2)
| min_precedes(X2,sK12(sK2(X0,X1,X2)),tptp0)
| sK12(sK2(X0,X1,X2)) = X2
| ~ min_precedes(X1,X2,X0)
| ~ occurrence_of(sK2(X0,X1,X2),tptp0)
| ~ min_precedes(X2,sK13(sK2(X0,X1,X2)),tptp0)
| ~ occurrence_of(sK2(X0,X1,X2),tptp0) ),
inference(resolution,[],[f402,f274]) ).
fof(f1899,plain,
! [X2,X0,X1] :
( ~ min_precedes(X2,sK13(sK2(X0,X1,X2)),tptp0)
| ~ arboreal(X2)
| min_precedes(X2,sK12(sK2(X0,X1,X2)),tptp0)
| sK12(sK2(X0,X1,X2)) = X2
| ~ min_precedes(X1,X2,X0)
| ~ occurrence_of(sK2(X0,X1,X2),tptp0) ),
inference(duplicate_literal_removal,[],[f1876]) ).
fof(f1904,plain,
! [X2,X0,X1] :
( ~ arboreal(X0)
| min_precedes(X0,sK12(sK2(X1,X2,X0)),tptp0)
| sK12(sK2(X1,X2,X0)) = X0
| ~ min_precedes(X2,X0,X1)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0)
| ~ subactivity_occurrence(X0,sK2(X1,X2,X0))
| sK13(sK2(X1,X2,X0)) = X0
| ~ arboreal(X0)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0) ),
inference(resolution,[],[f1899,f312]) ).
fof(f1906,plain,
! [X2,X0,X1] :
( ~ arboreal(X0)
| min_precedes(X0,sK12(sK2(X1,X2,X0)),tptp0)
| sK12(sK2(X1,X2,X0)) = X0
| ~ min_precedes(X2,X0,X1)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0)
| ~ subactivity_occurrence(X0,sK2(X1,X2,X0))
| sK13(sK2(X1,X2,X0)) = X0 ),
inference(duplicate_literal_removal,[],[f1904]) ).
fof(f1907,plain,
! [X2,X0,X1] :
( min_precedes(X0,sK12(sK2(X1,X2,X0)),tptp0)
| ~ arboreal(X0)
| sK12(sK2(X1,X2,X0)) = X0
| ~ min_precedes(X2,X0,X1)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0)
| sK13(sK2(X1,X2,X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f1906,f157]) ).
fof(f1911,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(sK12(sK2(X1,X2,X0)),X3)
| sK12(sK2(X1,X2,X0)) = X0
| ~ min_precedes(X2,X0,X1)
| ~ occurrence_of(sK2(X1,X2,X0),tptp0)
| sK13(sK2(X1,X2,X0)) = X0
| ~ occurrence_of(X3,tptp0)
| ~ arboreal(X0) ),
inference(resolution,[],[f1907,f164]) ).
fof(f2129,plain,
! [X2,X0,X1] :
( sK12(sK2(X0,X1,X2)) = X2
| ~ min_precedes(X1,X2,X0)
| ~ occurrence_of(sK2(X0,X1,X2),tptp0)
| sK13(sK2(X0,X1,X2)) = X2
| ~ occurrence_of(sK2(X0,X1,X2),tptp0)
| ~ arboreal(X2)
| ~ occurrence_of(sK2(X0,X1,X2),tptp0) ),
inference(resolution,[],[f1911,f208]) ).
fof(f2134,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK2(X0,X1,X2),tptp0)
| ~ min_precedes(X1,X2,X0)
| sK12(sK2(X0,X1,X2)) = X2
| sK13(sK2(X0,X1,X2)) = X2
| ~ arboreal(X2) ),
inference(duplicate_literal_removal,[],[f2129]) ).
fof(f2138,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| sK12(sK2(tptp0,X0,X1)) = X1
| sK13(sK2(tptp0,X0,X1)) = X1
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f2134,f159]) ).
fof(f2139,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| sK12(sK2(tptp0,X0,X1)) = X1
| sK13(sK2(tptp0,X0,X1)) = X1
| ~ arboreal(X1) ),
inference(duplicate_literal_removal,[],[f2138]) ).
fof(f2154,plain,
! [X0,X1] :
( sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1) = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1)))
| sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1) = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1)))
| ~ arboreal(sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1))
| ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| ~ occurrence_of(X0,sK20) ),
inference(resolution,[],[f2139,f338]) ).
fof(f2161,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK16(tptp0,sK21,X0))
| sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1) = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1)))
| sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1) = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,X0),sK18(tptp0,sK21,X0),sK21,tptp0,X1)))
| ~ occurrence_of(X0,sK20) ),
inference(forward_subsumption_resolution,[],[f2154,f1449]) ).
fof(f2191,plain,
( sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ occurrence_of(sK22,sK20)
| ~ spl23_5 ),
inference(resolution,[],[f2161,f458]) ).
fof(f2193,plain,
( sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK12(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_5 ),
inference(forward_subsumption_resolution,[],[f2191,f243]) ).
fof(f2194,plain,
( sK21 = sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))
| sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_5
| ~ spl23_51 ),
inference(forward_demodulation,[],[f2193,f1218]) ).
fof(f2196,definition,
( spl23_100
<=> sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))) ),
introduced(definition,[new_symbols(definition,[spl23_100])],[avatar_definition]) ).
fof(f2198,plain,
( sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) = sK13(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))))
| ~ spl23_100 ),
inference(avatar_component_clause,[],[f2196]) ).
fof(f2200,definition,
( spl23_101
<=> sK21 = sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) ),
introduced(definition,[new_symbols(definition,[spl23_101])],[avatar_definition]) ).
fof(f2202,plain,
( sK21 = sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))
| ~ spl23_101 ),
inference(avatar_component_clause,[],[f2200]) ).
fof(f2203,plain,
( spl23_100
| spl23_101
| ~ spl23_5
| ~ spl23_51 ),
inference(avatar_split_clause,[],[f2194,f1216,f456,f2200,f2196]) ).
fof(f2240,plain,
( occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp3)
| ~ occurrence_of(sK2(tptp0,sK21,sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))),tptp0)
| tptp2 = sK4(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ spl23_100 ),
inference(superposition,[],[f435,f2198]) ).
fof(f2273,plain,
( occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp3)
| tptp2 = sK4(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)))
| ~ spl23_22
| ~ spl23_100 ),
inference(forward_subsumption_resolution,[],[f2240,f902]) ).
fof(f2325,definition,
( spl23_107
<=> tptp2 = sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)) ),
introduced(definition,[new_symbols(definition,[spl23_107])],[avatar_definition]) ).
fof(f2327,plain,
( tptp2 = sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))
| ~ spl23_107 ),
inference(avatar_component_clause,[],[f2325]) ).
fof(f2386,plain,
( ~ root(sK21,tptp0)
| ~ occurrence_of(sK22,sK20)
| ~ occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ spl23_101 ),
inference(superposition,[],[f340,f2202]) ).
fof(f2393,plain,
( ~ root(sK21,tptp0)
| ~ occurrence_of(sK22,sK20)
| ~ spl23_101 ),
inference(forward_subsumption_resolution,[],[f2386,f250]) ).
fof(f2412,plain,
( ~ occurrence_of(sK22,sK20)
| ~ spl23_101 ),
inference(forward_subsumption_resolution,[],[f2393,f257]) ).
fof(f2415,plain,
( $false
| ~ spl23_101 ),
inference(forward_subsumption_resolution,[],[f2412,f243]) ).
fof(f2416,plain,
~ spl23_101,
inference(avatar_contradiction_clause,[],[f2415]) ).
fof(f2423,definition,
( spl23_108
<=> occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl23_108])],[avatar_definition]) ).
fof(f2425,plain,
( occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp3)
| ~ spl23_108 ),
inference(avatar_component_clause,[],[f2423]) ).
fof(f2432,plain,
( tptp2 = sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))
| occurrence_of(sK15(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22)),tptp3)
| ~ spl23_5
| ~ spl23_22
| ~ spl23_100 ),
inference(forward_demodulation,[],[f2273,f587]) ).
fof(f2440,plain,
( spl23_108
| spl23_107
| ~ spl23_5
| ~ spl23_22
| ~ spl23_100 ),
inference(avatar_split_clause,[],[f2432,f2196,f900,f456,f2325,f2423]) ).
fof(f2448,plain,
( tptp3 = sK14(sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0,sK19(tptp0,sK21,sK22))
| ~ spl23_17
| ~ spl23_108 ),
inference(resolution,[],[f2425,f615]) ).
fof(f2460,plain,
( send_message(tptp3,sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0)
| ~ occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ occurrence_of(sK22,sK20)
| ~ spl23_17
| ~ spl23_108 ),
inference(superposition,[],[f265,f2448]) ).
fof(f2461,plain,
( send_message(tptp3,sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0)
| ~ occurrence_of(sK22,sK20)
| ~ spl23_17
| ~ spl23_108 ),
inference(forward_subsumption_resolution,[],[f2460,f250]) ).
fof(f2465,plain,
( ~ occurrence_of(sK22,sK20)
| ~ spl23_17
| ~ spl23_108 ),
inference(forward_subsumption_resolution,[],[f2461,f246]) ).
fof(f2469,plain,
( $false
| ~ spl23_17
| ~ spl23_108 ),
inference(forward_subsumption_resolution,[],[f2465,f243]) ).
fof(f2470,plain,
( ~ spl23_17
| ~ spl23_108 ),
inference(avatar_contradiction_clause,[],[f2469]) ).
fof(f2570,plain,
( send_message(tptp2,sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0)
| ~ occurrence_of(sK19(tptp0,sK21,sK22),sK16(tptp0,sK21,sK22))
| ~ occurrence_of(sK22,sK20)
| ~ spl23_107 ),
inference(superposition,[],[f265,f2327]) ).
fof(f2571,plain,
( send_message(tptp2,sK17(tptp0,sK21,sK22),sK18(tptp0,sK21,sK22),sK21,tptp0)
| ~ occurrence_of(sK22,sK20)
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f2570,f250]) ).
fof(f2575,plain,
( ~ occurrence_of(sK22,sK20)
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f2571,f247]) ).
fof(f2579,plain,
( $false
| ~ spl23_107 ),
inference(forward_subsumption_resolution,[],[f2575,f243]) ).
fof(f2580,plain,
~ spl23_107,
inference(avatar_contradiction_clause,[],[f2579]) ).
cnf(s5,plain,
( spl23_5
| ~ spl23_6 ),
inference(sat_conversion,[],[f482]) ).
cnf(s7,plain,
spl23_6,
inference(sat_conversion,[],[f491]) ).
cnf(s14,plain,
( ~ spl23_5
| ~ spl23_16
| spl23_17 ),
inference(sat_conversion,[],[f597]) ).
cnf(s15,plain,
( ~ spl23_6
| spl23_16 ),
inference(sat_conversion,[],[f608]) ).
cnf(s18,plain,
( ~ spl23_5
| ~ spl23_21
| spl23_22 ),
inference(sat_conversion,[],[f903]) ).
cnf(s19,plain,
spl23_21,
inference(sat_conversion,[],[f910]) ).
cnf(s21,plain,
( ~ spl23_5
| ~ spl23_22
| ~ spl23_25
| spl23_26 ),
inference(sat_conversion,[],[f956]) ).
cnf(s22,plain,
( ~ spl23_22
| spl23_25 ),
inference(sat_conversion,[],[f959]) ).
cnf(s30,plain,
spl23_36,
inference(sat_conversion,[],[f1053]) ).
cnf(s38,plain,
( ~ spl23_22
| ~ spl23_38 ),
inference(sat_conversion,[],[f1179]) ).
cnf(s42,plain,
( ~ spl23_25
| ~ spl23_36
| spl23_50
| spl23_51 ),
inference(sat_conversion,[],[f1219]) ).
cnf(s51,plain,
( ~ spl23_22
| ~ spl23_50
| ~ spl23_54
| spl23_55 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s53,plain,
( ~ spl23_22
| ~ spl23_36
| spl23_38
| spl23_54 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s54,plain,
( ~ spl23_26
| ~ spl23_55 ),
inference(sat_conversion,[],[f1346]) ).
cnf(s94,plain,
( ~ spl23_5
| ~ spl23_51
| spl23_100
| spl23_101 ),
inference(sat_conversion,[],[f2203]) ).
cnf(s103,plain,
~ spl23_101,
inference(sat_conversion,[],[f2416]) ).
cnf(s109,plain,
( ~ spl23_5
| ~ spl23_22
| ~ spl23_100
| spl23_107
| spl23_108 ),
inference(sat_conversion,[],[f2440]) ).
cnf(s110,plain,
( ~ spl23_17
| ~ spl23_108 ),
inference(sat_conversion,[],[f2470]) ).
cnf(s111,plain,
~ spl23_107,
inference(sat_conversion,[],[f2580]) ).
cnf(s112,plain,
( ~ spl23_5
| ~ spl23_22
| ~ spl23_100
| spl23_108 ),
inference(rat,[],[s109,s111]) ).
cnf(s114,plain,
( ~ spl23_5
| ~ spl23_51
| spl23_100 ),
inference(rat,[],[s94,s103]) ).
cnf(s116,plain,
( ~ spl23_5
| spl23_22 ),
inference(rat,[],[s18,s19]) ).
cnf(s117,plain,
spl23_16,
inference(rat,[],[s15,s7]) ).
cnf(s119,plain,
spl23_5,
inference(rat,[],[s5,s7]) ).
cnf(s120,plain,
spl23_22,
inference(rat,[],[s116,s119]) ).
cnf(s121,plain,
spl23_17,
inference(rat,[],[s14,s117,s119]) ).
cnf(s125,plain,
~ spl23_38,
inference(rat,[],[s38,s120]) ).
cnf(s127,plain,
spl23_25,
inference(rat,[],[s22,s120]) ).
cnf(s128,plain,
~ spl23_108,
inference(rat,[],[s110,s121]) ).
cnf(s129,plain,
spl23_54,
inference(rat,[],[s53,s120,s30,s125]) ).
cnf(s134,plain,
spl23_26,
inference(rat,[],[s21,s120,s119,s127]) ).
cnf(s135,plain,
~ spl23_100,
inference(rat,[],[s112,s120,s119,s128]) ).
cnf(s136,plain,
~ spl23_55,
inference(rat,[],[s54,s134]) ).
cnf(s137,plain,
~ spl23_51,
inference(rat,[],[s114,s119,s135]) ).
cnf(s138,plain,
~ spl23_50,
inference(rat,[],[s51,s129,s120,s136]) ).
cnf(s139,plain,
$false,
inference(rat,[],[s42,s127,s30,s137,s138]) ).
fof(f2581,plain,
$false,
inference(avatar_sat_refutation,[],[s139]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO001+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 22:16:01 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.97/2.59 % (1224933)Detected formulas, will run a generic FOF schedule.
% 11.97/2.59 % (1224939)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=3432897582:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.97/2.59 % (1224942)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4078412736:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.97/2.59 % (1224940)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=1691902264:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.97/2.59 % (1224941)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=900309471:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.97/2.59 % (1224944)dis-21_1_sil=8000:lcm=predicate:random_seed=2986628833: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.97/2.59 % (1224938)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=4128583216:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.97/2.59 % (1224943)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3267334286:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.97/2.59 % (1224941)Refutation not found, incomplete strategy
% 11.97/2.59 % (1224941)------------------------------
% 11.97/2.59 % (1224941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.97/2.59 % (1224941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.97/2.59 % (1224941)CaDiCaL version: 2.1.3
% 11.97/2.59 % (1224941)Termination reason: Refutation not found, incomplete strategy
% 11.97/2.59 % (1224941)Time elapsed: 0.002 s
% 11.97/2.59 % (1224941)Peak memory usage: 88 MB
% 11.97/2.59 % (1224941)Instructions burned: 1 (million)
% 11.97/2.59 % (1224942)Refutation not found, incomplete strategy
% 11.97/2.59 % (1224942)------------------------------
% 11.97/2.59 % (1224942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.97/2.59 % (1224942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.97/2.59 % (1224942)CaDiCaL version: 2.1.3
% 11.97/2.59 % (1224942)Termination reason: Refutation not found, incomplete strategy
% 11.97/2.59 % (1224942)Time elapsed: 0.002 s
% 11.97/2.59 % (1224942)Peak memory usage: 87 MB
% 11.97/2.59 % (1224942)Instructions burned: 1 (million)
% 11.97/2.59 % (1224944)Instruction limit reached!
% 11.97/2.59 % (1224944)------------------------------
% 11.97/2.59 % (1224944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.97/2.59 % (1224944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.97/2.59 % (1224944)CaDiCaL version: 2.1.3
% 11.97/2.59 % (1224944)Termination reason: Instruction limit
% 11.97/2.59 % (1224944)Termination phase: Saturation
% 11.97/2.59 % (1224944)Time elapsed: 0.078 s
% 11.97/2.59 % (1224944)Peak memory usage: 89 MB
% 11.97/2.59 % (1224944)Instructions burned: 130 (million)
% 11.97/2.59 % (1224943)Instruction limit reached!
% 11.97/2.59 % (1224943)------------------------------
% 11.97/2.59 % (1224943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.97/2.59 % (1224943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.97/2.59 % (1224943)CaDiCaL version: 2.1.3
% 11.97/2.59 % (1224943)Termination reason: Instruction limit
% 11.97/2.59 % (1224943)Termination phase: Saturation
% 11.97/2.59 % (1224943)Time elapsed: 0.100 s
% 11.97/2.59 % (1224943)Peak memory usage: 90 MB
% 11.97/2.59 % (1224943)Instructions burned: 140 (million)
% 11.97/2.59 % (1224952)lrs+10_1_sil=8000:sp=occurrence:random_seed=2227722370:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.97/2.59 % (1224941)------------------------------
% 11.97/2.59 % (1224941)------------------------------
% 11.97/2.59 % (1224942)------------------------------
% 11.97/2.59 % (1224942)------------------------------
% 11.97/2.59 % (1224953)lrs+10_1_sil=32000:urr=on:br=off:random_seed=420189917:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.97/2.59 % (1224953)Refutation not found, incomplete strategy
% 11.97/2.59 % (1224953)------------------------------
% 11.97/2.59 % (1224953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.97/2.59 % (1224953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224953)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224953)Termination reason: Refutation not found, incomplete strategy
% 12.49/2.66 % (1224953)Time elapsed: 0.002 s
% 12.49/2.66 % (1224953)Peak memory usage: 88 MB
% 12.49/2.66 % (1224953)Instructions burned: 1 (million)
% 12.49/2.66 % (1224955)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2984275916:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.49/2.66 % (1224952)Instruction limit reached!
% 12.49/2.66 % (1224952)------------------------------
% 12.49/2.66 % (1224952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224952)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224952)Termination reason: Instruction limit
% 12.49/2.66 % (1224952)Termination phase: Saturation
% 12.49/2.66 % (1224952)Time elapsed: 0.173 s
% 12.49/2.66 % (1224952)Peak memory usage: 91 MB
% 12.49/2.66 % (1224952)Instructions burned: 285 (million)
% 12.49/2.66 % (1224956)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=4278680802:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 12.49/2.66 % (1224955)Instruction limit reached!
% 12.49/2.66 % (1224955)------------------------------
% 12.49/2.66 % (1224955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224955)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224955)Termination reason: Instruction limit
% 12.49/2.66 % (1224955)Termination phase: Saturation
% 12.49/2.66 % (1224955)Time elapsed: 0.093 s
% 12.49/2.66 % (1224955)Peak memory usage: 90 MB
% 12.49/2.66 % (1224955)Instructions burned: 325 (million)
% 12.49/2.66 % (1224953)------------------------------
% 12.49/2.66 % (1224953)------------------------------
% 12.49/2.66 % (1224956)Instruction limit reached!
% 12.49/2.66 % (1224956)------------------------------
% 12.49/2.66 % (1224956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224956)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224956)Termination reason: Instruction limit
% 12.49/2.66 % (1224956)Termination phase: Saturation
% 12.49/2.66 % (1224956)Time elapsed: 0.147 s
% 12.49/2.66 % (1224956)Peak memory usage: 90 MB
% 12.49/2.66 % (1224956)Instructions burned: 248 (million)
% 12.49/2.66 % (1224959)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1976408713:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 12.49/2.66 % (1224961)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2166630792:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 12.49/2.66 % (1224962)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1150351865:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 12.49/2.66 % (1224964)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4150910336:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 12.49/2.66 % (1224959)Instruction limit reached!
% 12.49/2.66 % (1224959)------------------------------
% 12.49/2.66 % (1224959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224959)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224959)Termination reason: Instruction limit
% 12.49/2.66 % (1224959)Termination phase: Saturation
% 12.49/2.66 % (1224959)Time elapsed: 0.161 s
% 12.49/2.66 % (1224959)Peak memory usage: 88 MB
% 12.49/2.66 % (1224959)Instructions burned: 294 (million)
% 12.49/2.66 % (1224962)Instruction limit reached!
% 12.49/2.66 % (1224962)------------------------------
% 12.49/2.66 % (1224962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224962)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224962)Termination reason: Instruction limit
% 12.49/2.66 % (1224962)Termination phase: Saturation
% 12.49/2.66 % (1224962)Time elapsed: 0.083 s
% 12.49/2.66 % (1224962)Peak memory usage: 90 MB
% 12.49/2.66 % (1224962)Instructions burned: 113 (million)
% 12.49/2.66 % (1224964)Instruction limit reached!
% 12.49/2.66 % (1224964)------------------------------
% 12.49/2.66 % (1224964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224964)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224964)Termination reason: Instruction limit
% 12.49/2.66 % (1224964)Termination phase: Saturation
% 12.49/2.66 % (1224964)Time elapsed: 0.070 s
% 12.49/2.66 % (1224964)Peak memory usage: 89 MB
% 12.49/2.66 % (1224964)Instructions burned: 127 (million)
% 12.49/2.66 % (1224969)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3168636177:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 12.49/2.66 % (1224970)lrs+10_1_sil=8000:sp=occurrence:random_seed=2263798675:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 12.49/2.66 % (1224969)Instruction limit reached!
% 12.49/2.66 % (1224969)------------------------------
% 12.49/2.66 % (1224969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224969)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224969)Termination reason: Instruction limit
% 12.49/2.66 % (1224969)Termination phase: Saturation
% 12.49/2.66 % (1224969)Time elapsed: 0.042 s
% 12.49/2.66 % (1224969)Peak memory usage: 88 MB
% 12.49/2.66 % (1224969)Instructions burned: 115 (million)
% 12.49/2.66 % (1224971)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2372688875:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 12.49/2.66 % (1224971)Refutation not found, incomplete strategy
% 12.49/2.66 % (1224971)------------------------------
% 12.49/2.66 % (1224971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224971)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224971)Termination reason: Refutation not found, incomplete strategy
% 12.49/2.66 % (1224971)Time elapsed: 0.005 s
% 12.49/2.66 % (1224971)Peak memory usage: 88 MB
% 12.49/2.66 % (1224971)Instructions burned: 5 (million)
% 12.49/2.66 % (1224974)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1150442737:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 12.49/2.66 % (1224971)------------------------------
% 12.49/2.66 % (1224971)------------------------------
% 12.49/2.66 % (1224961)First to succeed.
% 12.49/2.66 % (1224961)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1224933"
% 12.49/2.66 % (1224938)Also succeeded, but the first one will report.
% 12.49/2.66 % (1224977)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=619403830:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 12.49/2.66 % (1224970)Instruction limit reached!
% 12.49/2.66 % (1224970)------------------------------
% 12.49/2.66 % (1224970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224970)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224970)Termination reason: Instruction limit
% 12.49/2.66 % (1224970)Termination phase: Saturation
% 12.49/2.66 % (1224970)Time elapsed: 0.510 s
% 12.49/2.66 % (1224970)Peak memory usage: 95 MB
% 12.49/2.66 % (1224970)Instructions burned: 908 (million)
% 12.49/2.66 % (1224977)Instruction limit reached!
% 12.49/2.66 % (1224977)------------------------------
% 12.49/2.66 % (1224977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224977)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224977)Termination reason: Instruction limit
% 12.49/2.66 % (1224977)Termination phase: Saturation
% 12.49/2.66 % (1224977)Time elapsed: 0.085 s
% 12.49/2.66 % (1224977)Peak memory usage: 90 MB
% 12.49/2.66 % (1224977)Instructions burned: 135 (million)
% 12.49/2.66 % (1224979)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3143275390:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 12.49/2.66 % (1224979)Refutation not found, incomplete strategy
% 12.49/2.66 % (1224979)------------------------------
% 12.49/2.66 % (1224979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/2.66 % (1224979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/2.66 % (1224979)CaDiCaL version: 2.1.3
% 12.49/2.66 % (1224979)Termination reason: Refutation not found, incomplete strategy
% 12.49/2.66 % (1224979)Time elapsed: 0.004 s
% 12.49/2.66 % (1224979)Peak memory usage: 88 MB
% 12.49/2.66 % (1224979)Instructions burned: 4 (million)
% 12.49/2.66 % (1224961)Refutation found. Thanks to Tanya!
% 12.49/2.66 % SZS status Theorem for theBenchmark
% 12.49/2.66 % SZS output start Proof for theBenchmark
% See solution above
% 13.21/2.76 % (1224961)------------------------------
% 13.21/2.76 % (1224961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.21/2.76 % (1224961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.21/2.76 % (1224961)CaDiCaL version: 2.1.3
% 13.21/2.76 % (1224961)Termination reason: Refutation
% 13.21/2.76 % (1224961)Time elapsed: 0.760 s
% 13.21/2.76 % (1224961)Peak memory usage: 133 MB
% 13.21/2.76 % (1224961)Instructions burned: 1419 (million)
% 13.21/2.76 % (1224961)------------------------------
% 13.21/2.76 % (1224961)------------------------------
% 13.21/2.76 % (1224933)Success in time 1.806 s
% 13.21/2.76 % Vampire exiting
%------------------------------------------------------------------------------