%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PRO012+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:38 PM UTC 2026
% Result : Theorem 48.55s 7.33s
% Output : Refutation 48.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 33
% Syntax : Number of formulae : 219 ( 26 unt; 11 def)
% Number of atoms : 675 ( 47 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 763 ( 307 ~; 331 |; 85 &)
% ( 17 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 12 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 294 ( 0 sgn 261 !; 33 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
fof(f5,axiom,
! [X0,X1,X2,X3] :
( ( occurrence_of(X1,X0)
& arboreal(X2)
& arboreal(X3)
& subactivity_occurrence(X2,X1)
& subactivity_occurrence(X3,X1) )
=> ( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f6,axiom,
! [X0,X1] :
( root(X1,X0)
=> ? [X2] :
( subactivity(X2,X0)
& atocc(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_05) ).
fof(f7,axiom,
! [X0,X1,X2] :
( min_precedes(X1,X2,X0)
=> ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_06) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( occurrence_of(X0,X1)
& occurrence_of(X0,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f12,axiom,
! [X0,X1] :
( subactivity_occurrence(X0,X1)
=> ( activity_occurrence(X0)
& activity_occurrence(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
fof(f13,axiom,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] :
( activity(X1)
& occurrence_of(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_12) ).
fof(f14,axiom,
! [X0] :
( legal(X0)
=> arboreal(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(f15,axiom,
! [X0,X1] :
( atocc(X0,X1)
<=> ? [X2] :
( subactivity(X1,X2)
& atomic(X2)
& occurrence_of(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
fof(f17,axiom,
! [X0,X1] :
( occurrence_of(X0,X1)
=> ( arboreal(X0)
<=> atomic(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_16) ).
fof(f20,axiom,
! [X0,X1] :
( root_occ(X0,X1)
<=> ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_19) ).
fof(f22,axiom,
! [X0,X1] :
( precedes(X0,X1)
<=> ( earlier(X0,X1)
& legal(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(f23,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> ~ root(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
fof(f25,axiom,
! [X0,X1,X2] :
( min_precedes(X0,X1,X2)
=> precedes(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
fof(f26,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
=> ( arboreal(X0)
& arboreal(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_25) ).
fof(f27,axiom,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
<=> ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_26) ).
fof(f28,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X0,X1,X2)
& occurrence_of(X3,X2)
& subactivity_occurrence(X1,X3) )
=> subactivity_occurrence(X0,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_27) ).
fof(f33,axiom,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2,X3] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& occurrence_of(X2,tptp4)
& min_precedes(X1,X2,tptp0)
& ( occurrence_of(X3,tptp2)
| occurrence_of(X3,tptp1) )
& min_precedes(X2,X3,tptp0)
& ! [X4] :
( min_precedes(X1,X4,tptp0)
=> ( X4 = X2
| X4 = X3 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
fof(f39,axiom,
atomic(tptp3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
fof(f43,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(f44,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(f46,conjecture,
! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp2)
| occurrence_of(X2,tptp1) )
& min_precedes(X1,X2,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f47,negated_conjecture,
~ ! [X0] :
( occurrence_of(X0,tptp0)
=> ? [X1,X2] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& ( occurrence_of(X2,tptp2)
| occurrence_of(X2,tptp1) )
& min_precedes(X1,X2,tptp0) ) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f48,plain,
! [X0,X1,X2] :
( ( min_precedes(X0,X1,X2)
& ~ ? [X3] :
( min_precedes(X0,X3,X2)
& min_precedes(X3,X1,X2) ) )
=> next_subocc(X0,X1,X2) ),
inference(unused_predicate_definition_removal,[],[f27]) ).
fof(f49,plain,
! [X0,X1] :
( atocc(X0,X1)
=> ? [X2] :
( subactivity(X1,X2)
& atomic(X2)
& occurrence_of(X0,X2) ) ),
inference(unused_predicate_definition_removal,[],[f15]) ).
fof(f50,plain,
! [X0,X1] :
( root(X1,X0)
=> ? [X2] : atocc(X1,X2) ),
inference(pure_predicate_removal,[],[f6]) ).
fof(f51,plain,
! [X0,X1] :
( atocc(X0,X1)
=> ? [X2] :
( atomic(X2)
& occurrence_of(X0,X2) ) ),
inference(pure_predicate_removal,[],[f49]) ).
fof(f52,plain,
! [X0] :
( activity_occurrence(X0)
=> ? [X1] : occurrence_of(X0,X1) ),
inference(pure_predicate_removal,[],[f13]) ).
fof(f53,plain,
! [X0,X1] :
( occurrence_of(X1,X0)
=> activity_occurrence(X1) ),
inference(pure_predicate_removal,[],[f4]) ).
fof(f61,plain,
! [X0,X1] :
( activity_occurrence(X1)
| ~ occurrence_of(X1,X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f62,plain,
! [X0,X1,X2,X3] :
( min_precedes(X2,X3,X0)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| ~ subactivity_occurrence(X3,X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f63,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,[],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( ? [X2] : atocc(X1,X2)
| ~ root(X1,X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ? [X3] :
( occurrence_of(X3,X0)
& subactivity_occurrence(X1,X3)
& subactivity_occurrence(X2,X3) )
| ~ min_precedes(X1,X2,X0) ),
inference(ennf_transformation,[],[f7]) ).
fof(f68,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(ennf_transformation,[],[f9]) ).
fof(f69,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ occurrence_of(X0,X1)
| ~ occurrence_of(X0,X2) ),
inference(flattening,[],[f68]) ).
fof(f74,plain,
! [X0,X1] :
( ( activity_occurrence(X0)
& activity_occurrence(X1) )
| ~ subactivity_occurrence(X0,X1) ),
inference(ennf_transformation,[],[f12]) ).
fof(f75,plain,
! [X0] :
( ? [X1] : occurrence_of(X0,X1)
| ~ activity_occurrence(X0) ),
inference(ennf_transformation,[],[f52]) ).
fof(f76,plain,
! [X0] :
( arboreal(X0)
| ~ legal(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f77,plain,
! [X0,X1] :
( ? [X2] :
( atomic(X2)
& occurrence_of(X0,X2) )
| ~ atocc(X0,X1) ),
inference(ennf_transformation,[],[f51]) ).
fof(f79,plain,
! [X0,X1] :
( ( arboreal(X0)
<=> atomic(X1) )
| ~ occurrence_of(X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ root(X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f23]) ).
fof(f84,plain,
! [X0,X1,X2] :
( precedes(X0,X1)
| ~ min_precedes(X0,X1,X2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f85,plain,
! [X0,X1,X2] :
( ( arboreal(X0)
& arboreal(X1) )
| ~ next_subocc(X0,X1,X2) ),
inference(ennf_transformation,[],[f26]) ).
fof(f86,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,[],[f48]) ).
fof(f87,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(flattening,[],[f86]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(ennf_transformation,[],[f28]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( subactivity_occurrence(X0,X3)
| ~ min_precedes(X0,X1,X2)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(flattening,[],[f88]) ).
fof(f98,plain,
! [X0] :
( ? [X1,X2,X3] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& occurrence_of(X2,tptp4)
& min_precedes(X1,X2,tptp0)
& ( occurrence_of(X3,tptp2)
| occurrence_of(X3,tptp1) )
& min_precedes(X2,X3,tptp0)
& ! [X4] :
( X4 = X2
| X4 = X3
| ~ min_precedes(X1,X4,tptp0) ) )
| ~ occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f99,plain,
! [X0] :
( ? [X1,X2,X3] :
( occurrence_of(X1,tptp3)
& root_occ(X1,X0)
& occurrence_of(X2,tptp4)
& min_precedes(X1,X2,tptp0)
& ( occurrence_of(X3,tptp2)
| occurrence_of(X3,tptp1) )
& min_precedes(X2,X3,tptp0)
& ! [X4] :
( X4 = X2
| X4 = X3
| ~ min_precedes(X1,X4,tptp0) ) )
| ~ occurrence_of(X0,tptp0) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
? [X0] :
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,X0)
| ( ~ occurrence_of(X2,tptp2)
& ~ occurrence_of(X2,tptp1) )
| ~ min_precedes(X1,X2,tptp0) )
& occurrence_of(X0,tptp0) ),
inference(ennf_transformation,[],[f47]) ).
fof(f102,plain,
! [X0,X1] :
( atocc(X1,sK1(X1))
| ~ root(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X1))],[f64]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( occurrence_of(sK2(X0,X1,X2),X0)
& subactivity_occurrence(X1,sK2(X0,X1,X2))
& subactivity_occurrence(X2,sK2(X0,X1,X2)) )
| ~ min_precedes(X1,X2,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1,X2))],[f65]) ).
fof(f105,plain,
! [X0] :
( occurrence_of(X0,sK4(X0))
| ~ activity_occurrence(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f75]) ).
fof(f106,plain,
! [X0,X1] :
( ( atomic(sK5(X0))
& occurrence_of(X0,sK5(X0)) )
| ~ atocc(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0))],[f77]) ).
fof(f111,plain,
! [X0,X1] :
( ( ( arboreal(X0)
| ~ atomic(X1) )
& ( atomic(X1)
| ~ arboreal(X0) ) )
| ~ occurrence_of(X0,X1) ),
inference(nnf_transformation,[],[f79]) ).
fof(f115,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ? [X2] :
( occurrence_of(X1,X2)
& subactivity_occurrence(X0,X1)
& root(X0,X2) )
| ~ root_occ(X0,X1) ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f116,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,[],[f115]) ).
fof(f117,plain,
! [X0,X1] :
( ( root_occ(X0,X1)
| ! [X2] :
( ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X0,X1)
| ~ root(X0,X2) ) )
& ( ( occurrence_of(X1,sK9(X0,X1))
& subactivity_occurrence(X0,X1)
& root(X0,sK9(X0,X1)) )
| ~ root_occ(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X3,sK9(X0,X1))],[f116]) ).
fof(f118,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f119,plain,
! [X0,X1] :
( ( precedes(X0,X1)
| ~ earlier(X0,X1)
| ~ legal(X1) )
& ( ( earlier(X0,X1)
& legal(X1) )
| ~ precedes(X0,X1) ) ),
inference(flattening,[],[f118]) ).
fof(f121,plain,
! [X0,X1,X2] :
( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| ( min_precedes(X0,sK11(X0,X1,X2),X2)
& min_precedes(sK11(X0,X1,X2),X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X3,sK11(X0,X1,X2))],[f87]) ).
fof(f122,plain,
! [X0] :
( ( occurrence_of(sK12(X0),tptp3)
& root_occ(sK12(X0),X0)
& occurrence_of(sK13(X0),tptp4)
& min_precedes(sK12(X0),sK13(X0),tptp0)
& ( occurrence_of(sK14(X0),tptp2)
| occurrence_of(sK14(X0),tptp1) )
& min_precedes(sK13(X0),sK14(X0),tptp0)
& ! [X4] :
( sK13(X0) = X4
| sK14(X0) = X4
| ~ min_precedes(sK12(X0),X4,tptp0) ) )
| ~ occurrence_of(X0,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0)),skolemize(X3,sK14(X0))],[f99]) ).
fof(f123,plain,
( ! [X1,X2] :
( ~ occurrence_of(X1,tptp3)
| ~ root_occ(X1,sK15)
| ( ~ occurrence_of(X2,tptp2)
& ~ occurrence_of(X2,tptp1) )
| ~ min_precedes(X1,X2,tptp0) )
& occurrence_of(sK15,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X0,sK15)],[f100]) ).
fof(f128,plain,
! [X0,X1] :
( ~ occurrence_of(X1,X0)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f129,plain,
! [X2,X3,X0,X1] :
( ~ subactivity_occurrence(X3,X1)
| min_precedes(X3,X2,X0)
| X2 = X3
| ~ occurrence_of(X1,X0)
| ~ arboreal(X2)
| ~ arboreal(X3)
| ~ subactivity_occurrence(X2,X1)
| min_precedes(X2,X3,X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f130,plain,
! [X0,X1] :
( ~ root(X1,X0)
| atocc(X1,sK1(X1)) ),
inference(cnf_transformation,[],[f102]) ).
fof(f131,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X2,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f132,plain,
! [X2,X0,X1] :
( subactivity_occurrence(X1,sK2(X0,X1,X2))
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f133,plain,
! [X2,X0,X1] :
( occurrence_of(sK2(X0,X1,X2),X0)
| ~ min_precedes(X1,X2,X0) ),
inference(cnf_transformation,[],[f103]) ).
fof(f136,plain,
! [X2,X0,X1] :
( ~ occurrence_of(X0,X2)
| ~ occurrence_of(X0,X1)
| X1 = X2 ),
inference(cnf_transformation,[],[f69]) ).
fof(f139,plain,
! [X0,X1] :
( ~ subactivity_occurrence(X0,X1)
| activity_occurrence(X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f141,plain,
! [X0] :
( occurrence_of(X0,sK4(X0))
| ~ activity_occurrence(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f142,plain,
! [X0] :
( ~ legal(X0)
| arboreal(X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f143,plain,
! [X0,X1] :
( ~ atocc(X0,X1)
| occurrence_of(X0,sK5(X0)) ),
inference(cnf_transformation,[],[f106]) ).
fof(f150,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| ~ atomic(X1)
| arboreal(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f156,plain,
! [X0,X1] :
( root(X0,sK9(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f158,plain,
! [X0,X1] :
( occurrence_of(X1,sK9(X0,X1))
| ~ root_occ(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
fof(f161,plain,
! [X0,X1] :
( ~ precedes(X0,X1)
| legal(X1) ),
inference(cnf_transformation,[],[f119]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| ~ root(X1,X2) ),
inference(cnf_transformation,[],[f82]) ).
fof(f167,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| precedes(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
fof(f168,plain,
! [X2,X0,X1] :
( ~ next_subocc(X0,X1,X2)
| arboreal(X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f170,plain,
! [X2,X0,X1] :
( min_precedes(sK11(X0,X1,X2),X1,X2)
| ~ min_precedes(X0,X1,X2)
| next_subocc(X0,X1,X2) ),
inference(cnf_transformation,[],[f121]) ).
fof(f172,plain,
! [X2,X3,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| subactivity_occurrence(X0,X3)
| ~ occurrence_of(X3,X2)
| ~ subactivity_occurrence(X1,X3) ),
inference(cnf_transformation,[],[f89]) ).
fof(f178,plain,
! [X0] :
( min_precedes(sK13(X0),sK14(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f179,plain,
! [X0] :
( occurrence_of(sK14(X0),tptp1)
| occurrence_of(sK14(X0),tptp2)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f180,plain,
! [X0] :
( min_precedes(sK12(X0),sK13(X0),tptp0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f182,plain,
! [X0] :
( root_occ(sK12(X0),X0)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f183,plain,
! [X0] :
( occurrence_of(sK12(X0),tptp3)
| ~ occurrence_of(X0,tptp0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f188,plain,
atomic(tptp3),
inference(cnf_transformation,[],[f39]) ).
fof(f192,plain,
tptp3 != tptp2,
inference(cnf_transformation,[],[f43]) ).
fof(f193,plain,
tptp3 != tptp1,
inference(cnf_transformation,[],[f44]) ).
fof(f195,plain,
occurrence_of(sK15,tptp0),
inference(cnf_transformation,[],[f123]) ).
fof(f196,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK15)
| ~ occurrence_of(X2,tptp1)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[],[f123]) ).
fof(f197,plain,
! [X2,X1] :
( ~ min_precedes(X1,X2,tptp0)
| ~ root_occ(X1,sK15)
| ~ occurrence_of(X2,tptp2)
| ~ occurrence_of(X1,tptp3) ),
inference(cnf_transformation,[],[f123]) ).
fof(f210,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| ~ atomic(tptp3)
| arboreal(sK12(X0)) ),
inference(resolution,[],[f183,f150]) ).
fof(f213,plain,
! [X0] :
( arboreal(sK12(X0))
| ~ occurrence_of(X0,tptp0) ),
inference(forward_subsumption_resolution,[],[f210,f188]) ).
fof(f227,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK4(X0) = X1
| ~ activity_occurrence(X0) ),
inference(resolution,[],[f136,f141]) ).
fof(f230,plain,
! [X0,X1] :
( ~ occurrence_of(sK12(X0),X1)
| tptp3 = X1
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f136,f183]) ).
fof(f232,plain,
! [X0] :
( ~ occurrence_of(sK15,X0)
| tptp0 = X0 ),
inference(resolution,[],[f136,f195]) ).
fof(f233,plain,
! [X0,X1] :
( ~ occurrence_of(X0,X1)
| sK4(X0) = X1 ),
inference(forward_subsumption_resolution,[],[f227,f128]) ).
fof(f237,plain,
! [X0] :
( ~ root_occ(X0,sK15)
| tptp0 = sK9(X0,sK15) ),
inference(resolution,[],[f232,f158]) ).
fof(f246,plain,
( tptp0 = sK9(sK12(sK15),sK15)
| ~ occurrence_of(sK15,tptp0) ),
inference(resolution,[],[f237,f182]) ).
fof(f247,plain,
tptp0 = sK9(sK12(sK15),sK15),
inference(forward_subsumption_resolution,[],[f246,f195]) ).
fof(f257,plain,
( root(sK12(sK15),tptp0)
| ~ root_occ(sK12(sK15),sK15) ),
inference(superposition,[],[f156,f247]) ).
fof(f259,definition,
( spl16_1
<=> root_occ(sK12(sK15),sK15) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f260,plain,
( root_occ(sK12(sK15),sK15)
| ~ spl16_1 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f261,plain,
( ~ root_occ(sK12(sK15),sK15)
| spl16_1 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f263,definition,
( spl16_2
<=> root(sK12(sK15),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f265,plain,
( root(sK12(sK15),tptp0)
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f266,plain,
( ~ spl16_1
| spl16_2 ),
inference(avatar_split_clause,[],[f257,f263,f259]) ).
fof(f269,plain,
( ~ occurrence_of(sK15,tptp0)
| spl16_1 ),
inference(resolution,[],[f261,f182]) ).
fof(f270,plain,
( $false
| spl16_1 ),
inference(forward_subsumption_resolution,[],[f269,f195]) ).
fof(f271,plain,
spl16_1,
inference(avatar_contradiction_clause,[],[f270]) ).
fof(f279,plain,
! [X2,X0,X1] :
( activity_occurrence(sK2(X2,X0,X1))
| ~ min_precedes(X0,X1,X2) ),
inference(resolution,[],[f131,f139]) ).
fof(f287,plain,
( atocc(sK12(sK15),sK1(sK12(sK15)))
| ~ spl16_2 ),
inference(resolution,[],[f265,f130]) ).
fof(f300,plain,
( occurrence_of(sK12(sK15),sK5(sK12(sK15)))
| ~ spl16_2 ),
inference(resolution,[],[f287,f143]) ).
fof(f306,plain,
( ! [X0] :
( ~ occurrence_of(sK12(sK15),X0)
| sK5(sK12(sK15)) = X0 )
| ~ spl16_2 ),
inference(resolution,[],[f300,f136]) ).
fof(f316,plain,
( tptp3 = sK5(sK12(sK15))
| ~ occurrence_of(sK15,tptp0)
| ~ spl16_2 ),
inference(resolution,[],[f306,f183]) ).
fof(f322,plain,
( tptp3 = sK5(sK12(sK15))
| ~ spl16_2 ),
inference(forward_subsumption_resolution,[],[f316,f195]) ).
fof(f332,plain,
( occurrence_of(sK12(sK15),tptp3)
| ~ spl16_2 ),
inference(superposition,[],[f300,f322]) ).
fof(f377,plain,
! [X0,X1] :
( ~ subactivity_occurrence(sK13(X0),X1)
| ~ occurrence_of(X1,tptp0)
| subactivity_occurrence(sK12(X0),X1)
| ~ occurrence_of(X0,tptp0) ),
inference(resolution,[],[f172,f180]) ).
fof(f396,plain,
! [X2,X0,X1] :
( precedes(sK11(X0,X1,X2),X1)
| next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2) ),
inference(resolution,[],[f170,f167]) ).
fof(f444,plain,
! [X2,X3,X0,X1,X4] :
( ~ subactivity_occurrence(X1,sK2(X3,X4,X0))
| X0 = X1
| ~ occurrence_of(sK2(X3,X4,X0),X2)
| ~ arboreal(X1)
| ~ arboreal(X0)
| min_precedes(X0,X1,X2)
| min_precedes(X1,X0,X2)
| ~ min_precedes(X4,X0,X3) ),
inference(resolution,[],[f129,f131]) ).
fof(f519,plain,
! [X2,X0,X1] :
( ~ min_precedes(X1,X2,X0)
| sK4(sK2(X0,X1,X2)) = X0 ),
inference(resolution,[],[f233,f133]) ).
fof(f968,plain,
! [X2,X0,X1] :
( subactivity_occurrence(sK12(X1),sK2(X0,sK13(X1),X2))
| ~ occurrence_of(sK2(X0,sK13(X1),X2),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK13(X1),X2,X0) ),
inference(resolution,[],[f377,f132]) ).
fof(f972,plain,
! [X2,X0,X1] :
( next_subocc(X0,X1,X2)
| ~ min_precedes(X0,X1,X2)
| legal(X1) ),
inference(resolution,[],[f396,f161]) ).
fof(f1657,definition,
( spl16_47
<=> occurrence_of(sK14(sK15),tptp1) ),
introduced(definition,[new_symbols(definition,[spl16_47])],[avatar_definition]) ).
fof(f1658,plain,
( occurrence_of(sK14(sK15),tptp1)
| ~ spl16_47 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1659,plain,
( ~ occurrence_of(sK14(sK15),tptp1)
| spl16_47 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1665,definition,
( spl16_49
<=> occurrence_of(sK14(sK15),tptp2) ),
introduced(definition,[new_symbols(definition,[spl16_49])],[avatar_definition]) ).
fof(f1666,plain,
( occurrence_of(sK14(sK15),tptp2)
| ~ spl16_49 ),
inference(avatar_component_clause,[],[f1665]) ).
fof(f1726,plain,
( occurrence_of(sK14(sK15),tptp2)
| ~ occurrence_of(sK15,tptp0)
| spl16_47 ),
inference(resolution,[],[f1659,f179]) ).
fof(f1727,plain,
( occurrence_of(sK14(sK15),tptp2)
| spl16_47 ),
inference(forward_subsumption_resolution,[],[f1726,f195]) ).
fof(f1728,plain,
( spl16_49
| spl16_47 ),
inference(avatar_split_clause,[],[f1727,f1657,f1665]) ).
fof(f1897,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| legal(X1)
| arboreal(X1) ),
inference(resolution,[],[f972,f168]) ).
fof(f1898,plain,
! [X2,X0,X1] :
( ~ min_precedes(X0,X1,X2)
| arboreal(X1) ),
inference(forward_subsumption_resolution,[],[f1897,f142]) ).
fof(f1953,plain,
! [X0] :
( ~ occurrence_of(X0,tptp0)
| tptp0 = sK4(sK2(tptp0,sK13(X0),sK14(X0))) ),
inference(resolution,[],[f519,f178]) ).
fof(f3419,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X0,sK13(X1),X2),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK13(X1),X2,X0)
| sK12(X1) = X2
| ~ occurrence_of(sK2(X0,sK13(X1),X2),X3)
| ~ arboreal(sK12(X1))
| ~ arboreal(X2)
| min_precedes(X2,sK12(X1),X3)
| min_precedes(sK12(X1),X2,X3)
| ~ min_precedes(sK13(X1),X2,X0) ),
inference(resolution,[],[f968,f444]) ).
fof(f3424,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X0,sK13(X1),X2),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK13(X1),X2,X0)
| sK12(X1) = X2
| ~ occurrence_of(sK2(X0,sK13(X1),X2),X3)
| ~ arboreal(sK12(X1))
| ~ arboreal(X2)
| min_precedes(X2,sK12(X1),X3)
| min_precedes(sK12(X1),X2,X3) ),
inference(duplicate_literal_removal,[],[f3419]) ).
fof(f3429,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X0,sK13(X1),X2),tptp0)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK13(X1),X2,X0)
| sK12(X1) = X2
| ~ occurrence_of(sK2(X0,sK13(X1),X2),X3)
| ~ arboreal(X2)
| min_precedes(X2,sK12(X1),X3)
| min_precedes(sK12(X1),X2,X3) ),
inference(forward_subsumption_resolution,[],[f3424,f213]) ).
fof(f7108,plain,
tptp0 = sK4(sK2(tptp0,sK13(sK15),sK14(sK15))),
inference(resolution,[],[f1953,f195]) ).
fof(f7120,plain,
( occurrence_of(sK2(tptp0,sK13(sK15),sK14(sK15)),tptp0)
| ~ activity_occurrence(sK2(tptp0,sK13(sK15),sK14(sK15))) ),
inference(superposition,[],[f141,f7108]) ).
fof(f7122,definition,
( spl16_187
<=> activity_occurrence(sK2(tptp0,sK13(sK15),sK14(sK15))) ),
introduced(definition,[new_symbols(definition,[spl16_187])],[avatar_definition]) ).
fof(f7124,plain,
( ~ activity_occurrence(sK2(tptp0,sK13(sK15),sK14(sK15)))
| spl16_187 ),
inference(avatar_component_clause,[],[f7122]) ).
fof(f7126,definition,
( spl16_188
<=> occurrence_of(sK2(tptp0,sK13(sK15),sK14(sK15)),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_188])],[avatar_definition]) ).
fof(f7128,plain,
( occurrence_of(sK2(tptp0,sK13(sK15),sK14(sK15)),tptp0)
| ~ spl16_188 ),
inference(avatar_component_clause,[],[f7126]) ).
fof(f7129,plain,
( ~ spl16_187
| spl16_188 ),
inference(avatar_split_clause,[],[f7120,f7126,f7122]) ).
fof(f7144,plain,
( ~ min_precedes(sK13(sK15),sK14(sK15),tptp0)
| spl16_187 ),
inference(resolution,[],[f7124,f279]) ).
fof(f7145,plain,
( ~ occurrence_of(sK15,tptp0)
| spl16_187 ),
inference(resolution,[],[f7144,f178]) ).
fof(f7146,plain,
( $false
| spl16_187 ),
inference(forward_subsumption_resolution,[],[f7145,f195]) ).
fof(f7147,plain,
spl16_187,
inference(avatar_contradiction_clause,[],[f7146]) ).
fof(f11905,definition,
( spl16_350
<=> min_precedes(sK14(sK15),sK12(sK15),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_350])],[avatar_definition]) ).
fof(f11906,plain,
( min_precedes(sK14(sK15),sK12(sK15),tptp0)
| ~ spl16_350 ),
inference(avatar_component_clause,[],[f11905]) ).
fof(f14885,definition,
( spl16_414
<=> occurrence_of(sK12(sK15),tptp1) ),
introduced(definition,[new_symbols(definition,[spl16_414])],[avatar_definition]) ).
fof(f14886,plain,
( occurrence_of(sK12(sK15),tptp1)
| ~ spl16_414 ),
inference(avatar_component_clause,[],[f14885]) ).
fof(f14887,plain,
( ~ occurrence_of(sK12(sK15),tptp1)
| spl16_414 ),
inference(avatar_component_clause,[],[f14885]) ).
fof(f14894,definition,
( spl16_416
<=> occurrence_of(sK12(sK15),tptp2) ),
introduced(definition,[new_symbols(definition,[spl16_416])],[avatar_definition]) ).
fof(f14895,plain,
( occurrence_of(sK12(sK15),tptp2)
| ~ spl16_416 ),
inference(avatar_component_clause,[],[f14894]) ).
fof(f14896,plain,
( ~ occurrence_of(sK12(sK15),tptp2)
| spl16_416 ),
inference(avatar_component_clause,[],[f14894]) ).
fof(f19932,plain,
! [X2,X3,X0,X1] :
( ~ occurrence_of(sK2(X0,sK13(X1),X2),X3)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(sK13(X1),X2,X0)
| sK12(X1) = X2
| ~ occurrence_of(sK2(X0,sK13(X1),X2),tptp0)
| min_precedes(X2,sK12(X1),X3)
| min_precedes(sK12(X1),X2,X3) ),
inference(forward_subsumption_resolution,[],[f3429,f1898]) ).
fof(f19935,plain,
( ~ occurrence_of(sK15,tptp0)
| ~ min_precedes(sK13(sK15),sK14(sK15),tptp0)
| sK12(sK15) = sK14(sK15)
| ~ occurrence_of(sK2(tptp0,sK13(sK15),sK14(sK15)),tptp0)
| min_precedes(sK14(sK15),sK12(sK15),tptp0)
| min_precedes(sK12(sK15),sK14(sK15),tptp0)
| ~ spl16_188 ),
inference(resolution,[],[f19932,f7128]) ).
fof(f19943,plain,
( ~ occurrence_of(sK15,tptp0)
| sK12(sK15) = sK14(sK15)
| ~ occurrence_of(sK2(tptp0,sK13(sK15),sK14(sK15)),tptp0)
| min_precedes(sK14(sK15),sK12(sK15),tptp0)
| min_precedes(sK12(sK15),sK14(sK15),tptp0)
| ~ spl16_188 ),
inference(forward_subsumption_resolution,[],[f19935,f178]) ).
fof(f19946,plain,
( sK12(sK15) = sK14(sK15)
| ~ occurrence_of(sK2(tptp0,sK13(sK15),sK14(sK15)),tptp0)
| min_precedes(sK14(sK15),sK12(sK15),tptp0)
| min_precedes(sK12(sK15),sK14(sK15),tptp0)
| ~ spl16_188 ),
inference(forward_subsumption_resolution,[],[f19943,f195]) ).
fof(f19949,plain,
( sK12(sK15) = sK14(sK15)
| min_precedes(sK14(sK15),sK12(sK15),tptp0)
| min_precedes(sK12(sK15),sK14(sK15),tptp0)
| ~ spl16_188 ),
inference(forward_subsumption_resolution,[],[f19946,f7128]) ).
fof(f19967,definition,
( spl16_582
<=> min_precedes(sK12(sK15),sK14(sK15),tptp0) ),
introduced(definition,[new_symbols(definition,[spl16_582])],[avatar_definition]) ).
fof(f19969,plain,
( min_precedes(sK12(sK15),sK14(sK15),tptp0)
| ~ spl16_582 ),
inference(avatar_component_clause,[],[f19967]) ).
fof(f19971,definition,
( spl16_583
<=> sK12(sK15) = sK14(sK15) ),
introduced(definition,[new_symbols(definition,[spl16_583])],[avatar_definition]) ).
fof(f19972,plain,
( sK12(sK15) != sK14(sK15)
| spl16_583 ),
inference(avatar_component_clause,[],[f19971]) ).
fof(f19973,plain,
( sK12(sK15) = sK14(sK15)
| ~ spl16_583 ),
inference(avatar_component_clause,[],[f19971]) ).
fof(f20244,plain,
( occurrence_of(sK12(sK15),tptp1)
| occurrence_of(sK12(sK15),tptp2)
| ~ occurrence_of(sK15,tptp0)
| ~ spl16_583 ),
inference(superposition,[],[f179,f19973]) ).
fof(f20558,plain,
( occurrence_of(sK12(sK15),tptp2)
| ~ occurrence_of(sK15,tptp0)
| spl16_414
| ~ spl16_583 ),
inference(forward_subsumption_resolution,[],[f20244,f14887]) ).
fof(f20885,plain,
( ~ occurrence_of(sK15,tptp0)
| spl16_414
| spl16_416
| ~ spl16_583 ),
inference(forward_subsumption_resolution,[],[f20558,f14896]) ).
fof(f20981,plain,
( $false
| spl16_414
| spl16_416
| ~ spl16_583 ),
inference(forward_subsumption_resolution,[],[f20885,f195]) ).
fof(f20982,plain,
( spl16_414
| spl16_416
| ~ spl16_583 ),
inference(avatar_contradiction_clause,[],[f20981]) ).
fof(f21072,plain,
( ~ root_occ(sK12(sK15),sK15)
| ~ occurrence_of(sK14(sK15),tptp2)
| ~ occurrence_of(sK12(sK15),tptp3)
| ~ spl16_582 ),
inference(resolution,[],[f19969,f197]) ).
fof(f21102,plain,
( ~ occurrence_of(sK14(sK15),tptp2)
| ~ occurrence_of(sK12(sK15),tptp3)
| ~ spl16_1
| ~ spl16_582 ),
inference(forward_subsumption_resolution,[],[f21072,f260]) ).
fof(f21104,plain,
( ~ occurrence_of(sK12(sK15),tptp3)
| ~ spl16_1
| ~ spl16_49
| ~ spl16_582 ),
inference(forward_subsumption_resolution,[],[f21102,f1666]) ).
fof(f21114,plain,
( $false
| ~ spl16_1
| ~ spl16_2
| ~ spl16_49
| ~ spl16_582 ),
inference(forward_subsumption_resolution,[],[f21104,f332]) ).
fof(f21115,plain,
( ~ spl16_1
| ~ spl16_2
| ~ spl16_49
| ~ spl16_582 ),
inference(avatar_contradiction_clause,[],[f21114]) ).
fof(f21119,plain,
( min_precedes(sK14(sK15),sK12(sK15),tptp0)
| min_precedes(sK12(sK15),sK14(sK15),tptp0)
| ~ spl16_188
| spl16_583 ),
inference(forward_subsumption_resolution,[],[f19949,f19972]) ).
fof(f21123,plain,
( spl16_582
| spl16_350
| ~ spl16_188
| spl16_583 ),
inference(avatar_split_clause,[],[f21119,f19971,f7126,f11905,f19967]) ).
fof(f21422,plain,
( ~ root(sK12(sK15),tptp0)
| ~ spl16_350 ),
inference(resolution,[],[f11906,f164]) ).
fof(f21441,plain,
( $false
| ~ spl16_2
| ~ spl16_350 ),
inference(forward_subsumption_resolution,[],[f21422,f265]) ).
fof(f21442,plain,
( ~ spl16_2
| ~ spl16_350 ),
inference(avatar_contradiction_clause,[],[f21441]) ).
fof(f22265,plain,
( tptp3 = tptp1
| ~ occurrence_of(sK15,tptp0)
| ~ spl16_414 ),
inference(resolution,[],[f14886,f230]) ).
fof(f22274,plain,
( ~ occurrence_of(sK15,tptp0)
| ~ spl16_414 ),
inference(forward_subsumption_resolution,[],[f22265,f193]) ).
fof(f22280,plain,
( $false
| ~ spl16_414 ),
inference(forward_subsumption_resolution,[],[f22274,f195]) ).
fof(f22281,plain,
~ spl16_414,
inference(avatar_contradiction_clause,[],[f22280]) ).
fof(f22323,plain,
( tptp3 = tptp2
| ~ occurrence_of(sK15,tptp0)
| ~ spl16_416 ),
inference(resolution,[],[f14895,f230]) ).
fof(f22332,plain,
( ~ occurrence_of(sK15,tptp0)
| ~ spl16_416 ),
inference(forward_subsumption_resolution,[],[f22323,f192]) ).
fof(f22338,plain,
( $false
| ~ spl16_416 ),
inference(forward_subsumption_resolution,[],[f22332,f195]) ).
fof(f22339,plain,
~ spl16_416,
inference(avatar_contradiction_clause,[],[f22338]) ).
fof(f23333,plain,
( ~ root_occ(sK12(sK15),sK15)
| ~ occurrence_of(sK14(sK15),tptp1)
| ~ occurrence_of(sK12(sK15),tptp3)
| ~ spl16_582 ),
inference(resolution,[],[f19969,f196]) ).
fof(f23355,plain,
( ~ occurrence_of(sK14(sK15),tptp1)
| ~ occurrence_of(sK12(sK15),tptp3)
| ~ spl16_1
| ~ spl16_582 ),
inference(forward_subsumption_resolution,[],[f23333,f260]) ).
fof(f23357,plain,
( ~ occurrence_of(sK12(sK15),tptp3)
| ~ spl16_1
| ~ spl16_47
| ~ spl16_582 ),
inference(forward_subsumption_resolution,[],[f23355,f1658]) ).
fof(f23359,plain,
( $false
| ~ spl16_1
| ~ spl16_2
| ~ spl16_47
| ~ spl16_582 ),
inference(forward_subsumption_resolution,[],[f23357,f332]) ).
fof(f23360,plain,
( ~ spl16_1
| ~ spl16_2
| ~ spl16_47
| ~ spl16_582 ),
inference(avatar_contradiction_clause,[],[f23359]) ).
cnf(s1,plain,
( ~ spl16_1
| spl16_2 ),
inference(sat_conversion,[],[f266]) ).
cnf(s2,plain,
spl16_1,
inference(sat_conversion,[],[f271]) ).
cnf(s65,plain,
( spl16_47
| spl16_49 ),
inference(sat_conversion,[],[f1728]) ).
cnf(s245,plain,
( ~ spl16_187
| spl16_188 ),
inference(sat_conversion,[],[f7129]) ).
cnf(s247,plain,
spl16_187,
inference(sat_conversion,[],[f7147]) ).
cnf(s752,plain,
( spl16_414
| spl16_416
| ~ spl16_583 ),
inference(sat_conversion,[],[f20982]) ).
cnf(s758,plain,
( ~ spl16_1
| ~ spl16_2
| ~ spl16_49
| ~ spl16_582 ),
inference(sat_conversion,[],[f21115]) ).
cnf(s760,plain,
( ~ spl16_188
| spl16_350
| spl16_582
| spl16_583 ),
inference(sat_conversion,[],[f21123]) ).
cnf(s766,plain,
( ~ spl16_2
| ~ spl16_350 ),
inference(sat_conversion,[],[f21442]) ).
cnf(s925,plain,
~ spl16_414,
inference(sat_conversion,[],[f22281]) ).
cnf(s934,plain,
~ spl16_416,
inference(sat_conversion,[],[f22339]) ).
cnf(s969,plain,
( ~ spl16_1
| ~ spl16_2
| ~ spl16_47
| ~ spl16_582 ),
inference(sat_conversion,[],[f23360]) ).
cnf(s971,plain,
~ spl16_583,
inference(rat,[],[s752,s934,s925]) ).
cnf(s986,plain,
spl16_188,
inference(rat,[],[s245,s247]) ).
cnf(s1043,plain,
spl16_2,
inference(rat,[],[s1,s2]) ).
cnf(s1044,plain,
~ spl16_350,
inference(rat,[],[s766,s1043]) ).
cnf(s1055,plain,
spl16_582,
inference(rat,[],[s760,s971,s986,s1044]) ).
cnf(s1058,plain,
~ spl16_47,
inference(rat,[],[s969,s1043,s2,s1055]) ).
cnf(s1059,plain,
~ spl16_49,
inference(rat,[],[s758,s1043,s2,s1055]) ).
cnf(s1060,plain,
$false,
inference(rat,[],[s65,s1059,s1058]) ).
fof(f23361,plain,
$false,
inference(avatar_sat_refutation,[],[s1060]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PRO012+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 22:19:55 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.05/2.72 % (1830648)Will run a generic schedule for satisfiability detection.
% 16.05/2.72 % (1830657)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1478169237:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.05/2.72 % (1830654)% WARNING: option uhcvi not known.
% 16.05/2.72 % (1830653)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1233267376_2999 on theBenchmark for (2999ds/0Mi)
% 16.05/2.72 % (1830654)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3278857646:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.05/2.72 % (1830655)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1800295579:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.05/2.72 % (1830656)dis+10_1_sil=32000:sp=arity:random_seed=317202111:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.05/2.72 % (1830658)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3036862514:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.05/2.72 % (1830659)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1223793561:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.05/2.72 % Detected minimum model sizes of [4]
% 16.05/2.72 % Detected maximum model sizes of [max]
% 16.05/2.72 % TRYING [4]
% 16.05/2.72 % TRYING [5]
% 16.05/2.72 % (1830657)Instruction limit reached!
% 16.05/2.72 % (1830657)------------------------------
% 16.05/2.72 % (1830657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.05/2.72 % (1830657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.05/2.72 % (1830657)CaDiCaL version: 2.1.3
% 16.05/2.72 % (1830657)Termination reason: Instruction limit
% 16.05/2.72 % (1830657)Termination phase: Saturation
% 16.05/2.72 % (1830657)Time elapsed: 0.038 s
% 16.05/2.72 % (1830657)Peak memory usage: 12 MB
% 16.05/2.72 % (1830657)Instructions burned: 117 (million)
% 16.05/2.72 % TRYING [6]
% 16.05/2.72 % (1830667)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1817786929:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.05/2.72 % Detected minimum model sizes of [4]
% 16.05/2.72 % Detected maximum model sizes of [max]
% 16.05/2.72 % TRYING [4]
% 16.05/2.72 % TRYING [5]
% 16.05/2.72 % TRYING [6]
% 16.05/2.72 % (1830656)Instruction limit reached!
% 16.05/2.72 % (1830656)------------------------------
% 16.05/2.72 % (1830656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.05/2.72 % (1830656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.05/2.72 % (1830656)CaDiCaL version: 2.1.3
% 16.05/2.72 % (1830656)Termination reason: Instruction limit
% 16.05/2.72 % (1830656)Termination phase: Saturation
% 16.05/2.72 % (1830656)Time elapsed: 0.068 s
% 16.05/2.72 % (1830656)Peak memory usage: 12 MB
% 16.05/2.72 % (1830656)Instructions burned: 104 (million)
% 16.05/2.72 % (1830658)Instruction limit reached!
% 16.05/2.72 % (1830658)------------------------------
% 16.05/2.72 % (1830658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.05/2.72 % (1830658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.05/2.72 % (1830658)CaDiCaL version: 2.1.3
% 16.05/2.72 % (1830658)Termination reason: Instruction limit
% 16.05/2.72 % (1830658)Termination phase: Saturation
% 16.05/2.72 % (1830658)Time elapsed: 0.082 s
% 16.05/2.72 % (1830658)Peak memory usage: 13 MB
% 16.05/2.72 % (1830658)Instructions burned: 132 (million)
% 16.05/2.72 % TRYING [7]
% 16.05/2.72 % (1830669)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=394134006:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.05/2.72 % TRYING [7]
% 16.05/2.72 % (1830670)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=9362502:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.05/2.72 % (1830659)Instruction limit reached!
% 16.05/2.72 % (1830659)------------------------------
% 16.05/2.72 % (1830659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.05/2.72 % (1830659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.05/2.72 % (1830659)CaDiCaL version: 2.1.3
% 16.05/2.72 % (1830659)Termination reason: Instruction limit
% 16.05/2.72 % (1830659)Termination phase: Saturation
% 16.05/2.72 % (1830659)Time elapsed: 0.108 s
% 16.05/2.72 % (1830659)Peak memory usage: 14 MB
% 16.05/2.72 % (1830659)Instructions burned: 160 (million)
% 16.05/2.72 % (1830673)ott-21_1_sil=16000:fs=off:random_seed=1554538696:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.05/2.72 % TRYING [8]
% 16.05/2.72 % (1830669)Instruction limit reached!
% 39.72/6.12 % (1830669)------------------------------
% 39.72/6.12 % (1830669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.72/6.12 % (1830669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.72/6.12 % (1830669)CaDiCaL version: 2.1.3
% 39.72/6.12 % (1830669)Termination reason: Instruction limit
% 39.72/6.12 % (1830669)Termination phase: Saturation
% 39.72/6.12 % (1830669)Time elapsed: 0.090 s
% 39.72/6.12 % (1830669)Peak memory usage: 13 MB
% 39.72/6.12 % (1830669)Instructions burned: 133 (million)
% 39.72/6.12 % TRYING [8]
% 39.72/6.12 % (1830667)Instruction limit reached!
% 39.72/6.12 % (1830667)------------------------------
% 39.72/6.12 % (1830667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.72/6.12 % (1830667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.72/6.12 % (1830667)CaDiCaL version: 2.1.3
% 39.72/6.12 % (1830667)Termination reason: Instruction limit
% 39.72/6.12 % (1830667)Termination phase: Finite model building SAT solving
% 39.72/6.12 % (1830667)Time elapsed: 0.154 s
% 39.72/6.12 % (1830667)Peak memory usage: 30 MB
% 39.72/6.12 % (1830667)Instructions burned: 715 (million)
% 39.72/6.12 % (1830675)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3898212613:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 39.72/6.12 % (1830677)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4049186371:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 39.72/6.12 % Detected minimum model sizes of [4]
% 39.72/6.12 % Detected maximum model sizes of [max]
% 39.72/6.12 % TRYING [4]
% 39.72/6.12 % TRYING [5]
% 39.72/6.12 % (1830673)Instruction limit reached!
% 39.72/6.12 % (1830673)------------------------------
% 39.72/6.12 % (1830673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.72/6.12 % (1830673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.72/6.12 % (1830673)CaDiCaL version: 2.1.3
% 39.72/6.12 % (1830673)Termination reason: Instruction limit
% 39.72/6.12 % (1830673)Termination phase: Saturation
% 39.72/6.12 % (1830673)Time elapsed: 0.103 s
% 39.72/6.12 % (1830673)Peak memory usage: 12 MB
% 39.72/6.12 % (1830673)Instructions burned: 180 (million)
% 39.72/6.12 % TRYING [6]
% 39.72/6.12 % (1830679)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2332835345:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 39.72/6.12 % TRYING [7]
% 39.72/6.12 % (1830677)Instruction limit reached!
% 39.72/6.12 % (1830677)------------------------------
% 39.72/6.12 % (1830677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.72/6.12 % (1830677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.72/6.12 % (1830677)CaDiCaL version: 2.1.3
% 39.72/6.12 % (1830677)Termination reason: Instruction limit
% 39.72/6.12 % (1830677)Termination phase: Finite model building SAT solving
% 39.72/6.12 % (1830677)Time elapsed: 0.174 s
% 39.72/6.12 % (1830677)Peak memory usage: 20 MB
% 39.72/6.12 % (1830677)Instructions burned: 865 (million)
% 39.72/6.12 % (1830681)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3097412432:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 39.72/6.12 % TRYING [9]
% 39.72/6.12 % TRYING [14]
% 39.72/6.12 % (1830670)Instruction limit reached!
% 39.72/6.12 % (1830670)------------------------------
% 39.72/6.12 % (1830670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.72/6.12 % (1830670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.72/6.12 % (1830670)CaDiCaL version: 2.1.3
% 39.72/6.12 % (1830670)Termination reason: Instruction limit
% 39.72/6.12 % (1830670)Termination phase: Saturation
% 39.72/6.12 % (1830670)Time elapsed: 0.353 s
% 39.72/6.12 % (1830670)Peak memory usage: 21 MB
% 39.72/6.12 % (1830670)Instructions burned: 686 (million)
% 39.72/6.12 % (1830683)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=842229909:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 39.72/6.12 % (1830675)Instruction limit reached!
% 39.72/6.12 % (1830675)------------------------------
% 39.72/6.12 % (1830675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.72/6.12 % (1830675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.72/6.12 % (1830675)CaDiCaL version: 2.1.3
% 39.72/6.12 % (1830675)Termination reason: Instruction limit
% 39.72/6.12 % (1830675)Termination phase: Saturation
% 39.72/6.12 % (1830675)Time elapsed: 0.328 s
% 39.72/6.12 % (1830675)Peak memory usage: 14 MB
% 39.72/6.12 % (1830675)Instructions burned: 478 (million)
% 48.55/7.33 % (1830685)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2790079617:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 48.55/7.33 % (1830681)Instruction limit reached!
% 48.55/7.33 % (1830681)------------------------------
% 48.55/7.33 % (1830681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830681)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830681)Termination reason: Instruction limit
% 48.55/7.33 % (1830681)Termination phase: Finite model building constraint generation
% 48.55/7.33 % (1830681)Time elapsed: 0.189 s
% 48.55/7.33 % (1830681)Peak memory usage: 76 MB
% 48.55/7.33 % (1830681)Instructions burned: 891 (million)
% 48.55/7.33 % (1830687)fmb+10_1_sil=64000:random_seed=3898653402:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 48.55/7.33 % Detected minimum model sizes of [4]
% 48.55/7.33 % Detected maximum model sizes of [max]
% 48.55/7.33 % TRYING [4]
% 48.55/7.33 % TRYING [5]
% 48.55/7.33 % TRYING [6]
% 48.55/7.33 % TRYING [7]
% 48.55/7.33 % TRYING [8]
% 48.55/7.33 % TRYING [10]
% 48.55/7.33 % (1830683)Instruction limit reached!
% 48.55/7.33 % (1830683)------------------------------
% 48.55/7.33 % (1830683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830683)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830683)Termination reason: Instruction limit
% 48.55/7.33 % (1830683)Termination phase: Saturation
% 48.55/7.33 % (1830683)Time elapsed: 0.400 s
% 48.55/7.33 % (1830683)Peak memory usage: 22 MB
% 48.55/7.33 % (1830683)Instructions burned: 693 (million)
% 48.55/7.33 % (1830689)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2815426869:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 48.55/7.33 % Detected minimum model sizes of [4]
% 48.55/7.33 % Detected maximum model sizes of [max]
% 48.55/7.33 % TRYING [20]
% 48.55/7.33 % (1830679)Instruction limit reached!
% 48.55/7.33 % (1830679)------------------------------
% 48.55/7.33 % (1830679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830679)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830679)Termination reason: Instruction limit
% 48.55/7.33 % (1830679)Termination phase: Saturation
% 48.55/7.33 % (1830679)Time elapsed: 0.676 s
% 48.55/7.33 % (1830679)Peak memory usage: 26 MB
% 48.55/7.33 % (1830679)Instructions burned: 1181 (million)
% 48.55/7.33 % (1830691)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=546482298:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 48.55/7.33 % Detected minimum model sizes of [4]
% 48.55/7.33 % Detected maximum model sizes of [max]
% 48.55/7.33 % TRYING [8]
% 48.55/7.33 % (1830685)Instruction limit reached!
% 48.55/7.33 % (1830685)------------------------------
% 48.55/7.33 % (1830685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830685)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830685)Termination reason: Instruction limit
% 48.55/7.33 % (1830685)Termination phase: Saturation
% 48.55/7.33 % (1830685)Time elapsed: 0.511 s
% 48.55/7.33 % (1830685)Peak memory usage: 17 MB
% 48.55/7.33 % (1830685)Instructions burned: 879 (million)
% 48.55/7.33 % TRYING [9]
% 48.55/7.33 % (1830693)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1552848158:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 48.55/7.33 % TRYING [9]
% 48.55/7.33 % (1830691)Instruction limit reached!
% 48.55/7.33 % (1830691)------------------------------
% 48.55/7.33 % (1830691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830691)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830691)Termination reason: Instruction limit
% 48.55/7.33 % (1830691)Termination phase: Finite model building SAT solving
% 48.55/7.33 % (1830691)Time elapsed: 0.402 s
% 48.55/7.33 % (1830691)Peak memory usage: 42 MB
% 48.55/7.33 % (1830691)Instructions burned: 920 (million)
% 48.55/7.33 % (1830695)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2038354094:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 48.55/7.33 % TRYING [10]
% 48.55/7.33 % TRYING [11]
% 48.55/7.33 % (1830695)Instruction limit reached!
% 48.55/7.33 % (1830695)------------------------------
% 48.55/7.33 % (1830695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830695)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830695)Termination reason: Instruction limit
% 48.55/7.33 % (1830695)Termination phase: Saturation
% 48.55/7.33 % (1830695)Time elapsed: 0.868 s
% 48.55/7.33 % (1830695)Peak memory usage: 26 MB
% 48.55/7.33 % (1830695)Instructions burned: 1474 (million)
% 48.55/7.33 % (1830697)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1149960284:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 48.55/7.33 % Detected minimum model sizes of [4]
% 48.55/7.33 % Detected maximum model sizes of [max]
% 48.55/7.33 % TRYING [77]
% 48.55/7.33 % TRYING [11]
% 48.55/7.33 % (1830693)Instruction limit reached!
% 48.55/7.33 % (1830693)------------------------------
% 48.55/7.33 % (1830693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830693)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830693)Termination reason: Instruction limit
% 48.55/7.33 % (1830693)Termination phase: Saturation
% 48.55/7.33 % (1830693)Time elapsed: 2.837 s
% 48.55/7.33 % (1830693)Peak memory usage: 21 MB
% 48.55/7.33 % (1830693)Instructions burned: 5133 (million)
% 48.55/7.33 % (1830699)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2980363060:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 48.55/7.33 % Detected minimum model sizes of [4]
% 48.55/7.33 % Detected maximum model sizes of [max]
% 48.55/7.33 % TRYING [16]
% 48.55/7.33 % (1830697)Instruction limit reached!
% 48.55/7.33 % (1830697)------------------------------
% 48.55/7.33 % (1830697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830697)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830697)Termination reason: Instruction limit
% 48.55/7.33 % (1830697)Termination phase: Finite model building constraint generation
% 48.55/7.33 % (1830697)Time elapsed: 2.296 s
% 48.55/7.33 % (1830697)Peak memory usage: 437 MB
% 48.55/7.33 % (1830697)Instructions burned: 6328 (million)
% 48.55/7.33 % TRYING [12]
% 48.55/7.33 % (1830701)ott-2_1_sil=16000:newcnf=on:random_seed=1150466155:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi)
% 48.55/7.33 % (1830699)Instruction limit reached!
% 48.55/7.33 % (1830699)------------------------------
% 48.55/7.33 % (1830699)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830699)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830699)Termination reason: Instruction limit
% 48.55/7.33 % (1830699)Termination phase: Finite model building constraint generation
% 48.55/7.33 % (1830699)Time elapsed: 0.976 s
% 48.55/7.33 % (1830699)Peak memory usage: 195 MB
% 48.55/7.33 % (1830699)Instructions burned: 2175 (million)
% 48.55/7.33 % (1830703)ott+10_1_sil=32000:tgt=ground:random_seed=2382356085:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 48.55/7.33 % (1830701)Instruction limit reached!
% 48.55/7.33 % (1830701)------------------------------
% 48.55/7.33 % (1830701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830701)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830701)Termination reason: Instruction limit
% 48.55/7.33 % (1830701)Termination phase: Saturation
% 48.55/7.33 % (1830701)Time elapsed: 0.508 s
% 48.55/7.33 % (1830701)Peak memory usage: 16 MB
% 48.55/7.33 % (1830701)Instructions burned: 869 (million)
% 48.55/7.33 % (1830705)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1622625516:i=54282_2948 on theBenchmark for (2948ds/54282Mi)
% 48.55/7.33 % Detected minimum model sizes of [4]
% 48.55/7.33 % Detected maximum model sizes of [max]
% 48.55/7.33 % TRYING [4]
% 48.55/7.33 % TRYING [5]
% 48.55/7.33 % TRYING [6]
% 48.55/7.33 % TRYING [7]
% 48.55/7.33 % TRYING [8]
% 48.55/7.33 % (1830687)Instruction limit reached!
% 48.55/7.33 % (1830687)------------------------------
% 48.55/7.33 % (1830687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830687)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830687)Termination reason: Instruction limit
% 48.55/7.33 % (1830687)Termination phase: Finite model building SAT solving
% 48.55/7.33 % (1830687)Time elapsed: 5.028 s
% 48.55/7.33 % (1830687)Peak memory usage: 106 MB
% 48.55/7.33 % (1830687)Instructions burned: 22067 (million)
% 48.55/7.33 % (1830707)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3763005118:i=3512:aac=none_2943 on theBenchmark for (2943ds/3512Mi)
% 48.55/7.33 % TRYING [9]
% 48.55/7.33 % (1830689)Instruction limit reached!
% 48.55/7.33 % (1830689)------------------------------
% 48.55/7.33 % (1830689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830689)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830689)Termination reason: Instruction limit
% 48.55/7.33 % (1830689)Termination phase: Finite model building constraint generation
% 48.55/7.33 % (1830689)Time elapsed: 4.895 s
% 48.55/7.33 % (1830689)Peak memory usage: 770 MB
% 48.55/7.33 % (1830689)Instructions burned: 9515 (million)
% 48.55/7.33 % (1830709)dis+21_1_sil=32000:sas=cadical:random_seed=679207672:i=3773:amm=off_2940 on theBenchmark for (2940ds/3773Mi)
% 48.55/7.33 % TRYING [12]
% 48.55/7.33 % TRYING [10]
% 48.55/7.33 % (1830707)Instruction limit reached!
% 48.55/7.33 % (1830707)------------------------------
% 48.55/7.33 % (1830707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830707)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830707)Termination reason: Instruction limit
% 48.55/7.33 % (1830707)Termination phase: Saturation
% 48.55/7.33 % (1830707)Time elapsed: 1.019 s
% 48.55/7.33 % (1830707)Peak memory usage: 21 MB
% 48.55/7.33 % (1830707)Instructions burned: 3514 (million)
% 48.55/7.33 % (1830711)ott+11_1_sil=16000:gs=on:random_seed=3638835668:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi)
% 48.55/7.33 % (1830709) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1830648-1830709"...
% 48.55/7.33 % (1830709)...printing done.
% 48.55/7.33 % (1830709)Refutation found. Thanks to Tanya!
% 48.55/7.33 % SZS status Theorem for theBenchmark
% 48.55/7.33 % SZS output start Proof for theBenchmark
% See solution above
% 48.55/7.33 % (1830709)------------------------------
% 48.55/7.33 % (1830709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 48.55/7.33 % (1830709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.55/7.33 % (1830709)CaDiCaL version: 2.1.3
% 48.55/7.33 % (1830709)Termination reason: Refutation
% 48.55/7.33 % (1830709)Time elapsed: 0.925 s
% 48.55/7.33 % (1830709)Peak memory usage: 22 MB
% 48.55/7.33 % (1830709)Instructions burned: 1429 (million)
% 48.55/7.33 % (1830648)Success in time 6.902 s
% 48.55/7.33 % Vampire exiting
%------------------------------------------------------------------------------