%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET042-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:39:45 PM UTC 2026
% Result : Unsatisfiable 190.03s 38.41s
% Output : Refutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 51
% Syntax : Number of formulae : 291 ( 49 unt; 25 def)
% Number of atoms : 866 ( 158 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1074 ( 499 ~; 554 |; 0 &)
% ( 21 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 22 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-2 aty)
% Number of variables : 221 ( 0 sgn 221 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ member(X0,X1)
| little_set(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
! [X0,X1] :
( member(f1(X0,X1),X1)
| member(f1(X0,X1),X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality2) ).
fof(f4,axiom,
! [X0,X1] :
( ~ member(f1(X0,X1),X1)
| ~ member(f1(X0,X1),X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality3) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ member(X0,non_ordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair1) ).
fof(f6,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ little_set(X0)
| member(X0,non_ordered_pair(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair2) ).
fof(f7,axiom,
! [X2,X0,X1] :
( X0 != X2
| ~ little_set(X0)
| member(X0,non_ordered_pair(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair3) ).
fof(f8,axiom,
! [X0,X1] : little_set(non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair4) ).
fof(f9,axiom,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f10,axiom,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(singleton_set(X0),non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f15,axiom,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| X0 != ordered_pair(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair_predicate4) ).
fof(f16,plain,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| ordered_pair(X1,X2) != X0 ),
inference(reorient_equations,[],[f15]) ).
fof(f19,axiom,
! [X0,X1] :
( ~ member(X0,first(X1))
| X1 = ordered_pair(f4(X0,X1),f5(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first3) ).
fof(f20,plain,
! [X0,X1] :
( ~ member(X0,first(X1))
| ordered_pair(f4(X0,X1),f5(X0,X1)) = X1 ),
inference(reorient_equations,[],[f19]) ).
fof(f21,axiom,
! [X0,X1] :
( member(X0,f4(X0,X1))
| ~ member(X0,first(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first4) ).
fof(f22,axiom,
! [X2,X3,X0,X1] :
( member(X0,first(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3)
| ~ member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first5) ).
fof(f23,plain,
! [X2,X3,X0,X1] :
( member(X0,first(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| ordered_pair(X2,X3) != X1
| ~ member(X0,X2) ),
inference(reorient_equations,[],[f22]) ).
fof(f25,axiom,
! [X0,X1] :
( ~ member(X0,second(X1))
| little_set(f7(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second2) ).
fof(f26,axiom,
! [X0,X1] :
( ~ member(X0,second(X1))
| X1 = ordered_pair(f6(X0,X1),f7(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second3) ).
fof(f27,plain,
! [X0,X1] :
( ~ member(X0,second(X1))
| ordered_pair(f6(X0,X1),f7(X0,X1)) = X1 ),
inference(reorient_equations,[],[f26]) ).
fof(f28,axiom,
! [X0,X1] :
( member(X0,f7(X0,X1))
| ~ member(X0,second(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second4) ).
fof(f29,axiom,
! [X2,X3,X0,X1] :
( member(X0,second(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3)
| ~ member(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second5) ).
fof(f30,plain,
! [X2,X3,X0,X1] :
( member(X0,second(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| ordered_pair(X2,X3) != X1
| ~ member(X0,X3) ),
inference(reorient_equations,[],[f29]) ).
fof(f49,axiom,
! [X2,X0,X1] :
( member(X0,cross_product(X1,X2))
| ~ little_set(X0)
| ~ ordered_pair_predicate(X0)
| ~ member(first(X0),X1)
| ~ member(second(X0),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cross_product4) ).
fof(f70,axiom,
! [X0] : ~ member(X0,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',empty_set) ).
fof(f79,axiom,
! [X2,X0,X1] :
( ~ subset(X0,X1)
| ~ member(X2,X0)
| member(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset1) ).
fof(f80,axiom,
! [X0,X1] :
( member(f17(X0,X1),X0)
| subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset2) ).
fof(f81,axiom,
! [X0,X1] :
( ~ member(f17(X0,X1),X1)
| subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset3) ).
fof(f115,axiom,
! [X0] :
( ~ little_set(X0)
| X0 = empty_set
| member(f26(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',choice2) ).
fof(f116,plain,
! [X0] :
( member(f26(X0),X0)
| empty_set = X0
| ~ little_set(X0) ),
inference(reorient_equations,[],[f115]) ).
fof(f162,axiom,
member(a,set_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',member_of_set_a) ).
fof(f163,axiom,
member(b,set_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',member_of_set_b) ).
fof(f164,negated_conjecture,
~ member(ordered_pair(a,b),cross_product(set_a,set_b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ordered_pair_is_in_cross_product) ).
fof(f166,plain,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1)),
inference(definition_unfolding,[],[f10,f9]) ).
fof(f169,plain,
! [X2,X0,X1] :
( non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)) != X0
| ~ little_set(X1)
| ~ little_set(X2)
| ordered_pair_predicate(X0) ),
inference(definition_unfolding,[],[f16,f166]) ).
fof(f170,plain,
! [X0,X1] :
( non_ordered_pair(non_ordered_pair(f4(X0,X1),f4(X0,X1)),non_ordered_pair(f4(X0,X1),f5(X0,X1))) = X1
| ~ member(X0,first(X1)) ),
inference(definition_unfolding,[],[f20,f166]) ).
fof(f171,plain,
! [X2,X3,X0,X1] :
( non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3)) != X1
| ~ little_set(X2)
| ~ little_set(X3)
| member(X0,first(X1))
| ~ member(X0,X2) ),
inference(definition_unfolding,[],[f23,f166]) ).
fof(f172,plain,
! [X0,X1] :
( non_ordered_pair(non_ordered_pair(f6(X0,X1),f6(X0,X1)),non_ordered_pair(f6(X0,X1),f7(X0,X1))) = X1
| ~ member(X0,second(X1)) ),
inference(definition_unfolding,[],[f27,f166]) ).
fof(f173,plain,
! [X2,X3,X0,X1] :
( non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3)) != X1
| ~ little_set(X2)
| ~ little_set(X3)
| member(X0,second(X1))
| ~ member(X0,X3) ),
inference(definition_unfolding,[],[f30,f166]) ).
fof(f193,plain,
~ member(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)),cross_product(set_a,set_b)),
inference(definition_unfolding,[],[f164,f166]) ).
fof(f194,definition,
sF0 = non_ordered_pair(a,a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f195,plain,
non_ordered_pair(a,a) = sF0,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF1 = non_ordered_pair(a,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f197,plain,
non_ordered_pair(a,b) = sF1,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF2 = non_ordered_pair(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f199,plain,
non_ordered_pair(sF0,sF1) = sF2,
inference(reorient_equations,[],[f198]) ).
fof(f200,definition,
sF3 = cross_product(set_a,set_b),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f201,plain,
cross_product(set_a,set_b) = sF3,
inference(reorient_equations,[],[f200]) ).
fof(f202,plain,
~ member(sF2,sF3),
inference(definition_folding,[],[f193,f201,f199,f197,f195]) ).
fof(f203,plain,
! [X0,X1] :
( member(X0,non_ordered_pair(X1,X0))
| ~ little_set(X0) ),
inference(equality_resolution,[],[f7]) ).
fof(f206,plain,
! [X0,X1] :
( member(X0,non_ordered_pair(X0,X1))
| ~ little_set(X0) ),
inference(equality_resolution,[],[f6]) ).
fof(f207,plain,
( member(sF1,sF2)
| ~ little_set(sF1) ),
inference(superposition,[],[f203,f199]) ).
fof(f208,plain,
( member(a,sF0)
| ~ little_set(a) ),
inference(superposition,[],[f203,f195]) ).
fof(f209,plain,
( member(b,sF1)
| ~ little_set(b) ),
inference(superposition,[],[f203,f197]) ).
fof(f213,plain,
! [X0] :
( non_ordered_pair(non_ordered_pair(a,a),sF1) != X0
| ~ little_set(a)
| ~ little_set(b)
| ordered_pair_predicate(X0) ),
inference(superposition,[],[f169,f197]) ).
fof(f216,plain,
! [X0] :
( non_ordered_pair(sF0,sF1) != X0
| ~ little_set(a)
| ~ little_set(b)
| ordered_pair_predicate(X0) ),
inference(forward_demodulation,[],[f213,f195]) ).
fof(f217,plain,
! [X0] :
( sF2 != X0
| ~ little_set(a)
| ~ little_set(b)
| ordered_pair_predicate(X0) ),
inference(forward_demodulation,[],[f216,f199]) ).
fof(f220,plain,
( member(a,sF1)
| ~ little_set(a) ),
inference(superposition,[],[f206,f197]) ).
fof(f226,plain,
little_set(sF2),
inference(superposition,[],[f8,f199]) ).
fof(f227,plain,
little_set(sF0),
inference(superposition,[],[f8,f195]) ).
fof(f228,plain,
little_set(sF1),
inference(superposition,[],[f8,f197]) ).
fof(f232,plain,
! [X0] :
( ~ member(X0,sF2)
| sF0 = X0
| sF1 = X0 ),
inference(superposition,[],[f5,f199]) ).
fof(f233,plain,
! [X0] :
( ~ member(X0,sF0)
| a = X0
| a = X0 ),
inference(superposition,[],[f5,f195]) ).
fof(f234,plain,
! [X0] :
( ~ member(X0,sF1)
| a = X0
| b = X0 ),
inference(superposition,[],[f5,f197]) ).
fof(f235,plain,
! [X0] :
( ~ member(X0,sF0)
| a = X0 ),
inference(duplicate_literal_removal,[],[f233]) ).
fof(f250,definition,
( spl4_1
<=> little_set(b) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f251,plain,
( little_set(b)
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f252,plain,
( ~ little_set(b)
| spl4_1 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f254,definition,
( spl4_2
<=> little_set(a) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f255,plain,
( little_set(a)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f264,plain,
! [X0] :
( ~ member(second(X0),set_b)
| ~ little_set(X0)
| ~ ordered_pair_predicate(X0)
| ~ member(first(X0),set_a)
| member(X0,sF3) ),
inference(superposition,[],[f49,f201]) ).
fof(f269,plain,
! [X0,X1] :
( non_ordered_pair(non_ordered_pair(a,a),sF1) != X0
| ~ little_set(a)
| ~ little_set(b)
| member(X1,second(X0))
| ~ member(X1,b) ),
inference(superposition,[],[f173,f197]) ).
fof(f283,definition,
( spl4_4
<=> ! [X0] :
( sF2 != X0
| ordered_pair_predicate(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f284,plain,
( ! [X0] :
( sF2 != X0
| ordered_pair_predicate(X0) )
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f285,plain,
( ~ spl4_1
| ~ spl4_2
| spl4_4 ),
inference(avatar_split_clause,[],[f217,f283,f254,f250]) ).
fof(f293,plain,
little_set(a),
inference(resolution,[],[f1,f162]) ).
fof(f294,plain,
little_set(b),
inference(resolution,[],[f1,f163]) ).
fof(f295,plain,
( $false
| spl4_1 ),
inference(forward_subsumption_resolution,[],[f294,f252]) ).
fof(f296,plain,
spl4_1,
inference(avatar_contradiction_clause,[],[f295]) ).
fof(f299,plain,
! [X0,X1] :
( non_ordered_pair(non_ordered_pair(a,a),sF1) != X0
| ~ little_set(b)
| member(X1,second(X0))
| ~ member(X1,b) ),
inference(forward_subsumption_resolution,[],[f269,f293]) ).
fof(f300,plain,
( ! [X0,X1] :
( non_ordered_pair(non_ordered_pair(a,a),sF1) != X0
| member(X1,second(X0))
| ~ member(X1,b) )
| ~ spl4_1 ),
inference(forward_subsumption_resolution,[],[f299,f251]) ).
fof(f301,plain,
( ! [X0,X1] :
( non_ordered_pair(sF0,sF1) != X0
| member(X1,second(X0))
| ~ member(X1,b) )
| ~ spl4_1 ),
inference(forward_demodulation,[],[f300,f195]) ).
fof(f302,plain,
( ! [X0,X1] :
( sF2 != X0
| member(X1,second(X0))
| ~ member(X1,b) )
| ~ spl4_1 ),
inference(forward_demodulation,[],[f301,f199]) ).
fof(f303,plain,
( ordered_pair_predicate(sF2)
| ~ spl4_4 ),
inference(equality_resolution,[],[f284]) ).
fof(f304,plain,
( ! [X0] :
( member(X0,second(sF2))
| ~ member(X0,b) )
| ~ spl4_1 ),
inference(equality_resolution,[],[f302]) ).
fof(f324,plain,
spl4_2,
inference(avatar_split_clause,[],[f293,f254]) ).
fof(f330,plain,
! [X0,X1] :
( non_ordered_pair(non_ordered_pair(a,a),sF1) != X0
| ~ little_set(a)
| ~ little_set(b)
| member(X1,first(X0))
| ~ member(X1,a) ),
inference(superposition,[],[f171,f197]) ).
fof(f333,plain,
( ! [X0,X1] :
( non_ordered_pair(non_ordered_pair(a,a),sF1) != X0
| ~ little_set(b)
| member(X1,first(X0))
| ~ member(X1,a) )
| ~ spl4_2 ),
inference(forward_subsumption_resolution,[],[f330,f255]) ).
fof(f337,plain,
( ! [X0,X1] :
( non_ordered_pair(non_ordered_pair(a,a),sF1) != X0
| member(X1,first(X0))
| ~ member(X1,a) )
| ~ spl4_1
| ~ spl4_2 ),
inference(forward_subsumption_resolution,[],[f333,f251]) ).
fof(f339,plain,
( ! [X0,X1] :
( non_ordered_pair(sF0,sF1) != X0
| member(X1,first(X0))
| ~ member(X1,a) )
| ~ spl4_1
| ~ spl4_2 ),
inference(forward_demodulation,[],[f337,f195]) ).
fof(f340,plain,
( ! [X0,X1] :
( sF2 != X0
| member(X1,first(X0))
| ~ member(X1,a) )
| ~ spl4_1
| ~ spl4_2 ),
inference(forward_demodulation,[],[f339,f199]) ).
fof(f341,plain,
( ! [X0] :
( member(X0,first(sF2))
| ~ member(X0,a) )
| ~ spl4_1
| ~ spl4_2 ),
inference(equality_resolution,[],[f340]) ).
fof(f402,definition,
( spl4_6
<=> member(a,sF0) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f404,plain,
( member(a,sF0)
| ~ spl4_6 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f405,plain,
( ~ spl4_2
| spl4_6 ),
inference(avatar_split_clause,[],[f208,f402,f254]) ).
fof(f434,definition,
( spl4_8
<=> little_set(sF1) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f436,plain,
( ~ little_set(sF1)
| spl4_8 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,definition,
( spl4_9
<=> member(sF1,sF2) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f440,plain,
( member(sF1,sF2)
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( ~ spl4_8
| spl4_9 ),
inference(avatar_split_clause,[],[f207,f438,f434]) ).
fof(f442,plain,
( $false
| spl4_8 ),
inference(forward_subsumption_resolution,[],[f436,f228]) ).
fof(f443,plain,
spl4_8,
inference(avatar_contradiction_clause,[],[f442]) ).
fof(f500,definition,
( spl4_11
<=> member(b,sF1) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f502,plain,
( member(b,sF1)
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f503,plain,
( ~ spl4_1
| spl4_11 ),
inference(avatar_split_clause,[],[f209,f500,f250]) ).
fof(f520,definition,
( spl4_14
<=> member(a,sF1) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f522,plain,
( member(a,sF1)
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f523,plain,
( ~ spl4_2
| spl4_14 ),
inference(avatar_split_clause,[],[f220,f520,f254]) ).
fof(f567,plain,
( ! [X0] :
( ~ member(f1(X0,first(sF2)),a)
| first(sF2) = X0
| ~ member(f1(X0,first(sF2)),X0) )
| ~ spl4_1
| ~ spl4_2 ),
inference(resolution,[],[f4,f341]) ).
fof(f571,plain,
( ! [X0] :
( ~ member(f1(X0,second(sF2)),b)
| second(sF2) = X0
| ~ member(f1(X0,second(sF2)),X0) )
| ~ spl4_1 ),
inference(resolution,[],[f4,f304]) ).
fof(f599,plain,
( empty_set = sF0
| ~ little_set(sF0)
| a = f26(sF0) ),
inference(resolution,[],[f116,f235]) ).
fof(f605,plain,
( empty_set = sF0
| a = f26(sF0) ),
inference(forward_subsumption_resolution,[],[f599,f227]) ).
fof(f869,plain,
! [X0] :
( a = f17(sF0,X0)
| subset(sF0,X0) ),
inference(resolution,[],[f80,f235]) ).
fof(f1019,definition,
( spl4_29
<=> a = f26(sF0) ),
introduced(definition,[new_symbols(definition,[spl4_29])],[avatar_definition]) ).
fof(f1021,plain,
( a = f26(sF0)
| ~ spl4_29 ),
inference(avatar_component_clause,[],[f1019]) ).
fof(f1023,definition,
( spl4_30
<=> empty_set = sF0 ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f1025,plain,
( empty_set = sF0
| ~ spl4_30 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1026,plain,
( spl4_29
| spl4_30 ),
inference(avatar_split_clause,[],[f605,f1023,f1019]) ).
fof(f1076,definition,
( spl4_33
<=> sF0 = sF1 ),
introduced(definition,[new_symbols(definition,[spl4_33])],[avatar_definition]) ).
fof(f1077,plain,
( sF0 != sF1
| spl4_33 ),
inference(avatar_component_clause,[],[f1076]) ).
fof(f1078,plain,
( sF0 = sF1
| ~ spl4_33 ),
inference(avatar_component_clause,[],[f1076]) ).
fof(f1526,plain,
( member(a,empty_set)
| ~ spl4_6
| ~ spl4_30 ),
inference(superposition,[],[f404,f1025]) ).
fof(f1537,plain,
( $false
| ~ spl4_6
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f1526,f70]) ).
fof(f1538,plain,
( ~ spl4_6
| ~ spl4_30 ),
inference(avatar_contradiction_clause,[],[f1537]) ).
fof(f2485,plain,
! [X0] :
( ~ member(a,X0)
| subset(sF0,X0)
| subset(sF0,X0) ),
inference(superposition,[],[f81,f869]) ).
fof(f2490,plain,
! [X0] :
( ~ member(a,X0)
| subset(sF0,X0) ),
inference(duplicate_literal_removal,[],[f2485]) ).
fof(f2507,plain,
( subset(sF0,sF1)
| ~ spl4_14 ),
inference(resolution,[],[f2490,f522]) ).
fof(f2600,definition,
( spl4_48
<=> member(b,sF0) ),
introduced(definition,[new_symbols(definition,[spl4_48])],[avatar_definition]) ).
fof(f2601,plain,
( member(b,sF0)
| ~ spl4_48 ),
inference(avatar_component_clause,[],[f2600]) ).
fof(f2602,plain,
( ~ member(b,sF0)
| spl4_48 ),
inference(avatar_component_clause,[],[f2600]) ).
fof(f2664,definition,
( spl4_50
<=> b = f26(sF1) ),
introduced(definition,[new_symbols(definition,[spl4_50])],[avatar_definition]) ).
fof(f2665,plain,
( b != f26(sF1)
| spl4_50 ),
inference(avatar_component_clause,[],[f2664]) ).
fof(f2666,plain,
( b = f26(sF1)
| ~ spl4_50 ),
inference(avatar_component_clause,[],[f2664]) ).
fof(f3439,plain,
! [X2,X0,X1] :
( non_ordered_pair(f6(X2,X0),f7(X2,X0)) = X1
| non_ordered_pair(f6(X2,X0),f6(X2,X0)) = X1
| ~ member(X1,X0)
| ~ member(X2,second(X0)) ),
inference(superposition,[],[f5,f172]) ).
fof(f3448,plain,
! [X0,X1] :
( member(non_ordered_pair(f6(X1,X0),f7(X1,X0)),X0)
| ~ little_set(non_ordered_pair(f6(X1,X0),f7(X1,X0)))
| ~ member(X1,second(X0)) ),
inference(superposition,[],[f203,f172]) ).
fof(f3449,plain,
! [X0,X1] :
( member(non_ordered_pair(f6(X1,X0),f6(X1,X0)),X0)
| ~ little_set(non_ordered_pair(f6(X1,X0),f6(X1,X0)))
| ~ member(X1,second(X0)) ),
inference(superposition,[],[f206,f172]) ).
fof(f3477,plain,
! [X0,X1] :
( member(non_ordered_pair(f6(X1,X0),f6(X1,X0)),X0)
| ~ member(X1,second(X0)) ),
inference(forward_subsumption_resolution,[],[f3449,f8]) ).
fof(f3478,plain,
! [X0,X1] :
( member(non_ordered_pair(f6(X1,X0),f7(X1,X0)),X0)
| ~ member(X1,second(X0)) ),
inference(forward_subsumption_resolution,[],[f3448,f8]) ).
fof(f3555,plain,
! [X0] :
( sF1 = non_ordered_pair(f6(X0,sF2),f7(X0,sF2))
| sF0 = non_ordered_pair(f6(X0,sF2),f7(X0,sF2))
| ~ member(X0,second(sF2)) ),
inference(resolution,[],[f3478,f232]) ).
fof(f3574,plain,
! [X0] :
( sF1 = non_ordered_pair(f6(X0,sF2),f6(X0,sF2))
| sF0 = non_ordered_pair(f6(X0,sF2),f6(X0,sF2))
| ~ member(X0,second(sF2)) ),
inference(resolution,[],[f3477,f232]) ).
fof(f4974,definition,
( spl4_88
<=> a = b ),
introduced(definition,[new_symbols(definition,[spl4_88])],[avatar_definition]) ).
fof(f4976,plain,
( a = b
| ~ spl4_88 ),
inference(avatar_component_clause,[],[f4974]) ).
fof(f5936,plain,
! [X0,X1] :
( member(non_ordered_pair(f4(X1,X0),f4(X1,X0)),X0)
| ~ little_set(non_ordered_pair(f4(X1,X0),f4(X1,X0)))
| ~ member(X1,first(X0)) ),
inference(superposition,[],[f206,f170]) ).
fof(f5968,plain,
! [X0,X1] :
( member(non_ordered_pair(f4(X1,X0),f4(X1,X0)),X0)
| ~ member(X1,first(X0)) ),
inference(forward_subsumption_resolution,[],[f5936,f8]) ).
fof(f6093,plain,
! [X0] :
( sF1 = non_ordered_pair(f4(X0,sF2),f4(X0,sF2))
| sF0 = non_ordered_pair(f4(X0,sF2),f4(X0,sF2))
| ~ member(X0,first(sF2)) ),
inference(resolution,[],[f5968,f232]) ).
fof(f10533,plain,
( ! [X0] :
( ~ member(X0,sF0)
| member(X0,sF1) )
| ~ spl4_14 ),
inference(resolution,[],[f2507,f79]) ).
fof(f20054,plain,
! [X0] :
( member(f7(X0,sF2),sF1)
| ~ little_set(f7(X0,sF2))
| sF0 = non_ordered_pair(f6(X0,sF2),f7(X0,sF2))
| ~ member(X0,second(sF2)) ),
inference(superposition,[],[f203,f3555]) ).
fof(f20113,plain,
! [X0] :
( sF0 = non_ordered_pair(f6(X0,sF2),f7(X0,sF2))
| member(f7(X0,sF2),sF1)
| ~ member(X0,second(sF2)) ),
inference(forward_subsumption_resolution,[],[f20054,f25]) ).
fof(f20351,plain,
! [X0] :
( member(f7(X0,sF2),sF0)
| ~ little_set(f7(X0,sF2))
| member(f7(X0,sF2),sF1)
| ~ member(X0,second(sF2)) ),
inference(superposition,[],[f203,f20113]) ).
fof(f20411,plain,
! [X0] :
( member(f7(X0,sF2),sF0)
| member(f7(X0,sF2),sF1)
| ~ member(X0,second(sF2)) ),
inference(forward_subsumption_resolution,[],[f20351,f25]) ).
fof(f20442,plain,
( ! [X0] :
( member(f7(X0,sF2),sF1)
| ~ member(X0,second(sF2)) )
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f20411,f10533]) ).
fof(f20468,plain,
( ! [X0] :
( b = f7(X0,sF2)
| a = f7(X0,sF2)
| ~ member(X0,second(sF2)) )
| ~ spl4_14 ),
inference(resolution,[],[f20442,f234]) ).
fof(f20476,plain,
( ! [X0] :
( member(X0,b)
| ~ member(X0,second(sF2))
| a = f7(X0,sF2)
| ~ member(X0,second(sF2)) )
| ~ spl4_14 ),
inference(superposition,[],[f28,f20468]) ).
fof(f20488,plain,
( ! [X0] :
( a = f7(X0,sF2)
| ~ member(X0,second(sF2))
| member(X0,b) )
| ~ spl4_14 ),
inference(duplicate_literal_removal,[],[f20476]) ).
fof(f20500,plain,
( ! [X0] :
( member(X0,a)
| ~ member(X0,second(sF2))
| ~ member(X0,second(sF2))
| member(X0,b) )
| ~ spl4_14 ),
inference(superposition,[],[f28,f20488]) ).
fof(f20511,plain,
( ! [X0] :
( ~ member(X0,second(sF2))
| member(X0,a)
| member(X0,b) )
| ~ spl4_14 ),
inference(duplicate_literal_removal,[],[f20500]) ).
fof(f20520,plain,
( ! [X0] :
( member(f1(X0,second(sF2)),b)
| member(f1(X0,second(sF2)),a)
| member(f1(X0,second(sF2)),X0)
| second(sF2) = X0 )
| ~ spl4_14 ),
inference(resolution,[],[f20511,f3]) ).
fof(f22471,plain,
! [X0,X1] :
( ~ member(X0,sF1)
| f6(X1,sF2) = X0
| f6(X1,sF2) = X0
| sF0 = non_ordered_pair(f6(X1,sF2),f6(X1,sF2))
| ~ member(X1,second(sF2)) ),
inference(superposition,[],[f5,f3574]) ).
fof(f22544,plain,
! [X0,X1] :
( sF0 = non_ordered_pair(f6(X1,sF2),f6(X1,sF2))
| f6(X1,sF2) = X0
| ~ member(X0,sF1)
| ~ member(X1,second(sF2)) ),
inference(duplicate_literal_removal,[],[f22471]) ).
fof(f22802,plain,
! [X2,X0,X1] :
( ~ member(X0,sF0)
| f6(X1,sF2) = X0
| f6(X1,sF2) = X0
| f6(X1,sF2) = X2
| ~ member(X2,sF1)
| ~ member(X1,second(sF2)) ),
inference(superposition,[],[f5,f22544]) ).
fof(f22875,plain,
! [X2,X0,X1] :
( f6(X1,sF2) = X2
| f6(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X2,sF1)
| ~ member(X1,second(sF2)) ),
inference(duplicate_literal_removal,[],[f22802]) ).
fof(f23086,plain,
! [X0,X1] :
( f6(X1,sF2) != f6(X1,sF2)
| f6(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X0,sF1)
| ~ member(X1,second(sF2)) ),
inference(equality_factoring,[],[f22875]) ).
fof(f23087,plain,
! [X0,X1] :
( f6(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X0,sF1)
| ~ member(X1,second(sF2)) ),
inference(trivial_inequality_removal,[],[f23086]) ).
fof(f23117,plain,
( ! [X0,X1] :
( f6(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X1,second(sF2)) )
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f23087,f10533]) ).
fof(f23142,plain,
( ! [X2,X0,X1] :
( non_ordered_pair(X0,f7(X1,sF2)) = X2
| non_ordered_pair(X0,X0) = X2
| ~ member(X2,sF2)
| ~ member(X1,second(sF2))
| ~ member(X0,sF0)
| ~ member(X1,second(sF2)) )
| ~ spl4_14 ),
inference(superposition,[],[f3439,f23117]) ).
fof(f23155,plain,
( ! [X2,X0,X1] :
( non_ordered_pair(X0,f7(X1,sF2)) = X2
| non_ordered_pair(X0,X0) = X2
| ~ member(X2,sF2)
| ~ member(X1,second(sF2))
| ~ member(X0,sF0) )
| ~ spl4_14 ),
inference(duplicate_literal_removal,[],[f23142]) ).
fof(f25150,plain,
( ! [X0,X1] :
( X1 != X1
| non_ordered_pair(f7(X0,sF2),f7(X0,sF2)) = X1
| ~ member(X1,sF2)
| ~ member(X0,second(sF2))
| ~ member(f7(X0,sF2),sF0) )
| ~ spl4_14 ),
inference(equality_factoring,[],[f23155]) ).
fof(f25152,plain,
( ! [X0,X1] :
( non_ordered_pair(f7(X0,sF2),f7(X0,sF2)) = X1
| ~ member(X1,sF2)
| ~ member(X0,second(sF2))
| ~ member(f7(X0,sF2),sF0) )
| ~ spl4_14 ),
inference(trivial_inequality_removal,[],[f25150]) ).
fof(f27676,definition,
( spl4_175
<=> a = first(sF2) ),
introduced(definition,[new_symbols(definition,[spl4_175])],[avatar_definition]) ).
fof(f27677,plain,
( a != first(sF2)
| spl4_175 ),
inference(avatar_component_clause,[],[f27676]) ).
fof(f27678,plain,
( a = first(sF2)
| ~ spl4_175 ),
inference(avatar_component_clause,[],[f27676]) ).
fof(f29369,plain,
( ! [X0,X1] :
( non_ordered_pair(a,a) = X1
| ~ member(X1,sF2)
| ~ member(X0,second(sF2))
| ~ member(a,sF0)
| ~ member(X0,second(sF2))
| member(X0,b) )
| ~ spl4_14 ),
inference(superposition,[],[f25152,f20488]) ).
fof(f29529,plain,
( ! [X0,X1] :
( non_ordered_pair(a,a) = X1
| ~ member(X1,sF2)
| ~ member(X0,second(sF2))
| ~ member(a,sF0)
| member(X0,b) )
| ~ spl4_14 ),
inference(duplicate_literal_removal,[],[f29369]) ).
fof(f29608,plain,
( ! [X0,X1] :
( non_ordered_pair(a,a) = X1
| ~ member(X1,sF2)
| ~ member(X0,second(sF2))
| member(X0,b) )
| ~ spl4_6
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f29529,f404]) ).
fof(f29668,plain,
( ! [X0,X1] :
( sF0 = X1
| ~ member(X1,sF2)
| ~ member(X0,second(sF2))
| member(X0,b) )
| ~ spl4_6
| ~ spl4_14 ),
inference(forward_demodulation,[],[f29608,f195]) ).
fof(f29711,definition,
( spl4_181
<=> ! [X0] :
( ~ member(X0,second(sF2))
| member(X0,b) ) ),
introduced(definition,[new_symbols(definition,[spl4_181])],[avatar_definition]) ).
fof(f29712,plain,
( ! [X0] :
( ~ member(X0,second(sF2))
| member(X0,b) )
| ~ spl4_181 ),
inference(avatar_component_clause,[],[f29711]) ).
fof(f29714,definition,
( spl4_182
<=> ! [X1] :
( sF0 = X1
| ~ member(X1,sF2) ) ),
introduced(definition,[new_symbols(definition,[spl4_182])],[avatar_definition]) ).
fof(f29715,plain,
( ! [X1] :
( ~ member(X1,sF2)
| sF0 = X1 )
| ~ spl4_182 ),
inference(avatar_component_clause,[],[f29714]) ).
fof(f29716,plain,
( spl4_181
| spl4_182
| ~ spl4_6
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f29668,f520,f402,f29714,f29711]) ).
fof(f29774,plain,
( sF0 = sF1
| ~ spl4_9
| ~ spl4_182 ),
inference(resolution,[],[f29715,f440]) ).
fof(f29777,plain,
( $false
| ~ spl4_9
| spl4_33
| ~ spl4_182 ),
inference(forward_subsumption_resolution,[],[f29774,f1077]) ).
fof(f29778,plain,
( ~ spl4_9
| spl4_33
| ~ spl4_182 ),
inference(avatar_contradiction_clause,[],[f29777]) ).
fof(f29822,plain,
( ! [X0] :
( member(f1(X0,second(sF2)),b)
| member(f1(X0,second(sF2)),X0)
| second(sF2) = X0 )
| ~ spl4_181 ),
inference(resolution,[],[f29712,f3]) ).
fof(f29887,plain,
( member(f1(b,second(sF2)),b)
| b = second(sF2)
| ~ spl4_181 ),
inference(factoring,[],[f29822]) ).
fof(f29914,definition,
( spl4_183
<=> b = second(sF2) ),
introduced(definition,[new_symbols(definition,[spl4_183])],[avatar_definition]) ).
fof(f29916,plain,
( b = second(sF2)
| ~ spl4_183 ),
inference(avatar_component_clause,[],[f29914]) ).
fof(f29918,definition,
( spl4_184
<=> member(f1(b,second(sF2)),b) ),
introduced(definition,[new_symbols(definition,[spl4_184])],[avatar_definition]) ).
fof(f29919,plain,
( ~ member(f1(b,second(sF2)),b)
| spl4_184 ),
inference(avatar_component_clause,[],[f29918]) ).
fof(f29920,plain,
( member(f1(b,second(sF2)),b)
| ~ spl4_184 ),
inference(avatar_component_clause,[],[f29918]) ).
fof(f29921,plain,
( spl4_183
| spl4_184
| ~ spl4_181 ),
inference(avatar_split_clause,[],[f29887,f29711,f29918,f29914]) ).
fof(f29922,plain,
( b = second(sF2)
| ~ member(f1(b,second(sF2)),b)
| ~ spl4_1
| ~ spl4_184 ),
inference(resolution,[],[f29920,f571]) ).
fof(f29935,plain,
( b = second(sF2)
| ~ spl4_1
| ~ spl4_184 ),
inference(forward_subsumption_resolution,[],[f29922,f29920]) ).
fof(f29936,plain,
( spl4_183
| ~ spl4_1
| ~ spl4_184 ),
inference(avatar_split_clause,[],[f29935,f29918,f250,f29914]) ).
fof(f29963,plain,
( ~ member(b,set_b)
| ~ little_set(sF2)
| ~ ordered_pair_predicate(sF2)
| ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_183 ),
inference(superposition,[],[f264,f29916]) ).
fof(f30036,plain,
( ~ little_set(sF2)
| ~ ordered_pair_predicate(sF2)
| ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_183 ),
inference(forward_subsumption_resolution,[],[f29963,f163]) ).
fof(f30041,plain,
( ~ ordered_pair_predicate(sF2)
| ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_183 ),
inference(forward_subsumption_resolution,[],[f30036,f226]) ).
fof(f30045,plain,
( ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_4
| ~ spl4_183 ),
inference(forward_subsumption_resolution,[],[f30041,f303]) ).
fof(f30046,plain,
( ~ member(first(sF2),set_a)
| ~ spl4_4
| ~ spl4_183 ),
inference(forward_subsumption_resolution,[],[f30045,f202]) ).
fof(f43847,plain,
! [X0,X1] :
( ~ member(X0,sF1)
| f4(X1,sF2) = X0
| f4(X1,sF2) = X0
| sF0 = non_ordered_pair(f4(X1,sF2),f4(X1,sF2))
| ~ member(X1,first(sF2)) ),
inference(superposition,[],[f5,f6093]) ).
fof(f43929,plain,
! [X0,X1] :
( sF0 = non_ordered_pair(f4(X1,sF2),f4(X1,sF2))
| f4(X1,sF2) = X0
| ~ member(X0,sF1)
| ~ member(X1,first(sF2)) ),
inference(duplicate_literal_removal,[],[f43847]) ).
fof(f44236,plain,
! [X2,X0,X1] :
( ~ member(X0,sF0)
| f4(X1,sF2) = X0
| f4(X1,sF2) = X0
| f4(X1,sF2) = X2
| ~ member(X2,sF1)
| ~ member(X1,first(sF2)) ),
inference(superposition,[],[f5,f43929]) ).
fof(f44318,plain,
! [X2,X0,X1] :
( f4(X1,sF2) = X2
| f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X2,sF1)
| ~ member(X1,first(sF2)) ),
inference(duplicate_literal_removal,[],[f44236]) ).
fof(f44567,plain,
! [X0,X1] :
( f4(X1,sF2) != f4(X1,sF2)
| f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X0,sF1)
| ~ member(X1,first(sF2)) ),
inference(equality_factoring,[],[f44318]) ).
fof(f44568,plain,
! [X0,X1] :
( f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X0,sF1)
| ~ member(X1,first(sF2)) ),
inference(trivial_inequality_removal,[],[f44567]) ).
fof(f44606,plain,
( ! [X0,X1] :
( f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X1,first(sF2)) )
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f44568,f10533]) ).
fof(f44634,plain,
( ! [X0,X1] :
( member(X1,X0)
| ~ member(X1,first(sF2))
| ~ member(X0,sF0)
| ~ member(X1,first(sF2)) )
| ~ spl4_14 ),
inference(superposition,[],[f21,f44606]) ).
fof(f44657,plain,
( ! [X0,X1] :
( ~ member(X1,first(sF2))
| member(X1,X0)
| ~ member(X0,sF0) )
| ~ spl4_14 ),
inference(duplicate_literal_removal,[],[f44634]) ).
fof(f44700,plain,
( ! [X0,X1] :
( member(f1(X0,first(sF2)),X1)
| ~ member(X1,sF0)
| member(f1(X0,first(sF2)),X0)
| first(sF2) = X0 )
| ~ spl4_14 ),
inference(resolution,[],[f44657,f3]) ).
fof(f44904,plain,
( ! [X0] :
( member(f1(X0,first(sF2)),X0)
| ~ member(X0,sF0)
| first(sF2) = X0 )
| ~ spl4_14 ),
inference(factoring,[],[f44700]) ).
fof(f44949,plain,
( ~ member(a,sF0)
| a = first(sF2)
| a = first(sF2)
| ~ member(f1(a,first(sF2)),a)
| ~ spl4_1
| ~ spl4_2
| ~ spl4_14 ),
inference(resolution,[],[f44904,f567]) ).
fof(f45028,plain,
( ~ member(a,sF0)
| a = first(sF2)
| ~ member(f1(a,first(sF2)),a)
| ~ spl4_1
| ~ spl4_2
| ~ spl4_14 ),
inference(duplicate_literal_removal,[],[f44949]) ).
fof(f45037,plain,
( ~ member(a,sF0)
| a = first(sF2)
| ~ spl4_1
| ~ spl4_2
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f45028,f44904]) ).
fof(f45039,plain,
( a = first(sF2)
| ~ spl4_1
| ~ spl4_2
| ~ spl4_6
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f45037,f404]) ).
fof(f45040,plain,
( $false
| ~ spl4_1
| ~ spl4_2
| ~ spl4_6
| ~ spl4_14
| spl4_175 ),
inference(forward_subsumption_resolution,[],[f45039,f27677]) ).
fof(f45041,plain,
( ~ spl4_1
| ~ spl4_2
| ~ spl4_6
| ~ spl4_14
| spl4_175 ),
inference(avatar_contradiction_clause,[],[f45040]) ).
fof(f45070,plain,
( ~ member(a,set_a)
| ~ spl4_4
| ~ spl4_175
| ~ spl4_183 ),
inference(superposition,[],[f30046,f27678]) ).
fof(f45178,plain,
( $false
| ~ spl4_4
| ~ spl4_175
| ~ spl4_183 ),
inference(forward_subsumption_resolution,[],[f45070,f162]) ).
fof(f45179,plain,
( ~ spl4_4
| ~ spl4_175
| ~ spl4_183 ),
inference(avatar_contradiction_clause,[],[f45178]) ).
fof(f46057,plain,
( member(b,sF0)
| ~ spl4_11
| ~ spl4_33 ),
inference(superposition,[],[f502,f1078]) ).
fof(f46065,plain,
( b = f26(sF0)
| ~ spl4_33
| ~ spl4_50 ),
inference(superposition,[],[f2666,f1078]) ).
fof(f46120,plain,
( a = b
| ~ spl4_29
| ~ spl4_33
| ~ spl4_50 ),
inference(forward_demodulation,[],[f46065,f1021]) ).
fof(f46123,plain,
( $false
| ~ spl4_11
| ~ spl4_33
| spl4_48 ),
inference(forward_subsumption_resolution,[],[f46057,f2602]) ).
fof(f46124,plain,
( ~ spl4_11
| ~ spl4_33
| spl4_48 ),
inference(avatar_contradiction_clause,[],[f46123]) ).
fof(f46129,plain,
( b != f26(sF0)
| ~ spl4_33
| spl4_50 ),
inference(forward_demodulation,[],[f2665,f1078]) ).
fof(f46156,plain,
( a != b
| ~ spl4_29
| ~ spl4_33
| spl4_50 ),
inference(forward_demodulation,[],[f46129,f1021]) ).
fof(f46370,plain,
( a = b
| ~ spl4_48 ),
inference(resolution,[],[f2601,f235]) ).
fof(f46387,plain,
( $false
| ~ spl4_29
| ~ spl4_33
| ~ spl4_48
| spl4_50 ),
inference(forward_subsumption_resolution,[],[f46370,f46156]) ).
fof(f46388,plain,
( ~ spl4_29
| ~ spl4_33
| ~ spl4_48
| spl4_50 ),
inference(avatar_contradiction_clause,[],[f46387]) ).
fof(f48438,plain,
( spl4_88
| ~ spl4_29
| ~ spl4_33
| ~ spl4_50 ),
inference(avatar_split_clause,[],[f46120,f2664,f1076,f1019,f4974]) ).
fof(f52568,plain,
( member(a,set_b)
| ~ spl4_88 ),
inference(superposition,[],[f163,f4976]) ).
fof(f52594,plain,
( ! [X0] :
( member(f1(X0,second(sF2)),a)
| member(f1(X0,second(sF2)),a)
| member(f1(X0,second(sF2)),X0)
| second(sF2) = X0 )
| ~ spl4_14
| ~ spl4_88 ),
inference(superposition,[],[f20520,f4976]) ).
fof(f52605,plain,
( ! [X0] :
( member(f1(X0,second(sF2)),a)
| member(f1(X0,second(sF2)),X0)
| second(sF2) = X0 )
| ~ spl4_14
| ~ spl4_88 ),
inference(duplicate_literal_removal,[],[f52594]) ).
fof(f53447,plain,
( member(f1(a,second(sF2)),a)
| a = second(sF2)
| ~ spl4_14
| ~ spl4_88 ),
inference(factoring,[],[f52605]) ).
fof(f54242,plain,
( ~ member(f1(a,second(sF2)),a)
| ~ spl4_88
| spl4_184 ),
inference(superposition,[],[f29919,f4976]) ).
fof(f56568,definition,
( spl4_217
<=> a = second(sF2) ),
introduced(definition,[new_symbols(definition,[spl4_217])],[avatar_definition]) ).
fof(f56570,plain,
( a = second(sF2)
| ~ spl4_217 ),
inference(avatar_component_clause,[],[f56568]) ).
fof(f56572,definition,
( spl4_218
<=> member(f1(a,second(sF2)),a) ),
introduced(definition,[new_symbols(definition,[spl4_218])],[avatar_definition]) ).
fof(f56574,plain,
( member(f1(a,second(sF2)),a)
| ~ spl4_218 ),
inference(avatar_component_clause,[],[f56572]) ).
fof(f56575,plain,
( spl4_217
| spl4_218
| ~ spl4_14
| ~ spl4_88 ),
inference(avatar_split_clause,[],[f53447,f4974,f520,f56572,f56568]) ).
fof(f56609,plain,
( ~ member(a,set_b)
| ~ little_set(sF2)
| ~ ordered_pair_predicate(sF2)
| ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_217 ),
inference(superposition,[],[f264,f56570]) ).
fof(f56691,plain,
( ~ little_set(sF2)
| ~ ordered_pair_predicate(sF2)
| ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_88
| ~ spl4_217 ),
inference(forward_subsumption_resolution,[],[f56609,f52568]) ).
fof(f56708,plain,
( ~ ordered_pair_predicate(sF2)
| ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_88
| ~ spl4_217 ),
inference(forward_subsumption_resolution,[],[f56691,f226]) ).
fof(f56716,plain,
( ~ member(first(sF2),set_a)
| member(sF2,sF3)
| ~ spl4_4
| ~ spl4_88
| ~ spl4_217 ),
inference(forward_subsumption_resolution,[],[f56708,f303]) ).
fof(f56721,plain,
( ~ member(first(sF2),set_a)
| ~ spl4_4
| ~ spl4_88
| ~ spl4_217 ),
inference(forward_subsumption_resolution,[],[f56716,f202]) ).
fof(f56723,plain,
( ~ member(a,set_a)
| ~ spl4_4
| ~ spl4_88
| ~ spl4_175
| ~ spl4_217 ),
inference(forward_demodulation,[],[f56721,f27678]) ).
fof(f56725,plain,
( $false
| ~ spl4_4
| ~ spl4_88
| ~ spl4_175
| ~ spl4_217 ),
inference(forward_subsumption_resolution,[],[f56723,f162]) ).
fof(f56726,plain,
( ~ spl4_4
| ~ spl4_88
| ~ spl4_175
| ~ spl4_217 ),
inference(avatar_contradiction_clause,[],[f56725]) ).
fof(f56727,plain,
( $false
| ~ spl4_88
| spl4_184
| ~ spl4_218 ),
inference(forward_subsumption_resolution,[],[f56574,f54242]) ).
fof(f56728,plain,
( ~ spl4_88
| spl4_184
| ~ spl4_218 ),
inference(avatar_contradiction_clause,[],[f56727]) ).
cnf(s2,plain,
( ~ spl4_1
| ~ spl4_2
| spl4_4 ),
inference(sat_conversion,[],[f285]) ).
cnf(s3,plain,
spl4_1,
inference(sat_conversion,[],[f296]) ).
cnf(s5,plain,
spl4_2,
inference(sat_conversion,[],[f324]) ).
cnf(s7,plain,
( ~ spl4_2
| spl4_6 ),
inference(sat_conversion,[],[f405]) ).
cnf(s9,plain,
( ~ spl4_8
| spl4_9 ),
inference(sat_conversion,[],[f441]) ).
cnf(s10,plain,
spl4_8,
inference(sat_conversion,[],[f443]) ).
cnf(s12,plain,
( ~ spl4_1
| spl4_11 ),
inference(sat_conversion,[],[f503]) ).
cnf(s15,plain,
( ~ spl4_2
| spl4_14 ),
inference(sat_conversion,[],[f523]) ).
cnf(s23,plain,
( spl4_29
| spl4_30 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s32,plain,
( ~ spl4_6
| ~ spl4_30 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s139,plain,
( ~ spl4_6
| ~ spl4_14
| spl4_181
| spl4_182 ),
inference(sat_conversion,[],[f29716]) ).
cnf(s140,plain,
( ~ spl4_9
| spl4_33
| ~ spl4_182 ),
inference(sat_conversion,[],[f29778]) ).
cnf(s142,plain,
( ~ spl4_181
| spl4_183
| spl4_184 ),
inference(sat_conversion,[],[f29921]) ).
cnf(s143,plain,
( ~ spl4_1
| spl4_183
| ~ spl4_184 ),
inference(sat_conversion,[],[f29936]) ).
cnf(s160,plain,
( ~ spl4_1
| ~ spl4_2
| ~ spl4_6
| ~ spl4_14
| spl4_175 ),
inference(sat_conversion,[],[f45041]) ).
cnf(s161,plain,
( ~ spl4_4
| ~ spl4_175
| ~ spl4_183 ),
inference(sat_conversion,[],[f45179]) ).
cnf(s167,plain,
( ~ spl4_11
| ~ spl4_33
| spl4_48 ),
inference(sat_conversion,[],[f46124]) ).
cnf(s171,plain,
( ~ spl4_29
| ~ spl4_33
| ~ spl4_48
| spl4_50 ),
inference(sat_conversion,[],[f46388]) ).
cnf(s182,plain,
( ~ spl4_29
| ~ spl4_33
| ~ spl4_50
| spl4_88 ),
inference(sat_conversion,[],[f48438]) ).
cnf(s203,plain,
( ~ spl4_14
| ~ spl4_88
| spl4_217
| spl4_218 ),
inference(sat_conversion,[],[f56575]) ).
cnf(s205,plain,
( ~ spl4_4
| ~ spl4_88
| ~ spl4_175
| ~ spl4_217 ),
inference(sat_conversion,[],[f56726]) ).
cnf(s206,plain,
( ~ spl4_88
| spl4_184
| ~ spl4_218 ),
inference(sat_conversion,[],[f56728]) ).
cnf(s212,plain,
spl4_9,
inference(rat,[],[s9,s10]) ).
cnf(s216,plain,
spl4_14,
inference(rat,[],[s15,s5]) ).
cnf(s219,plain,
spl4_6,
inference(rat,[],[s7,s5]) ).
cnf(s222,plain,
~ spl4_30,
inference(rat,[],[s32,s219]) ).
cnf(s225,plain,
spl4_29,
inference(rat,[],[s23,s222]) ).
cnf(s226,plain,
spl4_175,
inference(rat,[],[s160,s219,s216,s5,s3]) ).
cnf(s227,plain,
spl4_11,
inference(rat,[],[s12,s3]) ).
cnf(s228,plain,
spl4_4,
inference(rat,[],[s2,s5,s3]) ).
cnf(s229,plain,
~ spl4_183,
inference(rat,[],[s161,s226,s228]) ).
cnf(s232,plain,
~ spl4_184,
inference(rat,[],[s143,s3,s229]) ).
cnf(s233,plain,
~ spl4_181,
inference(rat,[],[s142,s232,s229]) ).
cnf(s238,plain,
spl4_182,
inference(rat,[],[s139,s219,s216,s233]) ).
cnf(s242,plain,
spl4_33,
inference(rat,[],[s140,s212,s238]) ).
cnf(s243,plain,
spl4_48,
inference(rat,[],[s167,s227,s242]) ).
cnf(s244,plain,
spl4_50,
inference(rat,[],[s171,s242,s225,s243]) ).
cnf(s245,plain,
spl4_88,
inference(rat,[],[s182,s242,s225,s244]) ).
cnf(s247,plain,
~ spl4_218,
inference(rat,[],[s206,s232,s245]) ).
cnf(s248,plain,
~ spl4_217,
inference(rat,[],[s205,s228,s226,s245]) ).
cnf(s249,plain,
$false,
inference(rat,[],[s203,s247,s216,s248,s245]) ).
fof(f56729,plain,
$false,
inference(avatar_sat_refutation,[],[s249]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET042-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n008.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 00:21:25 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 11.68/2.52 % (1751777)Input is clausal, will run a generic CNF schedule.
% 11.68/2.52 % (1751783)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3088932146:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.68/2.52 % (1751787)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1729229128:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.68/2.52 % (1751784)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3007450643:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.68/2.52 % (1751785)lrs+10_1_sil=8000:sp=occurrence:random_seed=547161809:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.68/2.52 % (1751788)dis-21_1_sil=8000:lcm=predicate:random_seed=1482313994:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.68/2.52 % (1751786)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3950592997:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.68/2.52 % (1751782)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=2760992515:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.68/2.52 % (1751785)Refutation not found, incomplete strategy
% 11.68/2.52 % (1751785)------------------------------
% 11.68/2.52 % (1751785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.52 % (1751785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.52 % (1751785)CaDiCaL version: 2.1.3
% 11.68/2.52 % (1751785)Termination reason: Refutation not found, incomplete strategy
% 11.68/2.52 % (1751785)Time elapsed: 0.002 s
% 11.68/2.52 % (1751785)Peak memory usage: 88 MB
% 11.68/2.52 % (1751785)Instructions burned: 1 (million)
% 11.68/2.52 % (1751786)Refutation not found, incomplete strategy
% 11.68/2.52 % (1751786)------------------------------
% 11.68/2.52 % (1751786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.52 % (1751786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.52 % (1751786)CaDiCaL version: 2.1.3
% 11.68/2.52 % (1751786)Termination reason: Refutation not found, incomplete strategy
% 11.68/2.52 % (1751786)Time elapsed: 0.006 s
% 11.68/2.52 % (1751786)Peak memory usage: 88 MB
% 11.68/2.52 % (1751786)Instructions burned: 8 (million)
% 11.68/2.52 % (1751787)Instruction limit reached!
% 11.68/2.52 % (1751787)------------------------------
% 11.68/2.52 % (1751787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.52 % (1751787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.52 % (1751787)CaDiCaL version: 2.1.3
% 11.68/2.52 % (1751787)Termination reason: Instruction limit
% 11.68/2.52 % (1751787)Termination phase: Saturation
% 11.68/2.52 % (1751787)Time elapsed: 0.063 s
% 11.68/2.52 % (1751787)Peak memory usage: 90 MB
% 11.68/2.52 % (1751787)Instructions burned: 181 (million)
% 11.68/2.52 % (1751788)Instruction limit reached!
% 11.68/2.52 % (1751788)------------------------------
% 11.68/2.52 % (1751788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.52 % (1751788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.52 % (1751788)CaDiCaL version: 2.1.3
% 11.68/2.52 % (1751788)Termination reason: Instruction limit
% 11.68/2.52 % (1751788)Termination phase: Saturation
% 11.68/2.52 % (1751788)Time elapsed: 0.069 s
% 11.68/2.52 % (1751788)Peak memory usage: 89 MB
% 11.68/2.52 % (1751788)Instructions burned: 118 (million)
% 11.68/2.52 % (1751796)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3958063032:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.68/2.52 % (1751796)Refutation not found, incomplete strategy
% 11.68/2.52 % (1751796)------------------------------
% 11.68/2.52 % (1751796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.52 % (1751796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.52 % (1751796)CaDiCaL version: 2.1.3
% 11.68/2.52 % (1751796)Termination reason: Refutation not found, incomplete strategy
% 11.68/2.52 % (1751796)Time elapsed: 0.001 s
% 11.68/2.52 % (1751796)Peak memory usage: 88 MB
% 11.68/2.52 % (1751796)Instructions burned: 2 (million)
% 11.68/2.52 % (1751797)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1679296237:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 20.71/3.84 % (1751786)------------------------------
% 20.71/3.84 % (1751786)------------------------------
% 20.71/3.84 % (1751785)------------------------------
% 20.71/3.84 % (1751785)------------------------------
% 20.71/3.84 % (1751796)------------------------------
% 20.71/3.84 % (1751796)------------------------------
% 20.71/3.84 % (1751797)Instruction limit reached!
% 20.71/3.84 % (1751797)------------------------------
% 20.71/3.84 % (1751797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.71/3.84 % (1751797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.71/3.84 % (1751797)CaDiCaL version: 2.1.3
% 20.71/3.84 % (1751797)Termination reason: Instruction limit
% 20.71/3.84 % (1751797)Termination phase: Saturation
% 20.71/3.84 % (1751797)Time elapsed: 0.107 s
% 20.71/3.84 % (1751797)Peak memory usage: 91 MB
% 20.71/3.84 % (1751797)Instructions burned: 190 (million)
% 20.71/3.84 % (1751800)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2638759275:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 20.71/3.84 % (1751800)Refutation not found, incomplete strategy
% 20.71/3.84 % (1751800)------------------------------
% 20.71/3.84 % (1751800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.71/3.84 % (1751800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.71/3.84 % (1751800)CaDiCaL version: 2.1.3
% 20.71/3.84 % (1751800)Termination reason: Refutation not found, incomplete strategy
% 20.71/3.84 % (1751800)Time elapsed: 0.004 s
% 20.71/3.84 % (1751800)Peak memory usage: 88 MB
% 20.71/3.84 % (1751800)Instructions burned: 3 (million)
% 20.71/3.84 % (1751801)lrs+10_64_to=lpo:sil=8000:random_seed=2993602907:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 20.71/3.84 % (1751802)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2669703125:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 20.71/3.84 % (1751803)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3797317607:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 20.71/3.84 % (1751801)Instruction limit reached!
% 20.71/3.84 % (1751801)------------------------------
% 20.71/3.84 % (1751801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.71/3.84 % (1751801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.71/3.84 % (1751801)CaDiCaL version: 2.1.3
% 20.71/3.84 % (1751801)Termination reason: Instruction limit
% 20.71/3.84 % (1751801)Termination phase: Saturation
% 20.71/3.84 % (1751801)Time elapsed: 0.074 s
% 20.71/3.84 % (1751801)Peak memory usage: 90 MB
% 20.71/3.84 % (1751801)Instructions burned: 126 (million)
% 20.71/3.84 % (1751802)Instruction limit reached!
% 20.71/3.84 % (1751802)------------------------------
% 20.71/3.84 % (1751802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.71/3.84 % (1751802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.71/3.84 % (1751802)CaDiCaL version: 2.1.3
% 20.71/3.84 % (1751802)Termination reason: Instruction limit
% 20.71/3.84 % (1751802)Termination phase: Saturation
% 20.71/3.84 % (1751802)Time elapsed: 0.066 s
% 20.71/3.84 % (1751802)Peak memory usage: 89 MB
% 20.71/3.84 % (1751802)Instructions burned: 197 (million)
% 20.71/3.84 % (1751803)Instruction limit reached!
% 20.71/3.84 % (1751803)------------------------------
% 20.71/3.84 % (1751803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.71/3.84 % (1751803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.71/3.84 % (1751803)CaDiCaL version: 2.1.3
% 20.71/3.84 % (1751803)Termination reason: Instruction limit
% 20.71/3.84 % (1751803)Termination phase: Saturation
% 20.71/3.84 % (1751803)Time elapsed: 0.099 s
% 20.71/3.84 % (1751803)Peak memory usage: 91 MB
% 20.71/3.84 % (1751803)Instructions burned: 158 (million)
% 20.71/3.84 % (1751800)------------------------------
% 20.71/3.84 % (1751800)------------------------------
% 20.71/3.84 % (1751808)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1818949568:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 20.71/3.84 % (1751809)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3052609564:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 33.87/5.70 % (1751809)Instruction limit reached!
% 33.87/5.70 % (1751809)------------------------------
% 33.87/5.70 % (1751809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.70 % (1751809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.70 % (1751809)CaDiCaL version: 2.1.3
% 33.87/5.70 % (1751809)Termination reason: Instruction limit
% 33.87/5.70 % (1751809)Termination phase: Saturation
% 33.87/5.70 % (1751809)Time elapsed: 0.058 s
% 33.87/5.70 % (1751809)Peak memory usage: 89 MB
% 33.87/5.70 % (1751809)Instructions burned: 108 (million)
% 33.87/5.70 % (1751810)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3191707785:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 33.87/5.70 % (1751810)Instruction limit reached!
% 33.87/5.70 % (1751810)------------------------------
% 33.87/5.70 % (1751810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.70 % (1751810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.70 % (1751810)CaDiCaL version: 2.1.3
% 33.87/5.70 % (1751810)Termination reason: Instruction limit
% 33.87/5.70 % (1751810)Termination phase: Saturation
% 33.87/5.70 % (1751810)Time elapsed: 0.065 s
% 33.87/5.70 % (1751810)Peak memory usage: 89 MB
% 33.87/5.70 % (1751810)Instructions burned: 108 (million)
% 33.87/5.70 % (1751813)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1062771148:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 33.87/5.70 % (1751814)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2665235816:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 33.87/5.70 % (1751816)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3566143378:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 33.87/5.70 % (1751816)Refutation not found, incomplete strategy
% 33.87/5.70 % (1751816)------------------------------
% 33.87/5.70 % (1751816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.70 % (1751816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.70 % (1751816)CaDiCaL version: 2.1.3
% 33.87/5.70 % (1751816)Termination reason: Refutation not found, incomplete strategy
% 33.87/5.70 % (1751816)Time elapsed: 0.003 s
% 33.87/5.70 % (1751816)Peak memory usage: 88 MB
% 33.87/5.70 % (1751816)Instructions burned: 3 (million)
% 33.87/5.70 % (1751813)Instruction limit reached!
% 33.87/5.70 % (1751813)------------------------------
% 33.87/5.70 % (1751813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.70 % (1751813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.70 % (1751813)CaDiCaL version: 2.1.3
% 33.87/5.70 % (1751813)Termination reason: Instruction limit
% 33.87/5.70 % (1751813)Termination phase: Saturation
% 33.87/5.70 % (1751813)Time elapsed: 0.162 s
% 33.87/5.70 % (1751813)Peak memory usage: 90 MB
% 33.87/5.70 % (1751813)Instructions burned: 242 (million)
% 33.87/5.70 % (1751820)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2581979217:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 33.87/5.70 % (1751816)------------------------------
% 33.87/5.70 % (1751816)------------------------------
% 33.87/5.70 % (1751822)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1651388184:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 33.87/5.70 % (1751820)Instruction limit reached!
% 33.87/5.70 % (1751820)------------------------------
% 33.87/5.70 % (1751820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.70 % (1751820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.70 % (1751820)CaDiCaL version: 2.1.3
% 33.87/5.70 % (1751820)Termination reason: Instruction limit
% 33.87/5.70 % (1751820)Termination phase: Saturation
% 33.87/5.70 % (1751820)Time elapsed: 0.272 s
% 33.87/5.70 % (1751820)Peak memory usage: 102 MB
% 33.87/5.70 % (1751820)Instructions burned: 502 (million)
% 33.87/5.70 % (1751822)Instruction limit reached!
% 33.87/5.70 % (1751822)------------------------------
% 33.87/5.70 % (1751822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.70 % (1751822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.70 % (1751822)CaDiCaL version: 2.1.3
% 33.87/5.70 % (1751822)Termination reason: Instruction limit
% 53.87/8.59 % (1751822)Termination phase: Saturation
% 53.87/8.59 % (1751822)Time elapsed: 0.123 s
% 53.87/8.59 % (1751822)Peak memory usage: 90 MB
% 53.87/8.59 % (1751822)Instructions burned: 191 (million)
% 53.87/8.59 % (1751824)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1408952964:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 53.87/8.59 % (1751825)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1446626958:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 53.87/8.59 % (1751824)Instruction limit reached!
% 53.87/8.59 % (1751824)------------------------------
% 53.87/8.59 % (1751824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.87/8.59 % (1751824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.87/8.59 % (1751824)CaDiCaL version: 2.1.3
% 53.87/8.59 % (1751824)Termination reason: Instruction limit
% 53.87/8.59 % (1751824)Termination phase: Saturation
% 53.87/8.59 % (1751824)Time elapsed: 0.162 s
% 53.87/8.59 % (1751824)Peak memory usage: 92 MB
% 53.87/8.59 % (1751824)Instructions burned: 265 (million)
% 53.87/8.59 % (1751825)Instruction limit reached!
% 53.87/8.59 % (1751825)------------------------------
% 53.87/8.59 % (1751825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.87/8.59 % (1751825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.87/8.59 % (1751825)CaDiCaL version: 2.1.3
% 53.87/8.59 % (1751825)Termination reason: Instruction limit
% 53.87/8.59 % (1751825)Termination phase: Saturation
% 53.87/8.59 % (1751825)Time elapsed: 0.090 s
% 53.87/8.59 % (1751825)Peak memory usage: 89 MB
% 53.87/8.59 % (1751825)Instructions burned: 156 (million)
% 53.87/8.59 % (1751829)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1202725502:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 53.87/8.59 % (1751828)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=652229824:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 53.87/8.59 % (1751829)Instruction limit reached!
% 53.87/8.59 % (1751829)------------------------------
% 53.87/8.59 % (1751829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.87/8.59 % (1751829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.87/8.59 % (1751829)CaDiCaL version: 2.1.3
% 53.87/8.59 % (1751829)Termination reason: Instruction limit
% 53.87/8.59 % (1751829)Termination phase: Saturation
% 53.87/8.59 % (1751829)Time elapsed: 0.237 s
% 53.87/8.59 % (1751829)Peak memory usage: 88 MB
% 53.87/8.59 % (1751829)Instructions burned: 537 (million)
% 53.87/8.59 % (1751832)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1899094816:i=180:bd=preordered:av=off_2976 on theBenchmark for (2976ds/180Mi)
% 53.87/8.59 % (1751832)Instruction limit reached!
% 53.87/8.59 % (1751832)------------------------------
% 53.87/8.59 % (1751832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.87/8.59 % (1751832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.87/8.59 % (1751832)CaDiCaL version: 2.1.3
% 53.87/8.59 % (1751832)Termination reason: Instruction limit
% 53.87/8.59 % (1751832)Termination phase: Saturation
% 53.87/8.59 % (1751832)Time elapsed: 0.100 s
% 53.87/8.59 % (1751832)Peak memory usage: 90 MB
% 53.87/8.60 % (1751832)Instructions burned: 181 (million)
% 53.87/8.60 % (1751834)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3015094351:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 53.87/8.60 % (1751808)Instruction limit reached!
% 53.87/8.60 % (1751808)------------------------------
% 53.87/8.60 % (1751808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.87/8.60 % (1751808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.87/8.60 % (1751808)CaDiCaL version: 2.1.3
% 53.87/8.60 % (1751808)Termination reason: Instruction limit
% 53.87/8.60 % (1751808)Termination phase: Saturation
% 53.87/8.60 % (1751808)Time elapsed: 1.967 s
% 53.87/8.60 % (1751808)Peak memory usage: 146 MB
% 53.87/8.60 % (1751808)Instructions burned: 3394 (million)
% 53.87/8.60 % (1751836)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=77940309:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 76.19/11.65 % (1751836)Instruction limit reached!
% 76.19/11.65 % (1751836)------------------------------
% 76.19/11.65 % (1751836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.19/11.65 % (1751836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.19/11.65 % (1751836)CaDiCaL version: 2.1.3
% 76.19/11.65 % (1751836)Termination reason: Instruction limit
% 76.19/11.65 % (1751836)Termination phase: Saturation
% 76.19/11.65 % (1751836)Time elapsed: 0.197 s
% 76.19/11.65 % (1751836)Peak memory usage: 90 MB
% 76.19/11.65 % (1751836)Instructions burned: 412 (million)
% 76.19/11.65 % (1751838)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2645262268:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 76.19/11.65 % (1751828)Instruction limit reached!
% 76.19/11.65 % (1751828)------------------------------
% 76.19/11.65 % (1751828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.19/11.65 % (1751828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.19/11.65 % (1751828)CaDiCaL version: 2.1.3
% 76.19/11.65 % (1751828)Termination reason: Instruction limit
% 76.19/11.65 % (1751828)Termination phase: Saturation
% 76.19/11.65 % (1751828)Time elapsed: 1.865 s
% 76.19/11.65 % (1751828)Peak memory usage: 151 MB
% 76.19/11.65 % (1751828)Instructions burned: 3256 (million)
% 76.19/11.65 % (1751840)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=1618975726:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2960 on theBenchmark for (2960ds/303Mi)
% 76.19/11.65 % (1751840)Refutation not found, incomplete strategy
% 76.19/11.65 % (1751840)------------------------------
% 76.19/11.65 % (1751840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.19/11.65 % (1751840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.19/11.65 % (1751840)CaDiCaL version: 2.1.3
% 76.19/11.65 % (1751840)Termination reason: Refutation not found, incomplete strategy
% 76.19/11.65 % (1751840)Time elapsed: 0.002 s
% 76.19/11.65 % (1751840)Peak memory usage: 88 MB
% 76.19/11.65 % (1751840)Instructions burned: 1 (million)
% 76.19/11.65 % (1751814)Instruction limit reached!
% 76.19/11.65 % (1751814)------------------------------
% 76.19/11.65 % (1751814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.19/11.65 % (1751814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.19/11.65 % (1751814)CaDiCaL version: 2.1.3
% 76.19/11.65 % (1751814)Termination reason: Instruction limit
% 76.19/11.65 % (1751814)Termination phase: Saturation
% 76.19/11.65 % (1751814)Time elapsed: 3.098 s
% 76.19/11.65 % (1751814)Peak memory usage: 162 MB
% 76.19/11.65 % (1751814)Instructions burned: 5210 (million)
% 76.19/11.65 % (1751842)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2147530996:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi)
% 76.19/11.65 % (1751842)Refutation not found, incomplete strategy
% 76.19/11.65 % (1751842)------------------------------
% 76.19/11.65 % (1751842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.19/11.65 % (1751842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.19/11.65 % (1751842)CaDiCaL version: 2.1.3
% 76.19/11.65 % (1751842)Termination reason: Refutation not found, incomplete strategy
% 76.19/11.65 % (1751842)Time elapsed: 0.010 s
% 76.19/11.65 % (1751842)Peak memory usage: 89 MB
% 76.19/11.65 % (1751842)Instructions burned: 13 (million)
% 76.19/11.65 % (1751840)------------------------------
% 76.19/11.65 % (1751840)------------------------------
% 76.19/11.65 % (1751844)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1563113793:i=598:bs=on:bd=preordered:av=off:ss=axioms_2956 on theBenchmark for (2956ds/598Mi)
% 76.19/11.65 % (1751842)------------------------------
% 76.19/11.65 % (1751842)------------------------------
% 76.19/11.65 % (1751846)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1010807601:i=2989:sd=3:ss=axioms:sgt=60_2954 on theBenchmark for (2954ds/2989Mi)
% 76.19/11.65 % (1751844)Instruction limit reached!
% 76.19/11.65 % (1751844)------------------------------
% 76.19/11.65 % (1751844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.19/11.65 % (1751844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.67 % (1751844)CaDiCaL version: 2.1.3
% 111.87/16.67 % (1751844)Termination reason: Instruction limit
% 111.87/16.67 % (1751844)Termination phase: Saturation
% 111.87/16.67 % (1751844)Time elapsed: 0.349 s
% 111.87/16.67 % (1751844)Peak memory usage: 93 MB
% 111.87/16.67 % (1751844)Instructions burned: 599 (million)
% 111.87/16.67 % (1751848)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2472217016:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2951 on theBenchmark for (2951ds/1997Mi)
% 111.87/16.67 % (1751848)Instruction limit reached!
% 111.87/16.67 % (1751848)------------------------------
% 111.87/16.67 % (1751848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.67 % (1751848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.67 % (1751848)CaDiCaL version: 2.1.3
% 111.87/16.67 % (1751848)Termination reason: Instruction limit
% 111.87/16.67 % (1751848)Termination phase: Saturation
% 111.87/16.67 % (1751848)Time elapsed: 1.248 s
% 111.87/16.67 % (1751848)Peak memory usage: 138 MB
% 111.87/16.67 % (1751848)Instructions burned: 1999 (million)
% 111.87/16.67 % (1751850)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3930309199:i=2088:bd=preordered:av=off_2937 on theBenchmark for (2937ds/2088Mi)
% 111.87/16.67 % (1751846)Instruction limit reached!
% 111.87/16.67 % (1751846)------------------------------
% 111.87/16.67 % (1751846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.67 % (1751846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.67 % (1751846)CaDiCaL version: 2.1.3
% 111.87/16.67 % (1751846)Termination reason: Instruction limit
% 111.87/16.67 % (1751846)Termination phase: Saturation
% 111.87/16.67 % (1751846)Time elapsed: 1.791 s
% 111.87/16.67 % (1751846)Peak memory usage: 143 MB
% 111.87/16.67 % (1751846)Instructions burned: 2991 (million)
% 111.87/16.67 % (1751852)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1432678337:i=1098:nicw=on_2934 on theBenchmark for (2934ds/1098Mi)
% 111.87/16.67 % (1751838)Instruction limit reached!
% 111.87/16.67 % (1751838)------------------------------
% 111.87/16.67 % (1751838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.67 % (1751838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.67 % (1751838)CaDiCaL version: 2.1.3
% 111.87/16.67 % (1751838)Termination reason: Instruction limit
% 111.87/16.67 % (1751838)Termination phase: Saturation
% 111.87/16.67 % (1751838)Time elapsed: 3.958 s
% 111.87/16.67 % (1751838)Peak memory usage: 187 MB
% 111.87/16.67 % (1751838)Instructions burned: 8478 (million)
% 111.87/16.67 % (1751852)Instruction limit reached!
% 111.87/16.67 % (1751852)------------------------------
% 111.87/16.67 % (1751852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.67 % (1751852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.67 % (1751852)CaDiCaL version: 2.1.3
% 111.87/16.67 % (1751852)Termination reason: Instruction limit
% 111.87/16.67 % (1751852)Termination phase: Saturation
% 111.87/16.67 % (1751852)Time elapsed: 0.634 s
% 111.87/16.67 % (1751852)Peak memory usage: 108 MB
% 111.87/16.67 % (1751852)Instructions burned: 1098 (million)
% 111.87/16.67 % (1751855)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2079909631:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2926 on theBenchmark for (2926ds/2942Mi)
% 111.87/16.67 % (1751854)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1810341749:i=433:bd=preordered_2926 on theBenchmark for (2926ds/433Mi)
% 111.87/16.67 % (1751850)Instruction limit reached!
% 111.87/16.67 % (1751850)------------------------------
% 111.87/16.67 % (1751850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.87/16.67 % (1751850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.87/16.67 % (1751850)CaDiCaL version: 2.1.3
% 111.87/16.67 % (1751850)Termination reason: Instruction limit
% 111.87/16.67 % (1751850)Termination phase: Saturation
% 111.87/16.67 % (1751850)Time elapsed: 1.277 s
% 111.87/16.67 % (1751850)Peak memory usage: 138 MB
% 111.87/16.67 % (1751850)Instructions burned: 2090 (million)
% 111.87/16.67 % (1751854)Instruction limit reached!
% 111.87/16.67 % (1751854)------------------------------
% 111.87/16.67 % (1751854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.34/18.56 % (1751854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.34/18.56 % (1751854)CaDiCaL version: 2.1.3
% 125.34/18.56 % (1751854)Termination reason: Instruction limit
% 125.34/18.56 % (1751854)Termination phase: Saturation
% 125.34/18.56 % (1751854)Time elapsed: 0.270 s
% 125.34/18.56 % (1751854)Peak memory usage: 92 MB
% 125.34/18.56 % (1751854)Instructions burned: 434 (million)
% 125.34/18.56 % (1751858)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3648064233:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2922 on theBenchmark for (2922ds/6922Mi)
% 125.34/18.56 % (1751859)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3948216301:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2922 on theBenchmark for (2922ds/596Mi)
% 125.34/18.56 % (1751834)Instruction limit reached!
% 125.34/18.56 % (1751834)------------------------------
% 125.34/18.56 % (1751834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.34/18.56 % (1751834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.34/18.56 % (1751834)CaDiCaL version: 2.1.3
% 125.34/18.56 % (1751834)Termination reason: Instruction limit
% 125.34/18.56 % (1751834)Termination phase: Saturation
% 125.34/18.56 % (1751834)Time elapsed: 5.387 s
% 125.34/18.56 % (1751834)Peak memory usage: 159 MB
% 125.34/18.56 % (1751834)Instructions burned: 10307 (million)
% 125.34/18.56 % (1751859)Instruction limit reached!
% 125.34/18.56 % (1751859)------------------------------
% 125.34/18.56 % (1751859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.34/18.56 % (1751859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.34/18.56 % (1751859)CaDiCaL version: 2.1.3
% 125.34/18.56 % (1751859)Termination reason: Instruction limit
% 125.34/18.56 % (1751859)Termination phase: Saturation
% 125.34/18.56 % (1751859)Time elapsed: 0.317 s
% 125.34/18.56 % (1751859)Peak memory usage: 98 MB
% 125.34/18.56 % (1751859)Instructions burned: 598 (million)
% 125.34/18.56 % (1751862)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1728107967:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2918 on theBenchmark for (2918ds/4123Mi)
% 125.34/18.56 % (1751863)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3542812564:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2917 on theBenchmark for (2917ds/16411Mi)
% 125.34/18.56 % (1751855)Instruction limit reached!
% 125.34/18.56 % (1751855)------------------------------
% 125.34/18.56 % (1751855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.34/18.56 % (1751855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.34/18.56 % (1751855)CaDiCaL version: 2.1.3
% 125.34/18.56 % (1751855)Termination reason: Instruction limit
% 125.34/18.56 % (1751855)Termination phase: Saturation
% 125.34/18.56 % (1751855)Time elapsed: 1.888 s
% 125.34/18.56 % (1751855)Peak memory usage: 146 MB
% 125.34/18.56 % (1751855)Instructions burned: 2943 (million)
% 125.34/18.56 % (1751866)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1588795211:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2906 on theBenchmark for (2906ds/1670Mi)
% 125.34/18.56 % (1751866)Instruction limit reached!
% 125.34/18.56 % (1751866)------------------------------
% 125.34/18.56 % (1751866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.34/18.56 % (1751866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.34/18.56 % (1751866)CaDiCaL version: 2.1.3
% 125.34/18.56 % (1751866)Termination reason: Instruction limit
% 125.34/18.56 % (1751866)Termination phase: Saturation
% 125.34/18.56 % (1751866)Time elapsed: 1.043 s
% 125.34/18.56 % (1751866)Peak memory usage: 137 MB
% 125.34/18.56 % (1751866)Instructions burned: 1671 (million)
% 125.34/18.56 % (1751862)Instruction limit reached!
% 125.34/18.56 % (1751862)------------------------------
% 125.34/18.56 % (1751862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.34/18.56 % (1751862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.34/18.56 % (1751862)CaDiCaL version: 2.1.3
% 125.34/18.56 % (1751862)Termination reason: Instruction limit
% 125.34/18.56 % (1751862)Termination phase: Saturation
% 125.34/18.56 % (1751862)Time elapsed: 2.288 s
% 125.34/18.56 % (1751862)Peak memory usage: 171 MB
% 125.34/18.56 % (1751862)Instructions burned: 4124 (million)
% 125.34/18.56 % (1751869)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1007036255:cts=off:cond=on:i=9530:bs=on:fsd=on_2894 on theBenchmark for (2894ds/9530Mi)
% 142.32/21.02 % (1751868)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2084891262:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2894 on theBenchmark for (2894ds/1722Mi)
% 142.32/21.02 % (1751868)Refutation not found, incomplete strategy
% 142.32/21.02 % (1751868)------------------------------
% 142.32/21.02 % (1751868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.32/21.02 % (1751868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.32/21.02 % (1751868)CaDiCaL version: 2.1.3
% 142.32/21.02 % (1751868)Termination reason: Refutation not found, incomplete strategy
% 142.32/21.02 % (1751868)Time elapsed: 0.606 s
% 142.32/21.02 % (1751868)Peak memory usage: 127 MB
% 142.32/21.02 % (1751868)Instructions burned: 920 (million)
% 142.32/21.02 % (1751858)Instruction limit reached!
% 142.32/21.02 % (1751858)------------------------------
% 142.32/21.02 % (1751858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.32/21.02 % (1751858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.32/21.02 % (1751858)CaDiCaL version: 2.1.3
% 142.32/21.02 % (1751858)Termination reason: Instruction limit
% 142.32/21.02 % (1751858)Termination phase: Saturation
% 142.32/21.02 % (1751858)Time elapsed: 3.716 s
% 142.32/21.02 % (1751858)Peak memory usage: 189 MB
% 142.32/21.02 % (1751858)Instructions burned: 6924 (million)
% 142.32/21.02 % (1751868)------------------------------
% 142.32/21.02 % (1751868)------------------------------
% 142.32/21.02 % (1751872)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4083603158:st=2:i=4495:sd=10:ss=included_2884 on theBenchmark for (2884ds/4495Mi)
% 142.32/21.02 % (1751873)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3707512691:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2883 on theBenchmark for (2883ds/4920Mi)
% 142.32/21.02 % (1751872)Instruction limit reached!
% 142.32/21.02 % (1751872)------------------------------
% 142.32/21.02 % (1751872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.32/21.02 % (1751872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.32/21.02 % (1751872)CaDiCaL version: 2.1.3
% 142.32/21.02 % (1751872)Termination reason: Instruction limit
% 142.32/21.02 % (1751872)Termination phase: Saturation
% 142.32/21.02 % (1751872)Time elapsed: 2.738 s
% 142.32/21.02 % (1751872)Peak memory usage: 158 MB
% 142.32/21.02 % (1751872)Instructions burned: 4496 (million)
% 142.32/21.02 % (1751876)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=511937149:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2854 on theBenchmark for (2854ds/2083Mi)
% 142.32/21.02 % (1751873)Instruction limit reached!
% 142.32/21.02 % (1751873)------------------------------
% 142.32/21.02 % (1751873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.32/21.02 % (1751873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.32/21.02 % (1751873)CaDiCaL version: 2.1.3
% 142.32/21.02 % (1751873)Termination reason: Instruction limit
% 142.32/21.02 % (1751873)Termination phase: Saturation
% 142.32/21.02 % (1751873)Time elapsed: 2.941 s
% 142.32/21.02 % (1751873)Peak memory usage: 154 MB
% 142.32/21.02 % (1751873)Instructions burned: 4921 (million)
% 142.32/21.02 % (1751878)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=289244970:i=4629:av=off:gsp=on_2852 on theBenchmark for (2852ds/4629Mi)
% 142.32/21.02 % (1751869)Instruction limit reached!
% 142.32/21.02 % (1751869)------------------------------
% 142.32/21.02 % (1751869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.32/21.02 % (1751869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.32/21.02 % (1751869)CaDiCaL version: 2.1.3
% 142.32/21.02 % (1751869)Termination reason: Instruction limit
% 142.32/21.02 % (1751869)Termination phase: Saturation
% 142.32/21.02 % (1751869)Time elapsed: 5.020 s
% 142.32/21.02 % (1751869)Peak memory usage: 155 MB
% 142.32/21.02 % (1751869)Instructions burned: 9531 (million)
% 169.96/24.90 % (1751876)Instruction limit reached!
% 169.96/24.90 % (1751876)------------------------------
% 169.96/24.90 % (1751876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.96/24.90 % (1751876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.90 % (1751876)CaDiCaL version: 2.1.3
% 169.96/24.90 % (1751876)Termination reason: Instruction limit
% 169.96/24.90 % (1751876)Termination phase: Saturation
% 169.96/24.90 % (1751876)Time elapsed: 1.280 s
% 169.96/24.90 % (1751876)Peak memory usage: 138 MB
% 169.96/24.90 % (1751876)Instructions burned: 2084 (million)
% 169.96/24.90 % (1751880)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2931016757:i=1258:av=off_2841 on theBenchmark for (2841ds/1258Mi)
% 169.96/24.90 % (1751881)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=298535384:i=7343:av=off:ss=included_2840 on theBenchmark for (2840ds/7343Mi)
% 169.96/24.90 % (1751880)Instruction limit reached!
% 169.96/24.90 % (1751880)------------------------------
% 169.96/24.90 % (1751880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.96/24.90 % (1751880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.90 % (1751880)CaDiCaL version: 2.1.3
% 169.96/24.90 % (1751880)Termination reason: Instruction limit
% 169.96/24.90 % (1751880)Termination phase: Saturation
% 169.96/24.90 % (1751880)Time elapsed: 0.724 s
% 169.96/24.90 % (1751880)Peak memory usage: 100 MB
% 169.96/24.90 % (1751880)Instructions burned: 1258 (million)
% 169.96/24.90 % (1751881)Refutation not found, incomplete strategy
% 169.96/24.90 % (1751881)------------------------------
% 169.96/24.90 % (1751881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.96/24.90 % (1751881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.90 % (1751881)CaDiCaL version: 2.1.3
% 169.96/24.90 % (1751881)Termination reason: Refutation not found, incomplete strategy
% 169.96/24.90 % (1751881)Time elapsed: 0.605 s
% 169.96/24.90 % (1751881)Peak memory usage: 128 MB
% 169.96/24.90 % (1751881)Instructions burned: 917 (million)
% 169.96/24.90 % (1751884)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1508745266:i=1325:sd=2:ss=axioms:sgt=16_2832 on theBenchmark for (2832ds/1325Mi)
% 169.96/24.90 % (1751884)Refutation not found, incomplete strategy
% 169.96/24.90 % (1751884)------------------------------
% 169.96/24.90 % (1751884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.96/24.90 % (1751884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.90 % (1751884)CaDiCaL version: 2.1.3
% 169.96/24.90 % (1751884)Termination reason: Refutation not found, incomplete strategy
% 169.96/24.90 % (1751884)Time elapsed: 0.002 s
% 169.96/24.90 % (1751884)Peak memory usage: 88 MB
% 169.96/24.90 % (1751884)Instructions burned: 1 (million)
% 169.96/24.90 % (1751881)------------------------------
% 169.96/24.90 % (1751881)------------------------------
% 169.96/24.90 % (1751884)------------------------------
% 169.96/24.90 % (1751884)------------------------------
% 169.96/24.90 % (1751886)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=1913594328:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2830 on theBenchmark for (2830ds/2646Mi)
% 169.96/24.90 % (1751887)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4032283666:i=1489:sd=2:ep=R:ss=axioms_2828 on theBenchmark for (2828ds/1489Mi)
% 169.96/24.90 % (1751878)Instruction limit reached!
% 169.96/24.90 % (1751878)------------------------------
% 169.96/24.90 % (1751878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.96/24.90 % (1751878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.90 % (1751878)CaDiCaL version: 2.1.3
% 169.96/24.90 % (1751878)Termination reason: Instruction limit
% 169.96/24.90 % (1751878)Termination phase: Saturation
% 169.96/24.90 % (1751878)Time elapsed: 2.719 s
% 169.96/24.90 % (1751878)Peak memory usage: 165 MB
% 169.96/24.90 % (1751878)Instructions burned: 4629 (million)
% 169.96/24.90 % (1751863)Instruction limit reached!
% 169.96/24.90 % (1751863)------------------------------
% 169.96/24.90 % (1751863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.96/24.90 % (1751863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.96/24.90 % (1751863)CaDiCaL version: 2.1.3
% 169.96/24.90 % (1751863)Termination reason: Instruction limit
% 169.96/24.90 % (1751863)Termination phase: Saturation
% 190.95/27.88 % (1751863)Time elapsed: 9.331 s
% 190.95/27.88 % (1751863)Peak memory usage: 194 MB
% 190.95/27.88 % (1751863)Instructions burned: 16412 (million)
% 190.95/27.88 % (1751890)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3162283721:i=1503_2823 on theBenchmark for (2823ds/1503Mi)
% 190.95/27.88 % (1751891)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1640663016:i=13942:kws=frequency_2822 on theBenchmark for (2822ds/13942Mi)
% 190.95/27.88 % (1751887)Refutation not found, incomplete strategy
% 190.95/27.88 % (1751887)------------------------------
% 190.95/27.88 % (1751887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.95/27.88 % (1751887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.95/27.88 % (1751887)CaDiCaL version: 2.1.3
% 190.95/27.88 % (1751887)Termination reason: Refutation not found, incomplete strategy
% 190.95/27.88 % (1751887)Time elapsed: 0.615 s
% 190.95/27.88 % (1751887)Peak memory usage: 128 MB
% 190.95/27.88 % (1751887)Instructions burned: 925 (million)
% 190.95/27.88 % (1751887)------------------------------
% 190.95/27.88 % (1751887)------------------------------
% 190.95/27.88 % (1751894)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=335154564:i=3604:fsr=off:er=filter_2818 on theBenchmark for (2818ds/3604Mi)
% 190.95/27.88 % (1751890)Instruction limit reached!
% 190.95/27.88 % (1751890)------------------------------
% 190.95/27.88 % (1751890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.95/27.88 % (1751890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.95/27.88 % (1751890)CaDiCaL version: 2.1.3
% 190.95/27.88 % (1751890)Termination reason: Instruction limit
% 190.95/27.88 % (1751890)Termination phase: Saturation
% 190.95/27.88 % (1751890)Time elapsed: 0.938 s
% 190.95/27.88 % (1751890)Peak memory usage: 135 MB
% 190.95/27.88 % (1751890)Instructions burned: 1503 (million)
% 190.95/27.88 % (1751896)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1990609717:i=1876:sd=1:ss=included:sgt=32_2812 on theBenchmark for (2812ds/1876Mi)
% 190.95/27.88 % (1751886)Instruction limit reached!
% 190.95/27.88 % (1751886)------------------------------
% 190.95/27.88 % (1751886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.95/27.88 % (1751886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.95/27.88 % (1751886)CaDiCaL version: 2.1.3
% 190.95/27.88 % (1751886)Termination reason: Instruction limit
% 190.95/27.88 % (1751886)Termination phase: Saturation
% 190.95/27.88 % (1751886)Time elapsed: 1.822 s
% 190.95/27.88 % (1751886)Peak memory usage: 140 MB
% 190.95/27.88 % (1751886)Instructions burned: 2647 (million)
% 190.95/27.88 % (1751898)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=4228273378:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2810 on theBenchmark for (2810ds/1932Mi)
% 190.95/27.88 % (1751898)Refutation not found, incomplete strategy
% 190.95/27.88 % (1751898)------------------------------
% 190.95/27.88 % (1751898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.95/27.88 % (1751898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.95/27.88 % (1751898)CaDiCaL version: 2.1.3
% 190.95/27.88 % (1751898)Termination reason: Refutation not found, incomplete strategy
% 190.95/27.88 % (1751898)Time elapsed: 0.592 s
% 190.95/27.88 % (1751898)Peak memory usage: 128 MB
% 190.95/27.88 % (1751898)Instructions burned: 897 (million)
% 190.95/27.88 % (1751898)------------------------------
% 190.95/27.88 % (1751898)------------------------------
% 190.95/27.88 % (1751896)Instruction limit reached!
% 190.95/27.88 % (1751896)------------------------------
% 190.95/27.88 % (1751896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.95/27.88 % (1751896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.95/27.88 % (1751896)CaDiCaL version: 2.1.3
% 190.95/27.88 % (1751896)Termination reason: Instruction limit
% 190.95/27.88 % (1751896)Termination phase: Saturation
% 190.95/27.88 % (1751896)Time elapsed: 1.137 s
% 190.95/27.88 % (1751896)Peak memory usage: 138 MB
% 190.95/27.88 % (1751896)Instructions burned: 1877 (million)
% 190.95/27.88 % (1751900)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=1768120912:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2800 on theBenchmark for (2800ds/1980Mi)
% 224.62/32.53 % (1751901)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=1748476112:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2799 on theBenchmark for (2799ds/3902Mi)
% 224.62/32.53 % (1751894)Instruction limit reached!
% 224.62/32.53 % (1751894)------------------------------
% 224.62/32.53 % (1751894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.62/32.53 % (1751894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.62/32.53 % (1751894)CaDiCaL version: 2.1.3
% 224.62/32.53 % (1751894)Termination reason: Instruction limit
% 224.62/32.53 % (1751894)Termination phase: Saturation
% 224.62/32.53 % (1751894)Time elapsed: 2.047 s
% 224.62/32.53 % (1751894)Peak memory usage: 159 MB
% 224.62/32.53 % (1751894)Instructions burned: 3605 (million)
% 224.62/32.53 % (1751904)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2073447220:avsq=on:i=3916:aac=none:amm=off_2796 on theBenchmark for (2796ds/3916Mi)
% 224.62/32.53 % (1751900)Instruction limit reached!
% 224.62/32.53 % (1751900)------------------------------
% 224.62/32.53 % (1751900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.62/32.53 % (1751900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.62/32.53 % (1751900)CaDiCaL version: 2.1.3
% 224.62/32.53 % (1751900)Termination reason: Instruction limit
% 224.62/32.53 % (1751900)Termination phase: Saturation
% 224.62/32.53 % (1751900)Time elapsed: 1.240 s
% 224.62/32.53 % (1751900)Peak memory usage: 137 MB
% 224.62/32.53 % (1751900)Instructions burned: 1981 (million)
% 224.62/32.53 % (1751906)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3294960501:cond=on:i=3940:av=off:er=known_2785 on theBenchmark for (2785ds/3940Mi)
% 224.62/32.53 % (1751901)Instruction limit reached!
% 224.62/32.53 % (1751901)------------------------------
% 224.62/32.53 % (1751901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.62/32.53 % (1751901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.62/32.53 % (1751901)CaDiCaL version: 2.1.3
% 224.62/32.53 % (1751901)Termination reason: Instruction limit
% 224.62/32.53 % (1751901)Termination phase: Saturation
% 224.62/32.53 % (1751901)Time elapsed: 2.231 s
% 224.62/32.53 % (1751901)Peak memory usage: 158 MB
% 224.62/32.53 % (1751901)Instructions burned: 3903 (million)
% 224.62/32.53 % (1751904)Instruction limit reached!
% 224.62/32.53 % (1751904)------------------------------
% 224.62/32.53 % (1751904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.62/32.53 % (1751904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.62/32.53 % (1751904)CaDiCaL version: 2.1.3
% 224.62/32.53 % (1751904)Termination reason: Instruction limit
% 224.62/32.53 % (1751904)Termination phase: Saturation
% 224.62/32.53 % (1751904)Time elapsed: 2.039 s
% 224.62/32.53 % (1751904)Peak memory usage: 111 MB
% 224.62/32.53 % (1751904)Instructions burned: 3917 (million)
% 224.62/32.53 % (1751908)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=828606776:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2775 on theBenchmark for (2775ds/3980Mi)
% 224.62/32.53 % (1751909)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2946687710:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2774 on theBenchmark for (2774ds/2087Mi)
% 224.62/32.53 % (1751906)Instruction limit reached!
% 224.62/32.53 % (1751906)------------------------------
% 224.62/32.53 % (1751906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 224.62/32.53 % (1751906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 224.62/32.53 % (1751906)CaDiCaL version: 2.1.3
% 224.62/32.53 % (1751906)Termination reason: Instruction limit
% 224.62/32.53 % (1751906)Termination phase: Saturation
% 224.62/32.53 % (1751906)Time elapsed: 2.310 s
% 224.62/32.53 % (1751906)Peak memory usage: 150 MB
% 224.62/32.53 % (1751906)Instructions burned: 3941 (million)
% 224.62/32.53 % (1751912)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=834310697:cts=off:cond=on:i=4272:bs=on:fsd=on_2761 on theBenchmark for (2761ds/4272Mi)
% 190.03/38.40 % (1751909)Instruction limit reached!
% 190.03/38.40 % (1751909)------------------------------
% 190.03/38.40 % (1751909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751909)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751909)Termination reason: Instruction limit
% 190.03/38.40 % (1751909)Termination phase: Saturation
% 190.03/38.40 % (1751909)Time elapsed: 1.323 s
% 190.03/38.40 % (1751909)Peak memory usage: 140 MB
% 190.03/38.40 % (1751909)Instructions burned: 2088 (million)
% 190.03/38.40 % (1751914)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2118596627:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2759 on theBenchmark for (2759ds/2197Mi)
% 190.03/38.40 % (1751908)Instruction limit reached!
% 190.03/38.40 % (1751908)------------------------------
% 190.03/38.40 % (1751908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751908)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751908)Termination reason: Instruction limit
% 190.03/38.40 % (1751908)Termination phase: Saturation
% 190.03/38.40 % (1751908)Time elapsed: 2.419 s
% 190.03/38.40 % (1751908)Peak memory usage: 157 MB
% 190.03/38.40 % (1751908)Instructions burned: 3980 (million)
% 190.03/38.40 % (1751916)dis+21_1_sil=8000:spb=goal_then_units:random_seed=3676752214:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2749 on theBenchmark for (2749ds/6508Mi)
% 190.03/38.40 % (1751914)Instruction limit reached!
% 190.03/38.40 % (1751914)------------------------------
% 190.03/38.40 % (1751914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751914)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751914)Termination reason: Instruction limit
% 190.03/38.40 % (1751914)Termination phase: Saturation
% 190.03/38.40 % (1751914)Time elapsed: 1.219 s
% 190.03/38.40 % (1751914)Peak memory usage: 145 MB
% 190.03/38.40 % (1751914)Instructions burned: 2198 (million)
% 190.03/38.40 % (1751918)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3189295770:i=2330:fgj=on:av=off:fsr=off_2745 on theBenchmark for (2745ds/2330Mi)
% 190.03/38.40 % (1751891)Instruction limit reached!
% 190.03/38.40 % (1751891)------------------------------
% 190.03/38.40 % (1751891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751891)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751891)Termination reason: Instruction limit
% 190.03/38.40 % (1751891)Termination phase: Saturation
% 190.03/38.40 % (1751891)Time elapsed: 7.965 s
% 190.03/38.40 % (1751891)Peak memory usage: 218 MB
% 190.03/38.40 % (1751891)Instructions burned: 13942 (million)
% 190.03/38.40 % (1751920)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1856254017:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2741 on theBenchmark for (2741ds/7592Mi)
% 190.03/38.40 % (1751912)Instruction limit reached!
% 190.03/38.40 % (1751912)------------------------------
% 190.03/38.40 % (1751912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751912)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751912)Termination reason: Instruction limit
% 190.03/38.40 % (1751912)Termination phase: Saturation
% 190.03/38.40 % (1751912)Time elapsed: 2.551 s
% 190.03/38.40 % (1751912)Peak memory usage: 148 MB
% 190.03/38.40 % (1751912)Instructions burned: 4273 (million)
% 190.03/38.40 % (1751922)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=1122885299:i=2693:kws=precedence:ins=1:av=off_2733 on theBenchmark for (2733ds/2693Mi)
% 190.03/38.40 % (1751918)Instruction limit reached!
% 190.03/38.40 % (1751918)------------------------------
% 190.03/38.40 % (1751918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751918)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751918)Termination reason: Instruction limit
% 190.03/38.40 % (1751918)Termination phase: Saturation
% 190.03/38.40 % (1751918)Time elapsed: 1.419 s
% 190.03/38.40 % (1751918)Peak memory usage: 140 MB
% 190.03/38.40 % (1751918)Instructions burned: 2331 (million)
% 190.03/38.40 % (1751924)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=2901742736:i=28651:sd=4:ss=included:sgt=64_2729 on theBenchmark for (2729ds/28651Mi)
% 190.03/38.40 % (1751922)Instruction limit reached!
% 190.03/38.40 % (1751922)------------------------------
% 190.03/38.40 % (1751922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751922)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751922)Termination reason: Instruction limit
% 190.03/38.40 % (1751922)Termination phase: Saturation
% 190.03/38.40 % (1751922)Time elapsed: 1.703 s
% 190.03/38.40 % (1751922)Peak memory usage: 143 MB
% 190.03/38.40 % (1751922)Instructions burned: 2693 (million)
% 190.03/38.40 % (1751926)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2633989703:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2715 on theBenchmark for (2715ds/2700Mi)
% 190.03/38.40 % (1751916)Instruction limit reached!
% 190.03/38.40 % (1751916)------------------------------
% 190.03/38.40 % (1751916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751916)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751916)Termination reason: Instruction limit
% 190.03/38.40 % (1751916)Termination phase: Saturation
% 190.03/38.40 % (1751916)Time elapsed: 3.594 s
% 190.03/38.40 % (1751916)Peak memory usage: 140 MB
% 190.03/38.40 % (1751916)Instructions burned: 6508 (million)
% 190.03/38.40 % (1751928)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3917290849:i=3196:nm=4_2711 on theBenchmark for (2711ds/3196Mi)
% 190.03/38.40 % (1751920)Instruction limit reached!
% 190.03/38.40 % (1751920)------------------------------
% 190.03/38.40 % (1751920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751920)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751920)Termination reason: Instruction limit
% 190.03/38.40 % (1751920)Termination phase: Saturation
% 190.03/38.40 % (1751920)Time elapsed: 3.629 s
% 190.03/38.40 % (1751920)Peak memory usage: 139 MB
% 190.03/38.40 % (1751920)Instructions burned: 7593 (million)
% 190.03/38.40 % (1751930)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1071106369:cts=off:i=3254:av=off_2703 on theBenchmark for (2703ds/3254Mi)
% 190.03/38.40 % (1751926)Instruction limit reached!
% 190.03/38.40 % (1751926)------------------------------
% 190.03/38.40 % (1751926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.40 % (1751926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.40 % (1751926)CaDiCaL version: 2.1.3
% 190.03/38.40 % (1751926)Termination reason: Instruction limit
% 190.03/38.40 % (1751926)Termination phase: Saturation
% 190.03/38.40 % (1751926)Time elapsed: 1.641 s
% 190.03/38.40 % (1751926)Peak memory usage: 141 MB
% 190.03/38.40 % (1751926)Instructions burned: 2702 (million)
% 190.03/38.40 % (1751932)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=3276154663:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2697 on theBenchmark for (2697ds/3264Mi)
% 190.03/38.41 % (1751928)Instruction limit reached!
% 190.03/38.41 % (1751928)------------------------------
% 190.03/38.41 % (1751928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.41 % (1751928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.41 % (1751928)CaDiCaL version: 2.1.3
% 190.03/38.41 % (1751928)Termination reason: Instruction limit
% 190.03/38.41 % (1751928)Termination phase: Saturation
% 190.03/38.41 % (1751928)Time elapsed: 1.969 s
% 190.03/38.41 % (1751928)Peak memory usage: 152 MB
% 190.03/38.41 % (1751928)Instructions burned: 3196 (million)
% 190.03/38.41 % (1751934)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=110021081:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2689 on theBenchmark for (2689ds/9708Mi)
% 190.03/38.41 % (1751930)Instruction limit reached!
% 190.03/38.41 % (1751930)------------------------------
% 190.03/38.41 % (1751930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.41 % (1751930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.41 % (1751930)CaDiCaL version: 2.1.3
% 190.03/38.41 % (1751930)Termination reason: Instruction limit
% 190.03/38.41 % (1751930)Termination phase: Saturation
% 190.03/38.41 % (1751930)Time elapsed: 1.872 s
% 190.03/38.41 % (1751930)Peak memory usage: 141 MB
% 190.03/38.41 % (1751930)Instructions burned: 3255 (million)
% 190.03/38.41 % (1751936)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2776406447:i=21997:s2at=5:gtg=all_2683 on theBenchmark for (2683ds/21997Mi)
% 190.03/38.41 % (1751932)Instruction limit reached!
% 190.03/38.41 % (1751932)------------------------------
% 190.03/38.41 % (1751932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.41 % (1751932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.41 % (1751932)CaDiCaL version: 2.1.3
% 190.03/38.41 % (1751932)Termination reason: Instruction limit
% 190.03/38.41 % (1751932)Termination phase: Saturation
% 190.03/38.41 % (1751932)Time elapsed: 2.361 s
% 190.03/38.41 % (1751932)Peak memory usage: 143 MB
% 190.03/38.41 % (1751932)Instructions burned: 3264 (million)
% 190.03/38.41 % (1751938)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=597415644:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2671 on theBenchmark for (2671ds/7551Mi)
% 190.03/38.41 % (1751934)Instruction limit reached!
% 190.03/38.41 % (1751934)------------------------------
% 190.03/38.41 % (1751934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.41 % (1751934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.41 % (1751934)CaDiCaL version: 2.1.3
% 190.03/38.41 % (1751934)Termination reason: Instruction limit
% 190.03/38.41 % (1751934)Termination phase: Saturation
% 190.03/38.41 % (1751934)Time elapsed: 5.278 s
% 190.03/38.41 % (1751934)Peak memory usage: 217 MB
% 190.03/38.41 % (1751934)Instructions burned: 9708 (million)
% 190.03/38.41 % (1751941)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3841795676:i=8924:sd=1:ss=included_2635 on theBenchmark for (2635ds/8924Mi)
% 190.03/38.41 % (1751936)First to succeed.
% 190.03/38.41 % (1751936)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1751777"
% 190.03/38.41 % (1751941)Refutation not found, incomplete strategy
% 190.03/38.41 % (1751941)------------------------------
% 190.03/38.41 % (1751941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.41 % (1751941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.41 % (1751941)CaDiCaL version: 2.1.3
% 190.03/38.41 % (1751941)Termination reason: Refutation not found, incomplete strategy
% 190.03/38.41 % (1751941)Time elapsed: 0.580 s
% 190.03/38.41 % (1751941)Peak memory usage: 128 MB
% 190.03/38.41 % (1751941)Instructions burned: 864 (million)
% 190.03/38.41 % (1751938)Instruction limit reached!
% 190.03/38.41 % (1751938)------------------------------
% 190.03/38.41 % (1751938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 190.03/38.41 % (1751938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.03/38.41 % (1751938)CaDiCaL version: 2.1.3
% 190.03/38.41 % (1751938)Termination reason: Instruction limit
% 190.03/38.41 % (1751938)Termination phase: Saturation
% 190.03/38.41 % (1751938)Time elapsed: 4.277 s
% 190.03/38.41 % (1751938)Peak memory usage: 153 MB
% 190.03/38.41 % (1751938)Instructions burned: 7551 (million)
% 190.03/38.41 % (1751936)Refutation found. Thanks to Tanya!
% 190.03/38.41 % SZS status Unsatisfiable for theBenchmark
% 190.03/38.41 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/38.61 % (1751936)------------------------------
% 0.15/38.61 % (1751936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.15/38.61 % (1751936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.15/38.61 % (1751936)CaDiCaL version: 2.1.3
% 0.15/38.61 % (1751936)Termination reason: Refutation
% 0.15/38.61 % (1751936)Time elapsed: 5.285 s
% 0.15/38.61 % (1751936)Peak memory usage: 185 MB
% 0.15/38.61 % (1751936)Instructions burned: 8740 (million)
% 0.15/38.61 % (1751936)------------------------------
% 0.15/38.61 % (1751936)------------------------------
% 0.15/38.61 % (1751777)Success in time 37.549 s
% 0.15/38.61 % Vampire exiting
%------------------------------------------------------------------------------