%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO004+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:33 PM UTC 2026
% Result : Theorem 16.79s 2.84s
% Output : Refutation 16.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 39
% Syntax : Number of formulae : 288 ( 30 unt; 15 def)
% Number of atoms : 860 ( 54 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 892 ( 320 ~; 481 |; 52 &)
% ( 22 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 32 ( 30 usr; 16 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-3 aty)
% Number of variables : 419 ( 0 sgn 394 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X3)
& min_precedes(X1,X2,X3) )
=> min_precedes(X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos) ).
fof(f4,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X2,X3)
& ~ atomic(X3)
& leaf_occ(X0,X2)
& leaf_occ(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_03) ).
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/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(f7,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_06) ).
fof(f9,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
fof(f11,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_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/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(f13,axiom,
! [X0,X1] :
( root(X0,X1)
=> legal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_12) ).
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/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(f18,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_17) ).
fof(f19,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_18) ).
fof(f21,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X2)
& root_occ(X1,X0) )
=> ~ ? [X3] : min_precedes(X3,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_20) ).
fof(f22,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_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(f26,axiom,
! [X0,X1] :
( ( leaf(X0,X1)
& ~ atomic(X1) )
=> ? [X2] :
( occurrence_of(X2,X1)
& leaf_occ(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_25) ).
fof(f29,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& arboreal(X2)
& arboreal(X3)
& subactivity_occurrence(X2,X1)
& subactivity_occurrence(X3,X1) )
=> ( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
fof(f30,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox2/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)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
fof(f35,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(f43,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_42) ).
fof(f46,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> root_occ(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_45) ).
fof(f48,axiom,
! [X0,X1] :
( ( occurrence_of(X1,tptp0)
& subactivity_occurrence(X0,X1)
& arboreal(X0)
& ~ leaf_occ(X0,X1) )
=> ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_47) ).
fof(f49,conjecture,
~ ? [X0] : occurrence_of(X0,tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f50,negated_conjecture,
~ ~ ? [X0] : occurrence_of(X0,tptp0),
inference(negated_conjecture,[status(cth)],[f49]) ).
fof(f51,plain,
? [X0] : occurrence_of(X0,tptp0),
inference(flattening,[],[f50]) ).
fof(f52,plain,
! [X0,X1] :
( precedes(X0,X1)
=> ( earlier(X0,X1)
& legal(X1) ) ),
inference(unused_predicate_definition_removal,[],[f9]) ).
fof(f53,plain,
! [X0,X1,X2,X3] :
( min_precedes(X0,X2,X3)
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(ennf_transformation,[],[f1]) ).
fof(f54,plain,
! [X0,X1,X2,X3] :
( min_precedes(X0,X2,X3)
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(flattening,[],[f53]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f60,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ occurrence_of(X2,X3)
| atomic(X3)
| ~ leaf_occ(X0,X2)
| ~ leaf_occ(X1,X2) ),
inference(flattening,[],[f59]) ).
fof(f61,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(f63,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f65,plain,
! [X0,X1] :
( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ),
inference(ennf_transformation,[],[f52]) ).
fof(f67,plain,
! [X0,X1] :
( legal(X0)
| ~ root(X0,X1) ),
inference(ennf_transformation,[],[f13]) ).
fof(f69,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(f72,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f73,plain,
! [X0] :
( ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) )
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X3,X1,X2)
| ~ occurrence_of(X0,X2)
| ~ root_occ(X1,X0) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ! [X3] : ~ min_precedes(X1,X3,X2)
| ~ occurrence_of(X0,X2)
| ~ leaf_occ(X1,X0) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f80,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f79]) ).
fof(f83,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(f84,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,X1)
& leaf_occ(X0,X2) )
| ~ leaf(X0,X1)
| atomic(X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f85,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,X1)
& leaf_occ(X0,X2) )
| ~ leaf(X0,X1)
| atomic(X1) ),
inference(flattening,[],[f84]) ).
fof(f88,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(f89,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,[],[f88]) ).
fof(f90,plain,
! [X0,X1] :
( ( activity(X0)
& activity_occurrence(X1) )
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f94,plain,
! [X0] :
( ? [X1,X2] :
( occurrence_of(X1,tptp4)
& root_occ(X1,X0)
& occurrence_of(X2,tptp3)
& leaf_occ(X2,X0)
& next_subocc(X1,X2,tptp0) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f95,plain,
! [X0,X1] :
( root_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f46]) ).
fof(f96,plain,
! [X0,X1] :
( root_occ(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f95]) ).
fof(f99,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(ennf_transformation,[],[f48]) ).
fof(f100,plain,
! [X0,X1] :
( ? [X2] :
( occurrence_of(X2,tptp1)
& next_subocc(X0,X2,tptp0) )
| ~ occurrence_of(X1,tptp0)
| ~ subactivity_occurrence(X0,X1)
| ~ arboreal(X0)
| leaf_occ(X0,X1) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3)
| min_precedes(X0,X2,X3) ),
inference(cnf_transformation,[],[f54]) ).
fof(f104,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X2)
| ~ leaf_occ(X0,X2)
| atomic(X3)
| ~ occurrence_of(X2,X3)
| X0 = X1 ),
inference(cnf_transformation,[],[f60]) ).
fof(f107,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X3,X1,X2)
| ~ min_precedes(X0,X3,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f61]) ).
fof(f108,plain,
! [X2,X0,X1] :
( min_precedes(X0,X1,X2)
| ~ next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f61]) ).
fof(f111,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f113,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f65]) ).
fof(f116,plain,
! [X0,X1] :
( root(X0,sK1(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f11]) ).
fof(f117,plain,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f11]) ).
fof(f118,plain,
! [X0,X1] :
( occurrence_of(X1,sK1(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f11]) ).
fof(f122,plain,
! [X0,X1] :
( occurrence_of(X1,sK2(X0,X1))
| ~ leaf_occ(X0,X1) ),
inference(cnf_transformation,[],[f12]) ).
fof(f124,plain,
! [X0,X1] :
( ~ root(X0,X1)
| legal(X0) ),
inference(cnf_transformation,[],[f67]) ).
fof(f127,plain,
! [X2,X0,X1] :
( min_precedes(X0,sK3(X0,X1),X1)
| ~ min_precedes(X2,X0,X1)
| leaf(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
fof(f136,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f137,plain,
! [X0] :
( ~ activity_occurrence(X0)
| occurrence_of(X0,sK6(X0)) ),
inference(cnf_transformation,[],[f73]) ).
fof(f141,plain,
! [X2,X3,X0,X1] :
( ~ root_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ min_precedes(X3,X1,X2) ),
inference(cnf_transformation,[],[f76]) ).
fof(f142,plain,
! [X2,X3,X0,X1] :
( ~ leaf_occ(X1,X0)
| ~ occurrence_of(X0,X2)
| ~ min_precedes(X1,X3,X2) ),
inference(cnf_transformation,[],[f78]) ).
fof(f143,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f80]) ).
fof(f146,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| subactivity_occurrence(X2,sK8(X0,X1,X2)) ),
inference(cnf_transformation,[],[f83]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| subactivity_occurrence(X1,sK8(X0,X1,X2)) ),
inference(cnf_transformation,[],[f83]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| occurrence_of(sK8(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f149,plain,
! [X0,X1] :
( atomic(X1)
| ~ leaf(X0,X1)
| leaf_occ(X0,sK9(X0,X1)) ),
inference(cnf_transformation,[],[f85]) ).
fof(f150,plain,
! [X0,X1] :
( atomic(X1)
| ~ leaf(X0,X1)
| occurrence_of(sK9(X0,X1),X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f157,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| ~ arboreal(X3)
| ~ arboreal(X2)
| ~ occurrence_of(X1,X0)
| X2 = X3
| min_precedes(X3,X2,X0)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f89]) ).
fof(f158,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f90]) ).
fof(f163,plain,
! [X0] :
( next_subocc(sK14(X0),sK15(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f94]) ).
fof(f164,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| leaf_occ(sK15(X0),X0) ),
inference(cnf_transformation,[],[f94]) ).
fof(f165,plain,
! [X0] :
( occurrence_of(sK15(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f94]) ).
fof(f166,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| root_occ(sK14(X0),X0) ),
inference(cnf_transformation,[],[f94]) ).
fof(f169,plain,
~ atomic(tptp0),
inference(cnf_transformation,[],[f35]) ).
fof(f177,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f43]) ).
fof(f180,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| root_occ(X0,X1) ),
inference(cnf_transformation,[],[f96]) ).
fof(f182,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK16(X0),tptp0) ),
inference(cnf_transformation,[],[f100]) ).
fof(f183,plain,
! [X0,X1] :
( leaf_occ(X0,X1)
| ~ arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16(X0),tptp1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f184,plain,
occurrence_of(sK17,tptp0),
inference(cnf_transformation,[],[f51]) ).
fof(f185,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X2,X3)
| min_precedes(X0,X1,X3)
| min_precedes(X1,X2,X3) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f187,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(X2,X3)
| leaf_occ(X0,X2)
| atomic(X3)
| leaf_occ(X1,X2)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f188,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f108]) ).
fof(f189,plain,
! [X2,X3,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| min_precedes(X0,X3,X2)
| min_precedes(X3,X1,X2) ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f194,plain,
! [X2,X0,X1] :
( min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f196,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| ~ legal(X1) ),
inference(consistent_polarity_flipping,[],[f113]) ).
fof(f198,plain,
! [X0,X1] :
( occurrence_of(X1,sK1(X0,X1))
| root_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f199,plain,
! [X0,X1] :
( root_occ(X0,X1)
| subactivity_occurrence(X0,X1) ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f200,plain,
! [X0,X1] :
( ~ root(X0,sK1(X0,X1))
| root_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f202,plain,
! [X0,X1] :
( occurrence_of(X1,sK2(X0,X1))
| leaf_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f205,plain,
! [X0,X1] :
( ~ legal(X0)
| root(X0,X1) ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f211,plain,
! [X2,X0,X1] :
( ~ leaf(X0,X1)
| min_precedes(X2,X0,X1)
| ~ min_precedes(X0,sK3(X0,X1),X1) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f213,plain,
! [X0] :
( ~ arboreal(X0)
| legal(X0) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f215,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(X0,X2)
| root_occ(X1,X0)
| min_precedes(X3,X1,X2) ),
inference(consistent_polarity_flipping,[],[f141]) ).
fof(f216,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(X0,X2)
| leaf_occ(X1,X0)
| min_precedes(X1,X3,X2) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f219,plain,
! [X2,X0,X1] :
( occurrence_of(sK8(X0,X1,X2),X0)
| min_precedes(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f220,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK8(X0,X1,X2))
| min_precedes(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f221,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK8(X0,X1,X2))
| min_precedes(X1,X2,X0) ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f222,plain,
! [X0,X1] :
( occurrence_of(sK9(X0,X1),X1)
| leaf(X0,X1)
| atomic(X1) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f223,plain,
! [X0,X1] :
( ~ leaf_occ(X0,sK9(X0,X1))
| leaf(X0,X1)
| atomic(X1) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f230,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| ~ subactivity_occurrence(X2,X1)
| arboreal(X3)
| arboreal(X2)
| ~ occurrence_of(X1,X0)
| X2 = X3
| ~ min_precedes(X3,X2,X0)
| ~ min_precedes(X2,X3,X0) ),
inference(consistent_polarity_flipping,[],[f157]) ).
fof(f234,plain,
! [X0] :
( ~ root_occ(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f235,plain,
! [X0] :
( ~ leaf_occ(sK15(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f237,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| ~ root_occ(X0,X1) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f239,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| occurrence_of(sK16(X0),tptp1) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f240,plain,
! [X0,X1] :
( ~ leaf_occ(X0,X1)
| arboreal(X0)
| ~ subactivity_occurrence(X0,X1)
| ~ occurrence_of(X1,tptp0)
| next_subocc(X0,sK16(X0),tptp0) ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f266,plain,
! [X0] :
( subactivity_occurrence(sK14(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f234,f199]) ).
fof(f278,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X1)
| sK2(X2,X0) = X1
| leaf_occ(X2,X0) ),
inference(resolution,[],[f143,f202]) ).
fof(f281,plain,
! [X0] :
( ~ occurrence_of(sK17,X0)
| tptp0 = X0 ),
inference(resolution,[],[f143,f184]) ).
fof(f283,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ min_precedes(sK14(X0),sK15(X0),tptp0) ),
inference(resolution,[],[f163,f188]) ).
fof(f290,plain,
! [X0,X1] :
( min_precedes(X1,X0,tptp0)
| root_occ(X0,sK17) ),
inference(resolution,[],[f215,f184]) ).
fof(f296,plain,
! [X0,X1] :
( min_precedes(X0,X1,tptp0)
| leaf_occ(X0,sK17) ),
inference(resolution,[],[f216,f184]) ).
fof(f305,plain,
! [X2,X3,X0,X1,X4] :
( leaf_occ(X3,sK8(X2,X0,X1))
| min_precedes(X3,X4,X2)
| min_precedes(X0,X1,X2) ),
inference(resolution,[],[f219,f216]) ).
fof(f307,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK8(X2,X0,X1),X3)
| min_precedes(X0,X1,X2)
| X2 = X3 ),
inference(resolution,[],[f219,f143]) ).
fof(f309,plain,
! [X2,X0,X1] :
( activity_occurrence(sK8(X2,X0,X1))
| min_precedes(X0,X1,X2) ),
inference(resolution,[],[f219,f158]) ).
fof(f332,plain,
! [X0] :
( root_occ(X0,sK17)
| tptp0 = sK1(X0,sK17) ),
inference(resolution,[],[f281,f198]) ).
fof(f351,plain,
! [X0,X1] :
( ~ occurrence_of(X0,tptp0)
| min_precedes(X1,sK15(X0),tptp0)
| min_precedes(sK14(X0),X1,tptp0) ),
inference(resolution,[],[f189,f163]) ).
fof(f363,plain,
! [X2,X3,X0,X1] :
( leaf_occ(X0,sK9(X1,X2))
| atomic(X2)
| leaf_occ(X3,sK9(X1,X2))
| X0 = X3
| leaf(X1,X2)
| atomic(X2) ),
inference(resolution,[],[f187,f222]) ).
fof(f368,plain,
! [X2,X3,X0,X1] :
( leaf_occ(X0,sK9(X1,X2))
| leaf_occ(X3,sK9(X1,X2))
| atomic(X2)
| X0 = X3
| leaf(X1,X2) ),
inference(duplicate_literal_removal,[],[f363]) ).
fof(f389,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X0,sK8(X1,X2,X3))
| arboreal(X2)
| arboreal(X0)
| ~ occurrence_of(sK8(X1,X2,X3),X4)
| X0 = X2
| ~ min_precedes(X2,X0,X4)
| ~ min_precedes(X0,X2,X4)
| min_precedes(X2,X3,X1) ),
inference(resolution,[],[f230,f220]) ).
fof(f450,plain,
( tptp0 = sK1(sK14(sK17),sK17)
| ~ occurrence_of(sK17,tptp0) ),
inference(resolution,[],[f332,f234]) ).
fof(f452,plain,
tptp0 = sK1(sK14(sK17),sK17),
inference(forward_subsumption_resolution,[],[f450,f184]) ).
fof(f461,plain,
( ~ root(sK14(sK17),tptp0)
| root_occ(sK14(sK17),sK17) ),
inference(superposition,[],[f200,f452]) ).
fof(f464,definition,
( spl18_3
<=> root_occ(sK14(sK17),sK17) ),
introduced(definition,[new_symbols(definition,[spl18_3])],[avatar_definition]) ).
fof(f465,plain,
( ~ root_occ(sK14(sK17),sK17)
| spl18_3 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f466,plain,
( root_occ(sK14(sK17),sK17)
| ~ spl18_3 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f468,definition,
( spl18_4
<=> root(sK14(sK17),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_4])],[avatar_definition]) ).
fof(f470,plain,
( ~ root(sK14(sK17),tptp0)
| spl18_4 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f471,plain,
( spl18_3
| ~ spl18_4 ),
inference(avatar_split_clause,[],[f461,f468,f464]) ).
fof(f475,plain,
~ min_precedes(sK14(sK17),sK15(sK17),tptp0),
inference(resolution,[],[f283,f184]) ).
fof(f484,plain,
leaf_occ(sK14(sK17),sK17),
inference(resolution,[],[f475,f296]) ).
fof(f493,plain,
( arboreal(sK14(sK17))
| ~ subactivity_occurrence(sK14(sK17),sK17)
| ~ occurrence_of(sK17,tptp0)
| next_subocc(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
inference(resolution,[],[f484,f240]) ).
fof(f494,plain,
( arboreal(sK14(sK17))
| ~ subactivity_occurrence(sK14(sK17),sK17)
| ~ occurrence_of(sK17,tptp0)
| occurrence_of(sK16(sK14(sK17)),tptp1) ),
inference(resolution,[],[f484,f239]) ).
fof(f505,plain,
( arboreal(sK14(sK17))
| ~ occurrence_of(sK17,tptp0)
| occurrence_of(sK16(sK14(sK17)),tptp1) ),
inference(forward_subsumption_resolution,[],[f494,f266]) ).
fof(f506,plain,
( arboreal(sK14(sK17))
| ~ occurrence_of(sK17,tptp0)
| next_subocc(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
inference(forward_subsumption_resolution,[],[f493,f266]) ).
fof(f507,plain,
( arboreal(sK14(sK17))
| occurrence_of(sK16(sK14(sK17)),tptp1) ),
inference(forward_subsumption_resolution,[],[f505,f184]) ).
fof(f508,plain,
( arboreal(sK14(sK17))
| next_subocc(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
inference(forward_subsumption_resolution,[],[f506,f184]) ).
fof(f510,definition,
( spl18_7
<=> occurrence_of(sK16(sK14(sK17)),tptp1) ),
introduced(definition,[new_symbols(definition,[spl18_7])],[avatar_definition]) ).
fof(f512,plain,
( occurrence_of(sK16(sK14(sK17)),tptp1)
| ~ spl18_7 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f514,definition,
( spl18_8
<=> arboreal(sK14(sK17)) ),
introduced(definition,[new_symbols(definition,[spl18_8])],[avatar_definition]) ).
fof(f515,plain,
( ~ arboreal(sK14(sK17))
| spl18_8 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f516,plain,
( arboreal(sK14(sK17))
| ~ spl18_8 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f517,plain,
( spl18_7
| spl18_8 ),
inference(avatar_split_clause,[],[f507,f514,f510]) ).
fof(f519,definition,
( spl18_9
<=> next_subocc(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_9])],[avatar_definition]) ).
fof(f521,plain,
( next_subocc(sK14(sK17),sK16(sK14(sK17)),tptp0)
| ~ spl18_9 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f522,plain,
( spl18_9
| spl18_8 ),
inference(avatar_split_clause,[],[f508,f514,f519]) ).
fof(f523,plain,
! [X2,X0,X1] :
( occurrence_of(sK8(X2,X0,X1),sK6(sK8(X2,X0,X1)))
| min_precedes(X0,X1,X2) ),
inference(resolution,[],[f309,f137]) ).
fof(f527,plain,
( legal(sK14(sK17))
| ~ spl18_8 ),
inference(resolution,[],[f516,f213]) ).
fof(f528,plain,
( ! [X0] : root(sK14(sK17),X0)
| ~ spl18_8 ),
inference(resolution,[],[f527,f205]) ).
fof(f615,plain,
( $false
| spl18_4
| ~ spl18_8 ),
inference(backward_subsumption_resolution,[],[f470,f528]) ).
fof(f619,plain,
( spl18_4
| ~ spl18_8 ),
inference(avatar_contradiction_clause,[],[f615]) ).
fof(f620,plain,
( ~ occurrence_of(sK17,tptp0)
| ~ spl18_3 ),
inference(resolution,[],[f466,f234]) ).
fof(f622,plain,
( $false
| ~ spl18_3 ),
inference(forward_subsumption_resolution,[],[f620,f184]) ).
fof(f623,plain,
~ spl18_3,
inference(avatar_contradiction_clause,[],[f622]) ).
fof(f669,plain,
! [X2,X0,X1] :
( leaf_occ(X0,sK9(X1,X2))
| sK2(X0,sK9(X1,X2)) = X2
| leaf(X1,X2)
| atomic(X2) ),
inference(resolution,[],[f278,f222]) ).
fof(f738,plain,
( ! [X0] :
( ~ occurrence_of(sK16(sK14(sK17)),X0)
| tptp1 = X0 )
| ~ spl18_7 ),
inference(resolution,[],[f512,f143]) ).
fof(f863,plain,
! [X0] :
( min_precedes(X0,sK15(sK17),tptp0)
| min_precedes(sK14(sK17),X0,tptp0) ),
inference(resolution,[],[f351,f184]) ).
fof(f896,plain,
! [X2,X3,X0,X1,X4] :
( ~ occurrence_of(sK8(X1,X2,X3),tptp0)
| min_precedes(X2,X3,X1)
| arboreal(X0)
| ~ subactivity_occurrence(X0,sK8(X1,X2,X3))
| min_precedes(X0,X4,X1)
| ~ root_occ(X0,sK8(X1,X2,X3)) ),
inference(resolution,[],[f305,f237]) ).
fof(f1015,plain,
( ~ min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| ~ spl18_9 ),
inference(resolution,[],[f521,f188]) ).
fof(f1033,plain,
! [X2,X0,X1] :
( ~ occurrence_of(sK9(X0,X1),tptp0)
| atomic(X1)
| sK15(sK9(X0,X1)) = X2
| leaf(X0,X1)
| leaf_occ(X2,sK9(X0,X1)) ),
inference(resolution,[],[f368,f235]) ).
fof(f1064,plain,
( root_occ(sK16(sK14(sK17)),sK17)
| ~ spl18_9 ),
inference(resolution,[],[f1015,f290]) ).
fof(f1065,plain,
( precedes(sK14(sK17),sK16(sK14(sK17)))
| ~ spl18_9 ),
inference(resolution,[],[f1015,f194]) ).
fof(f1092,definition,
( spl18_25
<=> leaf(sK16(sK14(sK17)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_25])],[avatar_definition]) ).
fof(f1093,plain,
( ~ leaf(sK16(sK14(sK17)),tptp0)
| spl18_25 ),
inference(avatar_component_clause,[],[f1092]) ).
fof(f1094,plain,
( leaf(sK16(sK14(sK17)),tptp0)
| ~ spl18_25 ),
inference(avatar_component_clause,[],[f1092]) ).
fof(f1112,plain,
! [X2,X3,X0,X1] :
( arboreal(X0)
| arboreal(X1)
| ~ occurrence_of(sK8(X2,X0,X1),X3)
| X0 = X1
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X1,X0,X3)
| min_precedes(X0,X1,X2)
| min_precedes(X0,X1,X2) ),
inference(resolution,[],[f389,f221]) ).
fof(f1116,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK8(X2,X0,X1),X3)
| arboreal(X1)
| arboreal(X0)
| X0 = X1
| ~ min_precedes(X0,X1,X3)
| ~ min_precedes(X1,X0,X3)
| min_precedes(X0,X1,X2) ),
inference(duplicate_literal_removal,[],[f1112]) ).
fof(f1221,plain,
min_precedes(sK14(sK17),sK14(sK17),tptp0),
inference(resolution,[],[f863,f475]) ).
fof(f1279,plain,
! [X0] :
( min_precedes(sK14(sK17),X0,tptp0)
| min_precedes(X0,sK14(sK17),tptp0) ),
inference(resolution,[],[f1221,f185]) ).
fof(f1307,plain,
( ~ legal(sK16(sK14(sK17)))
| ~ spl18_9 ),
inference(resolution,[],[f1065,f196]) ).
fof(f1782,definition,
( spl18_54
<=> arboreal(sK16(sK14(sK17))) ),
introduced(definition,[new_symbols(definition,[spl18_54])],[avatar_definition]) ).
fof(f1783,plain,
( ~ arboreal(sK16(sK14(sK17)))
| spl18_54 ),
inference(avatar_component_clause,[],[f1782]) ).
fof(f1784,plain,
( arboreal(sK16(sK14(sK17)))
| ~ spl18_54 ),
inference(avatar_component_clause,[],[f1782]) ).
fof(f1815,plain,
! [X2,X0,X1] :
( min_precedes(X0,X1,X2)
| min_precedes(X0,X1,X2)
| sK6(sK8(X2,X0,X1)) = X2 ),
inference(resolution,[],[f523,f307]) ).
fof(f1821,plain,
! [X2,X3,X0,X1,X4] :
( min_precedes(X4,X3,sK6(sK8(X2,X0,X1)))
| root_occ(X3,sK8(X2,X0,X1))
| min_precedes(X0,X1,X2) ),
inference(resolution,[],[f523,f215]) ).
fof(f1826,plain,
! [X2,X0,X1] :
( min_precedes(X0,X1,X2)
| sK6(sK8(X2,X0,X1)) = X2 ),
inference(duplicate_literal_removal,[],[f1815]) ).
fof(f2085,plain,
! [X0,X1] :
( sK2(X0,sK9(X0,X1)) = X1
| leaf(X0,X1)
| atomic(X1)
| leaf(X0,X1)
| atomic(X1) ),
inference(resolution,[],[f669,f223]) ).
fof(f2090,plain,
! [X0,X1] :
( leaf(X0,X1)
| sK2(X0,sK9(X0,X1)) = X1
| atomic(X1) ),
inference(duplicate_literal_removal,[],[f2085]) ).
fof(f2372,plain,
! [X0,X1] :
( atomic(tptp0)
| sK15(sK9(X0,tptp0)) = X1
| leaf(X0,tptp0)
| leaf_occ(X1,sK9(X0,tptp0))
| leaf(X0,tptp0)
| atomic(tptp0) ),
inference(resolution,[],[f1033,f222]) ).
fof(f2373,plain,
! [X0,X1] :
( atomic(tptp0)
| sK15(sK9(X0,tptp0)) = X1
| leaf(X0,tptp0)
| leaf_occ(X1,sK9(X0,tptp0)) ),
inference(duplicate_literal_removal,[],[f2372]) ).
fof(f2374,plain,
! [X0,X1] :
( leaf_occ(X1,sK9(X0,tptp0))
| leaf(X0,tptp0)
| sK15(sK9(X0,tptp0)) = X1 ),
inference(forward_subsumption_resolution,[],[f2373,f169]) ).
fof(f2665,plain,
! [X2,X0,X1] :
( arboreal(X0)
| arboreal(X1)
| X0 = X1
| ~ min_precedes(X1,X0,sK6(sK8(X2,X1,X0)))
| ~ min_precedes(X0,X1,sK6(sK8(X2,X1,X0)))
| min_precedes(X1,X0,X2)
| min_precedes(X1,X0,X2) ),
inference(resolution,[],[f1116,f523]) ).
fof(f2671,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X0,sK6(sK8(X2,X1,X0)))
| arboreal(X1)
| X0 = X1
| arboreal(X0)
| ~ min_precedes(X0,X1,sK6(sK8(X2,X1,X0)))
| min_precedes(X1,X0,X2) ),
inference(duplicate_literal_removal,[],[f2665]) ).
fof(f2853,plain,
! [X2,X3,X0,X1] :
( min_precedes(X0,X1,tptp0)
| arboreal(X2)
| ~ subactivity_occurrence(X2,sK8(tptp0,X0,X1))
| min_precedes(X2,X3,tptp0)
| ~ root_occ(X2,sK8(tptp0,X0,X1))
| min_precedes(X0,X1,tptp0) ),
inference(resolution,[],[f896,f219]) ).
fof(f2854,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X2,sK8(tptp0,X0,X1))
| arboreal(X2)
| min_precedes(X0,X1,tptp0)
| min_precedes(X2,X3,tptp0)
| ~ root_occ(X2,sK8(tptp0,X0,X1)) ),
inference(duplicate_literal_removal,[],[f2853]) ).
fof(f3246,definition,
( spl18_74
<=> min_precedes(sK16(sK14(sK17)),sK3(sK16(sK14(sK17)),tptp0),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_74])],[avatar_definition]) ).
fof(f3248,plain,
( ~ min_precedes(sK16(sK14(sK17)),sK3(sK16(sK14(sK17)),tptp0),tptp0)
| spl18_74 ),
inference(avatar_component_clause,[],[f3246]) ).
fof(f3250,definition,
( spl18_75
<=> ! [X0] : min_precedes(X0,sK16(sK14(sK17)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_75])],[avatar_definition]) ).
fof(f3251,plain,
( ! [X0] : min_precedes(X0,sK16(sK14(sK17)),tptp0)
| ~ spl18_75 ),
inference(avatar_component_clause,[],[f3250]) ).
fof(f3874,plain,
( tptp0 = sK6(sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| ~ spl18_9 ),
inference(resolution,[],[f1826,f1015]) ).
fof(f7992,plain,
! [X2,X0,X1] :
( arboreal(X0)
| min_precedes(X1,X0,tptp0)
| min_precedes(X0,X2,tptp0)
| ~ root_occ(X0,sK8(tptp0,X1,X0))
| min_precedes(X1,X0,tptp0) ),
inference(resolution,[],[f2854,f221]) ).
fof(f7996,plain,
! [X2,X0,X1] :
( ~ root_occ(X0,sK8(tptp0,X1,X0))
| min_precedes(X1,X0,tptp0)
| min_precedes(X0,X2,tptp0)
| arboreal(X0) ),
inference(duplicate_literal_removal,[],[f7992]) ).
fof(f9200,plain,
( tptp0 = sK2(sK16(sK14(sK17)),sK9(sK16(sK14(sK17)),tptp0))
| atomic(tptp0)
| spl18_25 ),
inference(resolution,[],[f1093,f2090]) ).
fof(f9201,plain,
( tptp0 = sK2(sK16(sK14(sK17)),sK9(sK16(sK14(sK17)),tptp0))
| spl18_25 ),
inference(forward_subsumption_resolution,[],[f9200,f169]) ).
fof(f9442,plain,
( $false
| ~ spl18_9
| ~ spl18_75 ),
inference(backward_subsumption_resolution,[],[f1015,f3251]) ).
fof(f9447,plain,
( ~ spl18_9
| ~ spl18_75 ),
inference(avatar_contradiction_clause,[],[f9442]) ).
fof(f9453,definition,
( spl18_275
<=> min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_275])],[avatar_definition]) ).
fof(f9454,plain,
( ~ min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| spl18_275 ),
inference(avatar_component_clause,[],[f9453]) ).
fof(f9463,plain,
( ~ spl18_275
| ~ spl18_9 ),
inference(avatar_split_clause,[],[f1015,f519,f9453]) ).
fof(f9761,plain,
! [X2,X0,X1] :
( arboreal(X0)
| X0 = X1
| arboreal(X1)
| ~ min_precedes(X1,X0,sK6(sK8(X2,X0,X1)))
| min_precedes(X0,X1,X2)
| root_occ(X1,sK8(X2,X0,X1))
| min_precedes(X0,X1,X2) ),
inference(resolution,[],[f2671,f1821]) ).
fof(f9865,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X0,sK6(sK8(X2,X0,X1)))
| X0 = X1
| arboreal(X1)
| arboreal(X0)
| min_precedes(X0,X1,X2)
| root_occ(X1,sK8(X2,X0,X1)) ),
inference(duplicate_literal_removal,[],[f9761]) ).
fof(f13907,plain,
( legal(sK16(sK14(sK17)))
| ~ spl18_54 ),
inference(resolution,[],[f1784,f213]) ).
fof(f13908,plain,
( $false
| ~ spl18_9
| ~ spl18_54 ),
inference(forward_subsumption_resolution,[],[f13907,f1307]) ).
fof(f13909,plain,
( ~ spl18_9
| ~ spl18_54 ),
inference(avatar_contradiction_clause,[],[f13908]) ).
fof(f14190,plain,
( occurrence_of(sK9(sK16(sK14(sK17)),tptp0),tptp0)
| leaf_occ(sK16(sK14(sK17)),sK9(sK16(sK14(sK17)),tptp0))
| spl18_25 ),
inference(superposition,[],[f202,f9201]) ).
fof(f14217,definition,
( spl18_364
<=> leaf_occ(sK16(sK14(sK17)),sK9(sK16(sK14(sK17)),tptp0)) ),
introduced(definition,[new_symbols(definition,[spl18_364])],[avatar_definition]) ).
fof(f14218,plain,
( ~ leaf_occ(sK16(sK14(sK17)),sK9(sK16(sK14(sK17)),tptp0))
| spl18_364 ),
inference(avatar_component_clause,[],[f14217]) ).
fof(f14219,plain,
( leaf_occ(sK16(sK14(sK17)),sK9(sK16(sK14(sK17)),tptp0))
| ~ spl18_364 ),
inference(avatar_component_clause,[],[f14217]) ).
fof(f14233,definition,
( spl18_367
<=> occurrence_of(sK9(sK16(sK14(sK17)),tptp0),tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_367])],[avatar_definition]) ).
fof(f14234,plain,
( occurrence_of(sK9(sK16(sK14(sK17)),tptp0),tptp0)
| ~ spl18_367 ),
inference(avatar_component_clause,[],[f14233]) ).
fof(f14276,plain,
( spl18_364
| spl18_367
| spl18_25 ),
inference(avatar_split_clause,[],[f14190,f1092,f14233,f14217]) ).
fof(f14335,plain,
( leaf(sK16(sK14(sK17)),tptp0)
| atomic(tptp0)
| ~ spl18_364 ),
inference(resolution,[],[f14219,f223]) ).
fof(f14351,plain,
( atomic(tptp0)
| spl18_25
| ~ spl18_364 ),
inference(forward_subsumption_resolution,[],[f14335,f1093]) ).
fof(f14367,plain,
( $false
| spl18_25
| ~ spl18_364 ),
inference(forward_subsumption_resolution,[],[f14351,f169]) ).
fof(f14368,plain,
( spl18_25
| ~ spl18_364 ),
inference(avatar_contradiction_clause,[],[f14367]) ).
fof(f15631,plain,
( leaf(sK16(sK14(sK17)),tptp0)
| sK16(sK14(sK17)) = sK15(sK9(sK16(sK14(sK17)),tptp0))
| spl18_364 ),
inference(resolution,[],[f14218,f2374]) ).
fof(f15679,plain,
( sK16(sK14(sK17)) = sK15(sK9(sK16(sK14(sK17)),tptp0))
| spl18_25
| spl18_364 ),
inference(forward_subsumption_resolution,[],[f15631,f1093]) ).
fof(f15865,definition,
( spl18_444
<=> sK16(sK14(sK17)) = sK15(sK9(sK16(sK14(sK17)),tptp0)) ),
introduced(definition,[new_symbols(definition,[spl18_444])],[avatar_definition]) ).
fof(f15867,plain,
( sK16(sK14(sK17)) = sK15(sK9(sK16(sK14(sK17)),tptp0))
| ~ spl18_444 ),
inference(avatar_component_clause,[],[f15865]) ).
fof(f16043,plain,
( spl18_444
| spl18_25
| spl18_364 ),
inference(avatar_split_clause,[],[f15679,f14217,f1092,f15865]) ).
fof(f16090,plain,
( occurrence_of(sK16(sK14(sK17)),tptp3)
| ~ occurrence_of(sK9(sK16(sK14(sK17)),tptp0),tptp0)
| ~ spl18_444 ),
inference(superposition,[],[f165,f15867]) ).
fof(f16101,plain,
( occurrence_of(sK16(sK14(sK17)),tptp3)
| ~ spl18_367
| ~ spl18_444 ),
inference(forward_subsumption_resolution,[],[f16090,f14234]) ).
fof(f16161,plain,
( tptp3 = tptp1
| ~ spl18_7
| ~ spl18_367
| ~ spl18_444 ),
inference(resolution,[],[f16101,f738]) ).
fof(f16199,plain,
( $false
| ~ spl18_7
| ~ spl18_367
| ~ spl18_444 ),
inference(forward_subsumption_resolution,[],[f16161,f177]) ).
fof(f16200,plain,
( ~ spl18_7
| ~ spl18_367
| ~ spl18_444 ),
inference(avatar_contradiction_clause,[],[f16199]) ).
fof(f16364,plain,
( ! [X0] :
( min_precedes(X0,sK16(sK14(sK17)),tptp0)
| ~ min_precedes(sK16(sK14(sK17)),sK3(sK16(sK14(sK17)),tptp0),tptp0) )
| ~ spl18_25 ),
inference(resolution,[],[f1094,f211]) ).
fof(f16366,plain,
( ~ spl18_74
| spl18_75
| ~ spl18_25 ),
inference(avatar_split_clause,[],[f16364,f1092,f3250,f3246]) ).
fof(f18065,definition,
( spl18_535
<=> sK14(sK17) = sK16(sK14(sK17)) ),
introduced(definition,[new_symbols(definition,[spl18_535])],[avatar_definition]) ).
fof(f18066,plain,
( sK14(sK17) != sK16(sK14(sK17))
| spl18_535 ),
inference(avatar_component_clause,[],[f18065]) ).
fof(f18067,plain,
( sK14(sK17) = sK16(sK14(sK17))
| ~ spl18_535 ),
inference(avatar_component_clause,[],[f18065]) ).
fof(f19016,plain,
( root_occ(sK14(sK17),sK17)
| ~ spl18_9
| ~ spl18_535 ),
inference(superposition,[],[f1064,f18067]) ).
fof(f19115,plain,
( $false
| spl18_3
| ~ spl18_9
| ~ spl18_535 ),
inference(forward_subsumption_resolution,[],[f19016,f465]) ).
fof(f19116,plain,
( spl18_3
| ~ spl18_9
| ~ spl18_535 ),
inference(avatar_contradiction_clause,[],[f19115]) ).
fof(f21738,definition,
( spl18_590
<=> ! [X0] : min_precedes(sK16(sK14(sK17)),X0,tptp0) ),
introduced(definition,[new_symbols(definition,[spl18_590])],[avatar_definition]) ).
fof(f21739,plain,
( ! [X0] : min_precedes(sK16(sK14(sK17)),X0,tptp0)
| ~ spl18_590 ),
inference(avatar_component_clause,[],[f21738]) ).
fof(f46972,plain,
( ~ min_precedes(sK16(sK14(sK17)),sK14(sK17),tptp0)
| sK14(sK17) = sK16(sK14(sK17))
| arboreal(sK16(sK14(sK17)))
| arboreal(sK14(sK17))
| min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| ~ spl18_9 ),
inference(superposition,[],[f9865,f3874]) ).
fof(f46984,plain,
( sK14(sK17) = sK16(sK14(sK17))
| arboreal(sK16(sK14(sK17)))
| arboreal(sK14(sK17))
| min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| ~ spl18_9 ),
inference(forward_subsumption_resolution,[],[f46972,f1279]) ).
fof(f47018,plain,
( arboreal(sK16(sK14(sK17)))
| arboreal(sK14(sK17))
| min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| ~ spl18_9
| spl18_535 ),
inference(forward_subsumption_resolution,[],[f46984,f18066]) ).
fof(f47020,plain,
( arboreal(sK14(sK17))
| min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| ~ spl18_9
| spl18_54
| spl18_535 ),
inference(forward_subsumption_resolution,[],[f47018,f1783]) ).
fof(f47022,plain,
( min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| spl18_8
| ~ spl18_9
| spl18_54
| spl18_535 ),
inference(forward_subsumption_resolution,[],[f47020,f515]) ).
fof(f47032,plain,
( root_occ(sK16(sK14(sK17)),sK8(tptp0,sK14(sK17),sK16(sK14(sK17))))
| spl18_8
| ~ spl18_9
| spl18_54
| spl18_275
| spl18_535 ),
inference(forward_subsumption_resolution,[],[f47022,f9454]) ).
fof(f47513,plain,
( ! [X0] :
( min_precedes(sK14(sK17),sK16(sK14(sK17)),tptp0)
| min_precedes(sK16(sK14(sK17)),X0,tptp0)
| arboreal(sK16(sK14(sK17))) )
| spl18_8
| ~ spl18_9
| spl18_54
| spl18_275
| spl18_535 ),
inference(resolution,[],[f47032,f7996]) ).
fof(f47523,plain,
( ! [X0] :
( min_precedes(sK16(sK14(sK17)),X0,tptp0)
| arboreal(sK16(sK14(sK17))) )
| spl18_8
| ~ spl18_9
| spl18_54
| spl18_275
| spl18_535 ),
inference(forward_subsumption_resolution,[],[f47513,f9454]) ).
fof(f47525,plain,
( ! [X0] : min_precedes(sK16(sK14(sK17)),X0,tptp0)
| spl18_8
| ~ spl18_9
| spl18_54
| spl18_275
| spl18_535 ),
inference(forward_subsumption_resolution,[],[f47523,f1783]) ).
fof(f47527,plain,
( spl18_590
| spl18_8
| ~ spl18_9
| spl18_54
| spl18_275
| spl18_535 ),
inference(avatar_split_clause,[],[f47525,f18065,f9453,f1782,f519,f514,f21738]) ).
fof(f47542,plain,
( $false
| spl18_74
| ~ spl18_590 ),
inference(backward_subsumption_resolution,[],[f3248,f21739]) ).
fof(f47554,plain,
( spl18_74
| ~ spl18_590 ),
inference(avatar_contradiction_clause,[],[f47542]) ).
cnf(s4,plain,
( spl18_3
| ~ spl18_4 ),
inference(sat_conversion,[],[f471]) ).
cnf(s6,plain,
( spl18_7
| spl18_8 ),
inference(sat_conversion,[],[f517]) ).
cnf(s7,plain,
( spl18_8
| spl18_9 ),
inference(sat_conversion,[],[f522]) ).
cnf(s15,plain,
( spl18_4
| ~ spl18_8 ),
inference(sat_conversion,[],[f619]) ).
cnf(s16,plain,
~ spl18_3,
inference(sat_conversion,[],[f623]) ).
cnf(s450,plain,
( ~ spl18_9
| ~ spl18_75 ),
inference(sat_conversion,[],[f9447]) ).
cnf(s456,plain,
( ~ spl18_9
| ~ spl18_275 ),
inference(sat_conversion,[],[f9463]) ).
cnf(s586,plain,
( ~ spl18_9
| ~ spl18_54 ),
inference(sat_conversion,[],[f13909]) ).
cnf(s606,plain,
( spl18_25
| spl18_364
| spl18_367 ),
inference(sat_conversion,[],[f14276]) ).
cnf(s620,plain,
( spl18_25
| ~ spl18_364 ),
inference(sat_conversion,[],[f14368]) ).
cnf(s733,plain,
( spl18_25
| spl18_364
| spl18_444 ),
inference(sat_conversion,[],[f16043]) ).
cnf(s734,plain,
( ~ spl18_7
| ~ spl18_367
| ~ spl18_444 ),
inference(sat_conversion,[],[f16200]) ).
cnf(s777,plain,
( ~ spl18_25
| ~ spl18_74
| spl18_75 ),
inference(sat_conversion,[],[f16366]) ).
cnf(s862,plain,
( spl18_3
| ~ spl18_9
| ~ spl18_535 ),
inference(sat_conversion,[],[f19116]) ).
cnf(s1422,plain,
( spl18_8
| ~ spl18_9
| spl18_54
| spl18_275
| spl18_535
| spl18_590 ),
inference(sat_conversion,[],[f47527]) ).
cnf(s1423,plain,
( spl18_74
| ~ spl18_590 ),
inference(sat_conversion,[],[f47554]) ).
cnf(s1574,plain,
~ spl18_4,
inference(rat,[],[s4,s16]) ).
cnf(s1581,plain,
~ spl18_8,
inference(rat,[],[s15,s1574]) ).
cnf(s1600,plain,
spl18_9,
inference(rat,[],[s7,s1581]) ).
cnf(s1601,plain,
spl18_7,
inference(rat,[],[s6,s1581]) ).
cnf(s1612,plain,
~ spl18_535,
inference(rat,[],[s862,s16,s1600]) ).
cnf(s1613,plain,
~ spl18_54,
inference(rat,[],[s586,s1600]) ).
cnf(s1614,plain,
~ spl18_275,
inference(rat,[],[s456,s1600]) ).
cnf(s1615,plain,
~ spl18_75,
inference(rat,[],[s450,s1600]) ).
cnf(s1630,plain,
spl18_590,
inference(rat,[],[s1422,s1613,s1612,s1600,s1581,s1614]) ).
cnf(s1646,plain,
spl18_74,
inference(rat,[],[s1423,s1630]) ).
cnf(s1647,plain,
~ spl18_25,
inference(rat,[],[s777,s1615,s1646]) ).
cnf(s1650,plain,
~ spl18_364,
inference(rat,[],[s620,s1647]) ).
cnf(s1653,plain,
spl18_444,
inference(rat,[],[s733,s1647,s1650]) ).
cnf(s1657,plain,
spl18_367,
inference(rat,[],[s606,s1647,s1650]) ).
cnf(s1687,plain,
$false,
inference(rat,[],[s734,s1601,s1653,s1657]) ).
fof(f47580,plain,
$false,
inference(avatar_sat_refutation,[],[s1687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO004+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n004.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 22:16:37 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42 Running first-order model finding
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.79/2.84 % (3938302)Will run a generic schedule for satisfiability detection.
% 16.79/2.84 % (3938312)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3534040720:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.79/2.84 % (3938308)% WARNING: option uhcvi not known.
% 16.79/2.84 % (3938308)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3262137107:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.79/2.84 % (3938307)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1539113789_2999 on theBenchmark for (2999ds/0Mi)
% 16.79/2.84 % (3938311)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3066245355:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.79/2.84 % (3938309)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1497223921:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.79/2.84 % (3938310)dis+10_1_sil=32000:sp=arity:random_seed=2086948892:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.79/2.84 % (3938313)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1304659624:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.79/2.84 % Detected minimum model sizes of [4]
% 16.79/2.84 % Detected maximum model sizes of [max]
% 16.79/2.84 % TRYING [4]
% 16.79/2.84 % TRYING [5]
% 16.79/2.84 % (3938312)Instruction limit reached!
% 16.79/2.84 % (3938312)------------------------------
% 16.79/2.84 % (3938312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938312)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938312)Termination reason: Instruction limit
% 16.79/2.84 % (3938312)Termination phase: Saturation
% 16.79/2.84 % (3938312)Time elapsed: 0.049 s
% 16.79/2.84 % (3938312)Peak memory usage: 13 MB
% 16.79/2.84 % (3938312)Instructions burned: 134 (million)
% 16.79/2.84 % TRYING [6]
% 16.79/2.84 % (3938321)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3752682152:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.79/2.84 % Detected minimum model sizes of [4]
% 16.79/2.84 % Detected maximum model sizes of [max]
% 16.79/2.84 % TRYING [4]
% 16.79/2.84 % TRYING [5]
% 16.79/2.84 % (3938310)Instruction limit reached!
% 16.79/2.84 % (3938310)------------------------------
% 16.79/2.84 % (3938310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938310)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938310)Termination reason: Instruction limit
% 16.79/2.84 % (3938310)Termination phase: Saturation
% 16.79/2.84 % (3938310)Time elapsed: 0.072 s
% 16.79/2.84 % (3938310)Peak memory usage: 13 MB
% 16.79/2.84 % (3938310)Instructions burned: 104 (million)
% 16.79/2.84 % (3938311)Instruction limit reached!
% 16.79/2.84 % (3938311)------------------------------
% 16.79/2.84 % (3938311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938311)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938311)Termination reason: Instruction limit
% 16.79/2.84 % (3938311)Termination phase: Saturation
% 16.79/2.84 % (3938311)Time elapsed: 0.075 s
% 16.79/2.84 % (3938311)Peak memory usage: 13 MB
% 16.79/2.84 % (3938311)Instructions burned: 116 (million)
% 16.79/2.84 % TRYING [6]
% 16.79/2.84 % (3938323)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3829285451:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.79/2.84 % (3938324)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2257009531:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.79/2.84 % (3938313)Instruction limit reached!
% 16.79/2.84 % (3938313)------------------------------
% 16.79/2.84 % (3938313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938313)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938313)Termination reason: Instruction limit
% 16.79/2.84 % (3938313)Termination phase: Saturation
% 16.79/2.84 % (3938313)Time elapsed: 0.109 s
% 16.79/2.84 % (3938313)Peak memory usage: 14 MB
% 16.79/2.84 % (3938313)Instructions burned: 160 (million)
% 16.79/2.84 % TRYING [7]
% 16.79/2.84 % (3938327)ott-21_1_sil=16000:fs=off:random_seed=511737772:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.79/2.84 % TRYING [7]
% 16.79/2.84 % (3938323)Instruction limit reached!
% 16.79/2.84 % (3938323)------------------------------
% 16.79/2.84 % (3938323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938323)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938323)Termination reason: Instruction limit
% 16.79/2.84 % (3938323)Termination phase: Saturation
% 16.79/2.84 % (3938323)Time elapsed: 0.087 s
% 16.79/2.84 % (3938323)Peak memory usage: 13 MB
% 16.79/2.84 % (3938323)Instructions burned: 131 (million)
% 16.79/2.84 % (3938329)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4222921479:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 16.79/2.84 % (3938327)Instruction limit reached!
% 16.79/2.84 % (3938327)------------------------------
% 16.79/2.84 % (3938327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938327)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938327)Termination reason: Instruction limit
% 16.79/2.84 % (3938327)Termination phase: Saturation
% 16.79/2.84 % (3938327)Time elapsed: 0.097 s
% 16.79/2.84 % (3938327)Peak memory usage: 13 MB
% 16.79/2.84 % (3938327)Instructions burned: 180 (million)
% 16.79/2.84 % (3938321)Instruction limit reached!
% 16.79/2.84 % (3938321)------------------------------
% 16.79/2.84 % (3938321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938321)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938321)Termination reason: Instruction limit
% 16.79/2.84 % (3938321)Termination phase: Finite model building SAT solving
% 16.79/2.84 % (3938321)Time elapsed: 0.181 s
% 16.79/2.84 % (3938321)Peak memory usage: 30 MB
% 16.79/2.84 % (3938321)Instructions burned: 717 (million)
% 16.79/2.84 % (3938332)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1302321309:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 16.79/2.84 % (3938331)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3057296100:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 16.79/2.84 % Detected minimum model sizes of [4]
% 16.79/2.84 % Detected maximum model sizes of [max]
% 16.79/2.84 % TRYING [4]
% 16.79/2.84 % TRYING [5]
% 16.79/2.84 % TRYING [6]
% 16.79/2.84 % TRYING [8]
% 16.79/2.84 % TRYING [7]
% 16.79/2.84 % (3938324)Instruction limit reached!
% 16.79/2.84 % (3938324)------------------------------
% 16.79/2.84 % (3938324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938324)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938324)Termination reason: Instruction limit
% 16.79/2.84 % (3938324)Termination phase: Saturation
% 16.79/2.84 % (3938324)Time elapsed: 0.412 s
% 16.79/2.84 % (3938324)Peak memory usage: 20 MB
% 16.79/2.84 % (3938324)Instructions burned: 684 (million)
% 16.79/2.84 % (3938335)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2440013696:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 16.79/2.84 % (3938329)Instruction limit reached!
% 16.79/2.84 % (3938329)------------------------------
% 16.79/2.84 % (3938329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938329)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938329)Termination reason: Instruction limit
% 16.79/2.84 % (3938329)Termination phase: Saturation
% 16.79/2.84 % (3938329)Time elapsed: 0.335 s
% 16.79/2.84 % (3938329)Peak memory usage: 14 MB
% 16.79/2.84 % (3938329)Instructions burned: 477 (million)
% 16.79/2.84 % (3938337)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2353691887:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 16.79/2.84 % (3938331)Instruction limit reached!
% 16.79/2.84 % (3938331)------------------------------
% 16.79/2.84 % (3938331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938331)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938331)Termination reason: Instruction limit
% 16.79/2.84 % (3938331)Termination phase: Finite model building SAT solving
% 16.79/2.84 % (3938331)Time elapsed: 0.363 s
% 16.79/2.84 % (3938331)Peak memory usage: 24 MB
% 16.79/2.84 % (3938331)Instructions burned: 866 (million)
% 16.79/2.84 % (3938332)Instruction limit reached!
% 16.79/2.84 % (3938332)------------------------------
% 16.79/2.84 % (3938332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938332)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938332)Termination reason: Instruction limit
% 16.79/2.84 % (3938332)Termination phase: Saturation
% 16.79/2.84 % (3938332)Time elapsed: 0.371 s
% 16.79/2.84 % (3938332)Peak memory usage: 25 MB
% 16.79/2.84 % (3938332)Instructions burned: 1180 (million)
% 16.79/2.84 % TRYING [14]
% 16.79/2.84 % (3938340)fmb+10_1_sil=64000:random_seed=2465921936:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 16.79/2.84 % Detected minimum model sizes of [4]
% 16.79/2.84 % Detected maximum model sizes of [max]
% 16.79/2.84 % TRYING [4]
% 16.79/2.84 % (3938339)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3548170296:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 16.79/2.84 % TRYING [5]
% 16.79/2.84 % TRYING [6]
% 16.79/2.84 % TRYING [7]
% 16.79/2.84 % (3938335)Instruction limit reached!
% 16.79/2.84 % (3938335)------------------------------
% 16.79/2.84 % (3938335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938335)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938335)Termination reason: Instruction limit
% 16.79/2.84 % (3938335)Termination phase: Finite model building constraint generation
% 16.79/2.84 % (3938335)Time elapsed: 0.346 s
% 16.79/2.84 % (3938335)Peak memory usage: 83 MB
% 16.79/2.84 % (3938335)Instructions burned: 889 (million)
% 16.79/2.84 % (3938337)Instruction limit reached!
% 16.79/2.84 % (3938337)------------------------------
% 16.79/2.84 % (3938337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938337)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938337)Termination reason: Instruction limit
% 16.79/2.84 % (3938337)Termination phase: Saturation
% 16.79/2.84 % (3938337)Time elapsed: 0.342 s
% 16.79/2.84 % (3938337)Peak memory usage: 16 MB
% 16.79/2.84 % (3938337)Instructions burned: 693 (million)
% 16.79/2.84 % (3938343)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1381035887:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 16.79/2.84 % Detected minimum model sizes of [4]
% 16.79/2.84 % Detected maximum model sizes of [max]
% 16.79/2.84 % TRYING [20]
% 16.79/2.84 % (3938344)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1996780260:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 16.79/2.84 % Detected minimum model sizes of [4]
% 16.79/2.84 % Detected maximum model sizes of [max]
% 16.79/2.84 % TRYING [8]
% 16.79/2.84 % TRYING [8]
% 16.79/2.84 % (3938339)Instruction limit reached!
% 16.79/2.84 % (3938339)------------------------------
% 16.79/2.84 % (3938339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938339)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938339)Termination reason: Instruction limit
% 16.79/2.84 % (3938339)Termination phase: Saturation
% 16.79/2.84 % (3938339)Time elapsed: 0.509 s
% 16.79/2.84 % (3938339)Peak memory usage: 18 MB
% 16.79/2.84 % (3938339)Instructions burned: 881 (million)
% 16.79/2.84 % (3938347)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2084600382:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 16.79/2.84 % TRYING [9]
% 16.79/2.84 % (3938344)Instruction limit reached!
% 16.79/2.84 % (3938344)------------------------------
% 16.79/2.84 % (3938344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.84 % (3938344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.84 % (3938344)CaDiCaL version: 2.1.3
% 16.79/2.84 % (3938344)Termination reason: Instruction limit
% 16.79/2.84 % (3938344)Termination phase: Finite model building SAT solving
% 16.79/2.84 % (3938344)Time elapsed: 0.502 s
% 16.79/2.84 % (3938344)Peak memory usage: 48 MB
% 16.79/2.84 % (3938344)Instructions burned: 921 (million)
% 16.79/2.84 % (3938349)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3474740106:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 16.79/2.84 % TRYING [9]
% 16.79/2.84 % (3938308) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3938302-3938308"...
% 16.79/2.84 % (3938308)...printing done.
% 16.79/2.84 % (3938308)Refutation found. Thanks to Tanya!
% 16.79/2.84 % SZS status Theorem for theBenchmark
% 16.79/2.84 % SZS output start Proof for theBenchmark
% See solution above
% 16.79/2.85 % (3938308)------------------------------
% 16.79/2.85 % (3938308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.79/2.85 % (3938308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.79/2.85 % (3938308)CaDiCaL version: 2.1.3
% 16.79/2.85 % (3938308)Termination reason: Refutation
% 16.79/2.85 % (3938308)Time elapsed: 2.346 s
% 16.79/2.85 % (3938308)Peak memory usage: 32 MB
% 16.79/2.85 % (3938308)Instructions burned: 3948 (million)
% 16.79/2.85 % (3938302)Success in time 2.416 s
% 16.79/2.85 % Vampire exiting
%------------------------------------------------------------------------------