%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET023-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:38 PM UTC 2026
% Result : Unsatisfiable 100.90s 26.42s
% Output : Refutation 181.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 51
% Syntax : Number of formulae : 445 ( 45 unt; 29 def)
% Number of atoms : 1656 ( 303 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1977 ( 766 ~;1182 |; 0 &)
% ( 29 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 34 ( 32 usr; 30 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 2 con; 0-2 aty)
% Number of variables : 111 ( 0 sgn 111 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ member(X0,X1)
| little_set(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
! [X0,X1] :
( member(f1(X0,X1),X1)
| member(f1(X0,X1),X0)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',extensionality2) ).
fof(f4,axiom,
! [X0,X1] :
( ~ member(f1(X0,X1),X1)
| ~ member(f1(X0,X1),X0)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',extensionality3) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ member(X0,non_ordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',non_ordered_pair1) ).
fof(f6,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',non_ordered_pair2) ).
fof(f7,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',non_ordered_pair3) ).
fof(f8,axiom,
! [X0,X1] : little_set(non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',non_ordered_pair4) ).
fof(f9,axiom,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',ordered_pair) ).
fof(f11,axiom,
! [X0] :
( little_set(f2(X0))
| ~ ordered_pair_predicate(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_predicate1) ).
fof(f12,axiom,
! [X0] :
( little_set(f3(X0))
| ~ ordered_pair_predicate(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_predicate2) ).
fof(f13,axiom,
! [X0] :
( ~ ordered_pair_predicate(X0)
| X0 = ordered_pair(f2(X0),f3(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_predicate3) ).
fof(f14,plain,
! [X0] :
( ~ ordered_pair_predicate(X0)
| ordered_pair(f2(X0),f3(X0)) = X0 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| X0 != ordered_pair(X1,X2) ),
file('/export/starexec/sandbox/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(f24,axiom,
! [X0,X1] :
( ~ member(X0,second(X1))
| little_set(f6(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',second1) ).
fof(f25,axiom,
! [X0,X1] :
( ~ member(X0,second(X1))
| little_set(f7(X0,X1)) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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(f70,axiom,
! [X0] : ~ member(X0,empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',empty_set) ).
fof(f110,axiom,
! [X0] :
( X0 = empty_set
| member(f24(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity1) ).
fof(f111,plain,
! [X0] :
( member(f24(X0),X0)
| empty_set = X0 ),
inference(reorient_equations,[],[f110]) ).
fof(f162,axiom,
ordered_pair_predicate(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_ordered_pair_predicate) ).
fof(f163,negated_conjecture,
~ little_set(second(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_second_component_is_small) ).
fof(f164,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(f168,plain,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)) != X0 ),
inference(definition_unfolding,[],[f16,f164]) ).
fof(f169,plain,
! [X0] :
( ~ ordered_pair_predicate(X0)
| non_ordered_pair(non_ordered_pair(f2(X0),f2(X0)),non_ordered_pair(f2(X0),f3(X0))) = X0 ),
inference(definition_unfolding,[],[f14,f164]) ).
fof(f175,plain,
! [X2,X3,X0,X1] :
( member(X0,second(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3)) != X1
| ~ member(X0,X3) ),
inference(definition_unfolding,[],[f30,f164]) ).
fof(f178,plain,
! [X0,X1] :
( ~ member(X0,second(X1))
| non_ordered_pair(non_ordered_pair(f6(X0,X1),f6(X0,X1)),non_ordered_pair(f6(X0,X1),f7(X0,X1))) = X1 ),
inference(definition_unfolding,[],[f27,f164]) ).
fof(f196,plain,
! [X2,X1] :
( ordered_pair_predicate(non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)))
| ~ little_set(X1)
| ~ little_set(X2) ),
inference(equality_resolution,[],[f168]) ).
fof(f200,plain,
! [X2,X3,X0] :
( member(X0,second(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3))))
| ~ little_set(X2)
| ~ little_set(X3)
| ~ member(X0,X3) ),
inference(equality_resolution,[],[f175]) ).
fof(f202,plain,
! [X2,X1] :
( member(X2,non_ordered_pair(X1,X2))
| ~ little_set(X2) ),
inference(equality_resolution,[],[f7]) ).
fof(f203,plain,
! [X2,X1] :
( member(X1,non_ordered_pair(X1,X2))
| ~ little_set(X1) ),
inference(equality_resolution,[],[f6]) ).
fof(f209,plain,
a = non_ordered_pair(non_ordered_pair(f2(a),f2(a)),non_ordered_pair(f2(a),f3(a))),
inference(resolution,[],[f169,f162]) ).
fof(f224,plain,
( member(non_ordered_pair(f2(a),f2(a)),a)
| ~ little_set(non_ordered_pair(f2(a),f2(a))) ),
inference(superposition,[],[f203,f209]) ).
fof(f225,plain,
member(non_ordered_pair(f2(a),f2(a)),a),
inference(forward_subsumption_resolution,[],[f224,f8]) ).
fof(f228,plain,
( member(non_ordered_pair(f2(a),f3(a)),a)
| ~ little_set(non_ordered_pair(f2(a),f3(a))) ),
inference(superposition,[],[f202,f209]) ).
fof(f229,plain,
member(non_ordered_pair(f2(a),f3(a)),a),
inference(forward_subsumption_resolution,[],[f228,f8]) ).
fof(f241,plain,
! [X0] :
( little_set(f6(f24(second(X0)),X0))
| second(X0) = empty_set ),
inference(resolution,[],[f111,f24]) ).
fof(f242,plain,
! [X0] :
( little_set(f7(f24(second(X0)),X0))
| second(X0) = empty_set ),
inference(resolution,[],[f111,f25]) ).
fof(f243,plain,
! [X0] :
( non_ordered_pair(non_ordered_pair(f6(f24(second(X0)),X0),f6(f24(second(X0)),X0)),non_ordered_pair(f6(f24(second(X0)),X0),f7(f24(second(X0)),X0))) = X0
| second(X0) = empty_set ),
inference(resolution,[],[f111,f178]) ).
fof(f245,plain,
! [X0] :
( ordered_pair_predicate(X0)
| ~ little_set(f6(f24(second(X0)),X0))
| ~ little_set(f7(f24(second(X0)),X0))
| second(X0) = empty_set ),
inference(superposition,[],[f196,f243]) ).
fof(f246,plain,
! [X0] :
( member(non_ordered_pair(f6(f24(second(X0)),X0),f7(f24(second(X0)),X0)),X0)
| ~ little_set(non_ordered_pair(f6(f24(second(X0)),X0),f7(f24(second(X0)),X0)))
| second(X0) = empty_set ),
inference(superposition,[],[f202,f243]) ).
fof(f247,plain,
! [X0] :
( member(non_ordered_pair(f6(f24(second(X0)),X0),f6(f24(second(X0)),X0)),X0)
| ~ little_set(non_ordered_pair(f6(f24(second(X0)),X0),f6(f24(second(X0)),X0)))
| second(X0) = empty_set ),
inference(superposition,[],[f203,f243]) ).
fof(f251,plain,
! [X0] :
( member(non_ordered_pair(f6(f24(second(X0)),X0),f6(f24(second(X0)),X0)),X0)
| second(X0) = empty_set ),
inference(forward_subsumption_resolution,[],[f247,f8]) ).
fof(f252,plain,
! [X0] :
( member(non_ordered_pair(f6(f24(second(X0)),X0),f7(f24(second(X0)),X0)),X0)
| second(X0) = empty_set ),
inference(forward_subsumption_resolution,[],[f246,f8]) ).
fof(f253,plain,
! [X0] :
( ordered_pair_predicate(X0)
| ~ little_set(f7(f24(second(X0)),X0))
| second(X0) = empty_set ),
inference(forward_subsumption_resolution,[],[f245,f241]) ).
fof(f255,plain,
! [X0] :
( ordered_pair_predicate(X0)
| second(X0) = empty_set ),
inference(forward_subsumption_resolution,[],[f253,f242]) ).
fof(f261,plain,
! [X0] :
( non_ordered_pair(non_ordered_pair(f2(X0),f2(X0)),non_ordered_pair(f2(X0),f3(X0))) = X0
| second(X0) = empty_set ),
inference(resolution,[],[f255,f169]) ).
fof(f263,plain,
! [X0] :
( member(non_ordered_pair(f2(X0),f3(X0)),X0)
| ~ little_set(non_ordered_pair(f2(X0),f3(X0)))
| second(X0) = empty_set ),
inference(superposition,[],[f202,f261]) ).
fof(f264,plain,
! [X0] :
( member(non_ordered_pair(f2(X0),f2(X0)),X0)
| ~ little_set(non_ordered_pair(f2(X0),f2(X0)))
| second(X0) = empty_set ),
inference(superposition,[],[f203,f261]) ).
fof(f268,plain,
! [X0] :
( member(non_ordered_pair(f2(X0),f2(X0)),X0)
| second(X0) = empty_set ),
inference(forward_subsumption_resolution,[],[f264,f8]) ).
fof(f269,plain,
! [X0] :
( member(non_ordered_pair(f2(X0),f3(X0)),X0)
| second(X0) = empty_set ),
inference(forward_subsumption_resolution,[],[f263,f8]) ).
fof(f380,plain,
! [X0,X1] :
( f24(non_ordered_pair(X0,X1)) = X1
| f24(non_ordered_pair(X0,X1)) = X0
| non_ordered_pair(X0,X1) = empty_set ),
inference(resolution,[],[f5,f111]) ).
fof(f381,plain,
! [X0] :
( ~ member(X0,a)
| non_ordered_pair(f2(a),f2(a)) = X0
| non_ordered_pair(f2(a),f3(a)) = X0 ),
inference(superposition,[],[f5,f209]) ).
fof(f384,plain,
! [X0,X1] :
( ~ member(X1,X0)
| non_ordered_pair(f2(X0),f2(X0)) = X1
| non_ordered_pair(f2(X0),f3(X0)) = X1
| second(X0) = empty_set ),
inference(superposition,[],[f5,f261]) ).
fof(f394,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f24(second(a)),a),f6(f24(second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f24(second(a)),a),f6(f24(second(a)),a))
| empty_set = second(a) ),
inference(resolution,[],[f381,f251]) ).
fof(f395,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f24(second(a)),a),f7(f24(second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f24(second(a)),a),f7(f24(second(a)),a))
| empty_set = second(a) ),
inference(resolution,[],[f381,f252]) ).
fof(f396,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| non_ordered_pair(f2(a),f3(a)) = f24(a)
| empty_set = a ),
inference(resolution,[],[f381,f111]) ).
fof(f398,definition,
( spl0_6
<=> empty_set = a ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f399,plain,
( empty_set != a
| spl0_6 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f400,plain,
( empty_set = a
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f402,definition,
( spl0_7
<=> non_ordered_pair(f2(a),f3(a)) = f24(a) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f403,plain,
( non_ordered_pair(f2(a),f3(a)) != f24(a)
| spl0_7 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( non_ordered_pair(f2(a),f3(a)) = f24(a)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f406,definition,
( spl0_8
<=> non_ordered_pair(f2(a),f2(a)) = f24(a) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f407,plain,
( non_ordered_pair(f2(a),f2(a)) != f24(a)
| spl0_8 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f408,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f409,plain,
( spl0_6
| spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f396,f406,f402,f398]) ).
fof(f411,definition,
( spl0_9
<=> empty_set = second(a) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f412,plain,
( empty_set != second(a)
| spl0_9 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f413,plain,
( empty_set = second(a)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f415,definition,
( spl0_10
<=> non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f24(second(a)),a),f7(f24(second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f417,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f24(second(a)),a),f7(f24(second(a)),a))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f419,definition,
( spl0_11
<=> non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f24(second(a)),a),f7(f24(second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f421,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f24(second(a)),a),f7(f24(second(a)),a))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,plain,
( spl0_9
| spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f395,f419,f415,f411]) ).
fof(f424,definition,
( spl0_12
<=> non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f24(second(a)),a),f6(f24(second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f426,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f24(second(a)),a),f6(f24(second(a)),a))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f428,definition,
( spl0_13
<=> non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f24(second(a)),a),f6(f24(second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f430,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f24(second(a)),a),f6(f24(second(a)),a))
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f431,plain,
( spl0_9
| spl0_12
| spl0_13 ),
inference(avatar_split_clause,[],[f394,f428,f424,f411]) ).
fof(f438,plain,
( member(non_ordered_pair(f2(empty_set),f2(empty_set)),empty_set)
| ~ spl0_6 ),
inference(superposition,[],[f225,f400]) ).
fof(f448,plain,
( $false
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f438,f70]) ).
fof(f449,plain,
~ spl0_6,
inference(avatar_contradiction_clause,[],[f448]) ).
fof(f455,plain,
( ~ little_set(empty_set)
| ~ spl0_9 ),
inference(superposition,[],[f163,f413]) ).
fof(f469,plain,
( member(f2(a),f24(a))
| ~ little_set(f2(a))
| ~ spl0_7 ),
inference(superposition,[],[f203,f404]) ).
fof(f473,definition,
( spl0_14
<=> little_set(f3(a)) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f474,plain,
( little_set(f3(a))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f475,plain,
( ~ little_set(f3(a))
| spl0_14 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f477,definition,
( spl0_15
<=> little_set(f2(a)) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f478,plain,
( little_set(f2(a))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f479,plain,
( ~ little_set(f2(a))
| spl0_15 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f486,definition,
( spl0_17
<=> member(f2(a),f24(a)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f488,plain,
( member(f2(a),f24(a))
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f489,plain,
( ~ spl0_15
| spl0_17
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f469,f402,f486,f477]) ).
fof(f500,plain,
( ~ ordered_pair_predicate(a)
| spl0_15 ),
inference(resolution,[],[f479,f11]) ).
fof(f504,plain,
( $false
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f500,f162]) ).
fof(f505,plain,
spl0_15,
inference(avatar_contradiction_clause,[],[f504]) ).
fof(f510,plain,
( a = non_ordered_pair(f24(a),non_ordered_pair(f2(a),f3(a)))
| ~ spl0_8 ),
inference(superposition,[],[f209,f408]) ).
fof(f518,plain,
( member(f2(a),f24(a))
| ~ little_set(f2(a))
| ~ spl0_8 ),
inference(superposition,[],[f203,f408]) ).
fof(f526,plain,
( member(f2(a),f24(a))
| ~ spl0_8
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f518,f478]) ).
fof(f528,plain,
( spl0_17
| ~ spl0_8
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f526,f477,f406,f486]) ).
fof(f530,plain,
( ~ ordered_pair_predicate(a)
| spl0_14 ),
inference(resolution,[],[f475,f12]) ).
fof(f534,plain,
( $false
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f530,f162]) ).
fof(f535,plain,
spl0_14,
inference(avatar_contradiction_clause,[],[f534]) ).
fof(f537,plain,
( non_ordered_pair(f2(a),f3(a)) = f24(a)
| non_ordered_pair(f2(a),f2(a)) = f24(a)
| empty_set = a ),
inference(superposition,[],[f380,f209]) ).
fof(f544,plain,
( f2(a) = f24(f24(a))
| f2(a) = f24(f24(a))
| empty_set = f24(a)
| ~ spl0_8 ),
inference(superposition,[],[f380,f408]) ).
fof(f555,plain,
! [X0,X1] :
( X0 != X1
| f24(non_ordered_pair(X0,X1)) = X0
| non_ordered_pair(X0,X1) = empty_set ),
inference(equality_factoring,[],[f380]) ).
fof(f560,plain,
( f2(a) = f24(f24(a))
| empty_set = f24(a)
| ~ spl0_8 ),
inference(duplicate_literal_removal,[],[f544]) ).
fof(f562,definition,
( spl0_19
<=> empty_set = f24(a) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f563,plain,
( empty_set != f24(a)
| spl0_19 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f564,plain,
( empty_set = f24(a)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl0_20
<=> f2(a) = f24(f24(a)) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f567,plain,
( f2(a) != f24(f24(a))
| spl0_20 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f568,plain,
( f2(a) = f24(f24(a))
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f571,plain,
( spl0_19
| spl0_20
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f560,f406,f566,f562]) ).
fof(f592,plain,
( ! [X0] :
( ~ member(X0,a)
| f24(a) = X0
| non_ordered_pair(f2(a),f3(a)) = X0 )
| ~ spl0_8 ),
inference(superposition,[],[f5,f510]) ).
fof(f627,plain,
( member(f2(a),empty_set)
| ~ spl0_17
| ~ spl0_19 ),
inference(superposition,[],[f488,f564]) ).
fof(f630,plain,
( $false
| ~ spl0_17
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f627,f70]) ).
fof(f631,plain,
( ~ spl0_17
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f630]) ).
fof(f744,plain,
! [X0] :
( f24(non_ordered_pair(X0,X0)) = X0
| non_ordered_pair(X0,X0) = empty_set ),
inference(equality_resolution,[],[f555]) ).
fof(f746,plain,
! [X0] :
( member(X0,non_ordered_pair(X0,X0))
| non_ordered_pair(X0,X0) = empty_set
| non_ordered_pair(X0,X0) = empty_set ),
inference(superposition,[],[f111,f744]) ).
fof(f747,plain,
! [X0] :
( member(X0,non_ordered_pair(X0,X0))
| non_ordered_pair(X0,X0) = empty_set ),
inference(duplicate_literal_removal,[],[f746]) ).
fof(f812,plain,
! [X0] :
( little_set(X0)
| non_ordered_pair(X0,X0) = empty_set ),
inference(resolution,[],[f747,f1]) ).
fof(f818,plain,
( empty_set = non_ordered_pair(empty_set,empty_set)
| ~ spl0_9 ),
inference(resolution,[],[f812,f455]) ).
fof(f821,plain,
( little_set(empty_set)
| ~ spl0_9 ),
inference(superposition,[],[f8,f818]) ).
fof(f828,plain,
( $false
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f821,f455]) ).
fof(f829,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f828]) ).
fof(f832,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(f2(a),f3(a)))
| f6(f24(second(a)),a) = X0
| f6(f24(second(a)),a) = X0 )
| ~ spl0_12 ),
inference(superposition,[],[f5,f426]) ).
fof(f845,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(f2(a),f3(a)))
| f6(f24(second(a)),a) = X0 )
| ~ spl0_12 ),
inference(duplicate_literal_removal,[],[f832]) ).
fof(f847,definition,
( spl0_40
<=> little_set(f6(f24(second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f848,plain,
( little_set(f6(f24(second(a)),a))
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f849,plain,
( ~ little_set(f6(f24(second(a)),a))
| spl0_40 ),
inference(avatar_component_clause,[],[f847]) ).
fof(f886,plain,
( member(f7(f24(second(a)),a),non_ordered_pair(f2(a),f3(a)))
| ~ little_set(f7(f24(second(a)),a))
| ~ spl0_10 ),
inference(superposition,[],[f202,f417]) ).
fof(f891,definition,
( spl0_46
<=> f7(f24(second(a)),a) = f24(non_ordered_pair(f2(a),f3(a))) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f892,plain,
( f7(f24(second(a)),a) != f24(non_ordered_pair(f2(a),f3(a)))
| spl0_46 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f893,plain,
( f7(f24(second(a)),a) = f24(non_ordered_pair(f2(a),f3(a)))
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f898,definition,
( spl0_47
<=> little_set(f7(f24(second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f899,plain,
( little_set(f7(f24(second(a)),a))
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f900,plain,
( ~ little_set(f7(f24(second(a)),a))
| spl0_47 ),
inference(avatar_component_clause,[],[f898]) ).
fof(f902,definition,
( spl0_48
<=> member(f7(f24(second(a)),a),non_ordered_pair(f2(a),f3(a))) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f904,plain,
( member(f7(f24(second(a)),a),non_ordered_pair(f2(a),f3(a)))
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f902]) ).
fof(f994,plain,
( f2(a) = f6(f24(second(a)),a)
| ~ little_set(f2(a))
| ~ spl0_12 ),
inference(resolution,[],[f845,f203]) ).
fof(f1010,plain,
( f2(a) = f6(f24(second(a)),a)
| ~ spl0_12
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f994,f478]) ).
fof(f1107,plain,
( empty_set = second(a)
| spl0_40 ),
inference(resolution,[],[f849,f241]) ).
fof(f1114,plain,
( $false
| spl0_9
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f1107,f412]) ).
fof(f1115,plain,
( spl0_9
| spl0_40 ),
inference(avatar_contradiction_clause,[],[f1114]) ).
fof(f1148,plain,
( empty_set = second(a)
| spl0_47 ),
inference(resolution,[],[f900,f242]) ).
fof(f1153,plain,
( $false
| spl0_9
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f1148,f412]) ).
fof(f1154,plain,
( spl0_9
| spl0_47 ),
inference(avatar_contradiction_clause,[],[f1153]) ).
fof(f1226,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f2(a),f3(a))
| ~ spl0_12
| ~ spl0_15 ),
inference(superposition,[],[f426,f1010]) ).
fof(f1249,plain,
( member(f7(f24(second(a)),a),non_ordered_pair(f2(a),f3(a)))
| ~ spl0_10
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f886,f899]) ).
fof(f3837,plain,
! [X0] :
( member(X0,second(a))
| ~ little_set(f2(a))
| ~ little_set(f3(a))
| ~ member(X0,f3(a)) ),
inference(superposition,[],[f200,f209]) ).
fof(f3864,plain,
( ! [X0] :
( member(X0,second(a))
| ~ little_set(f3(a))
| ~ member(X0,f3(a)) )
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f3837,f478]) ).
fof(f3906,plain,
( ! [X0] :
( ~ member(X0,f3(a))
| member(X0,second(a)) )
| ~ spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f3864,f474]) ).
fof(f6659,plain,
( ! [X0] :
( member(f1(f3(a),X0),second(a))
| member(f1(f3(a),X0),X0)
| f3(a) = X0 )
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f3906,f3]) ).
fof(f7099,definition,
( spl0_288
<=> second(a) = f3(a) ),
introduced(definition,[new_symbols(definition,[spl0_288])],[avatar_definition]) ).
fof(f7100,plain,
( second(a) != f3(a)
| spl0_288 ),
inference(avatar_component_clause,[],[f7099]) ).
fof(f7101,plain,
( second(a) = f3(a)
| ~ spl0_288 ),
inference(avatar_component_clause,[],[f7099]) ).
fof(f7140,definition,
( spl0_297
<=> f2(a) = f3(a) ),
introduced(definition,[new_symbols(definition,[spl0_297])],[avatar_definition]) ).
fof(f7141,plain,
( f2(a) != f3(a)
| spl0_297 ),
inference(avatar_component_clause,[],[f7140]) ).
fof(f7142,plain,
( f2(a) = f3(a)
| ~ spl0_297 ),
inference(avatar_component_clause,[],[f7140]) ).
fof(f7221,plain,
( little_set(second(a))
| ~ ordered_pair_predicate(a)
| ~ spl0_288 ),
inference(superposition,[],[f12,f7101]) ).
fof(f7233,plain,
( ~ ordered_pair_predicate(a)
| ~ spl0_288 ),
inference(forward_subsumption_resolution,[],[f7221,f163]) ).
fof(f7250,plain,
( $false
| ~ spl0_288 ),
inference(forward_subsumption_resolution,[],[f7233,f162]) ).
fof(f7251,plain,
~ spl0_288,
inference(avatar_contradiction_clause,[],[f7250]) ).
fof(f7319,plain,
( member(f1(f3(a),second(a)),second(a))
| second(a) = f3(a)
| ~ spl0_14
| ~ spl0_15 ),
inference(factoring,[],[f6659]) ).
fof(f7324,plain,
( member(f1(f3(a),second(a)),second(a))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_subsumption_resolution,[],[f7319,f7100]) ).
fof(f7462,plain,
( ~ member(f1(f3(a),second(a)),f3(a))
| second(a) = f3(a)
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7324,f4]) ).
fof(f7463,plain,
( little_set(f6(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7324,f24]) ).
fof(f7464,plain,
( little_set(f7(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7324,f25]) ).
fof(f7465,plain,
( a = non_ordered_pair(non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a)),non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a)))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7324,f178]) ).
fof(f7468,plain,
( ~ member(f1(f3(a),second(a)),f3(a))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_subsumption_resolution,[],[f7462,f7100]) ).
fof(f7472,plain,
( ! [X0] :
( ~ member(X0,a)
| non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a)) = X0
| non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a)) = X0 )
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(superposition,[],[f5,f7465]) ).
fof(f7476,plain,
( member(non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a)),a)
| ~ little_set(non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a)))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(superposition,[],[f202,f7465]) ).
fof(f7477,plain,
( member(non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a)),a)
| ~ little_set(non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a)))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(superposition,[],[f203,f7465]) ).
fof(f7487,plain,
( member(non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a)),a)
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_subsumption_resolution,[],[f7477,f8]) ).
fof(f7488,plain,
( member(non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a)),a)
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_subsumption_resolution,[],[f7476,f8]) ).
fof(f7495,definition,
( spl0_310
<=> f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_310])],[avatar_definition]) ).
fof(f7496,plain,
( f24(a) != non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| spl0_310 ),
inference(avatar_component_clause,[],[f7495]) ).
fof(f7497,plain,
( f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| ~ spl0_310 ),
inference(avatar_component_clause,[],[f7495]) ).
fof(f7499,definition,
( spl0_311
<=> f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_311])],[avatar_definition]) ).
fof(f7501,plain,
( f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| ~ spl0_311 ),
inference(avatar_component_clause,[],[f7499]) ).
fof(f7511,plain,
( f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7487,f592]) ).
fof(f7512,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7487,f381]) ).
fof(f7519,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7488,f381]) ).
fof(f7520,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| empty_set = second(a)
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7488,f384]) ).
fof(f7522,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_subsumption_resolution,[],[f7520,f412]) ).
fof(f7525,plain,
( f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| ~ spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_demodulation,[],[f7522,f408]) ).
fof(f7597,definition,
( spl0_322
<=> f3(a) = f7(f1(f3(a),second(a)),a) ),
introduced(definition,[new_symbols(definition,[spl0_322])],[avatar_definition]) ).
fof(f7598,plain,
( f3(a) != f7(f1(f3(a),second(a)),a)
| spl0_322 ),
inference(avatar_component_clause,[],[f7597]) ).
fof(f7599,plain,
( f3(a) = f7(f1(f3(a),second(a)),a)
| ~ spl0_322 ),
inference(avatar_component_clause,[],[f7597]) ).
fof(f10023,definition,
( spl0_463
<=> f2(a) = f7(f24(second(a)),a) ),
introduced(definition,[new_symbols(definition,[spl0_463])],[avatar_definition]) ).
fof(f10024,plain,
( f2(a) != f7(f24(second(a)),a)
| spl0_463 ),
inference(avatar_component_clause,[],[f10023]) ).
fof(f10025,plain,
( f2(a) = f7(f24(second(a)),a)
| ~ spl0_463 ),
inference(avatar_component_clause,[],[f10023]) ).
fof(f10472,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7472,f229]) ).
fof(f10474,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| empty_set = second(a)
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7472,f268]) ).
fof(f10476,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| empty_set = second(a)
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(resolution,[],[f7472,f269]) ).
fof(f10496,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_subsumption_resolution,[],[f10476,f412]) ).
fof(f10497,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_subsumption_resolution,[],[f10474,f412]) ).
fof(f10498,plain,
( non_ordered_pair(f2(a),f3(a)) = f24(a)
| non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310 ),
inference(forward_demodulation,[],[f10472,f7497]) ).
fof(f10510,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310 ),
inference(forward_subsumption_resolution,[],[f10498,f403]) ).
fof(f11192,plain,
( spl0_48
| ~ spl0_10
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f1249,f898,f415,f902]) ).
fof(f11202,definition,
( spl0_489
<=> non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a)) ),
introduced(definition,[new_symbols(definition,[spl0_489])],[avatar_definition]) ).
fof(f11203,plain,
( non_ordered_pair(f2(a),f3(a)) != non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| spl0_489 ),
inference(avatar_component_clause,[],[f11202]) ).
fof(f11204,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| ~ spl0_489 ),
inference(avatar_component_clause,[],[f11202]) ).
fof(f11207,plain,
( spl0_489
| spl0_311
| ~ spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(avatar_split_clause,[],[f7525,f7099,f477,f473,f411,f406,f7499,f11202]) ).
fof(f11222,plain,
( spl0_489
| spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310 ),
inference(avatar_split_clause,[],[f10510,f7495,f7099,f477,f473,f402,f11202]) ).
fof(f11503,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310 ),
inference(forward_subsumption_resolution,[],[f7511,f7496]) ).
fof(f11668,plain,
( f2(a) = f7(f24(second(a)),a)
| f3(a) = f7(f24(second(a)),a)
| ~ spl0_48 ),
inference(resolution,[],[f904,f5]) ).
fof(f11672,plain,
( f3(a) = f7(f24(second(a)),a)
| ~ spl0_48
| spl0_463 ),
inference(forward_subsumption_resolution,[],[f11668,f10024]) ).
fof(f12273,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(f2(a),f3(a)))
| f6(f1(f3(a),second(a)),a) = X0
| f6(f1(f3(a),second(a)),a) = X0 )
| ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310 ),
inference(superposition,[],[f5,f11503]) ).
fof(f12297,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(f2(a),f3(a)))
| f6(f1(f3(a),second(a)),a) = X0 )
| ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310 ),
inference(duplicate_literal_removal,[],[f12273]) ).
fof(f12488,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(f2(a),f3(a)))
| f6(f1(f3(a),second(a)),a) = X0
| f7(f1(f3(a),second(a)),a) = X0 )
| ~ spl0_489 ),
inference(superposition,[],[f5,f11204]) ).
fof(f12492,plain,
( member(f7(f1(f3(a),second(a)),a),non_ordered_pair(f2(a),f3(a)))
| ~ little_set(f7(f1(f3(a),second(a)),a))
| ~ spl0_489 ),
inference(superposition,[],[f202,f11204]) ).
fof(f12493,plain,
( member(f6(f1(f3(a),second(a)),a),non_ordered_pair(f2(a),f3(a)))
| ~ little_set(f6(f1(f3(a),second(a)),a))
| ~ spl0_489 ),
inference(superposition,[],[f203,f11204]) ).
fof(f12505,plain,
( member(f6(f1(f3(a),second(a)),a),non_ordered_pair(f2(a),f3(a)))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489 ),
inference(forward_subsumption_resolution,[],[f12493,f7463]) ).
fof(f12506,plain,
( member(f7(f1(f3(a),second(a)),a),non_ordered_pair(f2(a),f3(a)))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489 ),
inference(forward_subsumption_resolution,[],[f12492,f7464]) ).
fof(f12526,definition,
( spl0_573
<=> f2(a) = f7(f1(f3(a),second(a)),a) ),
introduced(definition,[new_symbols(definition,[spl0_573])],[avatar_definition]) ).
fof(f12527,plain,
( f2(a) != f7(f1(f3(a),second(a)),a)
| spl0_573 ),
inference(avatar_component_clause,[],[f12526]) ).
fof(f12528,plain,
( f2(a) = f7(f1(f3(a),second(a)),a)
| ~ spl0_573 ),
inference(avatar_component_clause,[],[f12526]) ).
fof(f12530,definition,
( spl0_574
<=> f2(a) = f6(f1(f3(a),second(a)),a) ),
introduced(definition,[new_symbols(definition,[spl0_574])],[avatar_definition]) ).
fof(f12531,plain,
( f2(a) != f6(f1(f3(a),second(a)),a)
| spl0_574 ),
inference(avatar_component_clause,[],[f12530]) ).
fof(f12532,plain,
( f2(a) = f6(f1(f3(a),second(a)),a)
| ~ spl0_574 ),
inference(avatar_component_clause,[],[f12530]) ).
fof(f12546,plain,
( f2(a) = f6(f1(f3(a),second(a)),a)
| f3(a) = f6(f1(f3(a),second(a)),a)
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489 ),
inference(resolution,[],[f12505,f5]) ).
fof(f12654,plain,
( member(f1(f3(a),second(a)),f3(a))
| ~ member(f1(f3(a),second(a)),second(a))
| ~ spl0_322 ),
inference(superposition,[],[f28,f7599]) ).
fof(f12655,plain,
( ~ member(f1(f3(a),second(a)),second(a))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_322 ),
inference(forward_subsumption_resolution,[],[f12654,f7468]) ).
fof(f12659,plain,
( $false
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_322 ),
inference(forward_subsumption_resolution,[],[f12655,f7324]) ).
fof(f12660,plain,
( ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_322 ),
inference(avatar_contradiction_clause,[],[f12659]) ).
fof(f12830,plain,
( f3(a) = f6(f1(f3(a),second(a)),a)
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489
| spl0_574 ),
inference(forward_subsumption_resolution,[],[f12546,f12531]) ).
fof(f13838,plain,
( f2(a) = f7(f1(f3(a),second(a)),a)
| f3(a) = f7(f1(f3(a),second(a)),a)
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489 ),
inference(resolution,[],[f12506,f5]) ).
fof(f14551,plain,
( f3(a) = f24(non_ordered_pair(f2(a),f3(a)))
| ~ spl0_46
| ~ spl0_48
| spl0_463 ),
inference(forward_demodulation,[],[f893,f11672]) ).
fof(f14806,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f3(a),f7(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489
| spl0_574 ),
inference(superposition,[],[f11204,f12830]) ).
fof(f14808,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f3(a),f2(a))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489
| ~ spl0_573
| spl0_574 ),
inference(forward_demodulation,[],[f14806,f12528]) ).
fof(f14819,plain,
( f2(a) != f3(a)
| spl0_322
| ~ spl0_573 ),
inference(superposition,[],[f7598,f12528]) ).
fof(f14822,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f2(a))
| ~ spl0_489
| ~ spl0_573 ),
inference(superposition,[],[f11204,f12528]) ).
fof(f14988,plain,
( f3(a) = f6(f1(f3(a),second(a)),a)
| f3(a) = f7(f1(f3(a),second(a)),a)
| ~ little_set(f3(a))
| ~ spl0_489 ),
inference(resolution,[],[f12488,f202]) ).
fof(f15271,plain,
( f24(f24(a)) = f6(f1(f3(a),second(a)),a)
| empty_set = f24(a)
| ~ spl0_310 ),
inference(superposition,[],[f744,f7497]) ).
fof(f15283,plain,
( f24(f24(a)) = f6(f1(f3(a),second(a)),a)
| spl0_19
| ~ spl0_310 ),
inference(forward_subsumption_resolution,[],[f15271,f563]) ).
fof(f15338,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f2(a),f3(a))
| ~ spl0_489
| ~ spl0_573
| ~ spl0_574 ),
inference(forward_demodulation,[],[f14822,f12532]) ).
fof(f15352,plain,
( f3(a) = f6(f1(f3(a),second(a)),a)
| ~ little_set(f3(a))
| spl0_322
| ~ spl0_489 ),
inference(forward_subsumption_resolution,[],[f14988,f7598]) ).
fof(f15373,plain,
( non_ordered_pair(f2(a),f3(a)) = f24(a)
| ~ spl0_8
| ~ spl0_489
| ~ spl0_573
| ~ spl0_574 ),
inference(forward_demodulation,[],[f15338,f408]) ).
fof(f15389,plain,
( f3(a) = f6(f1(f3(a),second(a)),a)
| ~ spl0_14
| spl0_322
| ~ spl0_489 ),
inference(forward_subsumption_resolution,[],[f15352,f474]) ).
fof(f15395,plain,
( $false
| spl0_7
| ~ spl0_8
| ~ spl0_489
| ~ spl0_573
| ~ spl0_574 ),
inference(forward_subsumption_resolution,[],[f15373,f403]) ).
fof(f15396,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_489
| ~ spl0_573
| ~ spl0_574 ),
inference(avatar_contradiction_clause,[],[f15395]) ).
fof(f15406,plain,
( f2(a) = f3(a)
| ~ spl0_14
| spl0_322
| ~ spl0_489
| ~ spl0_574 ),
inference(forward_demodulation,[],[f15389,f12532]) ).
fof(f15417,plain,
( $false
| ~ spl0_14
| spl0_297
| spl0_322
| ~ spl0_489
| ~ spl0_574 ),
inference(forward_subsumption_resolution,[],[f15406,f7141]) ).
fof(f15418,plain,
( ~ spl0_14
| spl0_297
| spl0_322
| ~ spl0_489
| ~ spl0_574 ),
inference(avatar_contradiction_clause,[],[f15417]) ).
fof(f15429,plain,
( non_ordered_pair(f2(a),f2(a)) != f24(a)
| spl0_310
| ~ spl0_574 ),
inference(forward_demodulation,[],[f7496,f12532]) ).
fof(f15470,plain,
( $false
| ~ spl0_8
| spl0_310
| ~ spl0_574 ),
inference(forward_subsumption_resolution,[],[f15429,f408]) ).
fof(f15471,plain,
( ~ spl0_8
| spl0_310
| ~ spl0_574 ),
inference(avatar_contradiction_clause,[],[f15470]) ).
fof(f15535,plain,
( non_ordered_pair(f2(a),f3(a)) != f24(a)
| ~ spl0_311
| spl0_489 ),
inference(forward_demodulation,[],[f11203,f7501]) ).
fof(f15803,plain,
( f2(a) = f6(f1(f3(a),second(a)),a)
| ~ little_set(f2(a))
| ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310 ),
inference(resolution,[],[f12297,f203]) ).
fof(f15840,plain,
( ~ little_set(f2(a))
| ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| spl0_574 ),
inference(forward_subsumption_resolution,[],[f15803,f12531]) ).
fof(f15848,plain,
( $false
| ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| spl0_574 ),
inference(forward_subsumption_resolution,[],[f15840,f478]) ).
fof(f15849,plain,
( ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| spl0_574 ),
inference(avatar_contradiction_clause,[],[f15848]) ).
fof(f15923,plain,
( f3(a) = f7(f1(f3(a),second(a)),a)
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489
| spl0_573 ),
inference(forward_subsumption_resolution,[],[f13838,f12527]) ).
fof(f16009,plain,
( $false
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_322
| ~ spl0_489
| spl0_573 ),
inference(forward_subsumption_resolution,[],[f15923,f7598]) ).
fof(f16010,plain,
( ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_322
| ~ spl0_489
| spl0_573 ),
inference(avatar_contradiction_clause,[],[f16009]) ).
fof(f16088,plain,
( $false
| ~ spl0_297
| spl0_322
| ~ spl0_573 ),
inference(forward_subsumption_resolution,[],[f14819,f7142]) ).
fof(f16089,plain,
( ~ spl0_297
| spl0_322
| ~ spl0_573 ),
inference(avatar_contradiction_clause,[],[f16088]) ).
fof(f16143,plain,
( non_ordered_pair(f2(a),f3(a)) = f24(a)
| empty_set = a
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f537,f407]) ).
fof(f16314,plain,
( non_ordered_pair(f2(a),f3(a)) = f24(a)
| spl0_6
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f16143,f399]) ).
fof(f16418,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| spl0_6
| spl0_8
| ~ spl0_297 ),
inference(forward_demodulation,[],[f16314,f7142]) ).
fof(f16499,plain,
( $false
| spl0_6
| spl0_8
| ~ spl0_297 ),
inference(forward_subsumption_resolution,[],[f16418,f407]) ).
fof(f16500,plain,
( spl0_6
| spl0_8
| ~ spl0_297 ),
inference(avatar_contradiction_clause,[],[f16499]) ).
fof(f16688,plain,
( non_ordered_pair(f2(a),f3(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_489 ),
inference(forward_subsumption_resolution,[],[f10496,f11203]) ).
fof(f16711,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_489 ),
inference(forward_subsumption_resolution,[],[f7519,f11203]) ).
fof(f16719,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310 ),
inference(forward_demodulation,[],[f10497,f7497]) ).
fof(f16782,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f2(a))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_489
| ~ spl0_573 ),
inference(forward_demodulation,[],[f16711,f12528]) ).
fof(f16788,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f7(f1(f3(a),second(a)),a))
| spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310 ),
inference(forward_subsumption_resolution,[],[f16719,f407]) ).
fof(f16820,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f2(a))
| spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310
| ~ spl0_573 ),
inference(forward_demodulation,[],[f16788,f12528]) ).
fof(f16866,plain,
( f7(f24(second(a)),a) != f24(f24(a))
| ~ spl0_7
| spl0_46 ),
inference(forward_demodulation,[],[f892,f404]) ).
fof(f17085,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(f2(a),f2(a)))
| f6(f24(second(a)),a) = X0
| f6(f24(second(a)),a) = X0 )
| ~ spl0_13 ),
inference(superposition,[],[f5,f430]) ).
fof(f17090,plain,
( member(f6(f24(second(a)),a),non_ordered_pair(f2(a),f2(a)))
| ~ little_set(f6(f24(second(a)),a))
| ~ spl0_13 ),
inference(superposition,[],[f203,f430]) ).
fof(f17091,plain,
( f6(f24(second(a)),a) = f24(non_ordered_pair(f2(a),f2(a)))
| f6(f24(second(a)),a) = f24(non_ordered_pair(f2(a),f2(a)))
| empty_set = non_ordered_pair(f2(a),f2(a))
| ~ spl0_13 ),
inference(superposition,[],[f380,f430]) ).
fof(f17106,plain,
( f6(f24(second(a)),a) = f24(non_ordered_pair(f2(a),f2(a)))
| empty_set = non_ordered_pair(f2(a),f2(a))
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f17091]) ).
fof(f17109,plain,
( ! [X0] :
( ~ member(X0,non_ordered_pair(f2(a),f2(a)))
| f6(f24(second(a)),a) = X0 )
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f17085]) ).
fof(f17112,definition,
( spl0_689
<=> empty_set = non_ordered_pair(f2(a),f2(a)) ),
introduced(definition,[new_symbols(definition,[spl0_689])],[avatar_definition]) ).
fof(f17113,plain,
( empty_set != non_ordered_pair(f2(a),f2(a))
| spl0_689 ),
inference(avatar_component_clause,[],[f17112]) ).
fof(f17114,plain,
( empty_set = non_ordered_pair(f2(a),f2(a))
| ~ spl0_689 ),
inference(avatar_component_clause,[],[f17112]) ).
fof(f17116,definition,
( spl0_690
<=> f6(f24(second(a)),a) = f24(non_ordered_pair(f2(a),f2(a))) ),
introduced(definition,[new_symbols(definition,[spl0_690])],[avatar_definition]) ).
fof(f17118,plain,
( f6(f24(second(a)),a) = f24(non_ordered_pair(f2(a),f2(a)))
| ~ spl0_690 ),
inference(avatar_component_clause,[],[f17116]) ).
fof(f17142,plain,
( spl0_689
| spl0_690
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f17106,f428,f17116,f17112]) ).
fof(f17162,definition,
( spl0_695
<=> member(f6(f24(second(a)),a),non_ordered_pair(f2(a),f2(a))) ),
introduced(definition,[new_symbols(definition,[spl0_695])],[avatar_definition]) ).
fof(f17164,plain,
( member(f6(f24(second(a)),a),non_ordered_pair(f2(a),f2(a)))
| ~ spl0_695 ),
inference(avatar_component_clause,[],[f17162]) ).
fof(f17166,plain,
( member(f6(f24(second(a)),a),non_ordered_pair(f2(a),f2(a)))
| ~ spl0_13
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f17090,f848]) ).
fof(f17174,plain,
( spl0_695
| ~ spl0_13
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f17166,f847,f428,f17162]) ).
fof(f17317,plain,
( member(f7(f24(second(a)),a),non_ordered_pair(f2(a),f2(a)))
| ~ little_set(f7(f24(second(a)),a))
| ~ spl0_11 ),
inference(superposition,[],[f202,f421]) ).
fof(f17325,plain,
( member(f7(f24(second(a)),a),non_ordered_pair(f2(a),f2(a)))
| ~ spl0_11
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f17317,f899]) ).
fof(f17417,plain,
( f2(a) = f7(f24(second(a)),a)
| f2(a) = f7(f24(second(a)),a)
| ~ spl0_11
| ~ spl0_47 ),
inference(resolution,[],[f17325,f5]) ).
fof(f17420,plain,
( f2(a) = f7(f24(second(a)),a)
| ~ spl0_11
| ~ spl0_47 ),
inference(duplicate_literal_removal,[],[f17417]) ).
fof(f17421,plain,
( $false
| ~ spl0_11
| ~ spl0_47
| spl0_463 ),
inference(forward_subsumption_resolution,[],[f17420,f10024]) ).
fof(f17422,plain,
( ~ spl0_11
| ~ spl0_47
| spl0_463 ),
inference(avatar_contradiction_clause,[],[f17421]) ).
fof(f17588,plain,
( member(f2(a),empty_set)
| ~ little_set(f2(a))
| ~ spl0_689 ),
inference(superposition,[],[f202,f17114]) ).
fof(f17602,plain,
( ~ little_set(f2(a))
| ~ spl0_689 ),
inference(forward_subsumption_resolution,[],[f17588,f70]) ).
fof(f17612,plain,
( $false
| ~ spl0_15
| ~ spl0_689 ),
inference(forward_subsumption_resolution,[],[f17602,f478]) ).
fof(f17613,plain,
( ~ spl0_15
| ~ spl0_689 ),
inference(avatar_contradiction_clause,[],[f17612]) ).
fof(f17649,plain,
( f2(a) = f24(f24(a))
| f3(a) = f24(f24(a))
| empty_set = f24(a)
| ~ spl0_7 ),
inference(superposition,[],[f380,f404]) ).
fof(f17650,plain,
( f3(a) = f24(f24(a))
| f2(a) = f24(f24(a))
| empty_set = f24(a)
| ~ spl0_7 ),
inference(superposition,[],[f380,f404]) ).
fof(f18309,plain,
( f2(a) = f6(f24(second(a)),a)
| f2(a) = f6(f24(second(a)),a)
| ~ spl0_695 ),
inference(resolution,[],[f17164,f5]) ).
fof(f18312,plain,
( f2(a) = f6(f24(second(a)),a)
| ~ spl0_695 ),
inference(duplicate_literal_removal,[],[f18309]) ).
fof(f20348,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| ~ spl0_310
| ~ spl0_574 ),
inference(superposition,[],[f7497,f12532]) ).
fof(f20357,plain,
( f24(f24(a)) = f6(f1(f3(a),second(a)),a)
| f24(f24(a)) = f6(f1(f3(a),second(a)),a)
| empty_set = f24(a)
| ~ spl0_310 ),
inference(superposition,[],[f380,f7497]) ).
fof(f20372,plain,
( f24(f24(a)) = f6(f1(f3(a),second(a)),a)
| empty_set = f24(a)
| ~ spl0_310 ),
inference(duplicate_literal_removal,[],[f20357]) ).
fof(f20382,plain,
( f24(f24(a)) = f6(f1(f3(a),second(a)),a)
| spl0_19
| ~ spl0_310 ),
inference(forward_subsumption_resolution,[],[f20372,f563]) ).
fof(f20384,plain,
( $false
| spl0_8
| ~ spl0_310
| ~ spl0_574 ),
inference(forward_subsumption_resolution,[],[f20348,f407]) ).
fof(f20385,plain,
( spl0_8
| ~ spl0_310
| ~ spl0_574 ),
inference(avatar_contradiction_clause,[],[f20384]) ).
fof(f20430,plain,
( f2(a) = f6(f1(f3(a),second(a)),a)
| spl0_19
| ~ spl0_20
| ~ spl0_310 ),
inference(forward_demodulation,[],[f20382,f568]) ).
fof(f20457,plain,
( $false
| spl0_19
| ~ spl0_20
| ~ spl0_310
| spl0_574 ),
inference(forward_subsumption_resolution,[],[f20430,f12531]) ).
fof(f20458,plain,
( spl0_19
| ~ spl0_20
| ~ spl0_310
| spl0_574 ),
inference(avatar_contradiction_clause,[],[f20457]) ).
fof(f20473,plain,
( $false
| ~ spl0_7
| ~ spl0_311
| spl0_489 ),
inference(forward_subsumption_resolution,[],[f15535,f404]) ).
fof(f20474,plain,
( ~ spl0_7
| ~ spl0_311
| spl0_489 ),
inference(avatar_contradiction_clause,[],[f20473]) ).
fof(f20487,plain,
( f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288 ),
inference(forward_demodulation,[],[f7512,f404]) ).
fof(f20495,plain,
( f24(a) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| ~ spl0_7
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_489 ),
inference(forward_demodulation,[],[f16688,f404]) ).
fof(f20517,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f6(f1(f3(a),second(a)),a),f6(f1(f3(a),second(a)),a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310 ),
inference(forward_subsumption_resolution,[],[f20487,f7496]) ).
fof(f20578,plain,
( f24(a) = non_ordered_pair(f3(a),f2(a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_489
| ~ spl0_573
| spl0_574 ),
inference(forward_demodulation,[],[f14808,f404]) ).
fof(f20723,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f3(a),f3(a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| ~ spl0_489
| spl0_574 ),
inference(forward_demodulation,[],[f20517,f12830]) ).
fof(f21039,plain,
( f3(a) = f24(non_ordered_pair(f2(a),f2(a)))
| empty_set = non_ordered_pair(f2(a),f2(a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| ~ spl0_489
| spl0_574 ),
inference(superposition,[],[f744,f20723]) ).
fof(f21051,plain,
( f3(a) = f24(non_ordered_pair(f2(a),f2(a)))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| ~ spl0_489
| spl0_574
| spl0_689 ),
inference(forward_subsumption_resolution,[],[f21039,f17113]) ).
fof(f21064,plain,
( f2(a) = f3(a)
| empty_set = non_ordered_pair(f2(a),f2(a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| ~ spl0_489
| spl0_574
| spl0_689 ),
inference(superposition,[],[f21051,f744]) ).
fof(f21076,plain,
( empty_set = non_ordered_pair(f2(a),f2(a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_297
| spl0_310
| ~ spl0_489
| spl0_574
| spl0_689 ),
inference(forward_subsumption_resolution,[],[f21064,f7141]) ).
fof(f21086,plain,
( $false
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_297
| spl0_310
| ~ spl0_489
| spl0_574
| spl0_689 ),
inference(forward_subsumption_resolution,[],[f21076,f17113]) ).
fof(f21087,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_297
| spl0_310
| ~ spl0_489
| spl0_574
| spl0_689 ),
inference(avatar_contradiction_clause,[],[f21086]) ).
fof(f21135,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f3(a),f2(a))
| spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310
| ~ spl0_489
| ~ spl0_573
| spl0_574 ),
inference(forward_demodulation,[],[f16820,f12830]) ).
fof(f21243,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| ~ spl0_7
| spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310
| ~ spl0_489
| ~ spl0_573
| spl0_574 ),
inference(forward_demodulation,[],[f21135,f20578]) ).
fof(f21314,plain,
( $false
| ~ spl0_7
| spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310
| ~ spl0_489
| ~ spl0_573
| spl0_574 ),
inference(forward_subsumption_resolution,[],[f21243,f407]) ).
fof(f21315,plain,
( ~ spl0_7
| spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310
| ~ spl0_489
| ~ spl0_573
| spl0_574 ),
inference(avatar_contradiction_clause,[],[f21314]) ).
fof(f21411,plain,
( spl0_310
| ~ spl0_7
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_489 ),
inference(avatar_split_clause,[],[f20495,f11202,f7099,f477,f473,f411,f402,f7495]) ).
fof(f21443,plain,
( f3(a) != f24(f24(a))
| ~ spl0_7
| spl0_46
| ~ spl0_48
| spl0_463 ),
inference(forward_demodulation,[],[f16866,f11672]) ).
fof(f21446,plain,
( f3(a) = f24(f24(a))
| empty_set = f24(a)
| ~ spl0_7
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f17650,f567]) ).
fof(f21447,plain,
( f3(a) = f24(f24(a))
| empty_set = f24(a)
| ~ spl0_7
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f17649,f567]) ).
fof(f21478,plain,
( empty_set = f24(a)
| ~ spl0_7
| spl0_20
| spl0_46
| ~ spl0_48
| spl0_463 ),
inference(forward_subsumption_resolution,[],[f21447,f21443]) ).
fof(f21492,plain,
( $false
| ~ spl0_7
| spl0_19
| spl0_20
| spl0_46
| ~ spl0_48
| spl0_463 ),
inference(forward_subsumption_resolution,[],[f21478,f563]) ).
fof(f21493,plain,
( ~ spl0_7
| spl0_19
| spl0_20
| spl0_46
| ~ spl0_48
| spl0_463 ),
inference(avatar_contradiction_clause,[],[f21492]) ).
fof(f21506,plain,
( f3(a) = f24(f24(a))
| ~ spl0_7
| ~ spl0_46
| ~ spl0_48
| spl0_463 ),
inference(forward_demodulation,[],[f14551,f404]) ).
fof(f21508,plain,
( f3(a) = f24(f24(a))
| ~ spl0_7
| spl0_19
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f21446,f563]) ).
fof(f21521,plain,
( a = non_ordered_pair(non_ordered_pair(f2(a),f2(a)),non_ordered_pair(f2(a),f7(f24(second(a)),a)))
| empty_set = second(a)
| ~ spl0_695 ),
inference(superposition,[],[f243,f18312]) ).
fof(f21522,plain,
( a = non_ordered_pair(non_ordered_pair(f2(a),f2(a)),non_ordered_pair(f2(a),f7(f24(second(a)),a)))
| spl0_9
| ~ spl0_695 ),
inference(forward_subsumption_resolution,[],[f21521,f412]) ).
fof(f21587,plain,
( member(f6(f1(f3(a),second(a)),a),non_ordered_pair(f2(a),f2(a)))
| ~ little_set(f6(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_489
| ~ spl0_573 ),
inference(superposition,[],[f203,f16782]) ).
fof(f21598,plain,
( member(f6(f1(f3(a),second(a)),a),non_ordered_pair(f2(a),f2(a)))
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_489
| ~ spl0_573 ),
inference(forward_subsumption_resolution,[],[f21587,f7463]) ).
fof(f21606,plain,
( member(f24(f24(a)),non_ordered_pair(f2(a),f2(a)))
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_288
| ~ spl0_310
| spl0_489
| ~ spl0_573 ),
inference(forward_demodulation,[],[f21598,f15283]) ).
fof(f22112,plain,
( member(f3(a),non_ordered_pair(f2(a),f2(a)))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| ~ spl0_46
| ~ spl0_48
| spl0_288
| ~ spl0_310
| spl0_463
| spl0_489
| ~ spl0_573 ),
inference(forward_demodulation,[],[f21606,f21506]) ).
fof(f22318,plain,
( f3(a) = f6(f24(second(a)),a)
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| spl0_19
| ~ spl0_46
| ~ spl0_48
| spl0_288
| ~ spl0_310
| spl0_463
| spl0_489
| ~ spl0_573 ),
inference(resolution,[],[f22112,f17109]) ).
fof(f22325,plain,
( f2(a) = f3(a)
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| spl0_19
| ~ spl0_46
| ~ spl0_48
| spl0_288
| ~ spl0_310
| spl0_463
| spl0_489
| ~ spl0_573
| ~ spl0_695 ),
inference(forward_demodulation,[],[f22318,f18312]) ).
fof(f22327,plain,
( $false
| ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| spl0_19
| ~ spl0_46
| ~ spl0_48
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_463
| spl0_489
| ~ spl0_573
| ~ spl0_695 ),
inference(forward_subsumption_resolution,[],[f22325,f7141]) ).
fof(f22328,plain,
( ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| spl0_19
| ~ spl0_46
| ~ spl0_48
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_463
| spl0_489
| ~ spl0_573
| ~ spl0_695 ),
inference(avatar_contradiction_clause,[],[f22327]) ).
fof(f22346,plain,
( a = non_ordered_pair(non_ordered_pair(f2(a),f2(a)),non_ordered_pair(f2(a),f2(a)))
| spl0_9
| ~ spl0_463
| ~ spl0_695 ),
inference(forward_demodulation,[],[f21522,f10025]) ).
fof(f23710,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| non_ordered_pair(f2(a),f2(a)) = f24(a)
| empty_set = a
| spl0_9
| ~ spl0_463
| ~ spl0_695 ),
inference(superposition,[],[f380,f22346]) ).
fof(f23725,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| empty_set = a
| spl0_9
| ~ spl0_463
| ~ spl0_695 ),
inference(duplicate_literal_removal,[],[f23710]) ).
fof(f23738,plain,
( empty_set = a
| spl0_8
| spl0_9
| ~ spl0_463
| ~ spl0_695 ),
inference(forward_subsumption_resolution,[],[f23725,f407]) ).
fof(f23751,plain,
( $false
| spl0_6
| spl0_8
| spl0_9
| ~ spl0_463
| ~ spl0_695 ),
inference(forward_subsumption_resolution,[],[f23738,f399]) ).
fof(f23752,plain,
( spl0_6
| spl0_8
| spl0_9
| ~ spl0_463
| ~ spl0_695 ),
inference(avatar_contradiction_clause,[],[f23751]) ).
fof(f23795,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f24(f24(a)),f7(f1(f3(a),second(a)),a))
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_288
| ~ spl0_310
| spl0_489 ),
inference(forward_demodulation,[],[f16711,f15283]) ).
fof(f23861,plain,
( non_ordered_pair(f2(a),f2(a)) = non_ordered_pair(f3(a),f7(f1(f3(a),second(a)),a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| ~ spl0_310
| spl0_489 ),
inference(forward_demodulation,[],[f23795,f21508]) ).
fof(f24612,plain,
( f3(a) = f24(non_ordered_pair(f2(a),f2(a)))
| f24(non_ordered_pair(f2(a),f2(a))) = f7(f1(f3(a),second(a)),a)
| empty_set = non_ordered_pair(f2(a),f2(a))
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| ~ spl0_310
| spl0_489 ),
inference(superposition,[],[f380,f23861]) ).
fof(f24623,plain,
( f3(a) = f24(non_ordered_pair(f2(a),f2(a)))
| f24(non_ordered_pair(f2(a),f2(a))) = f7(f1(f3(a),second(a)),a)
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| ~ spl0_310
| spl0_489
| spl0_689 ),
inference(forward_subsumption_resolution,[],[f24612,f17113]) ).
fof(f24634,plain,
( f3(a) = f6(f24(second(a)),a)
| f24(non_ordered_pair(f2(a),f2(a))) = f7(f1(f3(a),second(a)),a)
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| ~ spl0_310
| spl0_489
| spl0_689
| ~ spl0_690 ),
inference(forward_demodulation,[],[f24623,f17118]) ).
fof(f24643,plain,
( f2(a) = f3(a)
| f24(non_ordered_pair(f2(a),f2(a))) = f7(f1(f3(a),second(a)),a)
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| ~ spl0_310
| spl0_489
| spl0_689
| ~ spl0_690
| ~ spl0_695 ),
inference(forward_demodulation,[],[f24634,f18312]) ).
fof(f24651,plain,
( f24(non_ordered_pair(f2(a),f2(a))) = f7(f1(f3(a),second(a)),a)
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_489
| spl0_689
| ~ spl0_690
| ~ spl0_695 ),
inference(forward_subsumption_resolution,[],[f24643,f7141]) ).
fof(f24843,plain,
( f6(f24(second(a)),a) = f7(f1(f3(a),second(a)),a)
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_489
| spl0_689
| ~ spl0_690
| ~ spl0_695 ),
inference(forward_demodulation,[],[f24651,f17118]) ).
fof(f24856,plain,
( f2(a) = f7(f1(f3(a),second(a)),a)
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_489
| spl0_689
| ~ spl0_690
| ~ spl0_695 ),
inference(forward_demodulation,[],[f24843,f18312]) ).
fof(f24865,plain,
( $false
| ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_489
| spl0_573
| spl0_689
| ~ spl0_690
| ~ spl0_695 ),
inference(forward_subsumption_resolution,[],[f24856,f12527]) ).
fof(f24866,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_489
| spl0_573
| spl0_689
| ~ spl0_690
| ~ spl0_695 ),
inference(avatar_contradiction_clause,[],[f24865]) ).
fof(f24895,plain,
( non_ordered_pair(f2(a),f2(a)) = f24(a)
| ~ spl0_7
| ~ spl0_12
| ~ spl0_15 ),
inference(forward_demodulation,[],[f1226,f404]) ).
fof(f25008,plain,
( $false
| ~ spl0_7
| spl0_8
| ~ spl0_12
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f24895,f407]) ).
fof(f25009,plain,
( ~ spl0_7
| spl0_8
| ~ spl0_12
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f25008]) ).
cnf(s4,plain,
( spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f409]) ).
cnf(s5,plain,
( spl0_9
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f422]) ).
cnf(s6,plain,
( spl0_9
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f431]) ).
cnf(s8,plain,
~ spl0_6,
inference(sat_conversion,[],[f449]) ).
cnf(s11,plain,
( ~ spl0_7
| ~ spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f489]) ).
cnf(s13,plain,
spl0_15,
inference(sat_conversion,[],[f505]) ).
cnf(s14,plain,
( ~ spl0_8
| ~ spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f528]) ).
cnf(s16,plain,
spl0_14,
inference(sat_conversion,[],[f535]) ).
cnf(s18,plain,
( ~ spl0_8
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f571]) ).
cnf(s21,plain,
( ~ spl0_17
| ~ spl0_19 ),
inference(sat_conversion,[],[f631]) ).
cnf(s39,plain,
~ spl0_9,
inference(sat_conversion,[],[f829]) ).
cnf(s67,plain,
( spl0_9
| spl0_40 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s69,plain,
( spl0_9
| spl0_47 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s469,plain,
~ spl0_288,
inference(sat_conversion,[],[f7251]) ).
cnf(s735,plain,
( ~ spl0_10
| ~ spl0_47
| spl0_48 ),
inference(sat_conversion,[],[f11192]) ).
cnf(s738,plain,
( ~ spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_311
| spl0_489 ),
inference(sat_conversion,[],[f11207]) ).
cnf(s740,plain,
( spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310
| spl0_489 ),
inference(sat_conversion,[],[f11222]) ).
cnf(s869,plain,
( ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_322 ),
inference(sat_conversion,[],[f12660]) ).
cnf(s1037,plain,
( spl0_7
| ~ spl0_8
| ~ spl0_489
| ~ spl0_573
| ~ spl0_574 ),
inference(sat_conversion,[],[f15396]) ).
cnf(s1042,plain,
( ~ spl0_14
| spl0_297
| spl0_322
| ~ spl0_489
| ~ spl0_574 ),
inference(sat_conversion,[],[f15418]) ).
cnf(s1046,plain,
( ~ spl0_8
| spl0_310
| ~ spl0_574 ),
inference(sat_conversion,[],[f15471]) ).
cnf(s1105,plain,
( ~ spl0_8
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| spl0_574 ),
inference(sat_conversion,[],[f15849]) ).
cnf(s1117,plain,
( ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_322
| ~ spl0_489
| spl0_573 ),
inference(sat_conversion,[],[f16010]) ).
cnf(s1122,plain,
( ~ spl0_297
| spl0_322
| ~ spl0_573 ),
inference(sat_conversion,[],[f16089]) ).
cnf(s1141,plain,
( spl0_6
| spl0_8
| ~ spl0_297 ),
inference(sat_conversion,[],[f16500]) ).
cnf(s1209,plain,
( ~ spl0_13
| spl0_689
| spl0_690 ),
inference(sat_conversion,[],[f17142]) ).
cnf(s1215,plain,
( ~ spl0_13
| ~ spl0_40
| spl0_695 ),
inference(sat_conversion,[],[f17174]) ).
cnf(s1248,plain,
( ~ spl0_11
| ~ spl0_47
| spl0_463 ),
inference(sat_conversion,[],[f17422]) ).
cnf(s1262,plain,
( ~ spl0_15
| ~ spl0_689 ),
inference(sat_conversion,[],[f17613]) ).
cnf(s1479,plain,
( spl0_8
| ~ spl0_310
| ~ spl0_574 ),
inference(sat_conversion,[],[f20385]) ).
cnf(s1488,plain,
( spl0_19
| ~ spl0_20
| ~ spl0_310
| spl0_574 ),
inference(sat_conversion,[],[f20458]) ).
cnf(s1489,plain,
( ~ spl0_7
| ~ spl0_311
| spl0_489 ),
inference(sat_conversion,[],[f20474]) ).
cnf(s1520,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_297
| spl0_310
| ~ spl0_489
| spl0_574
| spl0_689 ),
inference(sat_conversion,[],[f21087]) ).
cnf(s1538,plain,
( ~ spl0_7
| spl0_8
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| ~ spl0_310
| ~ spl0_489
| ~ spl0_573
| spl0_574 ),
inference(sat_conversion,[],[f21315]) ).
cnf(s1542,plain,
( ~ spl0_7
| spl0_9
| ~ spl0_14
| ~ spl0_15
| spl0_288
| spl0_310
| spl0_489 ),
inference(sat_conversion,[],[f21411]) ).
cnf(s1548,plain,
( ~ spl0_7
| spl0_19
| spl0_20
| spl0_46
| ~ spl0_48
| spl0_463 ),
inference(sat_conversion,[],[f21493]) ).
cnf(s1597,plain,
( ~ spl0_7
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| spl0_19
| ~ spl0_46
| ~ spl0_48
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_463
| spl0_489
| ~ spl0_573
| ~ spl0_695 ),
inference(sat_conversion,[],[f22328]) ).
cnf(s1749,plain,
( spl0_6
| spl0_8
| spl0_9
| ~ spl0_463
| ~ spl0_695 ),
inference(sat_conversion,[],[f23752]) ).
cnf(s1793,plain,
( ~ spl0_7
| ~ spl0_14
| ~ spl0_15
| spl0_19
| spl0_20
| spl0_288
| spl0_297
| ~ spl0_310
| spl0_489
| spl0_573
| spl0_689
| ~ spl0_690
| ~ spl0_695 ),
inference(sat_conversion,[],[f24866]) ).
cnf(s1801,plain,
( ~ spl0_7
| spl0_8
| ~ spl0_12
| ~ spl0_15 ),
inference(sat_conversion,[],[f25009]) ).
cnf(s1844,plain,
spl0_47,
inference(rat,[],[s69,s39]) ).
cnf(s1845,plain,
spl0_40,
inference(rat,[],[s67,s39]) ).
cnf(s1848,plain,
~ spl0_689,
inference(rat,[],[s1262,s13]) ).
cnf(s1849,plain,
~ spl0_322,
inference(rat,[],[s869,s16,s469,s13]) ).
cnf(s1857,plain,
( ~ spl0_7
| spl0_17 ),
inference(rat,[],[s11,s13]) ).
cnf(s1860,plain,
( spl0_12
| spl0_13 ),
inference(rat,[],[s6,s39]) ).
cnf(s1861,plain,
( spl0_10
| spl0_11 ),
inference(rat,[],[s5,s39]) ).
cnf(s1862,plain,
( spl0_7
| spl0_8 ),
inference(rat,[],[s4,s8]) ).
cnf(s1865,plain,
( ~ spl0_310
| spl0_7 ),
inference(rat,[],[s1037,s1117,s1488,s740,s18,s21,s14,s1862,s469,s16,s13,s1849]) ).
cnf(s1866,plain,
( spl0_310
| ~ spl0_8 ),
inference(rat,[],[s1105,s1046,s13,s469,s16]) ).
cnf(s1867,plain,
spl0_7,
inference(rat,[],[s1866,s1865,s1862]) ).
cnf(s1869,plain,
spl0_17,
inference(rat,[],[s1857,s1867]) ).
cnf(s1871,plain,
~ spl0_19,
inference(rat,[],[s21,s1869]) ).
cnf(s1872,plain,
( ~ spl0_489
| ~ spl0_574 ),
inference(rat,[],[s1122,s1042,s1117,s1849,s16,s469,s13]) ).
cnf(s1873,plain,
( spl0_489
| ~ spl0_8 ),
inference(rat,[],[s1489,s738,s13,s469,s16,s39,s1867]) ).
cnf(s1874,plain,
~ spl0_8,
inference(rat,[],[s1873,s1872,s1488,s18,s1866,s1871]) ).
cnf(s1875,plain,
~ spl0_12,
inference(rat,[],[s1801,s13,s1867,s1874]) ).
cnf(s1876,plain,
~ spl0_297,
inference(rat,[],[s1141,s8,s1874]) ).
cnf(s1877,plain,
spl0_13,
inference(rat,[],[s1860,s1875]) ).
cnf(s1878,plain,
spl0_695,
inference(rat,[],[s1215,s1845,s1877]) ).
cnf(s1879,plain,
spl0_690,
inference(rat,[],[s1209,s1848,s1877]) ).
cnf(s1881,plain,
~ spl0_463,
inference(rat,[],[s1749,s1874,s8,s39,s1878]) ).
cnf(s1882,plain,
~ spl0_11,
inference(rat,[],[s1248,s1844,s1881]) ).
cnf(s1883,plain,
spl0_10,
inference(rat,[],[s1861,s1882]) ).
cnf(s1885,plain,
spl0_48,
inference(rat,[],[s735,s1844,s1883]) ).
cnf(s1889,plain,
( ~ spl0_489
| spl0_574
| ~ spl0_573 ),
inference(rat,[],[s1520,s1538,s1874,s39,s1848,s1876,s1867,s13,s469,s16]) ).
cnf(s1890,plain,
~ spl0_489,
inference(rat,[],[s1889,s1042,s1117,s16,s1849,s1876,s469,s13]) ).
cnf(s1891,plain,
spl0_310,
inference(rat,[],[s1542,s1867,s13,s469,s16,s39,s1890]) ).
cnf(s1893,plain,
~ spl0_574,
inference(rat,[],[s1479,s1874,s1891]) ).
cnf(s1896,plain,
~ spl0_20,
inference(rat,[],[s1488,s1891,s1871,s1893]) ).
cnf(s1900,plain,
spl0_573,
inference(rat,[],[s1793,s1878,s1879,s1848,s1891,s1890,s1876,s1871,s469,s1867,s13,s16,s1896]) ).
cnf(s1902,plain,
spl0_46,
inference(rat,[],[s1548,s1881,s1885,s1871,s1867,s1896]) ).
cnf(s1905,plain,
$false,
inference(rat,[],[s1597,s1878,s1890,s1891,s1881,s1877,s1876,s469,s1885,s1871,s1867,s13,s16,s1900,s1902]) ).
fof(f25105,plain,
$false,
inference(avatar_sat_refutation,[],[s1905]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET023-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n006.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 00:10:11 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.42/2.36 % (3474202)Input is clausal, will run a generic CNF schedule.
% 10.42/2.36 % (3474211)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=619748352:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.42/2.36 % (3474211)Refutation not found, incomplete strategy
% 10.42/2.36 % (3474211)------------------------------
% 10.42/2.36 % (3474211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.36 % (3474211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.36 % (3474211)CaDiCaL version: 2.1.3
% 10.42/2.36 % (3474211)Termination reason: Refutation not found, incomplete strategy
% 10.42/2.36 % (3474211)Time elapsed: 0.001 s
% 10.42/2.36 % (3474211)Peak memory usage: 87 MB
% 10.42/2.36 % (3474208)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=616420297:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.42/2.36 % (3474213)dis-21_1_sil=8000:lcm=predicate:random_seed=3882777620: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)
% 10.42/2.36 % (3474210)lrs+10_1_sil=8000:sp=occurrence:random_seed=3144716886:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.42/2.36 % (3474207)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=283833100:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.42/2.36 % (3474212)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1296227523:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.42/2.36 % (3474209)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2866774653:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.42/2.36 % (3474210)Refutation not found, incomplete strategy
% 10.42/2.36 % (3474210)------------------------------
% 10.42/2.36 % (3474210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.36 % (3474210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.36 % (3474210)CaDiCaL version: 2.1.3
% 10.42/2.36 % (3474210)Termination reason: Refutation not found, incomplete strategy
% 10.42/2.36 % (3474210)Time elapsed: 0.001 s
% 10.42/2.36 % (3474210)Peak memory usage: 87 MB
% 10.42/2.36 % (3474213)Instruction limit reached!
% 10.42/2.36 % (3474213)------------------------------
% 10.42/2.36 % (3474213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.36 % (3474213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.36 % (3474213)CaDiCaL version: 2.1.3
% 10.42/2.36 % (3474213)Termination reason: Instruction limit
% 10.42/2.36 % (3474213)Termination phase: Saturation
% 10.42/2.36 % (3474213)Time elapsed: 0.066 s
% 10.42/2.36 % (3474213)Peak memory usage: 88 MB
% 10.42/2.36 % (3474213)Instructions burned: 118 (million)
% 10.42/2.36 % (3474211)------------------------------
% 10.42/2.36 % (3474211)------------------------------
% 10.42/2.36 % (3474212)Instruction limit reached!
% 10.42/2.36 % (3474212)------------------------------
% 10.42/2.36 % (3474212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.36 % (3474212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.36 % (3474212)CaDiCaL version: 2.1.3
% 10.42/2.36 % (3474212)Termination reason: Instruction limit
% 10.42/2.36 % (3474212)Termination phase: Saturation
% 10.42/2.36 % (3474212)Time elapsed: 0.125 s
% 10.42/2.36 % (3474212)Peak memory usage: 90 MB
% 10.42/2.36 % (3474212)Instructions burned: 181 (million)
% 10.42/2.36 % (3474221)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=855926946:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.42/2.36 % (3474221)Refutation not found, incomplete strategy
% 10.42/2.36 % (3474221)------------------------------
% 10.42/2.36 % (3474221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.42/2.36 % (3474221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.42/2.36 % (3474221)CaDiCaL version: 2.1.3
% 10.42/2.36 % (3474221)Termination reason: Refutation not found, incomplete strategy
% 10.42/2.36 % (3474221)Time elapsed: 0.001 s
% 10.42/2.36 % (3474221)Peak memory usage: 87 MB
% 10.42/2.36 % (3474222)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4176208584: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)
% 19.97/3.76 % (3474210)------------------------------
% 19.97/3.76 % (3474210)------------------------------
% 19.97/3.76 % (3474223)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=149358194:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 19.97/3.76 % (3474223)Refutation not found, incomplete strategy
% 19.97/3.76 % (3474223)------------------------------
% 19.97/3.76 % (3474223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.97/3.76 % (3474223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.97/3.76 % (3474223)CaDiCaL version: 2.1.3
% 19.97/3.76 % (3474223)Termination reason: Refutation not found, incomplete strategy
% 19.97/3.76 % (3474223)Time elapsed: 0.003 s
% 19.97/3.76 % (3474223)Peak memory usage: 88 MB
% 19.97/3.76 % (3474223)Instructions burned: 3 (million)
% 19.97/3.76 % (3474222)Instruction limit reached!
% 19.97/3.76 % (3474222)------------------------------
% 19.97/3.76 % (3474222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.97/3.76 % (3474222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.97/3.76 % (3474222)CaDiCaL version: 2.1.3
% 19.97/3.76 % (3474222)Termination reason: Instruction limit
% 19.97/3.76 % (3474222)Termination phase: Saturation
% 19.97/3.76 % (3474222)Time elapsed: 0.052 s
% 19.97/3.76 % (3474222)Peak memory usage: 90 MB
% 19.97/3.76 % (3474222)Instructions burned: 191 (million)
% 19.97/3.76 % (3474228)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=990433381:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.97/3.76 % (3474226)lrs+10_64_to=lpo:sil=8000:random_seed=216011754:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 19.97/3.76 % (3474221)------------------------------
% 19.97/3.76 % (3474221)------------------------------
% 19.97/3.76 % (3474228)Instruction limit reached!
% 19.97/3.76 % (3474228)------------------------------
% 19.97/3.76 % (3474228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.97/3.76 % (3474228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.97/3.76 % (3474228)CaDiCaL version: 2.1.3
% 19.97/3.76 % (3474228)Termination reason: Instruction limit
% 19.97/3.76 % (3474228)Termination phase: Saturation
% 19.97/3.76 % (3474228)Time elapsed: 0.066 s
% 19.97/3.76 % (3474228)Peak memory usage: 89 MB
% 19.97/3.76 % (3474228)Instructions burned: 195 (million)
% 19.97/3.76 % (3474226)Instruction limit reached!
% 19.97/3.76 % (3474226)------------------------------
% 19.97/3.76 % (3474226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.97/3.76 % (3474226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.97/3.76 % (3474226)CaDiCaL version: 2.1.3
% 19.97/3.76 % (3474226)Termination reason: Instruction limit
% 19.97/3.76 % (3474226)Termination phase: Saturation
% 19.97/3.76 % (3474226)Time elapsed: 0.073 s
% 19.97/3.76 % (3474226)Peak memory usage: 90 MB
% 19.97/3.76 % (3474226)Instructions burned: 128 (million)
% 19.97/3.76 % (3474223)------------------------------
% 19.97/3.76 % (3474223)------------------------------
% 19.97/3.76 % (3474231)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1002896199:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 19.97/3.76 % (3474233)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=695503046:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.97/3.76 % (3474232)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2436907540:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 19.97/3.76 % (3474233)Refutation not found, incomplete strategy
% 19.97/3.76 % (3474233)------------------------------
% 19.97/3.76 % (3474233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.97/3.76 % (3474233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.97/3.76 % (3474233)CaDiCaL version: 2.1.3
% 19.97/3.76 % (3474233)Termination reason: Refutation not found, incomplete strategy
% 19.97/3.76 % (3474233)Time elapsed: 0.002 s
% 19.97/3.76 % (3474233)Peak memory usage: 88 MB
% 19.97/3.76 % (3474233)Instructions burned: 1 (million)
% 19.97/3.76 % (3474231)Instruction limit reached!
% 19.97/3.76 % (3474231)------------------------------
% 19.97/3.76 % (3474231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.87/5.01 % (3474231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.87/5.01 % (3474231)CaDiCaL version: 2.1.3
% 28.87/5.01 % (3474231)Termination reason: Instruction limit
% 28.87/5.01 % (3474231)Termination phase: Saturation
% 28.87/5.01 % (3474231)Time elapsed: 0.053 s
% 28.87/5.01 % (3474231)Peak memory usage: 91 MB
% 28.87/5.01 % (3474231)Instructions burned: 159 (million)
% 28.87/5.01 % (3474234)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1441018328:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 28.87/5.01 % (3474234)Instruction limit reached!
% 28.87/5.01 % (3474234)------------------------------
% 28.87/5.01 % (3474234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.87/5.01 % (3474234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.87/5.01 % (3474234)CaDiCaL version: 2.1.3
% 28.87/5.01 % (3474234)Termination reason: Instruction limit
% 28.87/5.01 % (3474234)Termination phase: Saturation
% 28.87/5.01 % (3474234)Time elapsed: 0.069 s
% 28.87/5.01 % (3474234)Peak memory usage: 89 MB
% 28.87/5.01 % (3474234)Instructions burned: 107 (million)
% 28.87/5.01 % (3474238)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3786725224:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 28.87/5.01 % (3474238)Instruction limit reached!
% 28.87/5.01 % (3474238)------------------------------
% 28.87/5.01 % (3474238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.87/5.01 % (3474238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.87/5.01 % (3474238)CaDiCaL version: 2.1.3
% 28.87/5.01 % (3474238)Termination reason: Instruction limit
% 28.87/5.01 % (3474238)Termination phase: Saturation
% 28.87/5.01 % (3474238)Time elapsed: 0.084 s
% 28.87/5.01 % (3474238)Peak memory usage: 90 MB
% 28.87/5.01 % (3474238)Instructions burned: 244 (million)
% 28.87/5.01 % (3474233)------------------------------
% 28.87/5.01 % (3474233)------------------------------
% 28.87/5.01 % (3474240)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3815964265:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 28.87/5.01 % (3474242)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3288717971:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 28.87/5.01 % (3474242)Refutation not found, incomplete strategy
% 28.87/5.01 % (3474242)------------------------------
% 28.87/5.01 % (3474242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.87/5.01 % (3474242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.87/5.01 % (3474242)CaDiCaL version: 2.1.3
% 28.87/5.01 % (3474242)Termination reason: Refutation not found, incomplete strategy
% 28.87/5.01 % (3474242)Time elapsed: 0.0000 s
% 28.87/5.01 % (3474242)Peak memory usage: 87 MB
% 28.87/5.01 % (3474243)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=443021013:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 28.87/5.01 % (3474242)------------------------------
% 28.87/5.01 % (3474242)------------------------------
% 28.87/5.01 % (3474247)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1872782086:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 28.87/5.01 % (3474247)Instruction limit reached!
% 28.87/5.01 % (3474247)------------------------------
% 28.87/5.01 % (3474247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.87/5.01 % (3474247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.87/5.01 % (3474247)CaDiCaL version: 2.1.3
% 28.87/5.01 % (3474247)Termination reason: Instruction limit
% 28.87/5.01 % (3474247)Termination phase: Saturation
% 28.87/5.01 % (3474247)Time elapsed: 0.066 s
% 28.87/5.01 % (3474247)Peak memory usage: 90 MB
% 28.87/5.01 % (3474247)Instructions burned: 193 (million)
% 28.87/5.01 % (3474243)Instruction limit reached!
% 28.87/5.01 % (3474243)------------------------------
% 28.87/5.01 % (3474243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.87/5.01 % (3474243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.87/5.01 % (3474243)CaDiCaL version: 2.1.3
% 28.87/5.01 % (3474243)Termination reason: Instruction limit
% 28.87/5.01 % (3474243)Termination phase: Saturation
% 28.87/5.01 % (3474243)Time elapsed: 0.301 s
% 28.87/5.01 % (3474243)Peak memory usage: 95 MB
% 47.60/7.66 % (3474243)Instructions burned: 501 (million)
% 47.60/7.66 % (3474249)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3114950326:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 47.60/7.66 % (3474250)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2658615345:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 47.60/7.66 % (3474249)Instruction limit reached!
% 47.60/7.66 % (3474249)------------------------------
% 47.60/7.66 % (3474249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.60/7.66 % (3474249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.60/7.66 % (3474249)CaDiCaL version: 2.1.3
% 47.60/7.66 % (3474249)Termination reason: Instruction limit
% 47.60/7.66 % (3474249)Termination phase: Saturation
% 47.60/7.66 % (3474249)Time elapsed: 0.088 s
% 47.60/7.66 % (3474249)Peak memory usage: 92 MB
% 47.60/7.66 % (3474249)Instructions burned: 266 (million)
% 47.60/7.66 % (3474250)Instruction limit reached!
% 47.60/7.66 % (3474250)------------------------------
% 47.60/7.66 % (3474250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.60/7.66 % (3474250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.60/7.66 % (3474250)CaDiCaL version: 2.1.3
% 47.60/7.66 % (3474250)Termination reason: Instruction limit
% 47.60/7.66 % (3474250)Termination phase: Saturation
% 47.60/7.66 % (3474250)Time elapsed: 0.094 s
% 47.60/7.66 % (3474250)Peak memory usage: 89 MB
% 47.60/7.66 % (3474250)Instructions burned: 156 (million)
% 47.60/7.66 % (3474253)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=1414604087:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 47.60/7.66 % (3474254)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2083863179:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 47.60/7.66 % (3474254)Refutation not found, incomplete strategy
% 47.60/7.66 % (3474254)------------------------------
% 47.60/7.66 % (3474254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.60/7.66 % (3474254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.60/7.66 % (3474254)CaDiCaL version: 2.1.3
% 47.60/7.66 % (3474254)Termination reason: Refutation not found, incomplete strategy
% 47.60/7.66 % (3474254)Time elapsed: 0.001 s
% 47.60/7.66 % (3474254)Peak memory usage: 87 MB
% 47.60/7.66 % (3474254)------------------------------
% 47.60/7.66 % (3474254)------------------------------
% 47.60/7.66 % (3474257)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4100626386:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 47.60/7.66 % (3474257)Instruction limit reached!
% 47.60/7.66 % (3474257)------------------------------
% 47.60/7.66 % (3474257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.60/7.66 % (3474257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.60/7.66 % (3474257)CaDiCaL version: 2.1.3
% 47.60/7.66 % (3474257)Termination reason: Instruction limit
% 47.60/7.66 % (3474257)Termination phase: Saturation
% 47.60/7.66 % (3474257)Time elapsed: 0.105 s
% 47.60/7.66 % (3474257)Peak memory usage: 91 MB
% 47.60/7.66 % (3474257)Instructions burned: 182 (million)
% 47.60/7.66 % (3474259)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=958447492:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 47.60/7.66 % (3474253)Instruction limit reached!
% 47.60/7.66 % (3474253)------------------------------
% 47.60/7.66 % (3474253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.60/7.66 % (3474253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.60/7.66 % (3474253)CaDiCaL version: 2.1.3
% 47.60/7.66 % (3474253)Termination reason: Instruction limit
% 47.60/7.66 % (3474253)Termination phase: Saturation
% 47.60/7.66 % (3474253)Time elapsed: 0.919 s
% 47.60/7.66 % (3474253)Peak memory usage: 134 MB
% 47.60/7.66 % (3474253)Instructions burned: 3260 (million)
% 47.60/7.66 % (3474261)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=2074082540:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 47.60/7.66 % (3474232)Instruction limit reached!
% 47.60/7.66 % (3474232)------------------------------
% 66.58/10.26 % (3474232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.58/10.26 % (3474232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.58/10.26 % (3474232)CaDiCaL version: 2.1.3
% 66.58/10.26 % (3474232)Termination reason: Instruction limit
% 66.58/10.26 % (3474232)Termination phase: Saturation
% 66.58/10.26 % (3474232)Time elapsed: 2.096 s
% 66.58/10.26 % (3474232)Peak memory usage: 150 MB
% 66.58/10.26 % (3474232)Instructions burned: 3395 (million)
% 66.58/10.26 % (3474261)Instruction limit reached!
% 66.58/10.26 % (3474261)------------------------------
% 66.58/10.26 % (3474261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.58/10.26 % (3474261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.58/10.26 % (3474261)CaDiCaL version: 2.1.3
% 66.58/10.26 % (3474261)Termination reason: Instruction limit
% 66.58/10.26 % (3474261)Termination phase: Saturation
% 66.58/10.26 % (3474261)Time elapsed: 0.109 s
% 66.58/10.26 % (3474261)Peak memory usage: 90 MB
% 66.58/10.26 % (3474261)Instructions burned: 414 (million)
% 66.58/10.26 % (3474263)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=886979762:s2pl=no:i=8478:s2at=4:nm=6_2970 on theBenchmark for (2970ds/8478Mi)
% 66.58/10.26 % (3474264)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=2708178634:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 66.58/10.26 % (3474264)Refutation not found, incomplete strategy
% 66.58/10.26 % (3474264)------------------------------
% 66.58/10.26 % (3474264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.58/10.26 % (3474264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.58/10.26 % (3474264)CaDiCaL version: 2.1.3
% 66.58/10.26 % (3474264)Termination reason: Refutation not found, incomplete strategy
% 66.58/10.26 % (3474264)Time elapsed: 0.001 s
% 66.58/10.26 % (3474264)Peak memory usage: 88 MB
% 66.58/10.26 % (3474264)Instructions burned: 1 (million)
% 66.58/10.26 % (3474264)------------------------------
% 66.58/10.26 % (3474264)------------------------------
% 66.58/10.26 % (3474267)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=400774069:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi)
% 66.58/10.26 % (3474267)Refutation not found, incomplete strategy
% 66.58/10.26 % (3474267)------------------------------
% 66.58/10.26 % (3474267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.58/10.26 % (3474267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.58/10.26 % (3474267)CaDiCaL version: 2.1.3
% 66.58/10.26 % (3474267)Termination reason: Refutation not found, incomplete strategy
% 66.58/10.26 % (3474267)Time elapsed: 0.002 s
% 66.58/10.26 % (3474267)Peak memory usage: 88 MB
% 66.58/10.26 % (3474267)Instructions burned: 6 (million)
% 66.58/10.26 % (3474267)------------------------------
% 66.58/10.26 % (3474267)------------------------------
% 66.58/10.26 % (3474269)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4163247898:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi)
% 66.58/10.26 % (3474269)Refutation not found, incomplete strategy
% 66.58/10.26 % (3474269)------------------------------
% 66.58/10.26 % (3474269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.58/10.26 % (3474269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.58/10.26 % (3474269)CaDiCaL version: 2.1.3
% 66.58/10.26 % (3474269)Termination reason: Refutation not found, incomplete strategy
% 66.58/10.26 % (3474269)Time elapsed: 0.002 s
% 66.58/10.26 % (3474269)Peak memory usage: 88 MB
% 66.58/10.26 % (3474269)Instructions burned: 1 (million)
% 66.58/10.26 % (3474269)------------------------------
% 66.58/10.26 % (3474269)------------------------------
% 66.58/10.26 % (3474271)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=639846969:i=2989:sd=3:ss=axioms:sgt=60_2960 on theBenchmark for (2960ds/2989Mi)
% 66.58/10.26 % (3474240)Instruction limit reached!
% 66.58/10.26 % (3474240)------------------------------
% 66.58/10.26 % (3474240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.58/10.26 % (3474240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.46/13.87 % (3474240)CaDiCaL version: 2.1.3
% 91.46/13.87 % (3474240)Termination reason: Instruction limit
% 91.46/13.87 % (3474240)Termination phase: Saturation
% 91.46/13.87 % (3474240)Time elapsed: 3.047 s
% 91.46/13.87 % (3474240)Peak memory usage: 148 MB
% 91.46/13.87 % (3474240)Instructions burned: 5210 (million)
% 91.46/13.87 % (3474273)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=3842654615:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2958 on theBenchmark for (2958ds/1997Mi)
% 91.46/13.87 % (3474273)Instruction limit reached!
% 91.46/13.87 % (3474273)------------------------------
% 91.46/13.87 % (3474273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.46/13.87 % (3474273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.46/13.87 % (3474273)CaDiCaL version: 2.1.3
% 91.46/13.87 % (3474273)Termination reason: Instruction limit
% 91.46/13.87 % (3474273)Termination phase: Saturation
% 91.46/13.87 % (3474273)Time elapsed: 1.246 s
% 91.46/13.87 % (3474273)Peak memory usage: 138 MB
% 91.46/13.87 % (3474273)Instructions burned: 1998 (million)
% 91.46/13.87 % (3474275)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=3889888216:i=2088:bd=preordered:av=off_2944 on theBenchmark for (2944ds/2088Mi)
% 91.46/13.87 % (3474271)Instruction limit reached!
% 91.46/13.87 % (3474271)------------------------------
% 91.46/13.87 % (3474271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.46/13.87 % (3474271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.46/13.87 % (3474271)CaDiCaL version: 2.1.3
% 91.46/13.87 % (3474271)Termination reason: Instruction limit
% 91.46/13.87 % (3474271)Termination phase: Saturation
% 91.46/13.87 % (3474271)Time elapsed: 1.721 s
% 91.46/13.87 % (3474271)Peak memory usage: 147 MB
% 91.46/13.87 % (3474271)Instructions burned: 2989 (million)
% 91.46/13.87 % (3474277)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=71685574:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi)
% 91.46/13.87 % (3474263)Instruction limit reached!
% 91.46/13.87 % (3474263)------------------------------
% 91.46/13.87 % (3474263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.46/13.87 % (3474263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.46/13.87 % (3474263)CaDiCaL version: 2.1.3
% 91.46/13.87 % (3474263)Termination reason: Instruction limit
% 91.46/13.87 % (3474263)Termination phase: Saturation
% 91.46/13.87 % (3474263)Time elapsed: 2.964 s
% 91.46/13.87 % (3474263)Peak memory usage: 149 MB
% 91.46/13.87 % (3474263)Instructions burned: 8478 (million)
% 91.46/13.87 % (3474279)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3808710936:i=433:bd=preordered_2939 on theBenchmark for (2939ds/433Mi)
% 91.46/13.87 % (3474279)Instruction limit reached!
% 91.46/13.87 % (3474279)------------------------------
% 91.46/13.87 % (3474279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.46/13.87 % (3474279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.46/13.87 % (3474279)CaDiCaL version: 2.1.3
% 91.46/13.87 % (3474279)Termination reason: Instruction limit
% 91.46/13.87 % (3474279)Termination phase: Saturation
% 91.46/13.87 % (3474279)Time elapsed: 0.126 s
% 91.46/13.87 % (3474279)Peak memory usage: 92 MB
% 91.46/13.87 % (3474279)Instructions burned: 436 (million)
% 91.46/13.87 % (3474281)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4176905073:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2937 on theBenchmark for (2937ds/2942Mi)
% 91.46/13.87 % (3474277)Instruction limit reached!
% 91.46/13.87 % (3474277)------------------------------
% 91.46/13.87 % (3474277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.46/13.87 % (3474277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.46/13.87 % (3474277)CaDiCaL version: 2.1.3
% 91.46/13.87 % (3474277)Termination reason: Instruction limit
% 91.46/13.87 % (3474277)Termination phase: Saturation
% 91.46/13.87 % (3474277)Time elapsed: 0.651 s
% 91.46/13.87 % (3474277)Peak memory usage: 107 MB
% 91.46/13.87 % (3474277)Instructions burned: 1098 (million)
% 91.46/13.87 % (3474283)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2962174916:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2933 on theBenchmark for (2933ds/6922Mi)
% 106.08/16.03 % (3474275)Instruction limit reached!
% 106.08/16.03 % (3474275)------------------------------
% 106.08/16.03 % (3474275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.08/16.03 % (3474275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.08/16.03 % (3474275)CaDiCaL version: 2.1.3
% 106.08/16.03 % (3474275)Termination reason: Instruction limit
% 106.08/16.03 % (3474275)Termination phase: Saturation
% 106.08/16.03 % (3474275)Time elapsed: 1.281 s
% 106.08/16.03 % (3474275)Peak memory usage: 136 MB
% 106.08/16.03 % (3474275)Instructions burned: 2089 (million)
% 106.08/16.03 % (3474285)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=1302991077:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2929 on theBenchmark for (2929ds/596Mi)
% 106.08/16.03 % (3474281)Instruction limit reached!
% 106.08/16.03 % (3474281)------------------------------
% 106.08/16.03 % (3474281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.08/16.03 % (3474281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.08/16.03 % (3474281)CaDiCaL version: 2.1.3
% 106.08/16.03 % (3474281)Termination reason: Instruction limit
% 106.08/16.03 % (3474281)Termination phase: Saturation
% 106.08/16.03 % (3474281)Time elapsed: 1.094 s
% 106.08/16.03 % (3474281)Peak memory usage: 142 MB
% 106.08/16.03 % (3474281)Instructions burned: 2942 (million)
% 106.08/16.03 % (3474285)Instruction limit reached!
% 106.08/16.03 % (3474285)------------------------------
% 106.08/16.03 % (3474285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.08/16.03 % (3474285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.08/16.03 % (3474285)CaDiCaL version: 2.1.3
% 106.08/16.03 % (3474285)Termination reason: Instruction limit
% 106.08/16.03 % (3474285)Termination phase: Saturation
% 106.08/16.03 % (3474285)Time elapsed: 0.314 s
% 106.08/16.03 % (3474285)Peak memory usage: 98 MB
% 106.08/16.03 % (3474285)Instructions burned: 597 (million)
% 106.08/16.03 % (3474287)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=1986207703:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2924 on theBenchmark for (2924ds/4123Mi)
% 106.08/16.03 % (3474288)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3846915725:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi)
% 106.08/16.03 % (3474259)Instruction limit reached!
% 106.08/16.03 % (3474259)------------------------------
% 106.08/16.03 % (3474259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.08/16.03 % (3474259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.08/16.03 % (3474259)CaDiCaL version: 2.1.3
% 106.08/16.03 % (3474259)Termination reason: Instruction limit
% 106.08/16.03 % (3474259)Termination phase: Saturation
% 106.08/16.03 % (3474259)Time elapsed: 6.005 s
% 106.08/16.03 % (3474259)Peak memory usage: 172 MB
% 106.08/16.03 % (3474259)Instructions burned: 10308 (million)
% 106.08/16.03 % (3474291)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3722015006:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2913 on theBenchmark for (2913ds/1670Mi)
% 106.08/16.03 % (3474287)Instruction limit reached!
% 106.08/16.03 % (3474287)------------------------------
% 106.08/16.03 % (3474287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.08/16.03 % (3474287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 106.08/16.03 % (3474287)CaDiCaL version: 2.1.3
% 106.08/16.03 % (3474287)Termination reason: Instruction limit
% 106.08/16.03 % (3474287)Termination phase: Saturation
% 106.08/16.03 % (3474287)Time elapsed: 1.317 s
% 106.08/16.03 % (3474287)Peak memory usage: 160 MB
% 106.08/16.03 % (3474287)Instructions burned: 4126 (million)
% 106.08/16.03 % (3474293)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=488741987:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2910 on theBenchmark for (2910ds/1722Mi)
% 106.08/16.03 % (3474293)Refutation not found, incomplete strategy
% 106.08/16.03 % (3474293)------------------------------
% 106.08/16.03 % (3474293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 106.08/16.03 % (3474293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.98/18.31 % (3474293)CaDiCaL version: 2.1.3
% 123.98/18.31 % (3474293)Termination reason: Refutation not found, incomplete strategy
% 123.98/18.31 % (3474293)Time elapsed: 0.313 s
% 123.98/18.31 % (3474293)Peak memory usage: 128 MB
% 123.98/18.31 % (3474293)Instructions burned: 868 (million)
% 123.98/18.31 % (3474293)------------------------------
% 123.98/18.31 % (3474293)------------------------------
% 123.98/18.31 % (3474295)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=4201244159:cts=off:cond=on:i=9530:bs=on:fsd=on_2904 on theBenchmark for (2904ds/9530Mi)
% 123.98/18.31 % (3474291)Instruction limit reached!
% 123.98/18.31 % (3474291)------------------------------
% 123.98/18.31 % (3474291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.98/18.31 % (3474291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.98/18.31 % (3474291)CaDiCaL version: 2.1.3
% 123.98/18.31 % (3474291)Termination reason: Instruction limit
% 123.98/18.31 % (3474291)Termination phase: Saturation
% 123.98/18.31 % (3474291)Time elapsed: 1.047 s
% 123.98/18.31 % (3474291)Peak memory usage: 136 MB
% 123.98/18.31 % (3474291)Instructions burned: 1671 (million)
% 123.98/18.31 % (3474297)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1178722575:st=2:i=4495:sd=10:ss=included_2901 on theBenchmark for (2901ds/4495Mi)
% 123.98/18.31 % (3474283)Instruction limit reached!
% 123.98/18.31 % (3474283)------------------------------
% 123.98/18.31 % (3474283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.98/18.31 % (3474283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.98/18.31 % (3474283)CaDiCaL version: 2.1.3
% 123.98/18.31 % (3474283)Termination reason: Instruction limit
% 123.98/18.31 % (3474283)Termination phase: Saturation
% 123.98/18.31 % (3474283)Time elapsed: 3.716 s
% 123.98/18.31 % (3474283)Peak memory usage: 187 MB
% 123.98/18.31 % (3474283)Instructions burned: 6923 (million)
% 123.98/18.31 % (3474297)Refutation not found, incomplete strategy
% 123.98/18.31 % (3474297)------------------------------
% 123.98/18.31 % (3474297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.98/18.31 % (3474297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.98/18.31 % (3474297)CaDiCaL version: 2.1.3
% 123.98/18.31 % (3474297)Termination reason: Refutation not found, incomplete strategy
% 123.98/18.31 % (3474297)Time elapsed: 0.566 s
% 123.98/18.31 % (3474297)Peak memory usage: 127 MB
% 123.98/18.31 % (3474297)Instructions burned: 853 (million)
% 123.98/18.31 % (3474299)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=2423528555:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2894 on theBenchmark for (2894ds/4920Mi)
% 123.98/18.31 % (3474297)------------------------------
% 123.98/18.31 % (3474297)------------------------------
% 123.98/18.31 % (3474301)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=2552272703:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2891 on theBenchmark for (2891ds/2083Mi)
% 123.98/18.31 % (3474301)Instruction limit reached!
% 123.98/18.31 % (3474301)------------------------------
% 123.98/18.31 % (3474301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.98/18.31 % (3474301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.98/18.31 % (3474301)CaDiCaL version: 2.1.3
% 123.98/18.31 % (3474301)Termination reason: Instruction limit
% 123.98/18.31 % (3474301)Termination phase: Saturation
% 123.98/18.31 % (3474301)Time elapsed: 1.297 s
% 123.98/18.31 % (3474301)Peak memory usage: 138 MB
% 123.98/18.31 % (3474301)Instructions burned: 2084 (million)
% 123.98/18.31 % (3474303)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=2402033134:i=4629:av=off:gsp=on_2877 on theBenchmark for (2877ds/4629Mi)
% 123.98/18.31 % (3474295)Instruction limit reached!
% 123.98/18.31 % (3474295)------------------------------
% 123.98/18.31 % (3474295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 123.98/18.31 % (3474295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 123.98/18.31 % (3474295)CaDiCaL version: 2.1.3
% 123.98/18.31 % (3474295)Termination reason: Instruction limit
% 123.98/18.31 % (3474295)Termination phase: Saturation
% 123.98/18.31 % (3474295)Time elapsed: 3.340 s
% 143.35/21.07 % (3474295)Peak memory usage: 176 MB
% 143.35/21.07 % (3474295)Instructions burned: 9532 (million)
% 143.35/21.07 % (3474305)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3425933139:i=1258:av=off_2869 on theBenchmark for (2869ds/1258Mi)
% 143.35/21.07 % (3474299)Instruction limit reached!
% 143.35/21.07 % (3474299)------------------------------
% 143.35/21.07 % (3474299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.35/21.07 % (3474299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.35/21.07 % (3474299)CaDiCaL version: 2.1.3
% 143.35/21.07 % (3474299)Termination reason: Instruction limit
% 143.35/21.07 % (3474299)Termination phase: Saturation
% 143.35/21.07 % (3474299)Time elapsed: 2.688 s
% 143.35/21.07 % (3474299)Peak memory usage: 153 MB
% 143.35/21.07 % (3474299)Instructions burned: 4921 (million)
% 143.35/21.07 % (3474305)Instruction limit reached!
% 143.35/21.07 % (3474305)------------------------------
% 143.35/21.07 % (3474305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.35/21.07 % (3474305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.35/21.07 % (3474305)CaDiCaL version: 2.1.3
% 143.35/21.07 % (3474305)Termination reason: Instruction limit
% 143.35/21.07 % (3474305)Termination phase: Saturation
% 143.35/21.07 % (3474305)Time elapsed: 0.382 s
% 143.35/21.07 % (3474305)Peak memory usage: 99 MB
% 143.35/21.07 % (3474305)Instructions burned: 1260 (million)
% 143.35/21.07 % (3474307)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=166951623:i=7343:av=off:ss=included_2866 on theBenchmark for (2866ds/7343Mi)
% 143.35/21.07 % (3474308)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2833921868:i=1325:sd=2:ss=axioms:sgt=16_2864 on theBenchmark for (2864ds/1325Mi)
% 143.35/21.07 % (3474308)Refutation not found, incomplete strategy
% 143.35/21.07 % (3474308)------------------------------
% 143.35/21.07 % (3474308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.35/21.07 % (3474308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.35/21.07 % (3474308)CaDiCaL version: 2.1.3
% 143.35/21.07 % (3474308)Termination reason: Refutation not found, incomplete strategy
% 143.35/21.07 % (3474308)Time elapsed: 0.0000 s
% 143.35/21.07 % (3474308)Peak memory usage: 87 MB
% 143.35/21.07 % (3474308)------------------------------
% 143.35/21.07 % (3474308)------------------------------
% 143.35/21.07 % (3474311)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=2485189760:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2862 on theBenchmark for (2862ds/2646Mi)
% 143.35/21.07 % (3474307)Refutation not found, incomplete strategy
% 143.35/21.07 % (3474307)------------------------------
% 143.35/21.07 % (3474307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.35/21.07 % (3474307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.35/21.07 % (3474307)CaDiCaL version: 2.1.3
% 143.35/21.07 % (3474307)Termination reason: Refutation not found, incomplete strategy
% 143.35/21.07 % (3474307)Time elapsed: 0.584 s
% 143.35/21.07 % (3474307)Peak memory usage: 127 MB
% 143.35/21.07 % (3474307)Instructions burned: 858 (million)
% 143.35/21.07 % (3474307)------------------------------
% 143.35/21.07 % (3474307)------------------------------
% 143.35/21.07 % (3474313)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3331333831:i=1489:sd=2:ep=R:ss=axioms_2855 on theBenchmark for (2855ds/1489Mi)
% 143.35/21.07 % (3474311)Instruction limit reached!
% 143.35/21.07 % (3474311)------------------------------
% 143.35/21.07 % (3474311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.35/21.07 % (3474311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.35/21.07 % (3474311)CaDiCaL version: 2.1.3
% 143.35/21.07 % (3474311)Termination reason: Instruction limit
% 143.35/21.07 % (3474311)Termination phase: Saturation
% 143.35/21.07 % (3474311)Time elapsed: 0.848 s
% 143.35/21.07 % (3474311)Peak memory usage: 136 MB
% 143.35/21.07 % (3474311)Instructions burned: 2648 (million)
% 143.35/21.07 % (3474315)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=1509931801:i=1503_2852 on theBenchmark for (2852ds/1503Mi)
% 143.35/21.07 % (3474313)Refutation not found, incomplete strategy
% 143.35/21.07 % (3474313)------------------------------
% 143.35/21.07 % (3474313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.61/23.73 % (3474313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.61/23.73 % (3474313)CaDiCaL version: 2.1.3
% 161.61/23.73 % (3474313)Termination reason: Refutation not found, incomplete strategy
% 161.61/23.73 % (3474313)Time elapsed: 0.592 s
% 161.61/23.73 % (3474313)Peak memory usage: 127 MB
% 161.61/23.73 % (3474313)Instructions burned: 884 (million)
% 161.61/23.73 % (3474303)Instruction limit reached!
% 161.61/23.73 % (3474303)------------------------------
% 161.61/23.73 % (3474303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.61/23.73 % (3474303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.61/23.73 % (3474303)CaDiCaL version: 2.1.3
% 161.61/23.73 % (3474303)Termination reason: Instruction limit
% 161.61/23.73 % (3474303)Termination phase: Saturation
% 161.61/23.73 % (3474303)Time elapsed: 2.754 s
% 161.61/23.73 % (3474303)Peak memory usage: 161 MB
% 161.61/23.73 % (3474303)Instructions burned: 4630 (million)
% 161.61/23.73 % (3474317)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2684502185:i=13942:kws=frequency_2847 on theBenchmark for (2847ds/13942Mi)
% 161.61/23.73 % (3474315)Instruction limit reached!
% 161.61/23.73 % (3474315)------------------------------
% 161.61/23.73 % (3474315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.61/23.73 % (3474315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.61/23.73 % (3474315)CaDiCaL version: 2.1.3
% 161.61/23.73 % (3474315)Termination reason: Instruction limit
% 161.61/23.73 % (3474315)Termination phase: Saturation
% 161.61/23.73 % (3474315)Time elapsed: 0.504 s
% 161.61/23.73 % (3474315)Peak memory usage: 136 MB
% 161.61/23.73 % (3474315)Instructions burned: 1504 (million)
% 161.61/23.73 % (3474313)------------------------------
% 161.61/23.73 % (3474313)------------------------------
% 161.61/23.73 % (3474319)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=1296352694:i=3604:fsr=off:er=filter_2845 on theBenchmark for (2845ds/3604Mi)
% 161.61/23.73 % (3474320)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3736982622:i=1876:sd=1:ss=included:sgt=32_2845 on theBenchmark for (2845ds/1876Mi)
% 161.61/23.73 % (3474288)Instruction limit reached!
% 161.61/23.73 % (3474288)------------------------------
% 161.61/23.73 % (3474288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.61/23.73 % (3474288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.61/23.73 % (3474288)CaDiCaL version: 2.1.3
% 161.61/23.73 % (3474288)Termination reason: Instruction limit
% 161.61/23.73 % (3474288)Termination phase: Saturation
% 161.61/23.73 % (3474288)Time elapsed: 9.012 s
% 161.61/23.73 % (3474288)Peak memory usage: 202 MB
% 161.61/23.73 % (3474288)Instructions burned: 16411 (million)
% 161.61/23.73 % (3474320)Instruction limit reached!
% 161.61/23.73 % (3474320)------------------------------
% 161.61/23.73 % (3474320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.61/23.73 % (3474320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.61/23.73 % (3474320)CaDiCaL version: 2.1.3
% 161.61/23.73 % (3474320)Termination reason: Instruction limit
% 161.61/23.73 % (3474320)Termination phase: Saturation
% 161.61/23.73 % (3474320)Time elapsed: 1.206 s
% 161.61/23.73 % (3474320)Peak memory usage: 137 MB
% 161.61/23.73 % (3474320)Instructions burned: 1877 (million)
% 161.61/23.73 % (3474323)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2466586870:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2832 on theBenchmark for (2832ds/1932Mi)
% 161.61/23.73 % (3474324)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=2074057512:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2832 on theBenchmark for (2832ds/1980Mi)
% 161.61/23.73 % (3474319)Instruction limit reached!
% 161.61/23.73 % (3474319)------------------------------
% 161.61/23.73 % (3474319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.61/23.73 % (3474319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.61/23.73 % (3474319)CaDiCaL version: 2.1.3
% 161.61/23.73 % (3474319)Termination reason: Instruction limit
% 161.61/23.73 % (3474319)Termination phase: Saturation
% 161.61/23.73 % (3474319)Time elapsed: 1.932 s
% 100.90/26.42 % (3474319)Peak memory usage: 138 MB
% 100.90/26.42 % (3474319)Instructions burned: 3604 (million)
% 100.90/26.42 % (3474323)Refutation not found, incomplete strategy
% 100.90/26.42 % (3474323)------------------------------
% 100.90/26.42 % (3474323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474323)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474323)Termination reason: Refutation not found, incomplete strategy
% 100.90/26.42 % (3474323)Time elapsed: 0.594 s
% 100.90/26.42 % (3474323)Peak memory usage: 127 MB
% 100.90/26.42 % (3474323)Instructions burned: 888 (million)
% 100.90/26.42 % (3474327)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=1181351887:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2825 on theBenchmark for (2825ds/3902Mi)
% 100.90/26.42 % (3474323)------------------------------
% 100.90/26.42 % (3474323)------------------------------
% 100.90/26.42 % (3474329)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2047614946:avsq=on:i=3916:aac=none:amm=off_2822 on theBenchmark for (2822ds/3916Mi)
% 100.90/26.42 % (3474327)Refutation not found, incomplete strategy
% 100.90/26.42 % (3474327)------------------------------
% 100.90/26.42 % (3474327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474327)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474327)Termination reason: Refutation not found, incomplete strategy
% 100.90/26.42 % (3474327)Time elapsed: 0.591 s
% 100.90/26.42 % (3474327)Peak memory usage: 127 MB
% 100.90/26.42 % (3474327)Instructions burned: 888 (million)
% 100.90/26.42 % (3474324)Instruction limit reached!
% 100.90/26.42 % (3474324)------------------------------
% 100.90/26.42 % (3474324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474324)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474324)Termination reason: Instruction limit
% 100.90/26.42 % (3474324)Termination phase: Saturation
% 100.90/26.42 % (3474324)Time elapsed: 1.273 s
% 100.90/26.42 % (3474324)Peak memory usage: 137 MB
% 100.90/26.42 % (3474324)Instructions burned: 1981 (million)
% 100.90/26.42 % (3474331)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2083064690:cond=on:i=3940:av=off:er=known_2817 on theBenchmark for (2817ds/3940Mi)
% 100.90/26.42 % (3474327)------------------------------
% 100.90/26.42 % (3474327)------------------------------
% 100.90/26.42 % (3474333)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2071832401:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2815 on theBenchmark for (2815ds/3980Mi)
% 100.90/26.42 % (3474329)Instruction limit reached!
% 100.90/26.42 % (3474329)------------------------------
% 100.90/26.42 % (3474329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474329)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474329)Termination reason: Instruction limit
% 100.90/26.42 % (3474329)Termination phase: Saturation
% 100.90/26.42 % (3474329)Time elapsed: 1.894 s
% 100.90/26.42 % (3474329)Peak memory usage: 117 MB
% 100.90/26.42 % (3474329)Instructions burned: 3917 (million)
% 100.90/26.42 % (3474335)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=2862326821:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2802 on theBenchmark for (2802ds/2087Mi)
% 100.90/26.42 % (3474317)Instruction limit reached!
% 100.90/26.42 % (3474317)------------------------------
% 100.90/26.42 % (3474317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474317)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474317)Termination reason: Instruction limit
% 100.90/26.42 % (3474317)Termination phase: Saturation
% 100.90/26.42 % (3474317)Time elapsed: 4.690 s
% 100.90/26.42 % (3474317)Peak memory usage: 241 MB
% 100.90/26.42 % (3474317)Instructions burned: 13943 (million)
% 100.90/26.42 % (3474337)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=884820846:cts=off:cond=on:i=4272:bs=on:fsd=on_2799 on theBenchmark for (2799ds/4272Mi)
% 100.90/26.42 % (3474331)Instruction limit reached!
% 100.90/26.42 % (3474331)------------------------------
% 100.90/26.42 % (3474331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474331)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474331)Termination reason: Instruction limit
% 100.90/26.42 % (3474331)Termination phase: Saturation
% 100.90/26.42 % (3474331)Time elapsed: 2.313 s
% 100.90/26.42 % (3474331)Peak memory usage: 152 MB
% 100.90/26.42 % (3474331)Instructions burned: 3941 (million)
% 100.90/26.42 % (3474339)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=888441921:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2792 on theBenchmark for (2792ds/2197Mi)
% 100.90/26.42 % (3474333)Instruction limit reached!
% 100.90/26.42 % (3474333)------------------------------
% 100.90/26.42 % (3474333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474333)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474333)Termination reason: Instruction limit
% 100.90/26.42 % (3474333)Termination phase: Saturation
% 100.90/26.42 % (3474333)Time elapsed: 2.499 s
% 100.90/26.42 % (3474333)Peak memory usage: 156 MB
% 100.90/26.42 % (3474333)Instructions burned: 3980 (million)
% 100.90/26.42 % (3474341)dis+21_1_sil=8000:spb=goal_then_units:random_seed=3566247354:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2788 on theBenchmark for (2788ds/6508Mi)
% 100.90/26.42 % (3474335)Instruction limit reached!
% 100.90/26.42 % (3474335)------------------------------
% 100.90/26.42 % (3474335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474335)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474335)Termination reason: Instruction limit
% 100.90/26.42 % (3474335)Termination phase: Saturation
% 100.90/26.42 % (3474335)Time elapsed: 1.364 s
% 100.90/26.42 % (3474335)Peak memory usage: 139 MB
% 100.90/26.42 % (3474335)Instructions burned: 2087 (million)
% 100.90/26.42 % (3474343)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3345928197:i=2330:fgj=on:av=off:fsr=off_2786 on theBenchmark for (2786ds/2330Mi)
% 100.90/26.42 % (3474337)Instruction limit reached!
% 100.90/26.42 % (3474337)------------------------------
% 100.90/26.42 % (3474337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474337)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474337)Termination reason: Instruction limit
% 100.90/26.42 % (3474337)Termination phase: Saturation
% 100.90/26.42 % (3474337)Time elapsed: 1.426 s
% 100.90/26.42 % (3474337)Peak memory usage: 158 MB
% 100.90/26.42 % (3474337)Instructions burned: 4274 (million)
% 100.90/26.42 % (3474345)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=4282894242:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2783 on theBenchmark for (2783ds/7592Mi)
% 100.90/26.42 % (3474339)Instruction limit reached!
% 100.90/26.42 % (3474339)------------------------------
% 100.90/26.42 % (3474339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474339)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474339)Termination reason: Instruction limit
% 100.90/26.42 % (3474339)Termination phase: Saturation
% 100.90/26.42 % (3474339)Time elapsed: 1.309 s
% 100.90/26.42 % (3474339)Peak memory usage: 141 MB
% 100.90/26.42 % (3474339)Instructions burned: 2197 (million)
% 100.90/26.42 % (3474347)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=1000502812:i=2693:kws=precedence:ins=1:av=off_2777 on theBenchmark for (2777ds/2693Mi)
% 100.90/26.42 % (3474343)Instruction limit reached!
% 100.90/26.42 % (3474343)------------------------------
% 100.90/26.42 % (3474343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474343)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474343)Termination reason: Instruction limit
% 100.90/26.42 % (3474343)Termination phase: Saturation
% 100.90/26.42 % (3474343)Time elapsed: 1.375 s
% 100.90/26.42 % (3474343)Peak memory usage: 140 MB
% 100.90/26.42 % (3474343)Instructions burned: 2330 (million)
% 100.90/26.42 % (3474349)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=851662471:i=28651:sd=4:ss=included:sgt=64_2771 on theBenchmark for (2771ds/28651Mi)
% 100.90/26.42 % (3474345)Instruction limit reached!
% 100.90/26.42 % (3474345)------------------------------
% 100.90/26.42 % (3474345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474345)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474345)Termination reason: Instruction limit
% 100.90/26.42 % (3474345)Termination phase: Saturation
% 100.90/26.42 % (3474345)Time elapsed: 1.963 s
% 100.90/26.42 % (3474345)Peak memory usage: 145 MB
% 100.90/26.42 % (3474345)Instructions burned: 7595 (million)
% 100.90/26.42 % (3474351)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1661566801:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2762 on theBenchmark for (2762ds/2700Mi)
% 100.90/26.42 % (3474347)Instruction limit reached!
% 100.90/26.42 % (3474347)------------------------------
% 100.90/26.42 % (3474347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474347)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474347)Termination reason: Instruction limit
% 100.90/26.42 % (3474347)Termination phase: Saturation
% 100.90/26.42 % (3474347)Time elapsed: 1.596 s
% 100.90/26.42 % (3474347)Peak memory usage: 143 MB
% 100.90/26.42 % (3474347)Instructions burned: 2694 (million)
% 100.90/26.42 % (3474353)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=169965318:i=3196:nm=4_2760 on theBenchmark for (2760ds/3196Mi)
% 100.90/26.42 % (3474351)Instruction limit reached!
% 100.90/26.42 % (3474351)------------------------------
% 100.90/26.42 % (3474351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474351)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474351)Termination reason: Instruction limit
% 100.90/26.42 % (3474351)Termination phase: Saturation
% 100.90/26.42 % (3474351)Time elapsed: 0.858 s
% 100.90/26.42 % (3474351)Peak memory usage: 147 MB
% 100.90/26.42 % (3474351)Instructions burned: 2703 (million)
% 100.90/26.42 % (3474355)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1063813341:cts=off:i=3254:av=off_2752 on theBenchmark for (2752ds/3254Mi)
% 100.90/26.42 % (3474341)Instruction limit reached!
% 100.90/26.42 % (3474341)------------------------------
% 100.90/26.42 % (3474341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.90/26.42 % (3474341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.90/26.42 % (3474341)CaDiCaL version: 2.1.3
% 100.90/26.42 % (3474341)Termination reason: Instruction limit
% 100.90/26.42 % (3474341)Termination phase: Saturation
% 100.90/26.42 % (3474341)Time elapsed: 3.668 s
% 100.90/26.42 % (3474341)Peak memory usage: 139 MB
% 100.90/26.42 % (3474341)Instructions burned: 6510 (million)
% 100.90/26.42 % (3474357)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1408068356:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2750 on theBenchmark for (2750ds/3264Mi)
% 100.90/26.42 % (3474349)First to succeed.
% 100.90/26.42 % (3474349)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3474202"
% 100.90/26.42 % (3474349)Refutation found. Thanks to Tanya!
% 100.90/26.42 % SZS status Unsatisfiable for theBenchmark
% 100.90/26.42 % SZS output start Proof for theBenchmark
% See solution above
% 181.43/26.62 % (3474349)------------------------------
% 181.43/26.62 % (3474349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.43/26.62 % (3474349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.43/26.62 % (3474349)CaDiCaL version: 2.1.3
% 181.43/26.62 % (3474349)Termination reason: Refutation
% 181.43/26.62 % (3474349)Time elapsed: 2.171 s
% 181.43/26.62 % (3474349)Peak memory usage: 149 MB
% 181.43/26.62 % (3474349)Instructions burned: 3190 (million)
% 181.43/26.62 % (3474349)------------------------------
% 181.43/26.62 % (3474349)------------------------------
% 181.43/26.62 % (3474202)Success in time 25.557 s
% 181.43/26.62 % Vampire exiting
%------------------------------------------------------------------------------