%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV620+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:58:26 PM UTC 2026
% Result : Theorem 118.51s 32.63s
% Output : Refutation 224.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 8
% Syntax : Number of formulae : 80 ( 13 unt; 2 def)
% Number of atoms : 208 ( 2 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 234 ( 106 ~; 95 |; 22 &)
% ( 8 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 3 prp; 0-5 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-3 aty)
% Number of variables : 142 ( 0 sgn 138 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f104,axiom,
! [X0,X1,X2] :
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
<=> ! [X3] :
( t(X3,X0)
=> ! [X4] :
( t(X4,X0)
=> ( p(happ(happ(X1,X3),X4))
=> p(happ(happ(X2,X3),X4)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_def_Coq.Relations.Relation_Definitions.inclusion') ).
fof(f107,axiom,
! [X0,X1,X2] :
( cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(X0,X1,X2)
<=> ( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
& cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_def_Coq.Relations.Relation_Definitions.same_relation') ).
fof(f111,axiom,
! [X0,X1,X2,X3,X4] :
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
<=> ( p(happ(happ(X1,X3),X4))
| p(happ(happ(X2,X3),X4)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_def_Coq.Relations.Relation_Operators.union') ).
fof(f2079,axiom,
! [X0,X1,X2,X3,X4] :
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),X3),X4))
<=> cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_Coq.Relations.Relation_Operators.union_$a5') ).
fof(f2244,axiom,
! [X0,X1,X2] : happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2) = cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_Coq.Relations.Relation_Operators.union_$a3') ).
fof(f2724,conjecture,
cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cr2),cr3),cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr2,cr3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof(f2725,negated_conjecture,
~ cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cr2),cr3),cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr2,cr3))),
inference(negated_conjecture,[status(cth)],[f2724]) ).
fof(f2762,plain,
~ cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cr2),cr3),cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr2,cr3))),
inference(flattening,[],[f2725]) ).
fof(f2949,plain,
! [X0,X1,X2] :
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
<=> ! [X3] :
( ! [X4] :
( p(happ(happ(X2,X3),X4))
| ~ p(happ(happ(X1,X3),X4))
| ~ t(X4,X0) )
| ~ t(X3,X0) ) ),
inference(ennf_transformation,[],[f104]) ).
fof(f2950,plain,
! [X0,X1,X2] :
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
<=> ! [X3] :
( ! [X4] :
( p(happ(happ(X2,X3),X4))
| ~ p(happ(happ(X1,X3),X4))
| ~ t(X4,X0) )
| ~ t(X3,X0) ) ),
inference(flattening,[],[f2949]) ).
fof(f4747,plain,
! [X0,X1,X2] :
( ( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ? [X3] :
( ? [X4] :
( ~ p(happ(happ(X2,X3),X4))
& p(happ(happ(X1,X3),X4))
& t(X4,X0) )
& t(X3,X0) ) )
& ( ! [X3] :
( ! [X4] :
( p(happ(happ(X2,X3),X4))
| ~ p(happ(happ(X1,X3),X4))
| ~ t(X4,X0) )
| ~ t(X3,X0) )
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f2950]) ).
fof(f4748,plain,
! [X0,X1,X2] :
( ( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ? [X3] :
( ? [X4] :
( ~ p(happ(happ(X2,X3),X4))
& p(happ(happ(X1,X3),X4))
& t(X4,X0) )
& t(X3,X0) ) )
& ( ! [X5] :
( ! [X6] :
( p(happ(happ(X2,X5),X6))
| ~ p(happ(happ(X1,X5),X6))
| ~ t(X6,X0) )
| ~ t(X5,X0) )
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2) ) ),
inference(rectify,[],[f4747]) ).
fof(f4749,plain,
! [X0,X1,X2] :
( ( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ( ~ p(happ(happ(X2,sK280(X0,X1,X2)),sK281(X0,X1,X2)))
& p(happ(happ(X1,sK280(X0,X1,X2)),sK281(X0,X1,X2)))
& t(sK281(X0,X1,X2),X0)
& t(sK280(X0,X1,X2),X0) ) )
& ( ! [X5] :
( ! [X6] :
( p(happ(happ(X2,X5),X6))
| ~ p(happ(happ(X1,X5),X6))
| ~ t(X6,X0) )
| ~ t(X5,X0) )
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK280,sK281]),skolemize(X3,sK280(X0,X1,X2)),skolemize(X4,sK281(X0,X1,X2))],[f4748]) ).
fof(f4753,plain,
! [X0,X1,X2] :
( ( cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(X0,X1,X2)
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X2,X1) )
& ( ( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
& cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X2,X1) )
| ~ cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f107]) ).
fof(f4754,plain,
! [X0,X1,X2] :
( ( cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(X0,X1,X2)
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X2,X1) )
& ( ( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
& cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X2,X1) )
| ~ cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(X0,X1,X2) ) ),
inference(flattening,[],[f4753]) ).
fof(f4762,plain,
! [X0,X1,X2,X3,X4] :
( ( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ( ~ p(happ(happ(X1,X3),X4))
& ~ p(happ(happ(X2,X3),X4)) ) )
& ( p(happ(happ(X1,X3),X4))
| p(happ(happ(X2,X3),X4))
| ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) ) ),
inference(nnf_transformation,[],[f111]) ).
fof(f4763,plain,
! [X0,X1,X2,X3,X4] :
( ( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ( ~ p(happ(happ(X1,X3),X4))
& ~ p(happ(happ(X2,X3),X4)) ) )
& ( p(happ(happ(X1,X3),X4))
| p(happ(happ(X2,X3),X4))
| ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) ) ),
inference(flattening,[],[f4762]) ).
fof(f6498,plain,
! [X0,X1,X2,X3,X4] :
( ( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),X3),X4))
| ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) )
& ( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ~ p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),X3),X4)) ) ),
inference(nnf_transformation,[],[f2079]) ).
fof(f7568,plain,
! [X2,X0,X1] :
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| p(happ(happ(X1,sK280(X0,X1,X2)),sK281(X0,X1,X2))) ),
inference(cnf_transformation,[],[f4749]) ).
fof(f7569,plain,
! [X2,X0,X1] :
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ~ p(happ(happ(X2,sK280(X0,X1,X2)),sK281(X0,X1,X2))) ),
inference(cnf_transformation,[],[f4749]) ).
fof(f7576,plain,
! [X2,X0,X1] :
( cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(X0,X1,X2)
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X2,X1) ),
inference(cnf_transformation,[],[f4754]) ).
fof(f7591,plain,
! [X2,X3,X0,X1,X4] :
( p(happ(happ(X1,X3),X4))
| p(happ(happ(X2,X3),X4))
| ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f4763]) ).
fof(f7592,plain,
! [X2,X3,X0,X1,X4] :
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ~ p(happ(happ(X2,X3),X4)) ),
inference(cnf_transformation,[],[f4763]) ).
fof(f7593,plain,
! [X2,X3,X0,X1,X4] :
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ~ p(happ(happ(X1,X3),X4)) ),
inference(cnf_transformation,[],[f4763]) ).
fof(f12609,plain,
! [X2,X3,X0,X1,X4] :
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ~ p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),X3),X4)) ),
inference(cnf_transformation,[],[f6498]) ).
fof(f12610,plain,
! [X2,X3,X0,X1,X4] :
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),X3),X4))
| ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f6498]) ).
fof(f12811,plain,
! [X2,X0,X1] : cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(X0,X1,X2) = happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),
inference(cnf_transformation,[],[f2244]) ).
fof(f13685,plain,
~ cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cr2),cr3),cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr1,cCoq_2eRelations_2eRelation__Operators_2eunion___24a3(cA,cr2,cr3))),
inference(cnf_transformation,[],[f2762]) ).
fof(f15507,plain,
~ cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))),
inference(definition_unfolding,[],[f13685,f12811,f12811,f12811,f12811]) ).
fof(f16050,plain,
! [X2,X0,X1] :
( ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| ~ p(happ(happ(X2,sK280(X0,X1,X2)),sK281(X0,X1,X2))) ),
inference(consistent_polarity_flipping,[],[f7569]) ).
fof(f16051,plain,
! [X2,X0,X1] :
( ~ cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| p(happ(happ(X1,sK280(X0,X1,X2)),sK281(X0,X1,X2))) ),
inference(consistent_polarity_flipping,[],[f7568]) ).
fof(f16057,plain,
! [X2,X0,X1] :
( cCoq_2eRelations_2eRelation__Definitions_2esame__relation___24a3(X0,X1,X2)
| cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X1,X2)
| cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(X0,X2,X1) ),
inference(consistent_polarity_flipping,[],[f7576]) ).
fof(f16067,plain,
! [X2,X3,X0,X1,X4] :
( ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ~ p(happ(happ(X1,X3),X4)) ),
inference(consistent_polarity_flipping,[],[f7593]) ).
fof(f16068,plain,
! [X2,X3,X0,X1,X4] :
( ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| ~ p(happ(happ(X2,X3),X4)) ),
inference(consistent_polarity_flipping,[],[f7592]) ).
fof(f16069,plain,
! [X2,X3,X0,X1,X4] :
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4)
| p(happ(happ(X2,X3),X4))
| p(happ(happ(X1,X3),X4)) ),
inference(consistent_polarity_flipping,[],[f7591]) ).
fof(f19655,plain,
! [X2,X3,X0,X1,X4] :
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),X3),X4))
| cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) ),
inference(consistent_polarity_flipping,[],[f12610]) ).
fof(f19656,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,X0),X1),X2),X3),X4))
| ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(X0,X1,X2,X3,X4) ),
inference(consistent_polarity_flipping,[],[f12609]) ).
fof(f20585,plain,
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))
| cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)) ),
inference(resolution,[],[f15507,f16057]) ).
fof(f20587,definition,
( spl1470_1
<=> cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)) ),
introduced(definition,[new_symbols(definition,[spl1470_1])],[avatar_definition]) ).
fof(f20588,plain,
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))
| ~ spl1470_1 ),
inference(avatar_component_clause,[],[f20587]) ).
fof(f20590,definition,
( spl1470_2
<=> cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))) ),
introduced(definition,[new_symbols(definition,[spl1470_2])],[avatar_definition]) ).
fof(f20591,plain,
( cCoq_2eRelations_2eRelation__Definitions_2einclusion___24a3(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))
| ~ spl1470_2 ),
inference(avatar_component_clause,[],[f20590]) ).
fof(f20592,plain,
( spl1470_1
| spl1470_2 ),
inference(avatar_split_clause,[],[f20585,f20590,f20587]) ).
fof(f20713,plain,
( ~ p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20591,f16050]) ).
fof(f20714,plain,
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20591,f16051]) ).
fof(f20721,plain,
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,cr1,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))))
| ~ spl1470_2 ),
inference(resolution,[],[f20713,f19655]) ).
fof(f20722,plain,
( ~ p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20721,f16068]) ).
fof(f20723,plain,
( ~ p(happ(happ(cr1,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20721,f16067]) ).
fof(f20724,plain,
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,cr2,cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))))
| ~ spl1470_2 ),
inference(resolution,[],[f20722,f19655]) ).
fof(f20725,plain,
( ~ p(happ(happ(cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20724,f16068]) ).
fof(f20726,plain,
( ~ p(happ(happ(cr2,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20724,f16067]) ).
fof(f20727,plain,
( ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2),cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))))
| ~ spl1470_2 ),
inference(resolution,[],[f20714,f19656]) ).
fof(f20728,plain,
( p(happ(happ(cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20727,f16069]) ).
fof(f20729,plain,
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(forward_subsumption_resolution,[],[f20728,f20725]) ).
fof(f20730,plain,
( ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,cr1,cr2,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3))))
| ~ spl1470_2 ),
inference(resolution,[],[f20729,f19656]) ).
fof(f20731,plain,
( p(happ(happ(cr2,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| p(happ(happ(cr1,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(resolution,[],[f20730,f16069]) ).
fof(f20732,plain,
( p(happ(happ(cr1,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)))))
| ~ spl1470_2 ),
inference(forward_subsumption_resolution,[],[f20731,f20726]) ).
fof(f20733,plain,
( $false
| ~ spl1470_2 ),
inference(forward_subsumption_resolution,[],[f20732,f20723]) ).
fof(f20734,plain,
~ spl1470_2,
inference(avatar_contradiction_clause,[],[f20733]) ).
fof(f20743,plain,
( ~ p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20588,f16050]) ).
fof(f20744,plain,
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20588,f16051]) ).
fof(f20751,plain,
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2),cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)))
| ~ spl1470_1 ),
inference(resolution,[],[f20743,f19655]) ).
fof(f20752,plain,
( ~ p(happ(happ(cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20751,f16068]) ).
fof(f20753,plain,
( ~ p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20751,f16067]) ).
fof(f20754,plain,
( cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,cr1,cr2,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)))
| ~ spl1470_1 ),
inference(resolution,[],[f20753,f19655]) ).
fof(f20755,plain,
( ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,cr1,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)))
| ~ spl1470_1 ),
inference(resolution,[],[f20744,f19656]) ).
fof(f20756,plain,
( ~ p(happ(happ(cr2,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20754,f16068]) ).
fof(f20757,plain,
( ~ p(happ(happ(cr1,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20754,f16067]) ).
fof(f20758,plain,
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| p(happ(happ(cr1,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20755,f16069]) ).
fof(f20759,plain,
( p(happ(happ(happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3),sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(forward_subsumption_resolution,[],[f20758,f20757]) ).
fof(f20760,plain,
( ~ cCoq_2eRelations_2eRelation__Operators_2eunion___24a5(cA,cr2,cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3)))
| ~ spl1470_1 ),
inference(resolution,[],[f20759,f19656]) ).
fof(f20761,plain,
( p(happ(happ(cr3,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| p(happ(happ(cr2,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(resolution,[],[f20760,f16069]) ).
fof(f20762,plain,
( p(happ(happ(cr2,sK280(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))),sK281(cA,happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr2),cr3)),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),happ(happ(happ(cCoq_2eRelations_2eRelation__Operators_2eunion,cA),cr1),cr2)),cr3))))
| ~ spl1470_1 ),
inference(forward_subsumption_resolution,[],[f20761,f20752]) ).
fof(f20763,plain,
( $false
| ~ spl1470_1 ),
inference(forward_subsumption_resolution,[],[f20762,f20756]) ).
fof(f20764,plain,
~ spl1470_1,
inference(avatar_contradiction_clause,[],[f20763]) ).
cnf(s1,plain,
( spl1470_1
| spl1470_2 ),
inference(sat_conversion,[],[f20592]) ).
cnf(s15,plain,
~ spl1470_2,
inference(sat_conversion,[],[f20734]) ).
cnf(s16,plain,
~ spl1470_1,
inference(sat_conversion,[],[f20764]) ).
cnf(s17,plain,
$false,
inference(rat,[],[s1,s15,s16]) ).
fof(f20765,plain,
$false,
inference(avatar_sat_refutation,[],[s17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEV620+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 % Computer : n019.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 28 06:43:03 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 Running first-order theorem proving
% 0.22/0.48 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.76/3.62 % (3806708)Detected formulas, will run a generic FOF schedule.
% 17.76/3.62 % (3806720)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2714488477:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 17.76/3.62 % (3806720)Instruction limit reached!
% 17.76/3.62 % (3806720)------------------------------
% 17.76/3.62 % (3806720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.62 % (3806720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.62 % (3806720)CaDiCaL version: 2.1.3
% 17.76/3.62 % (3806720)Termination reason: Instruction limit
% 17.76/3.62 % (3806720)Termination phase: Preprocessing 3
% 17.76/3.62 % (3806720)Time elapsed: 0.041 s
% 17.76/3.62 % (3806720)Peak memory usage: 93 MB
% 17.76/3.62 % (3806720)Instructions burned: 141 (million)
% 17.76/3.62 % (3806715)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1599760439:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 17.76/3.62 % (3806719)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1871211174:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 17.76/3.62 % (3806718)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2094696031:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 17.76/3.62 % (3806716)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3360536502:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 17.76/3.62 % (3806717)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=733230791:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 17.76/3.62 % (3806721)dis-21_1_sil=8000:lcm=predicate:random_seed=2689311484:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 17.76/3.62 % (3806718)Refutation not found, incomplete strategy
% 17.76/3.62 % (3806718)------------------------------
% 17.76/3.62 % (3806718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.62 % (3806718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.62 % (3806718)CaDiCaL version: 2.1.3
% 17.76/3.62 % (3806718)Termination reason: Refutation not found, incomplete strategy
% 17.76/3.62 % (3806718)Time elapsed: 0.025 s
% 17.76/3.62 % (3806718)Peak memory usage: 92 MB
% 17.76/3.62 % (3806718)Instructions burned: 32 (million)
% 17.76/3.62 % (3806719)Instruction limit reached!
% 17.76/3.62 % (3806719)------------------------------
% 17.76/3.62 % (3806719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.62 % (3806719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.62 % (3806719)CaDiCaL version: 2.1.3
% 17.76/3.62 % (3806719)Termination reason: Instruction limit
% 17.76/3.62 % (3806719)Termination phase: Saturation
% 17.76/3.62 % (3806719)Time elapsed: 0.097 s
% 17.76/3.62 % (3806719)Peak memory usage: 91 MB
% 17.76/3.62 % (3806719)Instructions burned: 120 (million)
% 17.76/3.62 % (3806721)Instruction limit reached!
% 17.76/3.62 % (3806721)------------------------------
% 17.76/3.62 % (3806721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.62 % (3806721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.62 % (3806721)CaDiCaL version: 2.1.3
% 17.76/3.62 % (3806721)Termination reason: Instruction limit
% 17.76/3.62 % (3806721)Termination phase: Property scanning
% 17.76/3.62 % (3806721)Time elapsed: 0.123 s
% 17.76/3.62 % (3806721)Peak memory usage: 94 MB
% 17.76/3.62 % (3806721)Instructions burned: 130 (million)
% 17.76/3.62 % (3806723)lrs+10_1_sil=8000:sp=occurrence:random_seed=2228685264:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 17.76/3.62 % (3806723)Instruction limit reached!
% 17.76/3.62 % (3806723)------------------------------
% 17.76/3.62 % (3806723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.76/3.62 % (3806723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.76/3.62 % (3806723)CaDiCaL version: 2.1.3
% 17.76/3.62 % (3806723)Termination reason: Instruction limit
% 17.76/3.62 % (3806723)Termination phase: Saturation
% 17.76/3.62 % (3806723)Time elapsed: 0.130 s
% 17.76/3.62 % (3806723)Peak memory usage: 94 MB
% 17.76/3.62 % (3806723)Instructions burned: 286 (million)
% 31.10/5.36 % (3806730)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2733138194:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 31.10/5.36 % (3806732)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1539584238:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 31.10/5.36 % (3806718)------------------------------
% 31.10/5.36 % (3806718)------------------------------
% 31.10/5.36 % (3806730)Refutation not found, incomplete strategy
% 31.10/5.36 % (3806730)------------------------------
% 31.10/5.36 % (3806730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.10/5.36 % (3806730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.10/5.36 % (3806730)CaDiCaL version: 2.1.3
% 31.10/5.36 % (3806730)Termination reason: Refutation not found, incomplete strategy
% 31.10/5.36 % (3806730)Time elapsed: 0.084 s
% 31.10/5.36 % (3806730)Peak memory usage: 92 MB
% 31.10/5.36 % (3806730)Instructions burned: 107 (million)
% 31.10/5.36 % (3806732)Refutation not found, incomplete strategy
% 31.10/5.36 % (3806732)------------------------------
% 31.10/5.36 % (3806732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.10/5.36 % (3806732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.10/5.36 % (3806732)CaDiCaL version: 2.1.3
% 31.10/5.36 % (3806732)Termination reason: Refutation not found, incomplete strategy
% 31.10/5.36 % (3806732)Time elapsed: 0.049 s
% 31.10/5.36 % (3806732)Peak memory usage: 92 MB
% 31.10/5.36 % (3806732)Instructions burned: 50 (million)
% 31.10/5.36 % (3806733)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4225501341:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 31.10/5.36 % (3806733)Instruction limit reached!
% 31.10/5.36 % (3806733)------------------------------
% 31.10/5.36 % (3806733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.10/5.36 % (3806733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.10/5.36 % (3806733)CaDiCaL version: 2.1.3
% 31.10/5.36 % (3806733)Termination reason: Instruction limit
% 31.10/5.36 % (3806733)Termination phase: Saturation
% 31.10/5.36 % (3806733)Time elapsed: 0.116 s
% 31.10/5.36 % (3806733)Peak memory usage: 96 MB
% 31.10/5.36 % (3806733)Instructions burned: 250 (million)
% 31.10/5.36 % (3806736)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=716727102:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 31.10/5.36 % (3806736)Refutation not found, incomplete strategy
% 31.10/5.36 % (3806736)------------------------------
% 31.10/5.36 % (3806736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.10/5.36 % (3806736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.10/5.36 % (3806736)CaDiCaL version: 2.1.3
% 31.10/5.36 % (3806736)Termination reason: Refutation not found, incomplete strategy
% 31.10/5.36 % (3806736)Time elapsed: 0.042 s
% 31.10/5.36 % (3806736)Peak memory usage: 92 MB
% 31.10/5.36 % (3806736)Instructions burned: 53 (million)
% 31.10/5.36 % (3806739)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1854248098:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 31.10/5.36 % (3806730)------------------------------
% 31.10/5.36 % (3806730)------------------------------
% 31.10/5.36 % (3806732)------------------------------
% 31.10/5.36 % (3806732)------------------------------
% 31.10/5.36 % (3806746)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3281401305:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 31.10/5.36 % (3806745)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3432743924:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 31.10/5.36 % (3806736)------------------------------
% 31.10/5.36 % (3806736)------------------------------
% 31.10/5.36 % (3806745)Instruction limit reached!
% 31.10/5.36 % (3806745)------------------------------
% 31.10/5.36 % (3806745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.10/5.36 % (3806745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.10/5.36 % (3806745)CaDiCaL version: 2.1.3
% 31.10/5.36 % (3806745)Termination reason: Instruction limit
% 31.10/5.36 % (3806745)Termination phase: Preprocessing 3
% 31.10/5.36 % (3806745)Time elapsed: 0.105 s
% 31.10/5.36 % (3806745)Peak memory usage: 93 MB
% 31.10/5.36 % (3806745)Instructions burned: 114 (million)
% 31.10/5.36 % (3806746)Instruction limit reached!
% 66.05/10.25 % (3806746)------------------------------
% 66.05/10.25 % (3806746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.25 % (3806746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.25 % (3806746)CaDiCaL version: 2.1.3
% 66.05/10.25 % (3806746)Termination reason: Instruction limit
% 66.05/10.25 % (3806746)Termination phase: Property scanning
% 66.05/10.25 % (3806746)Time elapsed: 0.127 s
% 66.05/10.25 % (3806746)Peak memory usage: 94 MB
% 66.05/10.25 % (3806746)Instructions burned: 131 (million)
% 66.05/10.25 % (3806753)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3111889460:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 66.05/10.25 % (3806754)lrs+10_1_sil=8000:sp=occurrence:random_seed=1307696204:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 66.05/10.25 % (3806755)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3892165251:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 66.05/10.25 % (3806753)Instruction limit reached!
% 66.05/10.25 % (3806753)------------------------------
% 66.05/10.25 % (3806753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.25 % (3806753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.25 % (3806753)CaDiCaL version: 2.1.3
% 66.05/10.25 % (3806753)Termination reason: Instruction limit
% 66.05/10.25 % (3806753)Termination phase: Preprocessing 3
% 66.05/10.25 % (3806753)Time elapsed: 0.094 s
% 66.05/10.25 % (3806753)Peak memory usage: 90 MB
% 66.05/10.25 % (3806753)Instructions burned: 114 (million)
% 66.05/10.25 % (3806761)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=630369546:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 66.05/10.25 % (3806755)Instruction limit reached!
% 66.05/10.25 % (3806755)------------------------------
% 66.05/10.25 % (3806755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.25 % (3806755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.25 % (3806755)CaDiCaL version: 2.1.3
% 66.05/10.25 % (3806755)Termination reason: Instruction limit
% 66.05/10.25 % (3806755)Termination phase: Saturation
% 66.05/10.25 % (3806755)Time elapsed: 0.378 s
% 66.05/10.25 % (3806755)Peak memory usage: 102 MB
% 66.05/10.25 % (3806755)Instructions burned: 438 (million)
% 66.05/10.25 % (3806739)Instruction limit reached!
% 66.05/10.25 % (3806739)------------------------------
% 66.05/10.25 % (3806739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.25 % (3806739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.25 % (3806739)CaDiCaL version: 2.1.3
% 66.05/10.25 % (3806739)Termination reason: Instruction limit
% 66.05/10.25 % (3806739)Termination phase: Saturation
% 66.05/10.25 % (3806739)Time elapsed: 1.259 s
% 66.05/10.25 % (3806739)Peak memory usage: 215 MB
% 66.05/10.25 % (3806739)Instructions burned: 2351 (million)
% 66.05/10.25 % (3806763)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=88725783:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 66.05/10.25 % (3806763)Instruction limit reached!
% 66.05/10.25 % (3806763)------------------------------
% 66.05/10.25 % (3806763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.25 % (3806763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.25 % (3806763)CaDiCaL version: 2.1.3
% 66.05/10.25 % (3806763)Termination reason: Instruction limit
% 66.05/10.25 % (3806763)Termination phase: NewCNF
% 66.05/10.25 % (3806763)Time elapsed: 0.068 s
% 66.05/10.25 % (3806763)Peak memory usage: 93 MB
% 66.05/10.25 % (3806763)Instructions burned: 134 (million)
% 66.05/10.25 % (3806764)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3425580808:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 66.05/10.25 % (3806754)Instruction limit reached!
% 66.05/10.25 % (3806754)------------------------------
% 66.05/10.25 % (3806754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.05/10.25 % (3806754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.05/10.25 % (3806754)CaDiCaL version: 2.1.3
% 66.05/10.25 % (3806754)Termination reason: Instruction limit
% 66.05/10.25 % (3806754)Termination phase: Saturation
% 66.05/10.25 % (3806754)Time elapsed: 0.853 s
% 66.05/10.25 % (3806754)Peak memory usage: 114 MB
% 66.05/10.25 % (3806754)Instructions burned: 907 (million)
% 66.05/10.25 % (3806764)Refutation not found, incomplete strategy
% 110.78/16.57 % (3806764)------------------------------
% 110.78/16.57 % (3806764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.78/16.57 % (3806764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.78/16.57 % (3806764)CaDiCaL version: 2.1.3
% 110.78/16.57 % (3806764)Termination reason: Refutation not found, incomplete strategy
% 110.78/16.57 % (3806764)Time elapsed: 0.089 s
% 110.78/16.57 % (3806764)Peak memory usage: 94 MB
% 110.78/16.57 % (3806764)Instructions burned: 106 (million)
% 110.78/16.57 % (3806766)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2434038197:st=3:i=13193:sd=3:ss=axioms_2973 on theBenchmark for (2973ds/13193Mi)
% 110.78/16.57 % (3806768)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3230708273:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 110.78/16.57 % (3806768)Refutation not found, incomplete strategy
% 110.78/16.57 % (3806768)------------------------------
% 110.78/16.57 % (3806768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.78/16.57 % (3806768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.78/16.57 % (3806768)CaDiCaL version: 2.1.3
% 110.78/16.57 % (3806768)Termination reason: Refutation not found, incomplete strategy
% 110.78/16.57 % (3806768)Time elapsed: 0.066 s
% 110.78/16.57 % (3806768)Peak memory usage: 92 MB
% 110.78/16.57 % (3806768)Instructions burned: 93 (million)
% 110.78/16.57 % (3806764)------------------------------
% 110.78/16.57 % (3806764)------------------------------
% 110.78/16.57 % (3806768)------------------------------
% 110.78/16.57 % (3806768)------------------------------
% 110.78/16.57 % (3806773)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2963511109:i=134:gtgl=5:slsql=off:gtg=exists_sym_2968 on theBenchmark for (2968ds/134Mi)
% 110.78/16.57 % (3806773)Instruction limit reached!
% 110.78/16.57 % (3806773)------------------------------
% 110.78/16.57 % (3806773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.78/16.57 % (3806773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.78/16.57 % (3806773)CaDiCaL version: 2.1.3
% 110.78/16.57 % (3806773)Termination reason: Instruction limit
% 110.78/16.57 % (3806773)Termination phase: Preprocessing 3
% 110.78/16.57 % (3806773)Time elapsed: 0.108 s
% 110.78/16.57 % (3806773)Peak memory usage: 90 MB
% 110.78/16.57 % (3806773)Instructions burned: 134 (million)
% 110.78/16.57 % (3806775)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3500941244:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/141Mi)
% 110.78/16.57 % (3806775)Refutation not found, incomplete strategy
% 110.78/16.57 % (3806775)------------------------------
% 110.78/16.57 % (3806775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.78/16.57 % (3806775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.78/16.57 % (3806775)CaDiCaL version: 2.1.3
% 110.78/16.57 % (3806775)Termination reason: Refutation not found, incomplete strategy
% 110.78/16.57 % (3806775)Time elapsed: 0.024 s
% 110.78/16.57 % (3806775)Peak memory usage: 92 MB
% 110.78/16.57 % (3806775)Instructions burned: 30 (million)
% 110.78/16.57 % (3806777)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=718167221:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2964 on theBenchmark for (2964ds/431Mi)
% 110.78/16.57 % (3806777)Refutation not found, incomplete strategy
% 110.78/16.57 % (3806777)------------------------------
% 110.78/16.57 % (3806777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.78/16.57 % (3806777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.78/16.57 % (3806777)CaDiCaL version: 2.1.3
% 110.78/16.57 % (3806777)Termination reason: Refutation not found, incomplete strategy
% 110.78/16.57 % (3806777)Time elapsed: 0.032 s
% 110.78/16.57 % (3806777)Peak memory usage: 92 MB
% 110.78/16.57 % (3806777)Instructions burned: 35 (million)
% 110.78/16.57 % (3806775)------------------------------
% 110.78/16.57 % (3806775)------------------------------
% 110.78/16.57 % (3806777)------------------------------
% 110.78/16.57 % (3806777)------------------------------
% 110.78/16.57 % (3806783)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1061746990:i=6060:aac=none:ins=25_2958 on theBenchmark for (2958ds/6060Mi)
% 110.78/16.57 % (3806784)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2634686496:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2957 on theBenchmark for (2957ds/150Mi)
% 151.71/22.40 % (3806784)Instruction limit reached!
% 151.71/22.40 % (3806784)------------------------------
% 151.71/22.40 % (3806784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.71/22.40 % (3806784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.71/22.40 % (3806784)CaDiCaL version: 2.1.3
% 151.71/22.40 % (3806784)Termination reason: Instruction limit
% 151.71/22.40 % (3806784)Termination phase: Property scanning
% 151.71/22.40 % (3806784)Time elapsed: 0.142 s
% 151.71/22.40 % (3806784)Peak memory usage: 94 MB
% 151.71/22.40 % (3806784)Instructions burned: 151 (million)
% 151.71/22.40 % (3806787)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1221965938:i=14155:bd=all_2953 on theBenchmark for (2953ds/14155Mi)
% 151.71/22.40 % (3806761)Instruction limit reached!
% 151.71/22.40 % (3806761)------------------------------
% 151.71/22.40 % (3806761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.71/22.40 % (3806761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.71/22.40 % (3806761)CaDiCaL version: 2.1.3
% 151.71/22.40 % (3806761)Termination reason: Instruction limit
% 151.71/22.40 % (3806761)Termination phase: Saturation
% 151.71/22.40 % (3806761)Time elapsed: 5.023 s
% 151.71/22.40 % (3806761)Peak memory usage: 190 MB
% 151.71/22.40 % (3806761)Instructions burned: 5202 (million)
% 151.71/22.40 % (3806793)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=533188846:i=667:av=off:fsr=off_2927 on theBenchmark for (2927ds/667Mi)
% 151.71/22.40 % (3806793)Instruction limit reached!
% 151.71/22.40 % (3806793)------------------------------
% 151.71/22.40 % (3806793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.71/22.40 % (3806793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.71/22.40 % (3806793)CaDiCaL version: 2.1.3
% 151.71/22.40 % (3806793)Termination reason: Instruction limit
% 151.71/22.40 % (3806793)Termination phase: Saturation
% 151.71/22.40 % (3806793)Time elapsed: 0.419 s
% 151.71/22.40 % (3806793)Peak memory usage: 102 MB
% 151.71/22.40 % (3806793)Instructions burned: 668 (million)
% 151.71/22.40 % (3806795)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=100642098:s2a=on:i=185:s2at=1.8:fdi=4_2921 on theBenchmark for (2921ds/185Mi)
% 151.71/22.40 % (3806795)Instruction limit reached!
% 151.71/22.40 % (3806795)------------------------------
% 151.71/22.40 % (3806795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.71/22.40 % (3806795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.71/22.40 % (3806795)CaDiCaL version: 2.1.3
% 151.71/22.40 % (3806795)Termination reason: Instruction limit
% 151.71/22.40 % (3806795)Termination phase: NewCNF
% 151.71/22.40 % (3806795)Time elapsed: 0.163 s
% 151.71/22.40 % (3806795)Peak memory usage: 94 MB
% 151.71/22.40 % (3806795)Instructions burned: 185 (million)
% 151.71/22.40 % (3806797)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=172215592:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2916 on theBenchmark for (2916ds/193Mi)
% 151.71/22.40 % (3806797)Instruction limit reached!
% 151.71/22.40 % (3806797)------------------------------
% 151.71/22.40 % (3806797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.71/22.40 % (3806797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.71/22.40 % (3806797)CaDiCaL version: 2.1.3
% 151.71/22.40 % (3806797)Termination reason: Instruction limit
% 151.71/22.40 % (3806797)Termination phase: Saturation
% 151.71/22.40 % (3806797)Time elapsed: 0.162 s
% 151.71/22.40 % (3806797)Peak memory usage: 94 MB
% 151.71/22.40 % (3806797)Instructions burned: 193 (million)
% 151.71/22.40 % (3806799)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1902046745:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2911 on theBenchmark for (2911ds/4850Mi)
% 151.71/22.40 % (3806766)Instruction limit reached!
% 151.71/22.40 % (3806766)------------------------------
% 151.71/22.40 % (3806766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 151.71/22.40 % (3806766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 151.71/22.40 % (3806766)CaDiCaL version: 2.1.3
% 151.71/22.40 % (3806766)Termination reason: Instruction limit
% 191.53/28.03 % (3806766)Termination phase: Saturation
% 191.53/28.03 % (3806766)Time elapsed: 6.528 s
% 191.53/28.03 % (3806766)Peak memory usage: 196 MB
% 191.53/28.03 % (3806766)Instructions burned: 13195 (million)
% 191.53/28.03 % (3806801)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1383104344:i=12111:sd=1:ss=included_2906 on theBenchmark for (2906ds/12111Mi)
% 191.53/28.03 % (3806783)Instruction limit reached!
% 191.53/28.03 % (3806783)------------------------------
% 191.53/28.03 % (3806783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.53/28.03 % (3806783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.53/28.03 % (3806783)CaDiCaL version: 2.1.3
% 191.53/28.03 % (3806783)Termination reason: Instruction limit
% 191.53/28.03 % (3806783)Termination phase: Saturation
% 191.53/28.03 % (3806783)Time elapsed: 5.698 s
% 191.53/28.03 % (3806783)Peak memory usage: 224 MB
% 191.53/28.03 % (3806783)Instructions burned: 6060 (million)
% 191.53/28.03 % (3806803)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2798388350:i=319:kws=precedence:fsr=off_2898 on theBenchmark for (2898ds/319Mi)
% 191.53/28.03 % (3806803)Instruction limit reached!
% 191.53/28.03 % (3806803)------------------------------
% 191.53/28.03 % (3806803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.53/28.03 % (3806803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.53/28.03 % (3806803)CaDiCaL version: 2.1.3
% 191.53/28.03 % (3806803)Termination reason: Instruction limit
% 191.53/28.03 % (3806803)Termination phase: Saturation
% 191.53/28.03 % (3806803)Time elapsed: 0.261 s
% 191.53/28.03 % (3806803)Peak memory usage: 98 MB
% 191.53/28.03 % (3806803)Instructions burned: 319 (million)
% 191.53/28.03 % (3806805)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3324723822:i=2064:ep=RST_2892 on theBenchmark for (2892ds/2064Mi)
% 191.53/28.03 % (3806805)Refutation not found, incomplete strategy
% 191.53/28.03 % (3806805)------------------------------
% 191.53/28.03 % (3806805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.53/28.03 % (3806805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.53/28.03 % (3806805)CaDiCaL version: 2.1.3
% 191.53/28.03 % (3806805)Termination reason: Refutation not found, incomplete strategy
% 191.53/28.03 % (3806805)Time elapsed: 0.409 s
% 191.53/28.03 % (3806805)Peak memory usage: 104 MB
% 191.53/28.03 % (3806805)Instructions burned: 500 (million)
% 191.53/28.03 % (3806805)------------------------------
% 191.53/28.03 % (3806805)------------------------------
% 191.53/28.03 % (3806807)dis-1011_128_sil=32000:random_seed=5487493:i=3706:ep=RST:av=off_2881 on theBenchmark for (2881ds/3706Mi)
% 191.53/28.03 % (3806799)Instruction limit reached!
% 191.53/28.03 % (3806799)------------------------------
% 191.53/28.03 % (3806799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.53/28.03 % (3806799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.53/28.03 % (3806799)CaDiCaL version: 2.1.3
% 191.53/28.03 % (3806799)Termination reason: Instruction limit
% 191.53/28.03 % (3806799)Termination phase: Saturation
% 191.53/28.03 % (3806799)Time elapsed: 3.870 s
% 191.53/28.03 % (3806799)Peak memory usage: 135 MB
% 191.53/28.03 % (3806799)Instructions burned: 4851 (million)
% 191.53/28.03 % (3806811)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2481535839:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2870 on theBenchmark for (2870ds/757Mi)
% 191.53/28.03 % (3806811)Instruction limit reached!
% 191.53/28.03 % (3806811)------------------------------
% 191.53/28.03 % (3806811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.53/28.03 % (3806811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.53/28.03 % (3806811)CaDiCaL version: 2.1.3
% 191.53/28.03 % (3806811)Termination reason: Instruction limit
% 191.53/28.03 % (3806811)Termination phase: Saturation
% 191.53/28.03 % (3806811)Time elapsed: 0.712 s
% 191.53/28.03 % (3806811)Peak memory usage: 98 MB
% 191.53/28.03 % (3806811)Instructions burned: 757 (million)
% 191.53/28.03 % (3806815)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2887533266:i=13913:ss=axioms:sgt=8_2860 on theBenchmark for (2860ds/13913Mi)
% 191.53/28.03 % (3806807)Instruction limit reached!
% 191.53/28.03 % (3806807)------------------------------
% 191.53/28.03 % (3806807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.53/28.03 % (3806807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.31/31.67 % (3806807)CaDiCaL version: 2.1.3
% 217.31/31.67 % (3806807)Termination reason: Instruction limit
% 217.31/31.67 % (3806807)Termination phase: Saturation
% 217.31/31.67 % (3806807)Time elapsed: 3.581 s
% 217.31/31.67 % (3806807)Peak memory usage: 129 MB
% 217.31/31.67 % (3806807)Instructions burned: 3706 (million)
% 217.31/31.67 % (3806819)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4113689451:i=9925:aac=none_2842 on theBenchmark for (2842ds/9925Mi)
% 217.31/31.67 % (3806801)Instruction limit reached!
% 217.31/31.67 % (3806801)------------------------------
% 217.31/31.67 % (3806801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 217.31/31.67 % (3806801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.31/31.67 % (3806801)CaDiCaL version: 2.1.3
% 217.31/31.67 % (3806801)Termination reason: Instruction limit
% 217.31/31.67 % (3806801)Termination phase: Saturation
% 217.31/31.67 % (3806801)Time elapsed: 6.529 s
% 217.31/31.67 % (3806801)Peak memory usage: 235 MB
% 217.31/31.67 % (3806801)Instructions burned: 12111 (million)
% 217.31/31.67 % (3806821)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1750213566:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2838 on theBenchmark for (2838ds/2479Mi)
% 217.31/31.67 % (3806821)Refutation not found, incomplete strategy
% 217.31/31.67 % (3806821)------------------------------
% 217.31/31.67 % (3806821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 217.31/31.67 % (3806821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.31/31.67 % (3806821)CaDiCaL version: 2.1.3
% 217.31/31.67 % (3806821)Termination reason: Refutation not found, incomplete strategy
% 217.31/31.67 % (3806821)Time elapsed: 0.037 s
% 217.31/31.67 % (3806821)Peak memory usage: 92 MB
% 217.31/31.67 % (3806821)Instructions burned: 62 (million)
% 217.31/31.67 % (3806821)------------------------------
% 217.31/31.67 % (3806821)------------------------------
% 217.31/31.67 % (3806823)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3142519867:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2832 on theBenchmark for (2832ds/440Mi)
% 217.31/31.67 % (3806823)Instruction limit reached!
% 217.31/31.67 % (3806823)------------------------------
% 217.31/31.67 % (3806823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 217.31/31.67 % (3806823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.31/31.67 % (3806823)CaDiCaL version: 2.1.3
% 217.31/31.67 % (3806823)Termination reason: Instruction limit
% 217.31/31.67 % (3806823)Termination phase: Saturation
% 217.31/31.67 % (3806823)Time elapsed: 0.212 s
% 217.31/31.67 % (3806823)Peak memory usage: 99 MB
% 217.31/31.67 % (3806823)Instructions burned: 441 (million)
% 217.31/31.67 % (3806825)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3013013597:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2828 on theBenchmark for (2828ds/11145Mi)
% 217.31/31.67 % (3806787)Instruction limit reached!
% 217.31/31.67 % (3806787)------------------------------
% 217.31/31.67 % (3806787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 217.31/31.67 % (3806787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.31/31.67 % (3806787)CaDiCaL version: 2.1.3
% 217.31/31.67 % (3806787)Termination reason: Instruction limit
% 217.31/31.67 % (3806787)Termination phase: Saturation
% 217.31/31.67 % (3806787)Time elapsed: 13.244 s
% 217.31/31.67 % (3806787)Peak memory usage: 281 MB
% 217.31/31.67 % (3806787)Instructions burned: 14155 (million)
% 217.31/31.67 % (3806827)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1434483182:cts=off:i=3034:av=off:er=known:fsd=on_2818 on theBenchmark for (2818ds/3034Mi)
% 217.31/31.67 % (3806827)Instruction limit reached!
% 217.31/31.67 % (3806827)------------------------------
% 217.31/31.67 % (3806827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 217.31/31.67 % (3806827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.31/31.67 % (3806827)CaDiCaL version: 2.1.3
% 217.31/31.67 % (3806827)Termination reason: Instruction limit
% 217.31/31.67 % (3806827)Termination phase: Saturation
% 217.31/31.67 % (3806827)Time elapsed: 2.861 s
% 217.31/31.67 % (3806827)Peak memory usage: 224 MB
% 217.31/31.67 % (3806827)Instructions burned: 3035 (million)
% 217.31/31.67 % (3806829)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3604387798:st=2:s2a=on:i=524:s2at=2:ss=axioms_2787 on theBenchmark for (2787ds/524Mi)
% 118.51/32.63 % (3806829)Instruction limit reached!
% 118.51/32.63 % (3806829)------------------------------
% 118.51/32.63 % (3806829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806829)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806829)Termination reason: Instruction limit
% 118.51/32.63 % (3806829)Termination phase: Saturation
% 118.51/32.63 % (3806829)Time elapsed: 0.424 s
% 118.51/32.63 % (3806829)Peak memory usage: 95 MB
% 118.51/32.63 % (3806829)Instructions burned: 524 (million)
% 118.51/32.63 % (3806831)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4185847330:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2780 on theBenchmark for (2780ds/1016Mi)
% 118.51/32.63 % (3806831)Refutation not found, incomplete strategy
% 118.51/32.63 % (3806831)------------------------------
% 118.51/32.63 % (3806831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806831)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806831)Termination reason: Refutation not found, incomplete strategy
% 118.51/32.63 % (3806831)Time elapsed: 0.230 s
% 118.51/32.63 % (3806831)Peak memory usage: 94 MB
% 118.51/32.63 % (3806831)Instructions burned: 256 (million)
% 118.51/32.63 % (3806831)------------------------------
% 118.51/32.63 % (3806831)------------------------------
% 118.51/32.63 % (3806833)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4074264349:i=14123:bd=preordered:ins=4_2771 on theBenchmark for (2771ds/14123Mi)
% 118.51/32.63 % (3806825)Instruction limit reached!
% 118.51/32.63 % (3806825)------------------------------
% 118.51/32.63 % (3806825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806825)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806825)Termination reason: Instruction limit
% 118.51/32.63 % (3806825)Termination phase: Saturation
% 118.51/32.63 % (3806825)Time elapsed: 6.410 s
% 118.51/32.63 % (3806825)Peak memory usage: 201 MB
% 118.51/32.63 % (3806825)Instructions burned: 11145 (million)
% 118.51/32.63 % (3806819)Instruction limit reached!
% 118.51/32.63 % (3806819)------------------------------
% 118.51/32.63 % (3806819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806819)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806819)Termination reason: Instruction limit
% 118.51/32.63 % (3806819)Termination phase: Saturation
% 118.51/32.63 % (3806819)Time elapsed: 7.976 s
% 118.51/32.63 % (3806819)Peak memory usage: 225 MB
% 118.51/32.63 % (3806819)Instructions burned: 9926 (million)
% 118.51/32.63 % (3806835)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=340039666:i=5781:kws=precedence:bd=all:rawr=on_2761 on theBenchmark for (2761ds/5781Mi)
% 118.51/32.63 % (3806836)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3141700988:i=2448:gtgl=5:bd=preordered:gtg=all_2760 on theBenchmark for (2760ds/2448Mi)
% 118.51/32.63 % (3806836)Instruction limit reached!
% 118.51/32.63 % (3806836)------------------------------
% 118.51/32.63 % (3806836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806836)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806836)Termination reason: Instruction limit
% 118.51/32.63 % (3806836)Termination phase: Saturation
% 118.51/32.63 % (3806836)Time elapsed: 1.267 s
% 118.51/32.63 % (3806836)Peak memory usage: 226 MB
% 118.51/32.63 % (3806836)Instructions burned: 2449 (million)
% 118.51/32.63 % (3806841)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1379368619:i=3223:kws=precedence:fgj=on:av=off_2745 on theBenchmark for (2745ds/3223Mi)
% 118.51/32.63 % (3806815)Instruction limit reached!
% 118.51/32.63 % (3806815)------------------------------
% 118.51/32.63 % (3806815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806815)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806815)Termination reason: Instruction limit
% 118.51/32.63 % (3806815)Termination phase: Saturation
% 118.51/32.63 % (3806815)Time elapsed: 12.921 s
% 118.51/32.63 % (3806815)Peak memory usage: 183 MB
% 118.51/32.63 % (3806815)Instructions burned: 13914 (million)
% 118.51/32.63 % (3806841)Instruction limit reached!
% 118.51/32.63 % (3806841)------------------------------
% 118.51/32.63 % (3806841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806841)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806841)Termination reason: Instruction limit
% 118.51/32.63 % (3806841)Termination phase: Saturation
% 118.51/32.63 % (3806841)Time elapsed: 1.631 s
% 118.51/32.63 % (3806841)Peak memory usage: 232 MB
% 118.51/32.63 % (3806841)Instructions burned: 3224 (million)
% 118.51/32.63 % (3806847)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1323036451:st=5.6:i=2033:sd=3:ss=axioms_2728 on theBenchmark for (2728ds/2033Mi)
% 118.51/32.63 % (3806848)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2879061522:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2727 on theBenchmark for (2727ds/2055Mi)
% 118.51/32.63 % (3806835)Instruction limit reached!
% 118.51/32.63 % (3806835)------------------------------
% 118.51/32.63 % (3806835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806835)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806835)Termination reason: Instruction limit
% 118.51/32.63 % (3806835)Termination phase: Saturation
% 118.51/32.63 % (3806835)Time elapsed: 4.435 s
% 118.51/32.63 % (3806835)Peak memory usage: 107 MB
% 118.51/32.63 % (3806835)Instructions burned: 5782 (million)
% 118.51/32.63 % (3806848)Instruction limit reached!
% 118.51/32.63 % (3806848)------------------------------
% 118.51/32.63 % (3806848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806848)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806848)Termination reason: Instruction limit
% 118.51/32.63 % (3806848)Termination phase: Saturation
% 118.51/32.63 % (3806848)Time elapsed: 1.099 s
% 118.51/32.63 % (3806848)Peak memory usage: 140 MB
% 118.51/32.63 % (3806848)Instructions burned: 2056 (million)
% 118.51/32.63 % (3806855)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1264671464:i=21611:sd=3:ss=axioms_2714 on theBenchmark for (2714ds/21611Mi)
% 118.51/32.63 % (3806856)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3574631854:i=4835:sd=13:ss=axioms:sgt=23_2713 on theBenchmark for (2713ds/4835Mi)
% 118.51/32.63 % (3806847)Instruction limit reached!
% 118.51/32.63 % (3806847)------------------------------
% 118.51/32.63 % (3806847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806847)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806847)Termination reason: Instruction limit
% 118.51/32.63 % (3806847)Termination phase: Saturation
% 118.51/32.63 % (3806847)Time elapsed: 1.833 s
% 118.51/32.63 % (3806847)Peak memory usage: 142 MB
% 118.51/32.63 % (3806847)Instructions burned: 2033 (million)
% 118.51/32.63 % (3806859)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1993914817:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2707 on theBenchmark for (2707ds/797Mi)
% 118.51/32.63 % (3806859)Instruction limit reached!
% 118.51/32.63 % (3806859)------------------------------
% 118.51/32.63 % (3806859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806859)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806859)Termination reason: Instruction limit
% 118.51/32.63 % (3806859)Termination phase: Saturation
% 118.51/32.63 % (3806859)Time elapsed: 0.673 s
% 118.51/32.63 % (3806859)Peak memory usage: 103 MB
% 118.51/32.63 % (3806859)Instructions burned: 797 (million)
% 118.51/32.63 % (3806863)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1266713783:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2697 on theBenchmark for (2697ds/2326Mi)
% 118.51/32.63 % (3806856)Instruction limit reached!
% 118.51/32.63 % (3806856)------------------------------
% 118.51/32.63 % (3806856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.51/32.63 % (3806856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.51/32.63 % (3806856)CaDiCaL version: 2.1.3
% 118.51/32.63 % (3806856)Termination reason: Instruction limit
% 118.51/32.63 % (3806856)Termination phase: Saturation
% 118.51/32.63 % (3806856)Time elapsed: 1.960 s
% 118.51/32.63 % (3806856)Peak memory usage: 122 MB
% 118.51/32.63 % (3806856)Instructions burned: 4835 (million)
% 118.51/32.63 % (3806865)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2027769592:i=6038:nm=6_2692 on theBenchmark for (2692ds/6038Mi)
% 118.51/32.63 % (3806863)First to succeed.
% 118.51/32.63 % (3806863)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3806708"
% 118.51/32.63 % (3806863)Refutation found. Thanks to Tanya!
% 118.51/32.63 % SZS status Theorem for theBenchmark
% 118.51/32.63 % SZS output start Proof for theBenchmark
% See solution above
% 224.91/32.85 % (3806863)------------------------------
% 224.91/32.85 % (3806863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.91/32.85 % (3806863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.91/32.85 % (3806863)CaDiCaL version: 2.1.3
% 224.91/32.85 % (3806863)Termination reason: Refutation
% 224.91/32.85 % (3806863)Time elapsed: 0.783 s
% 224.91/32.85 % (3806863)Peak memory usage: 111 MB
% 224.91/32.85 % (3806863)Instructions burned: 879 (million)
% 224.91/32.85 % (3806863)------------------------------
% 224.91/32.85 % (3806863)------------------------------
% 224.91/32.85 % (3806708)Success in time 31.751 s
% 224.91/32.85 % Vampire exiting
%------------------------------------------------------------------------------