%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO001+2 : 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 : n020.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 8.60s 2.08s
% Output : Refutation 9.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 43
% Syntax : Number of formulae : 329 ( 34 unt; 20 def)
% Number of atoms : 1004 ( 67 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1166 ( 491 ~; 498 |; 132 &)
% ( 29 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 21 prp; 0-5 aty)
% Number of functors : 25 ( 25 usr; 7 con; 0-5 aty)
% Number of variables : 506 ( 0 sgn 444 !; 62 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,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_04) ).
fof(f6,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
=> ( arboreal(X0)
& arboreal(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_05) ).
fof(f8,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f11,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_10) ).
fof(f12,axiom,
! [X0,X1] :
( leaf_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
fof(f14,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(f15,axiom,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ~ ? [X3] : min_precedes(X0,X3,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
fof(f16,axiom,
! [X0,X1] :
( atocc(X0,X1)
<=> ? [X2] :
( subactivity(X1,X2)
& atomic(X2)
& occurrence_of(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_15) ).
fof(f19,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_18) ).
fof(f20,axiom,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
=> ( activity_occurrence(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_19) ).
fof(f21,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_20) ).
fof(f23,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f25,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_24) ).
fof(f27,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/sandbox/benchmark/theBenchmark.p',sos_26) ).
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/sandbox/benchmark/theBenchmark.p',sos_28) ).
fof(f30,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_29) ).
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(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(f68,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,[],[f5]) ).
fof(f69,plain,
! [X0,X1,X2] :
( ( arboreal(X0)
& arboreal(X1) )
| ~ next_subocc(X0,X1,X2) ),
inference(ennf_transformation,[],[f6]) ).
fof(f71,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f8]) ).
fof(f75,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f14]) ).
fof(f76,plain,
! [X0,X1] :
( leaf(X0,X1)
<=> ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f80,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f81,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f20]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f83,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(flattening,[],[f82]) ).
fof(f86,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f87,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f86]) ).
fof(f90,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,[],[f25]) ).
fof(f93,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,[],[f27]) ).
fof(f95,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(f96,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,[],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f101,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(f103,plain,
! [X0,X1,X2,X3,X4] :
( ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 )
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f47]) ).
fof(f104,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(f105,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,[],[f104]) ).
fof(f108,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(f109,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,[],[f108]) ).
fof(f111,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(f112,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,[],[f111]) ).
fof(f113,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,[],[f68]) ).
fof(f114,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,[],[f113]) ).
fof(f115,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,[],[f114]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK0(X0,X1,X2),X2)
& min_precedes(sK0(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,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[f115]) ).
fof(f117,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,[],[f11]) ).
fof(f118,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,[],[f117]) ).
fof(f119,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK1(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK1(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1))],[f118]) ).
fof(f120,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& leaf(X0,X2) )
| ~ leaf_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f121,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ? [X3] :
( occurrence_of(X1,X3)
& subactivity_occurrence(X0,X1)
& leaf(X0,X3) )
| ~ leaf_occ(X0,X1) ) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0,X1] :
( ( leaf_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ leaf(X0,X2) ) )
& ( ( occurrence_of(X1,sK2(X0,X1))
& subactivity_occurrence(X0,X1)
& leaf(X0,sK2(X0,X1)) )
| ~ leaf_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1))],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f75]) ).
fof(f124,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ) ),
inference(nnf_transformation,[],[f76]) ).
fof(f125,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X2] : min_precedes(X2,X0,X1) )
& ! [X3] : ~ min_precedes(X0,X3,X1) )
| ~ leaf(X0,X1) ) ),
inference(flattening,[],[f124]) ).
fof(f126,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| ? [X3] : min_precedes(X0,X3,X1) )
& ( ( ( root(X0,X1)
| ? [X4] : min_precedes(X4,X0,X1) )
& ! [X5] : ~ min_precedes(X0,X5,X1) )
| ~ leaf(X0,X1) ) ),
inference(rectify,[],[f125]) ).
fof(f127,plain,
! [X0,X1] :
( ( leaf(X0,X1)
| ( ~ root(X0,X1)
& ! [X2] : ~ min_precedes(X2,X0,X1) )
| min_precedes(X0,sK3(X0,X1),X1) )
& ( ( ( root(X0,X1)
| min_precedes(sK4(X0,X1),X0,X1) )
& ! [X5] : ~ min_precedes(X0,X5,X1) )
| ~ leaf(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X3,sK3(X0,X1)),skolemize(X4,sK4(X0,X1))],[f126]) ).
fof(f128,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,[],[f16]) ).
fof(f129,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,[],[f128]) ).
fof(f130,plain,
! [X0,X1] :
( ( atocc(X0,X1)
| ! [X2] :
( ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X0,X2) ) )
& ( ( subactivity(X1,sK5(X0,X1))
& atomic(sK5(X0,X1))
& occurrence_of(X0,sK5(X0,X1)) )
| ~ atocc(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X3,sK5(X0,X1))],[f129]) ).
fof(f131,plain,
! [X0] :
( ( activity(sK6(X0))
& occurrence_of(X0,sK6(X0)) )
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X1,sK6(X0))],[f80]) ).
fof(f133,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK8(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK8(X0,X1,X2))
& subactivity_occurrence(X2,sK8(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1,X2))],[f90]) ).
fof(f135,plain,
! [X0,X1,X2] :
( ( subactivity(sK10(X0,X1,X2),X0)
& subactivity(sK11(X0,X1,X2),X0)
& atocc(X1,sK10(X0,X1,X2))
& atocc(X2,sK11(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11]),skolemize(X3,sK10(X0,X1,X2)),skolemize(X4,sK11(X0,X1,X2))],[f93]) ).
fof(f138,plain,
! [X0] :
( ( occurrence_of(sK14(X0),tptp4)
& root_occ(sK14(X0),X0)
& ( occurrence_of(sK15(X0),tptp3)
| occurrence_of(sK15(X0),tptp2) )
& leaf_occ(sK15(X0),X0)
& next_subocc(sK14(X0),sK15(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15]),skolemize(X1,sK14(X0)),skolemize(X2,sK15(X0))],[f101]) ).
fof(f139,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( send_message(sK16(X1,X2,X3,X4,X5),X1,X2,X3,X4)
& occurrence_of(sK17(X1,X2,X3,X4,X5),sK16(X1,X2,X3,X4,X5))
& root_occ(sK17(X1,X2,X3,X4,X5),X5) )
| ~ transmit_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X6,sK16(X1,X2,X3,X4,X5)),skolemize(X7,sK17(X1,X2,X3,X4,X5))],[f109]) ).
fof(f140,plain,
! [X0,X1,X2,X3] :
( ( transmit_message(sK18(X1,X2,X3),sK19(X1,X2,X3),sK20(X1,X2,X3),X2,X1)
& occurrence_of(sK21(X1,X2,X3),sK18(X1,X2,X3))
& subactivity_occurrence(sK21(X1,X2,X3),X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20,sK21]),skolemize(X4,sK18(X1,X2,X3)),skolemize(X5,sK19(X1,X2,X3)),skolemize(X6,sK20(X1,X2,X3)),skolemize(X7,sK21(X1,X2,X3))],[f112]) ).
fof(f141,plain,
( tptp1(sK22,tptp0,sK23)
& occurrence_of(sK24,sK22) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24]),skolemize(X0,sK22),skolemize(X1,sK23),skolemize(X2,sK24)],[f58]) ).
fof(f146,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| arboreal(X1) ),
inference(cnf_transformation,[],[f69]) ).
fof(f153,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f71]) ).
fof(f157,plain,
! [X0,X1] :
( root(X0,sK1(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f158,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f159,plain,
! [X0,X1] :
( occurrence_of(X1,sK1(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f161,plain,
! [X0,X1] :
( leaf(X0,sK2(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f162,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f163,plain,
! [X0,X1] :
( occurrence_of(X1,sK2(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f167,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f168,plain,
! [X0,X1,X5] :
( ~ min_precedes(X0,X5,X1)
| ~ leaf(X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f172,plain,
! [X0,X1] :
( occurrence_of(X0,sK5(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
fof(f173,plain,
! [X0,X1] :
( atomic(sK5(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f130]) ).
fof(f178,plain,
! [X0] :
( occurrence_of(X0,sK6(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f181,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f182,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f184,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f87]) ).
fof(f187,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK8(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f133]) ).
fof(f189,plain,
! [X2,X0,X1] :
( occurrence_of(sK8(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f133]) ).
fof(f192,plain,
! [X2,X0,X1] :
( atocc(X2,sK11(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f135]) ).
fof(f193,plain,
! [X2,X0,X1] :
( atocc(X1,sK10(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f135]) ).
fof(f198,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,[],[f96]) ).
fof(f199,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f97]) ).
fof(f204,plain,
! [X0] :
( next_subocc(sK14(X0),sK15(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f205,plain,
! [X0] :
( leaf_occ(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f206,plain,
! [X0] :
( occurrence_of(sK15(X0),tptp2)
| occurrence_of(sK15(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f207,plain,
! [X0] :
( root_occ(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f208,plain,
! [X0] :
( occurrence_of(sK14(X0),tptp4)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f211,plain,
atomic(tptp4),
inference(cnf_transformation,[],[f36]) ).
fof(f225,plain,
! [X2,X3,X0,X1,X4] :
( tptp2 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f103]) ).
fof(f226,plain,
! [X2,X3,X0,X1,X4] :
( tptp3 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f103]) ).
fof(f228,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,[],[f105]) ).
fof(f235,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| root_occ(sK17(X1,X2,X3,X4,X5),X5)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f236,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| occurrence_of(sK17(X1,X2,X3,X4,X5),sK16(X1,X2,X3,X4,X5))
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f237,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| send_message(sK16(X1,X2,X3,X4,X5),X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f243,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| occurrence_of(sK21(X1,X2,X3),sK18(X1,X2,X3))
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f244,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| transmit_message(sK18(X1,X2,X3),sK19(X1,X2,X3),sK20(X1,X2,X3),X2,X1)
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f246,plain,
occurrence_of(sK24,sK22),
inference(cnf_transformation,[],[f141]) ).
fof(f247,plain,
tptp1(sK22,tptp0,sK23),
inference(cnf_transformation,[],[f141]) ).
fof(f249,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp3,X1,X2,X3,X4),
inference(equality_resolution,[],[f226]) ).
fof(f250,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp2,X1,X2,X3,X4),
inference(equality_resolution,[],[f225]) ).
fof(f251,plain,
! [X0] :
( transmit_message(sK18(tptp0,sK23,X0),sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0)
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f244,f247]) ).
fof(f252,plain,
! [X0] :
( occurrence_of(sK21(tptp0,sK23,X0),sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f243,f247]) ).
fof(f254,plain,
! [X0,X1] :
( ~ occurrence_of(sK21(tptp0,sK23,X0),X1)
| sK18(tptp0,sK23,X0) = X1
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f184,f252]) ).
fof(f263,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X3,sK8(X2,X0,X1))
| min_precedes(X1,X3,X4)
| X1 = X3
| ~ occurrence_of(sK8(X2,X0,X1),X4)
| ~ arboreal(X3)
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,X2)
| min_precedes(X3,X1,X4) ),
inference(resolution,[],[f187,f198]) ).
fof(f265,plain,
! [X0,X1] :
( occurrence_of(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1),sK16(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1))
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f236,f251]) ).
fof(f277,plain,
! [X0,X1] :
( ~ min_precedes(sK14(X1),X0,tptp0)
| ~ min_precedes(X0,sK15(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f146,f204]) ).
fof(f278,plain,
! [X0,X1] :
( send_message(sK16(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1),sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0)
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f237,f251]) ).
fof(f283,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp4)
| arboreal(sK14(X0)) ),
inference(resolution,[],[f208,f167]) ).
fof(f285,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK14(X0)) ),
inference(forward_subsumption_resolution,[],[f283,f211]) ).
fof(f287,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK8(X2,X0,X1),X3)
| ~ min_precedes(X0,X1,X2)
| X2 = X3 ),
inference(resolution,[],[f189,f184]) ).
fof(f288,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X2,sK16(sK19(tptp0,sK23,X1),sK20(tptp0,sK23,X1),sK23,tptp0,X0))
| ~ occurrence_of(X1,sK22)
| min_precedes(sK23,X2,tptp0)
| ~ occurrence_of(X0,sK18(tptp0,sK23,X1)) ),
inference(resolution,[],[f278,f228]) ).
fof(f289,plain,
! [X0,X1] :
( root_occ(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1),X1)
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f235,f251]) ).
fof(f298,plain,
! [X0] :
( subactivity_occurrence(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f162,f205]) ).
fof(f301,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK17(sK19(tptp0,sK23,X1),sK20(tptp0,sK23,X1),sK23,tptp0,X0),X2)
| ~ occurrence_of(X1,sK22)
| ~ occurrence_of(X0,sK18(tptp0,sK23,X1))
| sK16(sK19(tptp0,sK23,X1),sK20(tptp0,sK23,X1),sK23,tptp0,X0) = X2 ),
inference(resolution,[],[f265,f184]) ).
fof(f306,plain,
! [X0] :
( subactivity_occurrence(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f158,f207]) ).
fof(f313,plain,
! [X0,X1] :
( activity_occurrence(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1))
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f199,f265]) ).
fof(f314,plain,
! [X0] :
( activity_occurrence(sK21(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f199,f252]) ).
fof(f317,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,tptp0)
| min_precedes(sK14(X0),X1,X2)
| sK14(X0) = X1
| ~ occurrence_of(X0,X2)
| ~ arboreal(X1)
| ~ arboreal(sK14(X0))
| ~ subactivity_occurrence(X1,X0)
| min_precedes(X1,sK14(X0),X2) ),
inference(resolution,[],[f306,f198]) ).
fof(f318,plain,
! [X2,X0,X1] :
( min_precedes(sK14(X0),X1,X2)
| min_precedes(X1,sK14(X0),X2)
| sK14(X0) = X1
| ~ occurrence_of(X0,X2)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f317,f285]) ).
fof(f341,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK22)
| min_precedes(sK23,sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1),tptp0)
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f288,f265]) ).
fof(f342,plain,
! [X0,X1] :
( min_precedes(sK23,sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1),tptp0)
| ~ occurrence_of(X0,sK22)
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0)) ),
inference(duplicate_literal_removal,[],[f341]) ).
fof(f380,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| arboreal(sK15(X0)) ),
inference(resolution,[],[f150,f204]) ).
fof(f413,plain,
! [X0,X1] :
( min_precedes(X1,sK14(X0),tptp0)
| sK14(X0) = X1
| ~ occurrence_of(X0,tptp0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0)
| ~ min_precedes(X1,sK15(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f318,f277]) ).
fof(f431,plain,
! [X0,X1] :
( min_precedes(X1,sK14(X0),tptp0)
| sK14(X0) = X1
| ~ occurrence_of(X0,tptp0)
| ~ arboreal(X1)
| ~ subactivity_occurrence(X1,X0)
| ~ min_precedes(X1,sK15(X0),tptp0) ),
inference(duplicate_literal_removal,[],[f413]) ).
fof(f457,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X3,sK8(X2,X0,X1))
| sK2(X3,sK8(X2,X0,X1)) = X2
| ~ min_precedes(X0,X1,X2) ),
inference(resolution,[],[f287,f163]) ).
fof(f460,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK8(X0,X1,X2),tptp0)
| ~ min_precedes(X1,X2,X0)
| sK2(sK15(sK8(X0,X1,X2)),sK8(X0,X1,X2)) = X0 ),
inference(resolution,[],[f457,f205]) ).
fof(f465,plain,
! [X0,X1] :
( ~ activity_occurrence(X0)
| ~ occurrence_of(X0,X1)
| sK6(X0) = X1 ),
inference(resolution,[],[f178,f184]) ).
fof(f468,plain,
! [X0,X1] :
( ~ activity_occurrence(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1))
| ~ occurrence_of(X0,sK22)
| ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| sK16(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1) = sK6(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1)) ),
inference(resolution,[],[f178,f301]) ).
fof(f469,plain,
! [X0] :
( ~ activity_occurrence(sK21(tptp0,sK23,X0))
| sK18(tptp0,sK23,X0) = sK6(sK21(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f178,f254]) ).
fof(f472,plain,
! [X0] :
( ~ occurrence_of(X0,sK22)
| sK18(tptp0,sK23,X0) = sK6(sK21(tptp0,sK23,X0)) ),
inference(forward_subsumption_resolution,[],[f469,f314]) ).
fof(f473,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22)
| sK16(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1) = sK6(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1)) ),
inference(forward_subsumption_resolution,[],[f468,f313]) ).
fof(f475,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK6(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f465,f199]) ).
fof(f477,plain,
! [X0,X1] :
( ~ root_occ(X1,X0)
| sK6(X0) = sK1(X1,X0) ),
inference(resolution,[],[f475,f159]) ).
fof(f486,plain,
sK18(tptp0,sK23,sK24) = sK6(sK21(tptp0,sK23,sK24)),
inference(resolution,[],[f472,f246]) ).
fof(f487,plain,
( occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24))
| ~ activity_occurrence(sK21(tptp0,sK23,sK24)) ),
inference(superposition,[],[f178,f486]) ).
fof(f489,definition,
( spl25_8
<=> activity_occurrence(sK21(tptp0,sK23,sK24)) ),
introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition]) ).
fof(f491,plain,
( ~ activity_occurrence(sK21(tptp0,sK23,sK24))
| spl25_8 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f493,definition,
( spl25_9
<=> occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24)) ),
introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition]) ).
fof(f495,plain,
( occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24))
| ~ spl25_9 ),
inference(avatar_component_clause,[],[f493]) ).
fof(f496,plain,
( ~ spl25_8
| spl25_9 ),
inference(avatar_split_clause,[],[f487,f493,f489]) ).
fof(f499,plain,
! [X0] :
( ~ occurrence_of(X0,sK22)
| sK16(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,sK21(tptp0,sK23,X0)) = sK6(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,sK21(tptp0,sK23,X0)))
| ~ occurrence_of(X0,sK22) ),
inference(resolution,[],[f473,f252]) ).
fof(f500,plain,
! [X0] :
( ~ occurrence_of(X0,sK22)
| sK16(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,sK21(tptp0,sK23,X0)) = sK6(sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,sK21(tptp0,sK23,X0))) ),
inference(duplicate_literal_removal,[],[f499]) ).
fof(f502,plain,
sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK6(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),
inference(resolution,[],[f500,f246]) ).
fof(f503,plain,
( occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))
| ~ activity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))) ),
inference(superposition,[],[f178,f502]) ).
fof(f505,definition,
( spl25_10
<=> activity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))) ),
introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition]) ).
fof(f507,plain,
( ~ activity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))
| spl25_10 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f509,definition,
( spl25_11
<=> occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))) ),
introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition]) ).
fof(f511,plain,
( occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))
| ~ spl25_11 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f512,plain,
( ~ spl25_10
| spl25_11 ),
inference(avatar_split_clause,[],[f503,f509,f505]) ).
fof(f514,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| sK6(X0) = sK1(sK14(X0),X0) ),
inference(resolution,[],[f477,f207]) ).
fof(f527,plain,
( ~ occurrence_of(sK24,sK22)
| spl25_8 ),
inference(resolution,[],[f314,f491]) ).
fof(f528,plain,
( $false
| spl25_8 ),
inference(forward_subsumption_resolution,[],[f527,f246]) ).
fof(f529,plain,
spl25_8,
inference(avatar_contradiction_clause,[],[f528]) ).
fof(f576,plain,
! [X2,X3,X0,X1] :
( min_precedes(X0,sK15(sK8(X1,X2,X0)),X3)
| sK15(sK8(X1,X2,X0)) = X0
| ~ occurrence_of(sK8(X1,X2,X0),X3)
| ~ arboreal(sK15(sK8(X1,X2,X0)))
| ~ arboreal(X0)
| ~ min_precedes(X2,X0,X1)
| min_precedes(sK15(sK8(X1,X2,X0)),X0,X3)
| ~ occurrence_of(sK8(X1,X2,X0),tptp0) ),
inference(resolution,[],[f263,f298]) ).
fof(f637,definition,
( spl25_16
<=> root_occ(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK21(tptp0,sK23,sK24)) ),
introduced(definition,[new_symbols(definition,[spl25_16])],[avatar_definition]) ).
fof(f638,plain,
( root_occ(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK21(tptp0,sK23,sK24))
| ~ spl25_16 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f639,plain,
( ~ root_occ(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK21(tptp0,sK23,sK24))
| spl25_16 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f645,plain,
( ~ occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24))
| ~ occurrence_of(sK24,sK22)
| spl25_16 ),
inference(resolution,[],[f639,f289]) ).
fof(f646,plain,
( ~ occurrence_of(sK24,sK22)
| spl25_16 ),
inference(forward_subsumption_resolution,[],[f645,f252]) ).
fof(f647,plain,
( $false
| spl25_16 ),
inference(forward_subsumption_resolution,[],[f646,f246]) ).
fof(f648,plain,
spl25_16,
inference(avatar_contradiction_clause,[],[f647]) ).
fof(f655,plain,
( subactivity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK21(tptp0,sK23,sK24))
| ~ spl25_16 ),
inference(resolution,[],[f638,f158]) ).
fof(f663,plain,
( activity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))
| ~ spl25_16 ),
inference(resolution,[],[f655,f181]) ).
fof(f674,plain,
( $false
| spl25_10
| ~ spl25_16 ),
inference(forward_subsumption_resolution,[],[f663,f507]) ).
fof(f675,plain,
( spl25_10
| ~ spl25_16 ),
inference(avatar_contradiction_clause,[],[f674]) ).
fof(f683,plain,
( ! [X0] :
( ~ occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),X0)
| sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = X0 )
| ~ spl25_11 ),
inference(resolution,[],[f511,f184]) ).
fof(f712,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| ~ atomic(sK5(X0,X1))
| arboreal(X0) ),
inference(resolution,[],[f172,f167]) ).
fof(f723,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| arboreal(X0) ),
inference(forward_subsumption_resolution,[],[f712,f173]) ).
fof(f724,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X0,X2)
| arboreal(X0) ),
inference(resolution,[],[f723,f192]) ).
fof(f725,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| arboreal(X0) ),
inference(resolution,[],[f723,f193]) ).
fof(f773,plain,
! [X0,X1] :
( ~ min_precedes(X1,sK15(X0),tptp0)
| sK14(X0) = X1
| ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(X1,X0)
| min_precedes(X1,sK14(X0),tptp0) ),
inference(forward_subsumption_resolution,[],[f431,f725]) ).
fof(f790,plain,
! [X2,X3,X0,X1] :
( min_precedes(X0,sK15(sK8(X1,X2,X0)),X3)
| sK15(sK8(X1,X2,X0)) = X0
| ~ occurrence_of(sK8(X1,X2,X0),X3)
| ~ arboreal(sK15(sK8(X1,X2,X0)))
| ~ min_precedes(X2,X0,X1)
| min_precedes(sK15(sK8(X1,X2,X0)),X0,X3)
| ~ occurrence_of(sK8(X1,X2,X0),tptp0) ),
inference(forward_subsumption_resolution,[],[f576,f724]) ).
fof(f817,plain,
! [X2,X3,X0,X1] :
( min_precedes(sK15(sK8(X1,X2,X0)),X0,X3)
| sK15(sK8(X1,X2,X0)) = X0
| ~ occurrence_of(sK8(X1,X2,X0),X3)
| ~ min_precedes(X2,X0,X1)
| min_precedes(X0,sK15(sK8(X1,X2,X0)),X3)
| ~ occurrence_of(sK8(X1,X2,X0),tptp0) ),
inference(forward_subsumption_resolution,[],[f790,f380]) ).
fof(f854,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK2(sK15(sK8(tptp0,X0,X1)),sK8(tptp0,X0,X1))
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f460,f189]) ).
fof(f855,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| tptp0 = sK2(sK15(sK8(tptp0,X0,X1)),sK8(tptp0,X0,X1)) ),
inference(duplicate_literal_removal,[],[f854]) ).
fof(f857,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK18(tptp0,sK23,X0))
| ~ occurrence_of(X0,sK22)
| tptp0 = sK2(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,X0),sK20(tptp0,sK23,X0),sK23,tptp0,X1))) ),
inference(resolution,[],[f855,f342]) ).
fof(f892,definition,
( spl25_29
<=> min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl25_29])],[avatar_definition]) ).
fof(f893,plain,
( ~ min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| spl25_29 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f894,plain,
( min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| ~ spl25_29 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f1322,plain,
( ~ occurrence_of(sK24,sK22)
| tptp0 = sK2(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_9 ),
inference(resolution,[],[f857,f495]) ).
fof(f1324,plain,
( tptp0 = sK2(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_9 ),
inference(forward_subsumption_resolution,[],[f1322,f246]) ).
fof(f1327,plain,
( leaf(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ leaf_occ(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_9 ),
inference(superposition,[],[f161,f1324]) ).
fof(f1329,definition,
( spl25_42
<=> leaf_occ(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))) ),
introduced(definition,[new_symbols(definition,[spl25_42])],[avatar_definition]) ).
fof(f1331,plain,
( ~ leaf_occ(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| spl25_42 ),
inference(avatar_component_clause,[],[f1329]) ).
fof(f1333,definition,
( spl25_43
<=> leaf(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl25_43])],[avatar_definition]) ).
fof(f1335,plain,
( leaf(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_43 ),
inference(avatar_component_clause,[],[f1333]) ).
fof(f1336,plain,
( ~ spl25_42
| spl25_43
| ~ spl25_9 ),
inference(avatar_split_clause,[],[f1327,f493,f1333,f1329]) ).
fof(f1338,definition,
( spl25_44
<=> occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl25_44])],[avatar_definition]) ).
fof(f1339,plain,
( ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| spl25_44 ),
inference(avatar_component_clause,[],[f1338]) ).
fof(f1340,plain,
( occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ spl25_44 ),
inference(avatar_component_clause,[],[f1338]) ).
fof(f1346,plain,
( ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| spl25_42 ),
inference(resolution,[],[f1331,f205]) ).
fof(f1347,plain,
( ~ spl25_44
| spl25_42 ),
inference(avatar_split_clause,[],[f1346,f1329,f1338]) ).
fof(f1348,plain,
( ~ min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| spl25_44 ),
inference(resolution,[],[f1339,f189]) ).
fof(f1349,plain,
( ~ spl25_29
| spl25_44 ),
inference(avatar_split_clause,[],[f1348,f1338,f892]) ).
fof(f1350,plain,
( ~ occurrence_of(sK24,sK22)
| ~ occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24))
| spl25_29 ),
inference(resolution,[],[f893,f342]) ).
fof(f1353,plain,
( ~ occurrence_of(sK24,sK22)
| spl25_29 ),
inference(forward_subsumption_resolution,[],[f1350,f252]) ).
fof(f1355,plain,
( $false
| spl25_29 ),
inference(forward_subsumption_resolution,[],[f1353,f246]) ).
fof(f1356,plain,
spl25_29,
inference(avatar_contradiction_clause,[],[f1355]) ).
fof(f1366,plain,
( sK1(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))) = sK6(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_44 ),
inference(resolution,[],[f1340,f514]) ).
fof(f1372,plain,
( tptp0 = sK6(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_44 ),
inference(resolution,[],[f1340,f475]) ).
fof(f1388,plain,
( tptp0 = sK1(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_44 ),
inference(forward_demodulation,[],[f1366,f1372]) ).
fof(f1400,plain,
( ! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ root_occ(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),X0) )
| ~ spl25_29 ),
inference(resolution,[],[f894,f182]) ).
fof(f1446,plain,
( root(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ root_occ(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_44 ),
inference(superposition,[],[f157,f1388]) ).
fof(f1449,definition,
( spl25_54
<=> root_occ(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))) ),
introduced(definition,[new_symbols(definition,[spl25_54])],[avatar_definition]) ).
fof(f1451,plain,
( ~ root_occ(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| spl25_54 ),
inference(avatar_component_clause,[],[f1449]) ).
fof(f1453,definition,
( spl25_55
<=> root(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl25_55])],[avatar_definition]) ).
fof(f1455,plain,
( root(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_55 ),
inference(avatar_component_clause,[],[f1453]) ).
fof(f1456,plain,
( ~ spl25_54
| spl25_55
| ~ spl25_44 ),
inference(avatar_split_clause,[],[f1446,f1338,f1453,f1449]) ).
fof(f1487,definition,
( spl25_58
<=> sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))) ),
introduced(definition,[new_symbols(definition,[spl25_58])],[avatar_definition]) ).
fof(f1488,plain,
( sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) != sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| spl25_58 ),
inference(avatar_component_clause,[],[f1487]) ).
fof(f1489,plain,
( sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_58 ),
inference(avatar_component_clause,[],[f1487]) ).
fof(f1511,plain,
( occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp2)
| occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp3)
| ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ spl25_58 ),
inference(superposition,[],[f206,f1489]) ).
fof(f1545,plain,
( occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp2)
| occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp3)
| ~ spl25_44
| ~ spl25_58 ),
inference(forward_subsumption_resolution,[],[f1511,f1340]) ).
fof(f1589,definition,
( spl25_63
<=> tptp2 = sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) ),
introduced(definition,[new_symbols(definition,[spl25_63])],[avatar_definition]) ).
fof(f1590,plain,
( tptp2 != sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))
| spl25_63 ),
inference(avatar_component_clause,[],[f1589]) ).
fof(f1591,plain,
( tptp2 = sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))
| ~ spl25_63 ),
inference(avatar_component_clause,[],[f1589]) ).
fof(f1726,definition,
( spl25_74
<=> min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl25_74])],[avatar_definition]) ).
fof(f1728,plain,
( min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_74 ),
inference(avatar_component_clause,[],[f1726]) ).
fof(f1737,definition,
( spl25_76
<=> occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl25_76])],[avatar_definition]) ).
fof(f1739,plain,
( occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp3)
| ~ spl25_76 ),
inference(avatar_component_clause,[],[f1737]) ).
fof(f1741,definition,
( spl25_77
<=> occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp2) ),
introduced(definition,[new_symbols(definition,[spl25_77])],[avatar_definition]) ).
fof(f1743,plain,
( occurrence_of(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp2)
| ~ spl25_77 ),
inference(avatar_component_clause,[],[f1741]) ).
fof(f1747,plain,
( sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ subactivity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_74 ),
inference(resolution,[],[f1728,f773]) ).
fof(f1779,plain,
( sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ subactivity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_44
| ~ spl25_74 ),
inference(forward_subsumption_resolution,[],[f1747,f1340]) ).
fof(f1781,definition,
( spl25_81
<=> min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl25_81])],[avatar_definition]) ).
fof(f1783,plain,
( min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_81 ),
inference(avatar_component_clause,[],[f1781]) ).
fof(f1785,definition,
( spl25_82
<=> subactivity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))) ),
introduced(definition,[new_symbols(definition,[spl25_82])],[avatar_definition]) ).
fof(f1787,plain,
( ~ subactivity_occurrence(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| spl25_82 ),
inference(avatar_component_clause,[],[f1785]) ).
fof(f1789,definition,
( spl25_83
<=> sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))) ),
introduced(definition,[new_symbols(definition,[spl25_83])],[avatar_definition]) ).
fof(f1791,plain,
( sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ spl25_83 ),
inference(avatar_component_clause,[],[f1789]) ).
fof(f1792,plain,
( spl25_81
| ~ spl25_82
| spl25_83
| ~ spl25_44
| ~ spl25_74 ),
inference(avatar_split_clause,[],[f1779,f1726,f1338,f1789,f1785,f1781]) ).
fof(f1851,definition,
( spl25_88
<=> min_precedes(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl25_88])],[avatar_definition]) ).
fof(f1852,plain,
( ~ min_precedes(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| spl25_88 ),
inference(avatar_component_clause,[],[f1851]) ).
fof(f1853,plain,
( min_precedes(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| ~ spl25_88 ),
inference(avatar_component_clause,[],[f1851]) ).
fof(f1908,plain,
( ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| spl25_54 ),
inference(resolution,[],[f1451,f207]) ).
fof(f1909,plain,
( $false
| ~ spl25_44
| spl25_54 ),
inference(forward_subsumption_resolution,[],[f1908,f1340]) ).
fof(f1910,plain,
( ~ spl25_44
| spl25_54 ),
inference(avatar_contradiction_clause,[],[f1909]) ).
fof(f2107,plain,
( sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| spl25_88 ),
inference(resolution,[],[f1852,f817]) ).
fof(f2108,plain,
( sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)) = sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| spl25_88 ),
inference(duplicate_literal_removal,[],[f2107]) ).
fof(f2110,plain,
( ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| spl25_58
| spl25_88 ),
inference(forward_subsumption_resolution,[],[f2108,f1488]) ).
fof(f2113,plain,
( ~ min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| spl25_58
| spl25_88 ),
inference(forward_subsumption_resolution,[],[f2110,f189]) ).
fof(f2116,plain,
( min_precedes(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_29
| spl25_58
| spl25_88 ),
inference(forward_subsumption_resolution,[],[f2113,f894]) ).
fof(f2207,plain,
( ~ min_precedes(sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),tptp0)
| spl25_82 ),
inference(resolution,[],[f1787,f187]) ).
fof(f2208,plain,
( $false
| ~ spl25_29
| spl25_82 ),
inference(forward_subsumption_resolution,[],[f2207,f894]) ).
fof(f2209,plain,
( ~ spl25_29
| spl25_82 ),
inference(avatar_contradiction_clause,[],[f2208]) ).
fof(f2214,plain,
( spl25_76
| spl25_77
| ~ spl25_44
| ~ spl25_58 ),
inference(avatar_split_clause,[],[f1545,f1487,f1338,f1741,f1737]) ).
fof(f2284,plain,
( tptp3 = sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))
| ~ spl25_11
| ~ spl25_76 ),
inference(resolution,[],[f1739,f683]) ).
fof(f2298,plain,
( send_message(tptp3,sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0)
| ~ occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24))
| ~ occurrence_of(sK24,sK22)
| ~ spl25_11
| ~ spl25_76 ),
inference(superposition,[],[f278,f2284]) ).
fof(f2299,plain,
( send_message(tptp3,sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0)
| ~ occurrence_of(sK24,sK22)
| ~ spl25_11
| ~ spl25_76 ),
inference(forward_subsumption_resolution,[],[f2298,f252]) ).
fof(f2301,plain,
( ~ occurrence_of(sK24,sK22)
| ~ spl25_11
| ~ spl25_76 ),
inference(forward_subsumption_resolution,[],[f2299,f249]) ).
fof(f2303,plain,
( $false
| ~ spl25_11
| ~ spl25_76 ),
inference(forward_subsumption_resolution,[],[f2301,f246]) ).
fof(f2304,plain,
( ~ spl25_11
| ~ spl25_76 ),
inference(avatar_contradiction_clause,[],[f2303]) ).
fof(f2310,plain,
( ~ occurrence_of(sK24,sK22)
| ~ occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24))
| tptp2 = sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))
| ~ spl25_77 ),
inference(resolution,[],[f1743,f301]) ).
fof(f2319,plain,
( ~ occurrence_of(sK24,sK22)
| tptp2 = sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))
| ~ spl25_77 ),
inference(forward_subsumption_resolution,[],[f2310,f252]) ).
fof(f2334,plain,
( send_message(tptp2,sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0)
| ~ occurrence_of(sK21(tptp0,sK23,sK24),sK18(tptp0,sK23,sK24))
| ~ occurrence_of(sK24,sK22)
| ~ spl25_63 ),
inference(superposition,[],[f278,f1591]) ).
fof(f2335,plain,
( send_message(tptp2,sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0)
| ~ occurrence_of(sK24,sK22)
| ~ spl25_63 ),
inference(forward_subsumption_resolution,[],[f2334,f252]) ).
fof(f2337,plain,
( ~ occurrence_of(sK24,sK22)
| ~ spl25_63 ),
inference(forward_subsumption_resolution,[],[f2335,f250]) ).
fof(f2339,plain,
( $false
| ~ spl25_63 ),
inference(forward_subsumption_resolution,[],[f2337,f246]) ).
fof(f2340,plain,
~ spl25_63,
inference(avatar_contradiction_clause,[],[f2339]) ).
fof(f2341,plain,
( spl25_74
| ~ spl25_29
| spl25_58
| spl25_88 ),
inference(avatar_split_clause,[],[f2116,f1851,f1487,f892,f1726]) ).
fof(f2347,plain,
( tptp2 = sK16(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))
| ~ spl25_77 ),
inference(forward_subsumption_resolution,[],[f2319,f246]) ).
fof(f2348,plain,
( $false
| spl25_63
| ~ spl25_77 ),
inference(forward_subsumption_resolution,[],[f2347,f1590]) ).
fof(f2349,plain,
( spl25_63
| ~ spl25_77 ),
inference(avatar_contradiction_clause,[],[f2348]) ).
fof(f2396,plain,
( ~ root(sK14(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_81 ),
inference(resolution,[],[f1783,f153]) ).
fof(f2410,plain,
( $false
| ~ spl25_55
| ~ spl25_81 ),
inference(forward_subsumption_resolution,[],[f2396,f1455]) ).
fof(f2411,plain,
( ~ spl25_55
| ~ spl25_81 ),
inference(avatar_contradiction_clause,[],[f2410]) ).
fof(f2424,plain,
( root_occ(sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)),sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))))
| ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ spl25_83 ),
inference(superposition,[],[f207,f1791]) ).
fof(f2445,plain,
( ~ occurrence_of(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24))),tptp0)
| ~ spl25_29
| ~ spl25_83 ),
inference(forward_subsumption_resolution,[],[f2424,f1400]) ).
fof(f2450,plain,
( $false
| ~ spl25_29
| ~ spl25_44
| ~ spl25_83 ),
inference(forward_subsumption_resolution,[],[f2445,f1340]) ).
fof(f2451,plain,
( ~ spl25_29
| ~ spl25_44
| ~ spl25_83 ),
inference(avatar_contradiction_clause,[],[f2450]) ).
fof(f2462,plain,
( ~ leaf(sK15(sK8(tptp0,sK23,sK17(sK19(tptp0,sK23,sK24),sK20(tptp0,sK23,sK24),sK23,tptp0,sK21(tptp0,sK23,sK24)))),tptp0)
| ~ spl25_88 ),
inference(resolution,[],[f1853,f168]) ).
fof(f2473,plain,
( $false
| ~ spl25_43
| ~ spl25_88 ),
inference(forward_subsumption_resolution,[],[f2462,f1335]) ).
fof(f2474,plain,
( ~ spl25_43
| ~ spl25_88 ),
inference(avatar_contradiction_clause,[],[f2473]) ).
cnf(s6,plain,
( ~ spl25_8
| spl25_9 ),
inference(sat_conversion,[],[f496]) ).
cnf(s7,plain,
( ~ spl25_10
| spl25_11 ),
inference(sat_conversion,[],[f512]) ).
cnf(s8,plain,
spl25_8,
inference(sat_conversion,[],[f529]) ).
cnf(s16,plain,
spl25_16,
inference(sat_conversion,[],[f648]) ).
cnf(s18,plain,
( spl25_10
| ~ spl25_16 ),
inference(sat_conversion,[],[f675]) ).
cnf(s38,plain,
( ~ spl25_9
| ~ spl25_42
| spl25_43 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s41,plain,
( spl25_42
| ~ spl25_44 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s42,plain,
( ~ spl25_29
| spl25_44 ),
inference(sat_conversion,[],[f1349]) ).
cnf(s43,plain,
spl25_29,
inference(sat_conversion,[],[f1356]) ).
cnf(s49,plain,
( ~ spl25_44
| ~ spl25_54
| spl25_55 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s72,plain,
( ~ spl25_44
| ~ spl25_74
| spl25_81
| ~ spl25_82
| spl25_83 ),
inference(sat_conversion,[],[f1792]) ).
cnf(s79,plain,
( ~ spl25_44
| spl25_54 ),
inference(sat_conversion,[],[f1910]) ).
cnf(s109,plain,
( ~ spl25_29
| spl25_82 ),
inference(sat_conversion,[],[f2209]) ).
cnf(s114,plain,
( ~ spl25_44
| ~ spl25_58
| spl25_76
| spl25_77 ),
inference(sat_conversion,[],[f2214]) ).
cnf(s119,plain,
( ~ spl25_11
| ~ spl25_76 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s120,plain,
~ spl25_63,
inference(sat_conversion,[],[f2340]) ).
cnf(s121,plain,
( ~ spl25_29
| spl25_58
| spl25_74
| spl25_88 ),
inference(sat_conversion,[],[f2341]) ).
cnf(s124,plain,
( spl25_63
| ~ spl25_77 ),
inference(sat_conversion,[],[f2349]) ).
cnf(s126,plain,
( ~ spl25_55
| ~ spl25_81 ),
inference(sat_conversion,[],[f2411]) ).
cnf(s130,plain,
( ~ spl25_29
| ~ spl25_44
| ~ spl25_83 ),
inference(sat_conversion,[],[f2451]) ).
cnf(s132,plain,
( ~ spl25_43
| ~ spl25_88 ),
inference(sat_conversion,[],[f2474]) ).
cnf(s133,plain,
~ spl25_77,
inference(rat,[],[s124,s120]) ).
cnf(s134,plain,
( ~ spl25_44
| ~ spl25_58
| spl25_76 ),
inference(rat,[],[s114,s133]) ).
cnf(s140,plain,
spl25_82,
inference(rat,[],[s109,s43]) ).
cnf(s142,plain,
spl25_44,
inference(rat,[],[s42,s43]) ).
cnf(s143,plain,
~ spl25_83,
inference(rat,[],[s130,s43,s142]) ).
cnf(s144,plain,
spl25_54,
inference(rat,[],[s79,s142]) ).
cnf(s145,plain,
spl25_55,
inference(rat,[],[s49,s142,s144]) ).
cnf(s146,plain,
~ spl25_81,
inference(rat,[],[s126,s145]) ).
cnf(s147,plain,
~ spl25_74,
inference(rat,[],[s72,s143,s140,s142,s146]) ).
cnf(s148,plain,
spl25_42,
inference(rat,[],[s41,s142]) ).
cnf(s150,plain,
( ~ spl25_9
| spl25_43 ),
inference(rat,[],[s38,s148]) ).
cnf(s153,plain,
spl25_10,
inference(rat,[],[s18,s16]) ).
cnf(s156,plain,
spl25_11,
inference(rat,[],[s7,s153]) ).
cnf(s157,plain,
~ spl25_76,
inference(rat,[],[s119,s156]) ).
cnf(s158,plain,
~ spl25_58,
inference(rat,[],[s134,s142,s157]) ).
cnf(s159,plain,
spl25_88,
inference(rat,[],[s121,s147,s43,s158]) ).
cnf(s161,plain,
~ spl25_43,
inference(rat,[],[s132,s159]) ).
cnf(s165,plain,
~ spl25_9,
inference(rat,[],[s150,s161]) ).
cnf(s171,plain,
$false,
inference(rat,[],[s6,s165,s8]) ).
fof(f2475,plain,
$false,
inference(avatar_sat_refutation,[],[s171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO001+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n020.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 22:16:49 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 8.60/2.08 % (3816889)Detected formulas, will run a generic FOF schedule.
% 8.60/2.08 % (3816996)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=393532406:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.60/2.08 % (3816999)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3289866028:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.60/2.08 % (3816998)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2381247199:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.60/2.08 % (3816997)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=2265714823:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.60/2.08 % (3816995)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=2233949465:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.60/2.08 % (3816998)Refutation not found, incomplete strategy
% 8.60/2.08 % (3816998)------------------------------
% 8.60/2.08 % (3816998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3816998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3816998)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3816998)Termination reason: Refutation not found, incomplete strategy
% 8.60/2.08 % (3816998)Time elapsed: 0.002 s
% 8.60/2.08 % (3816998)Peak memory usage: 88 MB
% 8.60/2.08 % (3816998)Instructions burned: 1 (million)
% 8.60/2.08 % (3816999)Refutation not found, incomplete strategy
% 8.60/2.08 % (3816999)------------------------------
% 8.60/2.08 % (3816999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3816999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3816999)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3816999)Termination reason: Refutation not found, incomplete strategy
% 8.60/2.08 % (3816999)Time elapsed: 0.002 s
% 8.60/2.08 % (3816999)Peak memory usage: 88 MB
% 8.60/2.08 % (3816999)Instructions burned: 1 (million)
% 8.60/2.08 % (3817000)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3404900418:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.60/2.08 % (3817001)dis-21_1_sil=8000:lcm=predicate:random_seed=372996251: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)
% 8.60/2.08 % (3817001)Instruction limit reached!
% 8.60/2.08 % (3817001)------------------------------
% 8.60/2.08 % (3817001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817001)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817001)Termination reason: Instruction limit
% 8.60/2.08 % (3817001)Termination phase: Saturation
% 8.60/2.08 % (3817001)Time elapsed: 0.076 s
% 8.60/2.08 % (3817001)Peak memory usage: 89 MB
% 8.60/2.08 % (3817001)Instructions burned: 129 (million)
% 8.60/2.08 % (3817000)Instruction limit reached!
% 8.60/2.08 % (3817000)------------------------------
% 8.60/2.08 % (3817000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817000)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817000)Termination reason: Instruction limit
% 8.60/2.08 % (3817000)Termination phase: Saturation
% 8.60/2.08 % (3817000)Time elapsed: 0.104 s
% 8.60/2.08 % (3817000)Peak memory usage: 90 MB
% 8.60/2.08 % (3817000)Instructions burned: 140 (million)
% 8.60/2.08 % (3816999)------------------------------
% 8.60/2.08 % (3816999)------------------------------
% 8.60/2.08 % (3817023)lrs+10_1_sil=32000:urr=on:br=off:random_seed=244742432:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.60/2.08 % (3817023)Refutation not found, incomplete strategy
% 8.60/2.08 % (3817023)------------------------------
% 8.60/2.08 % (3817023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817023)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817023)Termination reason: Refutation not found, incomplete strategy
% 8.60/2.08 % (3817023)Time elapsed: 0.002 s
% 8.60/2.08 % (3817023)Peak memory usage: 88 MB
% 8.60/2.08 % (3817023)Instructions burned: 1 (million)
% 8.60/2.08 % (3817022)lrs+10_1_sil=8000:sp=occurrence:random_seed=3285918333:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.60/2.08 % (3816998)------------------------------
% 8.60/2.08 % (3816998)------------------------------
% 8.60/2.08 % (3817024)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2623547316:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 8.60/2.08 % (3817022)Instruction limit reached!
% 8.60/2.08 % (3817022)------------------------------
% 8.60/2.08 % (3817022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817022)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817022)Termination reason: Instruction limit
% 8.60/2.08 % (3817022)Termination phase: Saturation
% 8.60/2.08 % (3817022)Time elapsed: 0.206 s
% 8.60/2.08 % (3817022)Peak memory usage: 90 MB
% 8.60/2.08 % (3817022)Instructions burned: 286 (million)
% 8.60/2.08 % (3817023)------------------------------
% 8.60/2.08 % (3817023)------------------------------
% 8.60/2.08 % (3817024)Instruction limit reached!
% 8.60/2.08 % (3817024)------------------------------
% 8.60/2.08 % (3817024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817024)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817024)Termination reason: Instruction limit
% 8.60/2.08 % (3817024)Termination phase: Saturation
% 8.60/2.08 % (3817024)Time elapsed: 0.122 s
% 8.60/2.08 % (3817024)Peak memory usage: 92 MB
% 8.60/2.08 % (3817024)Instructions burned: 326 (million)
% 8.60/2.08 % (3817027)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=3429260875:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 8.60/2.08 % (3817030)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1197523455:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.60/2.08 % (3817029)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2376225119:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 8.60/2.08 % (3817027)Instruction limit reached!
% 8.60/2.08 % (3817027)------------------------------
% 8.60/2.08 % (3817027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817027)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817027)Termination reason: Instruction limit
% 8.60/2.08 % (3817027)Termination phase: Saturation
% 8.60/2.08 % (3817027)Time elapsed: 0.168 s
% 8.60/2.08 % (3817027)Peak memory usage: 90 MB
% 8.60/2.08 % (3817027)Instructions burned: 248 (million)
% 8.60/2.08 % (3817031)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2352392990:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.60/2.08 % (3816995)First to succeed.
% 8.60/2.08 % (3816995)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3816889"
% 8.60/2.08 % (3817031)Instruction limit reached!
% 8.60/2.08 % (3817031)------------------------------
% 8.60/2.08 % (3817031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817031)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817031)Termination reason: Instruction limit
% 8.60/2.08 % (3817031)Termination phase: Saturation
% 8.60/2.08 % (3817031)Time elapsed: 0.119 s
% 8.60/2.08 % (3817031)Peak memory usage: 90 MB
% 8.60/2.08 % (3817031)Instructions burned: 113 (million)
% 8.60/2.08 % (3817029)Instruction limit reached!
% 8.60/2.08 % (3817029)------------------------------
% 8.60/2.08 % (3817029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.08 % (3817029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.08 % (3817029)CaDiCaL version: 2.1.3
% 8.60/2.08 % (3817029)Termination reason: Instruction limit
% 8.60/2.08 % (3817029)Termination phase: Saturation
% 8.60/2.08 % (3817029)Time elapsed: 0.240 s
% 8.60/2.08 % (3817029)Peak memory usage: 88 MB
% 8.60/2.08 % (3817029)Instructions burned: 294 (million)
% 8.60/2.08 % (3817044)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3900658106:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 8.60/2.08 % (3816995)Refutation found. Thanks to Tanya!
% 8.60/2.08 % SZS status Theorem for theBenchmark
% 8.60/2.08 % SZS output start Proof for theBenchmark
% See solution above
% 9.16/2.31 % (3816995)------------------------------
% 9.16/2.31 % (3816995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.16/2.31 % (3816995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/2.31 % (3816995)CaDiCaL version: 2.1.3
% 9.16/2.31 % (3816995)Termination reason: Refutation
% 9.16/2.31 % (3816995)Time elapsed: 0.780 s
% 9.16/2.31 % (3816995)Peak memory usage: 132 MB
% 9.16/2.31 % (3816995)Instructions burned: 1364 (million)
% 9.16/2.31 % (3816995)------------------------------
% 9.16/2.31 % (3816995)------------------------------
% 9.16/2.31 % (3816889)Success in time 1.206 s
% 9.16/2.31 % Vampire exiting
%------------------------------------------------------------------------------