%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PRO001+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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 9.84s 2.28s
% Output : Refutation 10.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 38
% Syntax : Number of formulae : 288 ( 32 unt; 16 def)
% Number of atoms : 905 ( 112 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1067 ( 450 ~; 462 |; 115 &)
% ( 22 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 17 prp; 0-5 aty)
% Number of functors : 22 ( 22 usr; 7 con; 0-5 aty)
% Number of variables : 476 ( 0 sgn 426 !; 50 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos) ).
fof(f2,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
fof(f3,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(f8,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(f12,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3,X4] :
( subactivity(X3,X0)
& subactivity(X4,X0)
& atocc(X1,X3)
& atocc(X2,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(f15,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(f23,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(f24,axiom,
! [X0,X1] :
( atocc(X0,X1)
<=> ? [X2] :
( subactivity(X1,X2)
& atomic(X2)
& occurrence_of(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_23) ).
fof(f25,axiom,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
=> ( activity_occurrence(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(f26,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_25) ).
fof(f34,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_33) ).
fof(f38,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& leaf_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& subactivity_occurrence(X2,X1)
& root_occ(X3,X1)
& arboreal(X2)
& ~ min_precedes(X3,X2,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_42) ).
fof(f44,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& subactivity_occurrence(X2,X1)
& leaf_occ(X3,X1)
& arboreal(X2)
& ~ min_precedes(X2,X3,X0) )
=> X3 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_43) ).
fof(f47,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> arboreal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_46) ).
fof(f50,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp3)
| occurrence_of(X2,tptp2) )
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_49) ).
fof(f64,axiom,
! [X0,X1,X2,X3,X4] :
( send_message(X0,X1,X2,X3,X4)
=> ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_63) ).
fof(f65,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( send_message(X0,X1,X2,X3,X4)
& occurrence_of(X5,X0) )
=> min_precedes(X3,X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_64) ).
fof(f69,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( transmit_message(X0,X1,X2,X3,X4)
& occurrence_of(X5,X0) )
=> ? [X6,X7] :
( send_message(X6,X1,X2,X3,X4)
& occurrence_of(X7,X6)
& root_occ(X7,X5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_68) ).
fof(f70,axiom,
! [X0,X1,X2] :
( tptp1(X0,X1,X2)
=> ( activity(X0)
& ~ atomic(X0)
& ~ atomic(X1)
& root(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_69) ).
fof(f71,axiom,
! [X0,X1,X2,X3] :
( ( tptp1(X0,X1,X2)
& occurrence_of(X3,X0) )
=> ? [X4,X5,X6,X7] :
( transmit_message(X4,X5,X6,X2,X1)
& occurrence_of(X7,X4)
& subactivity_occurrence(X7,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_70) ).
fof(f73,conjecture,
~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f74,negated_conjecture,
~ ~ ? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(negated_conjecture,[status(cth)],[f73]) ).
fof(f75,plain,
? [X0,X1,X2] :
( tptp1(X0,tptp0,X1)
& occurrence_of(X2,X0) ),
inference(flattening,[],[f74]) ).
fof(f76,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f77,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f78,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f3]) ).
fof(f79,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f78]) ).
fof(f86,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f90,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( subactivity(X3,X0)
& subactivity(X4,X0)
& atocc(X1,X3)
& atocc(X2,X4) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f93,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f15]) ).
fof(f104,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ! [X3] :
( ~ min_precedes(X0,X3,X2)
| ~ min_precedes(X3,X1,X2) ) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f105,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f106,plain,
! [X0,X1,X2] :
( ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f125,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f126,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f125]) ).
fof(f135,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ root_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X3,X2,X0) ),
inference(ennf_transformation,[],[f43]) ).
fof(f136,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ root_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X3,X2,X0) ),
inference(flattening,[],[f135]) ).
fof(f137,plain,
! [X0,X1,X2,X3] :
( X3 = X2
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| ~ leaf_occ(X3,X1)
| ~ arboreal(X2)
| min_precedes(X2,X3,X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f138,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,[],[f137]) ).
fof(f142,plain,
! [X0,X1,X2] :
( arboreal(X0)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f47]) ).
fof(f147,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,[],[f50]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4] :
( ( X0 != tptp4
& X0 != tptp3
& X0 != tptp2 )
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(ennf_transformation,[],[f64]) ).
fof(f150,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,[],[f65]) ).
fof(f151,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,[],[f150]) ).
fof(f154,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,[],[f69]) ).
fof(f155,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,[],[f154]) ).
fof(f156,plain,
! [X0,X1,X2] :
( ( activity(X0)
& ~ atomic(X0)
& ~ atomic(X1)
& root(X2,X1) )
| ~ tptp1(X0,X1,X2) ),
inference(ennf_transformation,[],[f70]) ).
fof(f157,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,[],[f71]) ).
fof(f158,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,[],[f157]) ).
fof(f159,plain,
! [X0] :
( ( activity(sK0(X0))
& occurrence_of(X0,sK0(X0)) )
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0(X0))],[f77]) ).
fof(f160,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f86]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ( subactivity(sK1(X0,X1,X2),X0)
& subactivity(sK2(X0,X1,X2),X0)
& atocc(X1,sK1(X0,X1,X2))
& atocc(X2,sK2(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X3,sK1(X0,X1,X2)),skolemize(X4,sK2(X0,X1,X2))],[f90]) ).
fof(f170,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,[],[f104]) ).
fof(f171,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,[],[f170]) ).
fof(f172,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,[],[f171]) ).
fof(f173,plain,
! [X0,X1,X2] :
( ( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK7(X0,X1,X2),X2)
& min_precedes(sK7(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,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f172]) ).
fof(f174,plain,
! [X0,X1] :
( ( atocc(X0,X1)
| ! [X2] :
( ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X0,X2) ) )
& ( ? [X2] :
( subactivity(X1,X2)
& atomic(X2)
& occurrence_of(X0,X2) )
| ~ atocc(X0,X1) ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f175,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,[],[f174]) ).
fof(f176,plain,
! [X0,X1] :
( ( atocc(X0,X1)
| ! [X2] :
( ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X0,X2) ) )
& ( ( subactivity(X1,sK8(X0,X1))
& atomic(sK8(X0,X1))
& occurrence_of(X0,sK8(X0,X1)) )
| ~ atocc(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1))],[f175]) ).
fof(f177,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK9(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK9(X0,X1,X2))
& subactivity_occurrence(X2,sK9(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1,X2))],[f106]) ).
fof(f181,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) )
| ~ root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f182,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,[],[f181]) ).
fof(f183,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK13(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK13(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1))],[f182]) ).
fof(f188,plain,
! [X0] :
( ( occurrence_of(sK16(X0),tptp4)
& root_occ(sK16(X0),X0)
& ( occurrence_of(sK17(X0),tptp3)
| occurrence_of(sK17(X0),tptp2) )
& leaf_occ(sK17(X0),X0)
& next_subocc(sK16(X0),sK17(X0),tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X1,sK16(X0)),skolemize(X2,sK17(X0))],[f147]) ).
fof(f189,plain,
! [X0,X1,X2,X3,X4,X5] :
( ( send_message(sK18(X1,X2,X3,X4,X5),X1,X2,X3,X4)
& occurrence_of(sK19(X1,X2,X3,X4,X5),sK18(X1,X2,X3,X4,X5))
& root_occ(sK19(X1,X2,X3,X4,X5),X5) )
| ~ transmit_message(X0,X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19]),skolemize(X6,sK18(X1,X2,X3,X4,X5)),skolemize(X7,sK19(X1,X2,X3,X4,X5))],[f155]) ).
fof(f190,plain,
! [X0,X1,X2,X3] :
( ( transmit_message(sK20(X1,X2,X3),sK21(X1,X2,X3),sK22(X1,X2,X3),X2,X1)
& occurrence_of(sK23(X1,X2,X3),sK20(X1,X2,X3))
& subactivity_occurrence(sK23(X1,X2,X3),X3) )
| ~ tptp1(X0,X1,X2)
| ~ occurrence_of(X3,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21,sK22,sK23]),skolemize(X4,sK20(X1,X2,X3)),skolemize(X5,sK21(X1,X2,X3)),skolemize(X6,sK22(X1,X2,X3)),skolemize(X7,sK23(X1,X2,X3))],[f158]) ).
fof(f191,plain,
( tptp1(sK24,tptp0,sK25)
& occurrence_of(sK26,sK24) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26]),skolemize(X0,sK24),skolemize(X1,sK25),skolemize(X2,sK26)],[f75]) ).
fof(f192,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f76]) ).
fof(f194,plain,
! [X0] :
( occurrence_of(X0,sK0(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f159]) ).
fof(f196,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f79]) ).
fof(f202,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f160]) ).
fof(f208,plain,
! [X2,X0,X1] :
( atocc(X2,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f163]) ).
fof(f216,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f227,plain,
! [X2,X0,X1,X4] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X4,X1,X2)
| ~ min_precedes(X0,X4,X2) ),
inference(cnf_transformation,[],[f173]) ).
fof(f231,plain,
! [X0,X1] :
( occurrence_of(X0,sK8(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f176]) ).
fof(f232,plain,
! [X0,X1] :
( atomic(sK8(X0,X1))
| ~ atocc(X0,X1) ),
inference(cnf_transformation,[],[f176]) ).
fof(f236,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f237,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f238,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK9(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f239,plain,
! [X2,X0,X1] :
( occurrence_of(sK9(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f251,plain,
! [X0,X1] :
( ~ root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(cnf_transformation,[],[f183]) ).
fof(f260,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f265,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X3,X1)
| ~ occurrence_of(X1,X0)
| ~ subactivity_occurrence(X2,X1)
| X2 = X3
| ~ arboreal(X2)
| min_precedes(X3,X2,X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f266,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,[],[f138]) ).
fof(f271,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| arboreal(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f274,plain,
! [X0] :
( next_subocc(sK16(X0),sK17(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f275,plain,
! [X0] :
( leaf_occ(sK17(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f276,plain,
! [X0] :
( occurrence_of(sK17(X0),tptp2)
| occurrence_of(sK17(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f277,plain,
! [X0] :
( root_occ(sK16(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f188]) ).
fof(f295,plain,
! [X2,X3,X0,X1,X4] :
( tptp2 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f149]) ).
fof(f296,plain,
! [X2,X3,X0,X1,X4] :
( tptp3 != X0
| ~ send_message(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f149]) ).
fof(f298,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,[],[f151]) ).
fof(f305,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| root_occ(sK19(X1,X2,X3,X4,X5),X5)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f306,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| occurrence_of(sK19(X1,X2,X3,X4,X5),sK18(X1,X2,X3,X4,X5))
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f307,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ transmit_message(X0,X1,X2,X3,X4)
| send_message(sK18(X1,X2,X3,X4,X5),X1,X2,X3,X4)
| ~ occurrence_of(X5,X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f308,plain,
! [X2,X0,X1] :
( ~ tptp1(X0,X1,X2)
| root(X2,X1) ),
inference(cnf_transformation,[],[f156]) ).
fof(f313,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| occurrence_of(sK23(X1,X2,X3),sK20(X1,X2,X3))
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f190]) ).
fof(f314,plain,
! [X2,X3,X0,X1] :
( ~ tptp1(X0,X1,X2)
| transmit_message(sK20(X1,X2,X3),sK21(X1,X2,X3),sK22(X1,X2,X3),X2,X1)
| ~ occurrence_of(X3,X0) ),
inference(cnf_transformation,[],[f190]) ).
fof(f316,plain,
occurrence_of(sK26,sK24),
inference(cnf_transformation,[],[f191]) ).
fof(f317,plain,
tptp1(sK24,tptp0,sK25),
inference(cnf_transformation,[],[f191]) ).
fof(f319,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp3,X1,X2,X3,X4),
inference(equality_resolution,[],[f296]) ).
fof(f320,plain,
! [X2,X3,X1,X4] : ~ send_message(tptp2,X1,X2,X3,X4),
inference(equality_resolution,[],[f295]) ).
fof(f321,plain,
! [X0] :
( occurrence_of(sK23(tptp0,sK25,X0),sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f313,f317]) ).
fof(f322,plain,
! [X0] :
( transmit_message(sK20(tptp0,sK25,X0),sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0)
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f314,f317]) ).
fof(f324,plain,
! [X0,X1] :
( ~ occurrence_of(sK23(tptp0,sK25,X0),X1)
| sK20(tptp0,sK25,X0) = X1
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f196,f321]) ).
fof(f331,plain,
root(sK25,tptp0),
inference(resolution,[],[f308,f317]) ).
fof(f336,plain,
! [X2,X0,X1] :
( min_precedes(sK16(X0),X2,X1)
| ~ subactivity_occurrence(X2,X0)
| sK16(X0) = X2
| ~ arboreal(X2)
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f265,f277]) ).
fof(f341,plain,
! [X2,X0,X1] :
( min_precedes(X2,sK17(X0),X1)
| ~ subactivity_occurrence(X2,X0)
| sK17(X0) = X2
| ~ arboreal(X2)
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f266,f275]) ).
fof(f354,plain,
! [X0,X1] :
( ~ occurrence_of(sK17(X0),X1)
| ~ occurrence_of(X0,tptp0)
| occurrence_of(sK17(X0),tptp3)
| tptp2 = X1 ),
inference(resolution,[],[f276,f196]) ).
fof(f365,plain,
! [X0,X1] :
( ~ min_precedes(sK16(X1),X0,tptp0)
| ~ min_precedes(X0,sK17(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f227,f274]) ).
fof(f371,plain,
! [X0] :
( activity_occurrence(sK17(X0))
| occurrence_of(sK17(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f192,f276]) ).
fof(f372,plain,
! [X0] :
( activity_occurrence(sK23(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f192,f321]) ).
fof(f374,plain,
! [X0] :
( activity_occurrence(sK17(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f371,f192]) ).
fof(f393,plain,
! [X0,X1] :
( occurrence_of(sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1),sK18(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1))
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f306,f322]) ).
fof(f395,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK20(tptp0,sK25,X1))
| ~ occurrence_of(X1,sK24)
| activity_occurrence(sK19(sK21(tptp0,sK25,X1),sK22(tptp0,sK25,X1),sK25,tptp0,X0)) ),
inference(resolution,[],[f393,f192]) ).
fof(f397,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK19(sK21(tptp0,sK25,X1),sK22(tptp0,sK25,X1),sK25,tptp0,X0),X2)
| ~ occurrence_of(X1,sK24)
| ~ occurrence_of(X0,sK20(tptp0,sK25,X1))
| sK18(sK21(tptp0,sK25,X1),sK22(tptp0,sK25,X1),sK25,tptp0,X0) = X2 ),
inference(resolution,[],[f393,f196]) ).
fof(f403,plain,
! [X0,X1] :
( ~ min_precedes(X0,sK17(X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| sK16(X1) = X0
| ~ arboreal(X0)
| ~ occurrence_of(X1,tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(resolution,[],[f365,f336]) ).
fof(f404,plain,
! [X0,X1] :
( ~ min_precedes(X0,sK17(X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| sK16(X1) = X0
| ~ arboreal(X0) ),
inference(duplicate_literal_removal,[],[f403]) ).
fof(f408,plain,
! [X0,X1] :
( ~ min_precedes(X0,sK17(X1),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| sK16(X1) = X0 ),
inference(forward_subsumption_resolution,[],[f404,f271]) ).
fof(f441,plain,
! [X0,X1] :
( ~ occurrence_of(X0,tptp0)
| ~ subactivity_occurrence(X1,X0)
| sK16(X0) = X1
| ~ subactivity_occurrence(X1,X0)
| sK17(X0) = X1
| ~ arboreal(X1)
| ~ occurrence_of(X0,tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f408,f341]) ).
fof(f448,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| ~ occurrence_of(X0,tptp0)
| sK16(X0) = X1
| sK17(X0) = X1
| ~ arboreal(X1) ),
inference(duplicate_literal_removal,[],[f441]) ).
fof(f452,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK9(X0,X1,X2),tptp0)
| sK16(sK9(X0,X1,X2)) = X2
| sK17(sK9(X0,X1,X2)) = X2
| ~ arboreal(X2)
| ~ min_precedes(X1,X2,X0) ),
inference(resolution,[],[f448,f237]) ).
fof(f453,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK9(X0,X1,X2),tptp0)
| sK16(sK9(X0,X1,X2)) = X1
| sK17(sK9(X0,X1,X2)) = X1
| ~ arboreal(X1)
| ~ min_precedes(X1,X2,X0) ),
inference(resolution,[],[f448,f238]) ).
fof(f459,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK9(X0,X1,X2),tptp0)
| sK16(sK9(X0,X1,X2)) = X1
| sK17(sK9(X0,X1,X2)) = X1
| ~ min_precedes(X1,X2,X0) ),
inference(forward_subsumption_resolution,[],[f453,f271]) ).
fof(f460,plain,
! [X0,X1] :
( sK16(sK9(tptp0,X0,X1)) = X0
| sK17(sK9(tptp0,X0,X1)) = X0
| ~ min_precedes(X0,X1,tptp0)
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f459,f239]) ).
fof(f461,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| sK17(sK9(tptp0,X0,X1)) = X0
| sK16(sK9(tptp0,X0,X1)) = X0 ),
inference(duplicate_literal_removal,[],[f460]) ).
fof(f471,plain,
! [X0,X1] :
( sK16(sK9(tptp0,X0,X1)) = X1
| sK17(sK9(tptp0,X0,X1)) = X1
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,tptp0)
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f452,f239]) ).
fof(f472,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| sK17(sK9(tptp0,X0,X1)) = X1
| ~ arboreal(X1)
| sK16(sK9(tptp0,X0,X1)) = X1 ),
inference(duplicate_literal_removal,[],[f471]) ).
fof(f476,plain,
! [X0,X1] :
( sK17(sK9(tptp0,sK16(X0),X1)) = X1
| ~ arboreal(X1)
| sK16(sK9(tptp0,sK16(X0),X1)) = X1
| ~ subactivity_occurrence(X1,X0)
| sK16(X0) = X1
| ~ arboreal(X1)
| ~ occurrence_of(X0,tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f472,f336]) ).
fof(f477,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X1,X0)
| ~ arboreal(X1)
| sK16(sK9(tptp0,sK16(X0),X1)) = X1
| sK17(sK9(tptp0,sK16(X0),X1)) = X1
| sK16(X0) = X1
| ~ occurrence_of(X0,tptp0) ),
inference(duplicate_literal_removal,[],[f476]) ).
fof(f521,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK9(X1,X2,X0),tptp0)
| sK16(sK9(tptp0,sK16(sK9(X1,X2,X0)),X0)) = X0
| sK17(sK9(tptp0,sK16(sK9(X1,X2,X0)),X0)) = X0
| sK16(sK9(X1,X2,X0)) = X0
| ~ arboreal(X0)
| ~ min_precedes(X2,X0,X1) ),
inference(resolution,[],[f477,f237]) ).
fof(f541,plain,
! [X0,X1] :
( send_message(sK18(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1),sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0)
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f307,f322]) ).
fof(f542,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X2,sK18(sK21(tptp0,sK25,X1),sK22(tptp0,sK25,X1),sK25,tptp0,X0))
| ~ occurrence_of(X1,sK24)
| min_precedes(sK25,X2,tptp0)
| ~ occurrence_of(X0,sK20(tptp0,sK25,X1)) ),
inference(resolution,[],[f541,f298]) ).
fof(f559,plain,
! [X0,X1] :
( ~ occurrence_of(X0,sK24)
| min_precedes(sK25,sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1),tptp0)
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f542,f393]) ).
fof(f560,plain,
! [X0,X1] :
( min_precedes(sK25,sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1),tptp0)
| ~ occurrence_of(X0,sK24)
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0)) ),
inference(duplicate_literal_removal,[],[f559]) ).
fof(f562,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24)
| sK25 = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1)))
| sK25 = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1))) ),
inference(resolution,[],[f560,f461]) ).
fof(f567,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,sK24)
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X2,tptp0)
| ~ leaf_occ(sK25,X2) ),
inference(resolution,[],[f560,f260]) ).
fof(f577,definition,
( spl27_6
<=> ! [X0,X1] :
( ~ occurrence_of(X0,sK24)
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl27_6])],[avatar_definition]) ).
fof(f578,plain,
( ! [X0,X1] :
( ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) )
| ~ spl27_6 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f581,definition,
( spl27_7
<=> ! [X2] :
( ~ occurrence_of(X2,tptp0)
| ~ leaf_occ(sK25,X2) ) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
fof(f582,plain,
( ! [X2] :
( ~ leaf_occ(sK25,X2)
| ~ occurrence_of(X2,tptp0) )
| ~ spl27_7 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( spl27_7
| spl27_6 ),
inference(avatar_split_clause,[],[f567,f577,f581]) ).
fof(f590,plain,
( ! [X0] :
( ~ occurrence_of(X0,sK24)
| ~ occurrence_of(X0,sK24) )
| ~ spl27_6 ),
inference(resolution,[],[f578,f321]) ).
fof(f591,plain,
( ! [X0] : ~ occurrence_of(X0,sK24)
| ~ spl27_6 ),
inference(duplicate_literal_removal,[],[f590]) ).
fof(f593,plain,
( $false
| ~ spl27_6 ),
inference(resolution,[],[f591,f316]) ).
fof(f594,plain,
~ spl27_6,
inference(avatar_contradiction_clause,[],[f593]) ).
fof(f674,plain,
! [X0] :
( ~ activity_occurrence(sK17(X0))
| ~ occurrence_of(X0,tptp0)
| occurrence_of(sK17(X0),tptp3)
| tptp2 = sK0(sK17(X0)) ),
inference(resolution,[],[f194,f354]) ).
fof(f675,plain,
! [X0,X1] :
( ~ activity_occurrence(sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1))
| ~ occurrence_of(X0,sK24)
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| sK18(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1) = sK0(sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1)) ),
inference(resolution,[],[f194,f397]) ).
fof(f676,plain,
! [X0] :
( ~ activity_occurrence(sK23(tptp0,sK25,X0))
| sK20(tptp0,sK25,X0) = sK0(sK23(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f194,f324]) ).
fof(f679,plain,
! [X0] :
( ~ occurrence_of(X0,sK24)
| sK20(tptp0,sK25,X0) = sK0(sK23(tptp0,sK25,X0)) ),
inference(forward_subsumption_resolution,[],[f676,f372]) ).
fof(f680,plain,
! [X0,X1] :
( ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24)
| sK18(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1) = sK0(sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1)) ),
inference(forward_subsumption_resolution,[],[f675,f395]) ).
fof(f681,plain,
! [X0] :
( occurrence_of(sK17(X0),tptp3)
| ~ occurrence_of(X0,tptp0)
| tptp2 = sK0(sK17(X0)) ),
inference(forward_subsumption_resolution,[],[f674,f374]) ).
fof(f693,plain,
sK20(tptp0,sK25,sK26) = sK0(sK23(tptp0,sK25,sK26)),
inference(resolution,[],[f679,f316]) ).
fof(f694,plain,
( occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| ~ activity_occurrence(sK23(tptp0,sK25,sK26)) ),
inference(superposition,[],[f194,f693]) ).
fof(f696,definition,
( spl27_9
<=> activity_occurrence(sK23(tptp0,sK25,sK26)) ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
fof(f698,plain,
( ~ activity_occurrence(sK23(tptp0,sK25,sK26))
| spl27_9 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f700,definition,
( spl27_10
<=> occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26)) ),
introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition]) ).
fof(f702,plain,
( occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| ~ spl27_10 ),
inference(avatar_component_clause,[],[f700]) ).
fof(f703,plain,
( ~ spl27_9
| spl27_10 ),
inference(avatar_split_clause,[],[f694,f700,f696]) ).
fof(f716,plain,
! [X0] :
( ~ occurrence_of(X0,sK24)
| sK18(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,sK23(tptp0,sK25,X0)) = sK0(sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,sK23(tptp0,sK25,X0)))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f680,f321]) ).
fof(f717,plain,
! [X0] :
( ~ occurrence_of(X0,sK24)
| sK18(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,sK23(tptp0,sK25,X0)) = sK0(sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,sK23(tptp0,sK25,X0))) ),
inference(duplicate_literal_removal,[],[f716]) ).
fof(f719,plain,
sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK0(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))),
inference(resolution,[],[f717,f316]) ).
fof(f720,plain,
( occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))
| ~ activity_occurrence(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))) ),
inference(superposition,[],[f194,f719]) ).
fof(f722,definition,
( spl27_11
<=> activity_occurrence(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
fof(f724,plain,
( ~ activity_occurrence(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))
| spl27_11 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f726,definition,
( spl27_12
<=> occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))) ),
introduced(definition,[new_symbols(definition,[spl27_12])],[avatar_definition]) ).
fof(f728,plain,
( occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))
| ~ spl27_12 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f729,plain,
( ~ spl27_11
| spl27_12 ),
inference(avatar_split_clause,[],[f720,f726,f722]) ).
fof(f761,definition,
( spl27_16
<=> occurrence_of(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))),tptp0) ),
introduced(definition,[new_symbols(definition,[spl27_16])],[avatar_definition]) ).
fof(f762,plain,
( ~ occurrence_of(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))),tptp0)
| spl27_16 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f763,plain,
( occurrence_of(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))),tptp0)
| ~ spl27_16 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f765,plain,
( ~ occurrence_of(sK26,sK24)
| spl27_9 ),
inference(resolution,[],[f372,f698]) ).
fof(f766,plain,
( $false
| spl27_9 ),
inference(forward_subsumption_resolution,[],[f765,f316]) ).
fof(f767,plain,
spl27_9,
inference(avatar_contradiction_clause,[],[f766]) ).
fof(f824,plain,
! [X0,X1] :
( root_occ(sK19(sK21(tptp0,sK25,X0),sK22(tptp0,sK25,X0),sK25,tptp0,X1),X1)
| ~ occurrence_of(X1,sK20(tptp0,sK25,X0))
| ~ occurrence_of(X0,sK24) ),
inference(resolution,[],[f305,f322]) ).
fof(f853,definition,
( spl27_19
<=> root_occ(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),sK23(tptp0,sK25,sK26)) ),
introduced(definition,[new_symbols(definition,[spl27_19])],[avatar_definition]) ).
fof(f854,plain,
( root_occ(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),sK23(tptp0,sK25,sK26))
| ~ spl27_19 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f855,plain,
( ~ root_occ(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),sK23(tptp0,sK25,sK26))
| spl27_19 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f861,plain,
( ~ occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| ~ occurrence_of(sK26,sK24)
| spl27_19 ),
inference(resolution,[],[f855,f824]) ).
fof(f862,plain,
( ~ occurrence_of(sK26,sK24)
| spl27_19 ),
inference(forward_subsumption_resolution,[],[f861,f321]) ).
fof(f863,plain,
( $false
| spl27_19 ),
inference(forward_subsumption_resolution,[],[f862,f316]) ).
fof(f864,plain,
spl27_19,
inference(avatar_contradiction_clause,[],[f863]) ).
fof(f865,plain,
( subactivity_occurrence(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),sK23(tptp0,sK25,sK26))
| ~ spl27_19 ),
inference(resolution,[],[f854,f251]) ).
fof(f885,plain,
( activity_occurrence(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))
| ~ spl27_19 ),
inference(resolution,[],[f865,f236]) ).
fof(f901,plain,
( $false
| spl27_11
| ~ spl27_19 ),
inference(forward_subsumption_resolution,[],[f885,f724]) ).
fof(f902,plain,
( spl27_11
| ~ spl27_19 ),
inference(avatar_contradiction_clause,[],[f901]) ).
fof(f910,plain,
( ! [X0] :
( ~ occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),X0)
| sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = X0 )
| ~ spl27_12 ),
inference(resolution,[],[f728,f196]) ).
fof(f1124,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| ~ atomic(sK8(X0,X1))
| arboreal(X0) ),
inference(resolution,[],[f231,f202]) ).
fof(f1133,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| arboreal(X0) ),
inference(forward_subsumption_resolution,[],[f1124,f232]) ).
fof(f1134,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X0,X2)
| arboreal(X0) ),
inference(resolution,[],[f1133,f208]) ).
fof(f1200,plain,
! [X0,X1] :
( sK16(sK9(tptp0,sK16(sK9(tptp0,X0,X1)),X1)) = X1
| sK17(sK9(tptp0,sK16(sK9(tptp0,X0,X1)),X1)) = X1
| sK16(sK9(tptp0,X0,X1)) = X1
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,tptp0)
| ~ min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f521,f239]) ).
fof(f1201,plain,
! [X0,X1] :
( sK16(sK9(tptp0,sK16(sK9(tptp0,X0,X1)),X1)) = X1
| sK17(sK9(tptp0,sK16(sK9(tptp0,X0,X1)),X1)) = X1
| sK16(sK9(tptp0,X0,X1)) = X1
| ~ arboreal(X1)
| ~ min_precedes(X0,X1,tptp0) ),
inference(duplicate_literal_removal,[],[f1200]) ).
fof(f1202,plain,
! [X0,X1] :
( ~ min_precedes(X0,X1,tptp0)
| sK17(sK9(tptp0,sK16(sK9(tptp0,X0,X1)),X1)) = X1
| sK16(sK9(tptp0,X0,X1)) = X1
| sK16(sK9(tptp0,sK16(sK9(tptp0,X0,X1)),X1)) = X1 ),
inference(forward_subsumption_resolution,[],[f1201,f1134]) ).
fof(f1434,plain,
( ~ occurrence_of(sK26,sK24)
| sK25 = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK25 = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_10 ),
inference(resolution,[],[f562,f702]) ).
fof(f1436,plain,
( sK25 = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK25 = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_10 ),
inference(forward_subsumption_resolution,[],[f1434,f316]) ).
fof(f1438,definition,
( spl27_29
<=> sK25 = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))) ),
introduced(definition,[new_symbols(definition,[spl27_29])],[avatar_definition]) ).
fof(f1440,plain,
( sK25 = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_29 ),
inference(avatar_component_clause,[],[f1438]) ).
fof(f1442,definition,
( spl27_30
<=> sK25 = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))) ),
introduced(definition,[new_symbols(definition,[spl27_30])],[avatar_definition]) ).
fof(f1444,plain,
( sK25 = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_30 ),
inference(avatar_component_clause,[],[f1442]) ).
fof(f1445,plain,
( spl27_29
| spl27_30
| ~ spl27_10 ),
inference(avatar_split_clause,[],[f1436,f700,f1442,f1438]) ).
fof(f1536,plain,
( ~ min_precedes(sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp0)
| spl27_16 ),
inference(resolution,[],[f762,f239]) ).
fof(f1537,plain,
( ~ occurrence_of(sK26,sK24)
| ~ occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| spl27_16 ),
inference(resolution,[],[f1536,f560]) ).
fof(f1538,plain,
( ~ occurrence_of(sK26,sK24)
| spl27_16 ),
inference(forward_subsumption_resolution,[],[f1537,f321]) ).
fof(f1539,plain,
( $false
| spl27_16 ),
inference(forward_subsumption_resolution,[],[f1538,f316]) ).
fof(f1540,plain,
spl27_16,
inference(avatar_contradiction_clause,[],[f1539]) ).
fof(f1542,plain,
( leaf_occ(sK25,sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ occurrence_of(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))),tptp0)
| ~ spl27_30 ),
inference(superposition,[],[f275,f1444]) ).
fof(f1589,plain,
( ~ occurrence_of(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))),tptp0)
| ~ spl27_7
| ~ spl27_30 ),
inference(forward_subsumption_resolution,[],[f1542,f582]) ).
fof(f1628,plain,
( $false
| ~ spl27_7
| ~ spl27_16
| ~ spl27_30 ),
inference(forward_subsumption_resolution,[],[f1589,f763]) ).
fof(f1629,plain,
( ~ spl27_7
| ~ spl27_16
| ~ spl27_30 ),
inference(avatar_contradiction_clause,[],[f1628]) ).
fof(f1840,definition,
( spl27_73
<=> min_precedes(sK25,sK25,tptp0) ),
introduced(definition,[new_symbols(definition,[spl27_73])],[avatar_definition]) ).
fof(f1841,plain,
( min_precedes(sK25,sK25,tptp0)
| ~ spl27_73 ),
inference(avatar_component_clause,[],[f1840]) ).
fof(f1842,plain,
( ~ min_precedes(sK25,sK25,tptp0)
| spl27_73 ),
inference(avatar_component_clause,[],[f1840]) ).
fof(f2318,definition,
( spl27_114
<=> min_precedes(sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl27_114])],[avatar_definition]) ).
fof(f2319,plain,
( min_precedes(sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp0)
| ~ spl27_114 ),
inference(avatar_component_clause,[],[f2318]) ).
fof(f2320,plain,
( ~ min_precedes(sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp0)
| spl27_114 ),
inference(avatar_component_clause,[],[f2318]) ).
fof(f2325,plain,
( ~ occurrence_of(sK26,sK24)
| ~ occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| spl27_114 ),
inference(resolution,[],[f2320,f560]) ).
fof(f2326,plain,
( ~ occurrence_of(sK26,sK24)
| spl27_114 ),
inference(forward_subsumption_resolution,[],[f2325,f321]) ).
fof(f2327,plain,
( $false
| spl27_114 ),
inference(forward_subsumption_resolution,[],[f2326,f316]) ).
fof(f2328,plain,
spl27_114,
inference(avatar_contradiction_clause,[],[f2327]) ).
fof(f2336,plain,
( sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))),sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK16(sK9(tptp0,sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))),sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_114 ),
inference(resolution,[],[f2319,f1202]) ).
fof(f2356,plain,
( sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK16(sK9(tptp0,sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))),sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_29
| ~ spl27_114 ),
inference(forward_demodulation,[],[f2336,f1440]) ).
fof(f2359,plain,
( sK25 = sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK16(sK9(tptp0,sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))),sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_29
| ~ spl27_114 ),
inference(forward_demodulation,[],[f2356,f1440]) ).
fof(f2360,plain,
( sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK16(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| sK25 = sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_29
| ~ spl27_114 ),
inference(forward_demodulation,[],[f2359,f1440]) ).
fof(f2361,plain,
( sK25 = sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| sK25 = sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_29
| ~ spl27_114 ),
inference(forward_demodulation,[],[f2360,f1440]) ).
fof(f2362,plain,
( sK25 = sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_29
| ~ spl27_114 ),
inference(duplicate_literal_removal,[],[f2361]) ).
fof(f2364,definition,
( spl27_116
<=> sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))) ),
introduced(definition,[new_symbols(definition,[spl27_116])],[avatar_definition]) ).
fof(f2366,plain,
( sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) = sK17(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))))
| ~ spl27_116 ),
inference(avatar_component_clause,[],[f2364]) ).
fof(f2368,definition,
( spl27_117
<=> sK25 = sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) ),
introduced(definition,[new_symbols(definition,[spl27_117])],[avatar_definition]) ).
fof(f2370,plain,
( sK25 = sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| ~ spl27_117 ),
inference(avatar_component_clause,[],[f2368]) ).
fof(f2371,plain,
( spl27_116
| spl27_117
| ~ spl27_29
| ~ spl27_114 ),
inference(avatar_split_clause,[],[f2362,f2318,f1438,f2368,f2364]) ).
fof(f2406,plain,
( occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp3)
| ~ occurrence_of(sK9(tptp0,sK25,sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))),tptp0)
| tptp2 = sK0(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))
| ~ spl27_116 ),
inference(superposition,[],[f681,f2366]) ).
fof(f2409,plain,
( occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp3)
| tptp2 = sK0(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)))
| ~ spl27_16
| ~ spl27_116 ),
inference(forward_subsumption_resolution,[],[f2406,f763]) ).
fof(f2436,plain,
( tptp2 = sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp3)
| ~ spl27_16
| ~ spl27_116 ),
inference(forward_demodulation,[],[f2409,f719]) ).
fof(f2458,definition,
( spl27_121
<=> occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp3) ),
introduced(definition,[new_symbols(definition,[spl27_121])],[avatar_definition]) ).
fof(f2460,plain,
( occurrence_of(sK19(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)),tptp3)
| ~ spl27_121 ),
inference(avatar_component_clause,[],[f2458]) ).
fof(f2480,definition,
( spl27_126
<=> tptp2 = sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26)) ),
introduced(definition,[new_symbols(definition,[spl27_126])],[avatar_definition]) ).
fof(f2482,plain,
( tptp2 = sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| ~ spl27_126 ),
inference(avatar_component_clause,[],[f2480]) ).
fof(f2534,plain,
( min_precedes(sK25,sK25,tptp0)
| ~ occurrence_of(sK26,sK24)
| ~ occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| ~ spl27_117 ),
inference(superposition,[],[f560,f2370]) ).
fof(f2546,plain,
( min_precedes(sK25,sK25,tptp0)
| ~ occurrence_of(sK26,sK24)
| ~ spl27_117 ),
inference(forward_subsumption_resolution,[],[f2534,f321]) ).
fof(f2571,plain,
( ~ occurrence_of(sK26,sK24)
| spl27_73
| ~ spl27_117 ),
inference(forward_subsumption_resolution,[],[f2546,f1842]) ).
fof(f2581,plain,
( $false
| spl27_73
| ~ spl27_117 ),
inference(forward_subsumption_resolution,[],[f2571,f316]) ).
fof(f2582,plain,
( spl27_73
| ~ spl27_117 ),
inference(avatar_contradiction_clause,[],[f2581]) ).
fof(f2662,plain,
( spl27_121
| spl27_126
| ~ spl27_16
| ~ spl27_116 ),
inference(avatar_split_clause,[],[f2436,f2364,f761,f2480,f2458]) ).
fof(f2718,plain,
( ~ root(sK25,tptp0)
| ~ spl27_73 ),
inference(resolution,[],[f1841,f216]) ).
fof(f2735,plain,
( $false
| ~ spl27_73 ),
inference(forward_subsumption_resolution,[],[f2718,f331]) ).
fof(f2736,plain,
~ spl27_73,
inference(avatar_contradiction_clause,[],[f2735]) ).
fof(f2888,plain,
( tptp3 = sK18(sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0,sK23(tptp0,sK25,sK26))
| ~ spl27_12
| ~ spl27_121 ),
inference(resolution,[],[f2460,f910]) ).
fof(f3180,plain,
( send_message(tptp3,sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0)
| ~ occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| ~ occurrence_of(sK26,sK24)
| ~ spl27_12
| ~ spl27_121 ),
inference(superposition,[],[f541,f2888]) ).
fof(f3182,plain,
( send_message(tptp3,sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0)
| ~ occurrence_of(sK26,sK24)
| ~ spl27_12
| ~ spl27_121 ),
inference(forward_subsumption_resolution,[],[f3180,f321]) ).
fof(f3184,plain,
( ~ occurrence_of(sK26,sK24)
| ~ spl27_12
| ~ spl27_121 ),
inference(forward_subsumption_resolution,[],[f3182,f319]) ).
fof(f3186,plain,
( $false
| ~ spl27_12
| ~ spl27_121 ),
inference(forward_subsumption_resolution,[],[f3184,f316]) ).
fof(f3187,plain,
( ~ spl27_12
| ~ spl27_121 ),
inference(avatar_contradiction_clause,[],[f3186]) ).
fof(f3204,plain,
( send_message(tptp2,sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0)
| ~ occurrence_of(sK23(tptp0,sK25,sK26),sK20(tptp0,sK25,sK26))
| ~ occurrence_of(sK26,sK24)
| ~ spl27_126 ),
inference(superposition,[],[f541,f2482]) ).
fof(f3206,plain,
( send_message(tptp2,sK21(tptp0,sK25,sK26),sK22(tptp0,sK25,sK26),sK25,tptp0)
| ~ occurrence_of(sK26,sK24)
| ~ spl27_126 ),
inference(forward_subsumption_resolution,[],[f3204,f321]) ).
fof(f3208,plain,
( ~ occurrence_of(sK26,sK24)
| ~ spl27_126 ),
inference(forward_subsumption_resolution,[],[f3206,f320]) ).
fof(f3210,plain,
( $false
| ~ spl27_126 ),
inference(forward_subsumption_resolution,[],[f3208,f316]) ).
fof(f3211,plain,
~ spl27_126,
inference(avatar_contradiction_clause,[],[f3210]) ).
cnf(s5,plain,
( spl27_6
| spl27_7 ),
inference(sat_conversion,[],[f583]) ).
cnf(s7,plain,
~ spl27_6,
inference(sat_conversion,[],[f594]) ).
cnf(s8,plain,
( ~ spl27_9
| spl27_10 ),
inference(sat_conversion,[],[f703]) ).
cnf(s9,plain,
( ~ spl27_11
| spl27_12 ),
inference(sat_conversion,[],[f729]) ).
cnf(s12,plain,
spl27_9,
inference(sat_conversion,[],[f767]) ).
cnf(s16,plain,
spl27_19,
inference(sat_conversion,[],[f864]) ).
cnf(s19,plain,
( spl27_11
| ~ spl27_19 ),
inference(sat_conversion,[],[f902]) ).
cnf(s23,plain,
( ~ spl27_10
| spl27_29
| spl27_30 ),
inference(sat_conversion,[],[f1445]) ).
cnf(s39,plain,
spl27_16,
inference(sat_conversion,[],[f1540]) ).
cnf(s49,plain,
( ~ spl27_7
| ~ spl27_16
| ~ spl27_30 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s118,plain,
spl27_114,
inference(sat_conversion,[],[f2328]) ).
cnf(s120,plain,
( ~ spl27_29
| ~ spl27_114
| spl27_116
| spl27_117 ),
inference(sat_conversion,[],[f2371]) ).
cnf(s138,plain,
( spl27_73
| ~ spl27_117 ),
inference(sat_conversion,[],[f2582]) ).
cnf(s143,plain,
( ~ spl27_16
| ~ spl27_116
| spl27_121
| spl27_126 ),
inference(sat_conversion,[],[f2662]) ).
cnf(s148,plain,
~ spl27_73,
inference(sat_conversion,[],[f2736]) ).
cnf(s179,plain,
( ~ spl27_12
| ~ spl27_121 ),
inference(sat_conversion,[],[f3187]) ).
cnf(s180,plain,
~ spl27_126,
inference(sat_conversion,[],[f3211]) ).
cnf(s181,plain,
( ~ spl27_16
| ~ spl27_116
| spl27_121 ),
inference(rat,[],[s143,s180]) ).
cnf(s182,plain,
~ spl27_117,
inference(rat,[],[s138,s148]) ).
cnf(s184,plain,
( ~ spl27_29
| ~ spl27_114
| spl27_116 ),
inference(rat,[],[s120,s182]) ).
cnf(s208,plain,
spl27_11,
inference(rat,[],[s19,s16]) ).
cnf(s210,plain,
spl27_12,
inference(rat,[],[s9,s208]) ).
cnf(s211,plain,
~ spl27_121,
inference(rat,[],[s179,s210]) ).
cnf(s213,plain,
~ spl27_116,
inference(rat,[],[s181,s39,s211]) ).
cnf(s214,plain,
~ spl27_29,
inference(rat,[],[s184,s118,s213]) ).
cnf(s215,plain,
spl27_10,
inference(rat,[],[s8,s12]) ).
cnf(s216,plain,
spl27_30,
inference(rat,[],[s23,s214,s215]) ).
cnf(s220,plain,
~ spl27_7,
inference(rat,[],[s49,s39,s216]) ).
cnf(s222,plain,
$false,
inference(rat,[],[s5,s220,s7]) ).
fof(f3212,plain,
$false,
inference(avatar_sat_refutation,[],[s222]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO001+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Sun Sep 27 22:18:51 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.84/2.28 % (3945961)Detected formulas, will run a generic FOF schedule.
% 9.84/2.28 % (3945971)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2323898106:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.84/2.28 % (3945966)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=1638377926:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.84/2.28 % (3945968)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=950648973:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.84/2.28 % (3945967)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=2147532605:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.84/2.28 % (3945969)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1664557448:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.84/2.28 % (3945972)dis-21_1_sil=8000:lcm=predicate:random_seed=2532040537: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)
% 9.84/2.28 % (3945971)Instruction limit reached!
% 9.84/2.28 % (3945971)------------------------------
% 9.84/2.28 % (3945971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945971)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945971)Termination reason: Instruction limit
% 9.84/2.28 % (3945971)Termination phase: Saturation
% 9.84/2.28 % (3945971)Time elapsed: 0.055 s
% 9.84/2.28 % (3945971)Peak memory usage: 90 MB
% 9.84/2.28 % (3945971)Instructions burned: 139 (million)
% 9.84/2.28 % (3945970)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3341326969:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.84/2.28 % (3945969)Refutation not found, incomplete strategy
% 9.84/2.28 % (3945969)------------------------------
% 9.84/2.28 % (3945969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945970)Refutation not found, incomplete strategy
% 9.84/2.28 % (3945970)------------------------------
% 9.84/2.28 % (3945970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945970)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945969)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945970)Termination reason: Refutation not found, incomplete strategy
% 9.84/2.28 % (3945970)Time elapsed: 0.025 s
% 9.84/2.28 % (3945969)Termination reason: Refutation not found, incomplete strategy
% 9.84/2.28 % (3945969)Time elapsed: 0.034 s
% 9.84/2.28 % (3945970)Peak memory usage: 87 MB
% 9.84/2.28 % (3945970)Instructions burned: 1 (million)
% 9.84/2.28 % (3945969)Peak memory usage: 88 MB
% 9.84/2.28 % (3945969)Instructions burned: 1 (million)
% 9.84/2.28 % (3945972)Instruction limit reached!
% 9.84/2.28 % (3945972)------------------------------
% 9.84/2.28 % (3945972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945972)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945972)Termination reason: Instruction limit
% 9.84/2.28 % (3945972)Termination phase: Saturation
% 9.84/2.28 % (3945972)Time elapsed: 0.101 s
% 9.84/2.28 % (3945972)Peak memory usage: 88 MB
% 9.84/2.28 % (3945972)Instructions burned: 130 (million)
% 9.84/2.28 % (3945980)lrs+10_1_sil=8000:sp=occurrence:random_seed=1765831230:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 9.84/2.28 % (3945970)------------------------------
% 9.84/2.28 % (3945970)------------------------------
% 9.84/2.28 % (3945981)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1407913488:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.84/2.28 % (3945981)Refutation not found, incomplete strategy
% 9.84/2.28 % (3945981)------------------------------
% 9.84/2.28 % (3945981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945981)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945981)Termination reason: Refutation not found, incomplete strategy
% 9.84/2.28 % (3945981)Time elapsed: 0.002 s
% 9.84/2.28 % (3945981)Peak memory usage: 88 MB
% 9.84/2.28 % (3945981)Instructions burned: 1 (million)
% 9.84/2.28 % (3945969)------------------------------
% 9.84/2.28 % (3945969)------------------------------
% 9.84/2.28 % (3945983)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3621495951:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 9.84/2.28 % (3945980)Instruction limit reached!
% 9.84/2.28 % (3945980)------------------------------
% 9.84/2.28 % (3945980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945980)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945980)Termination reason: Instruction limit
% 9.84/2.28 % (3945980)Termination phase: Saturation
% 9.84/2.28 % (3945980)Time elapsed: 0.185 s
% 9.84/2.28 % (3945980)Peak memory usage: 91 MB
% 9.84/2.28 % (3945980)Instructions burned: 286 (million)
% 9.84/2.28 % (3945983)Instruction limit reached!
% 9.84/2.28 % (3945983)------------------------------
% 9.84/2.28 % (3945983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945983)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945983)Termination reason: Instruction limit
% 9.84/2.28 % (3945983)Termination phase: Saturation
% 9.84/2.28 % (3945983)Time elapsed: 0.109 s
% 9.84/2.28 % (3945983)Peak memory usage: 91 MB
% 9.84/2.28 % (3945983)Instructions burned: 325 (million)
% 9.84/2.28 % (3945985)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=78499216:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.84/2.28 % (3945981)------------------------------
% 9.84/2.28 % (3945981)------------------------------
% 9.84/2.28 % (3945987)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=126284327:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 9.84/2.28 % (3945988)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2159286551:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 9.84/2.28 % (3945985)Instruction limit reached!
% 9.84/2.28 % (3945985)------------------------------
% 9.84/2.28 % (3945985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945985)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945985)Termination reason: Instruction limit
% 9.84/2.28 % (3945985)Termination phase: Saturation
% 9.84/2.28 % (3945985)Time elapsed: 0.143 s
% 9.84/2.28 % (3945985)Peak memory usage: 89 MB
% 9.84/2.28 % (3945985)Instructions burned: 249 (million)
% 9.84/2.28 % (3945991)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1098351129:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 9.84/2.28 % (3945987)Instruction limit reached!
% 9.84/2.28 % (3945987)------------------------------
% 9.84/2.28 % (3945987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945987)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945987)Termination reason: Instruction limit
% 9.84/2.28 % (3945987)Termination phase: Saturation
% 9.84/2.28 % (3945987)Time elapsed: 0.173 s
% 9.84/2.28 % (3945987)Peak memory usage: 88 MB
% 9.84/2.28 % (3945987)Instructions burned: 296 (million)
% 9.84/2.28 % (3945993)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3230760638:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 9.84/2.28 % (3945991)Instruction limit reached!
% 9.84/2.28 % (3945991)------------------------------
% 9.84/2.28 % (3945991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945991)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945991)Termination reason: Instruction limit
% 9.84/2.28 % (3945991)Termination phase: Saturation
% 9.84/2.28 % (3945991)Time elapsed: 0.082 s
% 9.84/2.28 % (3945991)Peak memory usage: 90 MB
% 9.84/2.28 % (3945991)Instructions burned: 113 (million)
% 9.84/2.28 % (3945993)Instruction limit reached!
% 9.84/2.28 % (3945993)------------------------------
% 9.84/2.28 % (3945993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945993)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945993)Termination reason: Instruction limit
% 9.84/2.28 % (3945993)Termination phase: Saturation
% 9.84/2.28 % (3945993)Time elapsed: 0.072 s
% 9.84/2.28 % (3945993)Peak memory usage: 89 MB
% 9.84/2.28 % (3945993)Instructions burned: 129 (million)
% 9.84/2.28 % (3945995)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1203096376:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 9.84/2.28 % (3945995)Instruction limit reached!
% 9.84/2.28 % (3945995)------------------------------
% 9.84/2.28 % (3945995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945995)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945995)Termination reason: Instruction limit
% 9.84/2.28 % (3945995)Termination phase: Saturation
% 9.84/2.28 % (3945995)Time elapsed: 0.043 s
% 9.84/2.28 % (3945995)Peak memory usage: 88 MB
% 9.84/2.28 % (3945995)Instructions burned: 116 (million)
% 9.84/2.28 % (3945997)lrs+10_1_sil=8000:sp=occurrence:random_seed=2732671029:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 9.84/2.28 % (3945998)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2171214018:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 9.84/2.28 % (3945998)Refutation not found, incomplete strategy
% 9.84/2.28 % (3945998)------------------------------
% 9.84/2.28 % (3945998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.84/2.28 % (3945998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.84/2.28 % (3945998)CaDiCaL version: 2.1.3
% 9.84/2.28 % (3945998)Termination reason: Refutation not found, incomplete strategy
% 9.84/2.28 % (3945998)Time elapsed: 0.006 s
% 9.84/2.28 % (3945998)Peak memory usage: 88 MB
% 9.84/2.28 % (3945998)Instructions burned: 8 (million)
% 9.84/2.28 % (3945966)First to succeed.
% 9.84/2.28 % (3945966)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3945961"
% 9.84/2.28 % (3946000)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1018769380:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 9.84/2.28 % (3945998)------------------------------
% 9.84/2.28 % (3945998)------------------------------
% 9.84/2.28 % (3945966)Refutation found. Thanks to Tanya!
% 9.84/2.28 % SZS status Theorem for theBenchmark
% 9.84/2.28 % SZS output start Proof for theBenchmark
% See solution above
% 10.59/2.48 % (3945966)------------------------------
% 10.59/2.48 % (3945966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.59/2.48 % (3945966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.59/2.48 % (3945966)CaDiCaL version: 2.1.3
% 10.59/2.48 % (3945966)Termination reason: Refutation
% 10.59/2.48 % (3945966)Time elapsed: 1.012 s
% 10.59/2.48 % (3945966)Peak memory usage: 133 MB
% 10.59/2.48 % (3945966)Instructions burned: 1455 (million)
% 10.59/2.48 % (3945966)------------------------------
% 10.59/2.48 % (3945966)------------------------------
% 10.59/2.48 % (3945961)Success in time 1.444 s
% 10.59/2.48 % Vampire exiting
%------------------------------------------------------------------------------