%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET276-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:40:40 PM UTC 2026
% Result : Unsatisfiable 93.90s 14.10s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 75
% Syntax : Number of formulae : 338 ( 78 unt; 53 def)
% Number of atoms : 799 ( 94 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 844 ( 383 ~; 415 |; 0 &)
% ( 46 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 50 ( 48 usr; 47 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 13 con; 0-3 aty)
% Number of variables : 175 ( 0 sgn 175 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f32,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = restrict(X1,singleton(X0),universal_class)
| member(X0,domain_of(X1)) ),
inference(reorient_equations,[],[f31]) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f122,negated_conjecture,
~ subclass(cross_product(domain_of(restrict(x,y,z)),u),cross_product(intersection(domain_of(x),y),u)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_2_to_domain_property4_1) ).
fof(f127,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f136,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f127]) ).
fof(f137,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f127]) ).
fof(f138,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(definition_unfolding,[],[f16,f127]) ).
fof(f139,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f127]) ).
fof(f143,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f144,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| member(X0,domain_of(X1)) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f185,plain,
~ subclass(cross_product(domain_of(intersection(x,cross_product(y,z))),u),cross_product(intersection(domain_of(x),y),u)),
inference(definition_unfolding,[],[f122,f28]) ).
fof(f190,definition,
sF0 = cross_product(y,z),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f191,plain,
cross_product(y,z) = sF0,
inference(reorient_equations,[],[f190]) ).
fof(f192,definition,
sF1 = intersection(x,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f193,plain,
intersection(x,sF0) = sF1,
inference(reorient_equations,[],[f192]) ).
fof(f194,definition,
sF2 = domain_of(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f195,plain,
domain_of(sF1) = sF2,
inference(reorient_equations,[],[f194]) ).
fof(f196,definition,
sF3 = cross_product(sF2,u),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f197,plain,
cross_product(sF2,u) = sF3,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF4 = domain_of(x),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f199,plain,
domain_of(x) = sF4,
inference(reorient_equations,[],[f198]) ).
fof(f200,definition,
sF5 = intersection(sF4,y),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f201,plain,
intersection(sF4,y) = sF5,
inference(reorient_equations,[],[f200]) ).
fof(f202,definition,
sF6 = cross_product(sF5,u),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f203,plain,
cross_product(sF5,u) = sF6,
inference(reorient_equations,[],[f202]) ).
fof(f204,plain,
~ subclass(sF3,sF6),
inference(definition_folding,[],[f185,f203,f201,f199,f197,f195,f193,f191]) ).
fof(f211,definition,
( spl7_1
<=> cross_product(sF2,u) = sF3 ),
introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition]) ).
fof(f213,plain,
( cross_product(sF2,u) = sF3
| ~ spl7_1 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f214,plain,
spl7_1,
inference(avatar_split_clause,[],[f197,f211]) ).
fof(f216,definition,
( spl7_2
<=> cross_product(sF5,u) = sF6 ),
introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition]) ).
fof(f218,plain,
( cross_product(sF5,u) = sF6
| ~ spl7_2 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f219,plain,
spl7_2,
inference(avatar_split_clause,[],[f203,f216]) ).
fof(f221,definition,
( spl7_3
<=> cross_product(y,z) = sF0 ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
fof(f223,plain,
( cross_product(y,z) = sF0
| ~ spl7_3 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f224,plain,
spl7_3,
inference(avatar_split_clause,[],[f191,f221]) ).
fof(f226,definition,
( spl7_4
<=> intersection(x,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition]) ).
fof(f228,plain,
( intersection(x,sF0) = sF1
| ~ spl7_4 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
spl7_4,
inference(avatar_split_clause,[],[f193,f226]) ).
fof(f233,plain,
( ! [X0] :
( ~ member(X0,sF1)
| member(X0,sF0) )
| ~ spl7_4 ),
inference(superposition,[],[f22,f228]) ).
fof(f234,plain,
( ! [X0] :
( ~ member(X0,sF1)
| member(X0,x) )
| ~ spl7_4 ),
inference(superposition,[],[f21,f228]) ).
fof(f236,plain,
( ! [X0] :
( ~ member(X0,sF3)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 )
| ~ spl7_1 ),
inference(superposition,[],[f139,f213]) ).
fof(f242,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF6)
| member(X0,sF5) )
| ~ spl7_2 ),
inference(superposition,[],[f136,f218]) ).
fof(f246,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,y) )
| ~ spl7_3 ),
inference(superposition,[],[f136,f223]) ).
fof(f256,definition,
( spl7_6
<=> ! [X0] :
( ~ member(X0,sF1)
| member(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition]) ).
fof(f257,plain,
( ! [X0] :
( member(X0,sF0)
| ~ member(X0,sF1) )
| ~ spl7_6 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( spl7_6
| ~ spl7_4 ),
inference(avatar_split_clause,[],[f233,f226,f256]) ).
fof(f260,definition,
( spl7_7
<=> domain_of(x) = sF4 ),
introduced(definition,[new_symbols(definition,[spl7_7])],[avatar_definition]) ).
fof(f262,plain,
( domain_of(x) = sF4
| ~ spl7_7 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f263,plain,
spl7_7,
inference(avatar_split_clause,[],[f199,f260]) ).
fof(f265,definition,
( spl7_8
<=> intersection(sF4,y) = sF5 ),
introduced(definition,[new_symbols(definition,[spl7_8])],[avatar_definition]) ).
fof(f267,plain,
( intersection(sF4,y) = sF5
| ~ spl7_8 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
spl7_8,
inference(avatar_split_clause,[],[f201,f265]) ).
fof(f271,plain,
( ! [X0] :
( member(X0,sF5)
| ~ member(X0,y)
| ~ member(X0,sF4) )
| ~ spl7_8 ),
inference(superposition,[],[f23,f267]) ).
fof(f275,definition,
( spl7_9
<=> ! [X0] :
( member(X0,sF5)
| ~ member(X0,y)
| ~ member(X0,sF4) ) ),
introduced(definition,[new_symbols(definition,[spl7_9])],[avatar_definition]) ).
fof(f276,plain,
( ! [X0] :
( member(X0,sF5)
| ~ member(X0,y)
| ~ member(X0,sF4) )
| ~ spl7_9 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f277,plain,
( spl7_9
| ~ spl7_8 ),
inference(avatar_split_clause,[],[f271,f265,f275]) ).
fof(f283,definition,
( spl7_11
<=> ! [X0] :
( ~ member(X0,sF1)
| member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl7_11])],[avatar_definition]) ).
fof(f284,plain,
( ! [X0] :
( member(X0,x)
| ~ member(X0,sF1) )
| ~ spl7_11 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f285,plain,
( spl7_11
| ~ spl7_4 ),
inference(avatar_split_clause,[],[f234,f226,f283]) ).
fof(f294,definition,
( spl7_13
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl7_13])],[avatar_definition]) ).
fof(f295,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,y) )
| ~ spl7_13 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f296,plain,
( spl7_13
| ~ spl7_3 ),
inference(avatar_split_clause,[],[f246,f221,f294]) ).
fof(f297,plain,
( ! [X0,X1] :
( member(X0,y)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1) )
| ~ spl7_6
| ~ spl7_13 ),
inference(resolution,[],[f295,f257]) ).
fof(f305,definition,
( spl7_15
<=> domain_of(sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl7_15])],[avatar_definition]) ).
fof(f307,plain,
( domain_of(sF1) = sF2
| ~ spl7_15 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f308,plain,
spl7_15,
inference(avatar_split_clause,[],[f195,f305]) ).
fof(f310,definition,
( spl7_16
<=> subclass(sF3,sF6) ),
introduced(definition,[new_symbols(definition,[spl7_16])],[avatar_definition]) ).
fof(f312,plain,
( ~ subclass(sF3,sF6)
| spl7_16 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f313,plain,
~ spl7_16,
inference(avatar_split_clause,[],[f204,f310]) ).
fof(f315,definition,
( spl7_17
<=> ! [X0] :
( ~ member(X0,sF3)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl7_17])],[avatar_definition]) ).
fof(f316,plain,
( ! [X0] :
( ~ member(X0,sF3)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 )
| ~ spl7_17 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f317,plain,
( spl7_17
| ~ spl7_1 ),
inference(avatar_split_clause,[],[f236,f211,f315]) ).
fof(f318,plain,
( ! [X0] :
( not_subclass_element(sF3,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF3,X0)),first(not_subclass_element(sF3,X0))),unordered_pair(first(not_subclass_element(sF3,X0)),unordered_pair(second(not_subclass_element(sF3,X0)),second(not_subclass_element(sF3,X0)))))
| subclass(sF3,X0) )
| ~ spl7_17 ),
inference(resolution,[],[f316,f2]) ).
fof(f320,definition,
( spl7_18
<=> ! [X0] :
( not_subclass_element(sF3,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF3,X0)),first(not_subclass_element(sF3,X0))),unordered_pair(first(not_subclass_element(sF3,X0)),unordered_pair(second(not_subclass_element(sF3,X0)),second(not_subclass_element(sF3,X0)))))
| subclass(sF3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_18])],[avatar_definition]) ).
fof(f321,plain,
( ! [X0] :
( subclass(sF3,X0)
| not_subclass_element(sF3,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF3,X0)),first(not_subclass_element(sF3,X0))),unordered_pair(first(not_subclass_element(sF3,X0)),unordered_pair(second(not_subclass_element(sF3,X0)),second(not_subclass_element(sF3,X0))))) )
| ~ spl7_18 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( spl7_18
| ~ spl7_17 ),
inference(avatar_split_clause,[],[f318,f315,f320]) ).
fof(f323,plain,
( not_subclass_element(sF3,sF6) = unordered_pair(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),unordered_pair(first(not_subclass_element(sF3,sF6)),unordered_pair(second(not_subclass_element(sF3,sF6)),second(not_subclass_element(sF3,sF6)))))
| spl7_16
| ~ spl7_18 ),
inference(resolution,[],[f321,f312]) ).
fof(f325,definition,
( spl7_19
<=> not_subclass_element(sF3,sF6) = unordered_pair(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),unordered_pair(first(not_subclass_element(sF3,sF6)),unordered_pair(second(not_subclass_element(sF3,sF6)),second(not_subclass_element(sF3,sF6))))) ),
introduced(definition,[new_symbols(definition,[spl7_19])],[avatar_definition]) ).
fof(f327,plain,
( not_subclass_element(sF3,sF6) = unordered_pair(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),unordered_pair(first(not_subclass_element(sF3,sF6)),unordered_pair(second(not_subclass_element(sF3,sF6)),second(not_subclass_element(sF3,sF6)))))
| ~ spl7_19 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f328,plain,
( spl7_19
| spl7_16
| ~ spl7_18 ),
inference(avatar_split_clause,[],[f323,f320,f310,f325]) ).
fof(f331,plain,
( ! [X0,X1] :
( member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| ~ member(second(not_subclass_element(sF3,sF6)),X1)
| ~ member(first(not_subclass_element(sF3,sF6)),X0) )
| ~ spl7_19 ),
inference(superposition,[],[f138,f327]) ).
fof(f332,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| member(second(not_subclass_element(sF3,sF6)),X1) )
| ~ spl7_19 ),
inference(superposition,[],[f137,f327]) ).
fof(f333,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| member(first(not_subclass_element(sF3,sF6)),X0) )
| ~ spl7_19 ),
inference(superposition,[],[f136,f327]) ).
fof(f335,definition,
( spl7_20
<=> member(first(not_subclass_element(sF3,sF6)),y) ),
introduced(definition,[new_symbols(definition,[spl7_20])],[avatar_definition]) ).
fof(f337,plain,
( member(first(not_subclass_element(sF3,sF6)),y)
| ~ spl7_20 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f345,definition,
( spl7_22
<=> ! [X0,X1] :
( member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| ~ member(second(not_subclass_element(sF3,sF6)),X1)
| ~ member(first(not_subclass_element(sF3,sF6)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_22])],[avatar_definition]) ).
fof(f346,plain,
( ! [X0,X1] :
( member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| ~ member(second(not_subclass_element(sF3,sF6)),X1)
| ~ member(first(not_subclass_element(sF3,sF6)),X0) )
| ~ spl7_22 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f347,plain,
( spl7_22
| ~ spl7_19 ),
inference(avatar_split_clause,[],[f331,f325,f345]) ).
fof(f349,definition,
( spl7_23
<=> ! [X0,X1] :
( ~ member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| member(first(not_subclass_element(sF3,sF6)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_23])],[avatar_definition]) ).
fof(f350,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| member(first(not_subclass_element(sF3,sF6)),X0) )
| ~ spl7_23 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f351,plain,
( spl7_23
| ~ spl7_19 ),
inference(avatar_split_clause,[],[f333,f325,f349]) ).
fof(f353,definition,
( spl7_24
<=> ! [X0,X1] :
( ~ member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| member(second(not_subclass_element(sF3,sF6)),X1) ) ),
introduced(definition,[new_symbols(definition,[spl7_24])],[avatar_definition]) ).
fof(f354,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(sF3,sF6),cross_product(X0,X1))
| member(second(not_subclass_element(sF3,sF6)),X1) )
| ~ spl7_24 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f355,plain,
( spl7_24
| ~ spl7_19 ),
inference(avatar_split_clause,[],[f332,f325,f353]) ).
fof(f356,plain,
( ~ member(not_subclass_element(sF3,sF6),sF3)
| member(first(not_subclass_element(sF3,sF6)),sF2)
| ~ spl7_1
| ~ spl7_23 ),
inference(superposition,[],[f350,f213]) ).
fof(f365,plain,
( ~ member(not_subclass_element(sF3,sF6),sF3)
| member(second(not_subclass_element(sF3,sF6)),u)
| ~ spl7_1
| ~ spl7_24 ),
inference(superposition,[],[f354,f213]) ).
fof(f372,plain,
( member(not_subclass_element(sF3,sF6),sF6)
| ~ member(second(not_subclass_element(sF3,sF6)),u)
| ~ member(first(not_subclass_element(sF3,sF6)),sF5)
| ~ spl7_2
| ~ spl7_22 ),
inference(superposition,[],[f346,f218]) ).
fof(f382,definition,
( spl7_27
<=> member(first(not_subclass_element(sF3,sF6)),sF5) ),
introduced(definition,[new_symbols(definition,[spl7_27])],[avatar_definition]) ).
fof(f383,plain,
( member(first(not_subclass_element(sF3,sF6)),sF5)
| ~ spl7_27 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f384,plain,
( ~ member(first(not_subclass_element(sF3,sF6)),sF5)
| spl7_27 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f388,definition,
( spl7_28
<=> member(not_subclass_element(sF3,sF6),sF6) ),
introduced(definition,[new_symbols(definition,[spl7_28])],[avatar_definition]) ).
fof(f389,plain,
( member(not_subclass_element(sF3,sF6),sF6)
| ~ spl7_28 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f393,definition,
( spl7_29
<=> member(first(not_subclass_element(sF3,sF6)),sF2) ),
introduced(definition,[new_symbols(definition,[spl7_29])],[avatar_definition]) ).
fof(f395,plain,
( member(first(not_subclass_element(sF3,sF6)),sF2)
| ~ spl7_29 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f397,definition,
( spl7_30
<=> member(not_subclass_element(sF3,sF6),sF3) ),
introduced(definition,[new_symbols(definition,[spl7_30])],[avatar_definition]) ).
fof(f398,plain,
( member(not_subclass_element(sF3,sF6),sF3)
| ~ spl7_30 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f399,plain,
( ~ member(not_subclass_element(sF3,sF6),sF3)
| spl7_30 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f400,plain,
( spl7_29
| ~ spl7_30
| ~ spl7_1
| ~ spl7_23 ),
inference(avatar_split_clause,[],[f356,f349,f211,f397,f393]) ).
fof(f402,plain,
( subclass(sF3,sF6)
| spl7_30 ),
inference(resolution,[],[f399,f2]) ).
fof(f404,plain,
( $false
| spl7_16
| spl7_30 ),
inference(forward_subsumption_resolution,[],[f402,f312]) ).
fof(f405,plain,
( spl7_16
| spl7_30 ),
inference(avatar_contradiction_clause,[],[f404]) ).
fof(f406,plain,
( member(second(not_subclass_element(sF3,sF6)),u)
| ~ spl7_1
| ~ spl7_24
| ~ spl7_30 ),
inference(forward_subsumption_resolution,[],[f365,f398]) ).
fof(f408,definition,
( spl7_31
<=> member(second(not_subclass_element(sF3,sF6)),u) ),
introduced(definition,[new_symbols(definition,[spl7_31])],[avatar_definition]) ).
fof(f410,plain,
( member(second(not_subclass_element(sF3,sF6)),u)
| ~ spl7_31 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f411,plain,
( spl7_31
| ~ spl7_1
| ~ spl7_24
| ~ spl7_30 ),
inference(avatar_split_clause,[],[f406,f397,f353,f211,f408]) ).
fof(f456,plain,
( member(not_subclass_element(sF3,sF6),sF6)
| ~ member(first(not_subclass_element(sF3,sF6)),sF5)
| ~ spl7_2
| ~ spl7_22
| ~ spl7_31 ),
inference(forward_subsumption_resolution,[],[f372,f410]) ).
fof(f457,plain,
( member(not_subclass_element(sF3,sF6),sF6)
| ~ spl7_2
| ~ spl7_22
| ~ spl7_27
| ~ spl7_31 ),
inference(forward_subsumption_resolution,[],[f456,f383]) ).
fof(f459,plain,
( spl7_28
| ~ spl7_2
| ~ spl7_22
| ~ spl7_27
| ~ spl7_31 ),
inference(avatar_split_clause,[],[f457,f408,f382,f345,f216,f388]) ).
fof(f461,plain,
( subclass(sF3,sF6)
| ~ spl7_28 ),
inference(resolution,[],[f389,f3]) ).
fof(f464,plain,
( $false
| spl7_16
| ~ spl7_28 ),
inference(forward_subsumption_resolution,[],[f461,f312]) ).
fof(f465,plain,
( spl7_16
| ~ spl7_28 ),
inference(avatar_contradiction_clause,[],[f464]) ).
fof(f467,plain,
( ~ member(first(not_subclass_element(sF3,sF6)),y)
| ~ member(first(not_subclass_element(sF3,sF6)),sF4)
| ~ spl7_9
| spl7_27 ),
inference(resolution,[],[f384,f276]) ).
fof(f469,plain,
( ~ member(first(not_subclass_element(sF3,sF6)),sF4)
| ~ spl7_9
| ~ spl7_20
| spl7_27 ),
inference(forward_subsumption_resolution,[],[f467,f337]) ).
fof(f471,definition,
( spl7_36
<=> member(first(not_subclass_element(sF3,sF6)),sF4) ),
introduced(definition,[new_symbols(definition,[spl7_36])],[avatar_definition]) ).
fof(f473,plain,
( ~ member(first(not_subclass_element(sF3,sF6)),sF4)
| spl7_36 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f474,plain,
( ~ spl7_36
| ~ spl7_9
| ~ spl7_20
| spl7_27 ),
inference(avatar_split_clause,[],[f469,f382,f335,f275,f471]) ).
fof(f578,plain,
! [X2,X0,X1] :
( null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| member(X1,domain_of(X0))
| ~ member(X1,X2)
| ~ subclass(X2,universal_class) ),
inference(resolution,[],[f144,f1]) ).
fof(f582,plain,
! [X2,X0,X1] :
( member(X1,domain_of(X0))
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,X2) ),
inference(forward_subsumption_resolution,[],[f578,f4]) ).
fof(f584,plain,
( ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl7_7 ),
inference(superposition,[],[f582,f262]) ).
fof(f587,definition,
( spl7_52
<=> ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl7_52])],[avatar_definition]) ).
fof(f588,plain,
( ! [X0,X1] :
( member(X0,sF4)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl7_52 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f589,plain,
( spl7_52
| ~ spl7_7 ),
inference(avatar_split_clause,[],[f584,f260,f587]) ).
fof(f595,plain,
( ! [X0] :
( null_class = intersection(x,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| ~ member(first(not_subclass_element(sF3,sF6)),X0) )
| spl7_36
| ~ spl7_52 ),
inference(resolution,[],[f588,f473]) ).
fof(f597,definition,
( spl7_54
<=> ! [X0] : ~ member(first(not_subclass_element(sF3,sF6)),X0) ),
introduced(definition,[new_symbols(definition,[spl7_54])],[avatar_definition]) ).
fof(f598,plain,
( ! [X0] : ~ member(first(not_subclass_element(sF3,sF6)),X0)
| ~ spl7_54 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f600,definition,
( spl7_55
<=> null_class = intersection(x,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl7_55])],[avatar_definition]) ).
fof(f602,plain,
( null_class = intersection(x,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| ~ spl7_55 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f603,plain,
( spl7_54
| spl7_55
| spl7_36
| ~ spl7_52 ),
inference(avatar_split_clause,[],[f595,f587,f471,f600,f597]) ).
fof(f607,plain,
( $false
| ~ spl7_29
| ~ spl7_54 ),
inference(unit_resulting_resolution,[],[f23,f395,f395,f598]) ).
fof(f628,plain,
( ~ spl7_29
| ~ spl7_54 ),
inference(avatar_contradiction_clause,[],[f607]) ).
fof(f642,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| ~ member(X0,x) )
| ~ spl7_55 ),
inference(superposition,[],[f23,f602]) ).
fof(f747,definition,
( spl7_63
<=> ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl7_63])],[avatar_definition]) ).
fof(f748,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| member(X0,null_class)
| ~ member(X0,x) )
| ~ spl7_63 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f749,plain,
( spl7_63
| ~ spl7_55 ),
inference(avatar_split_clause,[],[f642,f600,f747]) ).
fof(f839,definition,
( spl7_78
<=> ! [X0,X1] :
( member(X0,y)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1) ) ),
introduced(definition,[new_symbols(definition,[spl7_78])],[avatar_definition]) ).
fof(f840,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X0,y) )
| ~ spl7_78 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f841,plain,
( spl7_78
| ~ spl7_6
| ~ spl7_13 ),
inference(avatar_split_clause,[],[f297,f294,f256,f839]) ).
fof(f872,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f928,definition,
( spl7_86
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF6)
| member(X0,sF5) ) ),
introduced(definition,[new_symbols(definition,[spl7_86])],[avatar_definition]) ).
fof(f929,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF6)
| member(X0,sF5) )
| ~ spl7_86 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f930,plain,
( spl7_86
| ~ spl7_2 ),
inference(avatar_split_clause,[],[f242,f216,f928]) ).
fof(f1012,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f1013,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f1030,plain,
! [X2,X0,X1] :
( intersection(X0,cross_product(X1,X2)) = null_class
| regular(intersection(X0,cross_product(X1,X2))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),first(regular(intersection(X0,cross_product(X1,X2))))),unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),unordered_pair(second(regular(intersection(X0,cross_product(X1,X2)))),second(regular(intersection(X0,cross_product(X1,X2))))))) ),
inference(resolution,[],[f1012,f139]) ).
fof(f1048,plain,
! [X0,X1] :
( null_class != null_class
| ~ member(X1,domain_of(X0))
| regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))))) ),
inference(superposition,[],[f143,f1030]) ).
fof(f1057,plain,
! [X0,X1] :
( ~ member(X1,domain_of(X0))
| regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))),unordered_pair(first(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),unordered_pair(second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)))),second(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))))))) ),
inference(trivial_inequality_removal,[],[f1048]) ).
fof(f1069,plain,
( ! [X0] :
( ~ member(X0,sF2)
| regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl7_15 ),
inference(superposition,[],[f1057,f307]) ).
fof(f1084,definition,
( spl7_93
<=> ! [X0] :
( ~ member(X0,sF2)
| regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl7_93])],[avatar_definition]) ).
fof(f1085,plain,
( ! [X0] :
( ~ member(X0,sF2)
| regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl7_93 ),
inference(avatar_component_clause,[],[f1084]) ).
fof(f1086,plain,
( spl7_93
| ~ spl7_15 ),
inference(avatar_split_clause,[],[f1069,f305,f1084]) ).
fof(f1090,plain,
( regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))))))
| ~ spl7_29
| ~ spl7_93 ),
inference(resolution,[],[f1085,f395]) ).
fof(f1099,definition,
( spl7_94
<=> regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl7_94])],[avatar_definition]) ).
fof(f1101,plain,
( regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))))))
| ~ spl7_94 ),
inference(avatar_component_clause,[],[f1099]) ).
fof(f1102,plain,
( spl7_94
| ~ spl7_29
| ~ spl7_93 ),
inference(avatar_split_clause,[],[f1090,f1084,f393,f1099]) ).
fof(f1104,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X0) )
| ~ spl7_94 ),
inference(superposition,[],[f136,f1101]) ).
fof(f1105,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X1) )
| ~ spl7_94 ),
inference(superposition,[],[f137,f1101]) ).
fof(f1106,plain,
( ! [X0,X1] :
( member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| ~ member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X1)
| ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X0) )
| ~ spl7_94 ),
inference(superposition,[],[f138,f1101]) ).
fof(f1113,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF1)
| member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),y)
| ~ spl7_78
| ~ spl7_94 ),
inference(superposition,[],[f840,f1101]) ).
fof(f1116,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF6)
| member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),sF5)
| ~ spl7_86
| ~ spl7_94 ),
inference(superposition,[],[f929,f1101]) ).
fof(f1120,definition,
( spl7_95
<=> member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),y) ),
introduced(definition,[new_symbols(definition,[spl7_95])],[avatar_definition]) ).
fof(f1121,plain,
( ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),y)
| spl7_95 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1122,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),y)
| ~ spl7_95 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1134,definition,
( spl7_98
<=> member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),sF5) ),
introduced(definition,[new_symbols(definition,[spl7_98])],[avatar_definition]) ).
fof(f1138,definition,
( spl7_99
<=> member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF6) ),
introduced(definition,[new_symbols(definition,[spl7_99])],[avatar_definition]) ).
fof(f1140,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF6)
| spl7_99 ),
inference(avatar_component_clause,[],[f1138]) ).
fof(f1141,plain,
( spl7_98
| ~ spl7_99
| ~ spl7_86
| ~ spl7_94 ),
inference(avatar_split_clause,[],[f1116,f1099,f928,f1138,f1134]) ).
fof(f1156,definition,
( spl7_102
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_102])],[avatar_definition]) ).
fof(f1157,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X0) )
| ~ spl7_102 ),
inference(avatar_component_clause,[],[f1156]) ).
fof(f1158,plain,
( spl7_102
| ~ spl7_94 ),
inference(avatar_split_clause,[],[f1104,f1099,f1156]) ).
fof(f1159,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))))
| null_class = intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| ~ spl7_102 ),
inference(resolution,[],[f1157,f1012]) ).
fof(f1166,definition,
( spl7_103
<=> null_class = intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl7_103])],[avatar_definition]) ).
fof(f1167,plain,
( null_class != intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| spl7_103 ),
inference(avatar_component_clause,[],[f1166]) ).
fof(f1168,plain,
( null_class = intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| ~ spl7_103 ),
inference(avatar_component_clause,[],[f1166]) ).
fof(f1170,definition,
( spl7_104
<=> member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6)))) ),
introduced(definition,[new_symbols(definition,[spl7_104])],[avatar_definition]) ).
fof(f1172,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))))
| ~ spl7_104 ),
inference(avatar_component_clause,[],[f1170]) ).
fof(f1173,plain,
( spl7_103
| spl7_104
| ~ spl7_102 ),
inference(avatar_split_clause,[],[f1159,f1156,f1170,f1166]) ).
fof(f1179,plain,
( null_class != null_class
| ~ member(first(not_subclass_element(sF3,sF6)),domain_of(sF1))
| ~ spl7_103 ),
inference(superposition,[],[f143,f1168]) ).
fof(f1186,plain,
( ~ member(first(not_subclass_element(sF3,sF6)),domain_of(sF1))
| ~ spl7_103 ),
inference(trivial_inequality_removal,[],[f1179]) ).
fof(f1187,plain,
( ~ member(first(not_subclass_element(sF3,sF6)),sF2)
| ~ spl7_15
| ~ spl7_103 ),
inference(forward_demodulation,[],[f1186,f307]) ).
fof(f1188,plain,
( $false
| ~ spl7_15
| ~ spl7_29
| ~ spl7_103 ),
inference(forward_subsumption_resolution,[],[f1187,f395]) ).
fof(f1189,plain,
( ~ spl7_15
| ~ spl7_29
| ~ spl7_103 ),
inference(avatar_contradiction_clause,[],[f1188]) ).
fof(f1193,definition,
( spl7_105
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X1) ) ),
introduced(definition,[new_symbols(definition,[spl7_105])],[avatar_definition]) ).
fof(f1194,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X1) )
| ~ spl7_105 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1195,plain,
( spl7_105
| ~ spl7_94 ),
inference(avatar_split_clause,[],[f1105,f1099,f1193]) ).
fof(f1196,plain,
( member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),universal_class)
| null_class = intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| ~ spl7_105 ),
inference(resolution,[],[f1194,f1012]) ).
fof(f1202,plain,
( member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),universal_class)
| spl7_103
| ~ spl7_105 ),
inference(forward_subsumption_resolution,[],[f1196,f1167]) ).
fof(f1221,definition,
( spl7_107
<=> ! [X0,X1] :
( member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| ~ member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X1)
| ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl7_107])],[avatar_definition]) ).
fof(f1222,plain,
( ! [X0,X1] :
( member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),cross_product(X0,X1))
| ~ member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X1)
| ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),X0) )
| ~ spl7_107 ),
inference(avatar_component_clause,[],[f1221]) ).
fof(f1223,plain,
( spl7_107
| ~ spl7_94 ),
inference(avatar_split_clause,[],[f1106,f1099,f1221]) ).
fof(f1227,plain,
( ~ member(second(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),universal_class)
| ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))))
| member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),null_class)
| ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),x)
| ~ spl7_63
| ~ spl7_107 ),
inference(resolution,[],[f1222,f748]) ).
fof(f1232,plain,
( ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))))
| member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),null_class)
| ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),x)
| ~ spl7_63
| spl7_103
| ~ spl7_105
| ~ spl7_107 ),
inference(forward_subsumption_resolution,[],[f1227,f1202]) ).
fof(f1233,plain,
( member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),null_class)
| ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),x)
| ~ spl7_63
| spl7_103
| ~ spl7_104
| ~ spl7_105
| ~ spl7_107 ),
inference(forward_subsumption_resolution,[],[f1232,f1172]) ).
fof(f1235,definition,
( spl7_108
<=> member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),x) ),
introduced(definition,[new_symbols(definition,[spl7_108])],[avatar_definition]) ).
fof(f1237,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),x)
| spl7_108 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1239,definition,
( spl7_109
<=> member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),null_class) ),
introduced(definition,[new_symbols(definition,[spl7_109])],[avatar_definition]) ).
fof(f1241,plain,
( member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),null_class)
| ~ spl7_109 ),
inference(avatar_component_clause,[],[f1239]) ).
fof(f1242,plain,
( ~ spl7_108
| spl7_109
| ~ spl7_63
| spl7_103
| ~ spl7_104
| ~ spl7_105
| ~ spl7_107 ),
inference(avatar_split_clause,[],[f1233,f1221,f1193,f1170,f1166,f747,f1239,f1235]) ).
fof(f1298,definition,
( spl7_113
<=> null_class = sF6 ),
introduced(definition,[new_symbols(definition,[spl7_113])],[avatar_definition]) ).
fof(f1299,plain,
( null_class != sF6
| spl7_113 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1303,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF1)
| ~ spl7_78
| ~ spl7_94
| spl7_95 ),
inference(forward_subsumption_resolution,[],[f1113,f1121]) ).
fof(f1325,definition,
( spl7_115
<=> member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF1) ),
introduced(definition,[new_symbols(definition,[spl7_115])],[avatar_definition]) ).
fof(f1326,plain,
( member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF1)
| ~ spl7_115 ),
inference(avatar_component_clause,[],[f1325]) ).
fof(f1327,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF1)
| spl7_115 ),
inference(avatar_component_clause,[],[f1325]) ).
fof(f1328,plain,
( ~ spl7_115
| ~ spl7_78
| ~ spl7_94
| spl7_95 ),
inference(avatar_split_clause,[],[f1303,f1120,f1099,f839,f1325]) ).
fof(f1341,plain,
( null_class = intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))
| spl7_115 ),
inference(resolution,[],[f1327,f1013]) ).
fof(f1346,plain,
( $false
| spl7_103
| spl7_115 ),
inference(forward_subsumption_resolution,[],[f1341,f1167]) ).
fof(f1347,plain,
( spl7_103
| spl7_115 ),
inference(avatar_contradiction_clause,[],[f1346]) ).
fof(f1357,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF1)
| ~ spl7_11
| spl7_108 ),
inference(resolution,[],[f1237,f284]) ).
fof(f1361,plain,
( $false
| ~ spl7_11
| spl7_108
| ~ spl7_115 ),
inference(forward_subsumption_resolution,[],[f1357,f1326]) ).
fof(f1362,plain,
( ~ spl7_11
| spl7_108
| ~ spl7_115 ),
inference(avatar_contradiction_clause,[],[f1361]) ).
fof(f2655,plain,
( first(not_subclass_element(sF3,sF6)) = first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))
| first(not_subclass_element(sF3,sF6)) = first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))
| ~ spl7_104 ),
inference(resolution,[],[f8,f1172]) ).
fof(f2664,plain,
( first(not_subclass_element(sF3,sF6)) = first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))
| ~ spl7_104 ),
inference(duplicate_literal_removal,[],[f2655]) ).
fof(f2667,definition,
( spl7_207
<=> first(not_subclass_element(sF3,sF6)) = first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl7_207])],[avatar_definition]) ).
fof(f2669,plain,
( first(not_subclass_element(sF3,sF6)) = first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))
| ~ spl7_207 ),
inference(avatar_component_clause,[],[f2667]) ).
fof(f2670,plain,
( spl7_207
| ~ spl7_104 ),
inference(avatar_split_clause,[],[f2664,f1170,f2667]) ).
fof(f2673,plain,
( member(first(not_subclass_element(sF3,sF6)),y)
| ~ spl7_95
| ~ spl7_207 ),
inference(superposition,[],[f1122,f2669]) ).
fof(f2677,plain,
( spl7_20
| ~ spl7_95
| ~ spl7_207 ),
inference(avatar_split_clause,[],[f2673,f2667,f1120,f335]) ).
fof(f2843,plain,
( first(not_subclass_element(sF3,sF6)) != first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))))
| member(first(not_subclass_element(sF3,sF6)),sF5)
| ~ member(first(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class)))),sF5) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f5694,plain,
( null_class != sF6
| member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),sF6)
| ~ member(regular(intersection(sF1,cross_product(unordered_pair(first(not_subclass_element(sF3,sF6)),first(not_subclass_element(sF3,sF6))),universal_class))),null_class) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f6547,plain,
( $false
| spl7_99
| ~ spl7_109
| spl7_113 ),
inference(unit_resulting_resolution,[],[f872,f1241,f1140,f1299]) ).
fof(f6548,plain,
( spl7_99
| ~ spl7_109
| spl7_113 ),
inference(avatar_contradiction_clause,[],[f6547]) ).
cnf(s104,plain,
spl7_1,
inference(sat_conversion,[],[f214]) ).
cnf(s106,plain,
spl7_2,
inference(sat_conversion,[],[f219]) ).
cnf(s108,plain,
spl7_3,
inference(sat_conversion,[],[f224]) ).
cnf(s110,plain,
spl7_4,
inference(sat_conversion,[],[f229]) ).
cnf(s131,plain,
( ~ spl7_4
| spl7_6 ),
inference(sat_conversion,[],[f258]) ).
cnf(s133,plain,
spl7_7,
inference(sat_conversion,[],[f263]) ).
cnf(s135,plain,
spl7_8,
inference(sat_conversion,[],[f268]) ).
cnf(s142,plain,
( ~ spl7_8
| spl7_9 ),
inference(sat_conversion,[],[f277]) ).
cnf(s146,plain,
( ~ spl7_4
| spl7_11 ),
inference(sat_conversion,[],[f285]) ).
cnf(s153,plain,
( ~ spl7_3
| spl7_13 ),
inference(sat_conversion,[],[f296]) ).
cnf(s160,plain,
spl7_15,
inference(sat_conversion,[],[f308]) ).
cnf(s162,plain,
~ spl7_16,
inference(sat_conversion,[],[f313]) ).
cnf(s164,plain,
( ~ spl7_1
| spl7_17 ),
inference(sat_conversion,[],[f317]) ).
cnf(s167,plain,
( ~ spl7_17
| spl7_18 ),
inference(sat_conversion,[],[f322]) ).
cnf(s170,plain,
( spl7_16
| ~ spl7_18
| spl7_19 ),
inference(sat_conversion,[],[f328]) ).
cnf(s180,plain,
( ~ spl7_19
| spl7_22 ),
inference(sat_conversion,[],[f347]) ).
cnf(s182,plain,
( ~ spl7_19
| spl7_23 ),
inference(sat_conversion,[],[f351]) ).
cnf(s184,plain,
( ~ spl7_19
| spl7_24 ),
inference(sat_conversion,[],[f355]) ).
cnf(s202,plain,
( ~ spl7_1
| ~ spl7_23
| spl7_29
| ~ spl7_30 ),
inference(sat_conversion,[],[f400]) ).
cnf(s205,plain,
( spl7_16
| spl7_30 ),
inference(sat_conversion,[],[f405]) ).
cnf(s209,plain,
( ~ spl7_1
| ~ spl7_24
| ~ spl7_30
| spl7_31 ),
inference(sat_conversion,[],[f411]) ).
cnf(s250,plain,
( ~ spl7_2
| ~ spl7_22
| ~ spl7_27
| spl7_28
| ~ spl7_31 ),
inference(sat_conversion,[],[f459]) ).
cnf(s253,plain,
( spl7_16
| ~ spl7_28 ),
inference(sat_conversion,[],[f465]) ).
cnf(s259,plain,
( ~ spl7_9
| ~ spl7_20
| spl7_27
| ~ spl7_36 ),
inference(sat_conversion,[],[f474]) ).
cnf(s314,plain,
( ~ spl7_7
| spl7_52 ),
inference(sat_conversion,[],[f589]) ).
cnf(s320,plain,
( spl7_36
| ~ spl7_52
| spl7_54
| spl7_55 ),
inference(sat_conversion,[],[f603]) ).
cnf(s327,plain,
( ~ spl7_29
| ~ spl7_54 ),
inference(sat_conversion,[],[f628]) ).
cnf(s410,plain,
( ~ spl7_55
| spl7_63 ),
inference(sat_conversion,[],[f749]) ).
cnf(s453,plain,
( ~ spl7_6
| ~ spl7_13
| spl7_78 ),
inference(sat_conversion,[],[f841]) ).
cnf(s504,plain,
( ~ spl7_2
| spl7_86 ),
inference(sat_conversion,[],[f930]) ).
cnf(s585,plain,
( ~ spl7_15
| spl7_93 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s597,plain,
( ~ spl7_29
| ~ spl7_93
| spl7_94 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s616,plain,
( ~ spl7_86
| ~ spl7_94
| spl7_98
| ~ spl7_99 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s621,plain,
( ~ spl7_94
| spl7_102 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s625,plain,
( ~ spl7_102
| spl7_103
| spl7_104 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s635,plain,
( ~ spl7_15
| ~ spl7_29
| ~ spl7_103 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s638,plain,
( ~ spl7_94
| spl7_105 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s652,plain,
( ~ spl7_94
| spl7_107 ),
inference(sat_conversion,[],[f1223]) ).
cnf(s655,plain,
( ~ spl7_63
| spl7_103
| ~ spl7_104
| ~ spl7_105
| ~ spl7_107
| ~ spl7_108
| spl7_109 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s718,plain,
( ~ spl7_78
| ~ spl7_94
| spl7_95
| ~ spl7_115 ),
inference(sat_conversion,[],[f1328]) ).
cnf(s733,plain,
( spl7_103
| spl7_115 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s743,plain,
( ~ spl7_11
| spl7_108
| ~ spl7_115 ),
inference(sat_conversion,[],[f1362]) ).
cnf(s1338,plain,
( ~ spl7_104
| spl7_207 ),
inference(sat_conversion,[],[f2670]) ).
cnf(s1344,plain,
( spl7_20
| ~ spl7_95
| ~ spl7_207 ),
inference(sat_conversion,[],[f2677]) ).
cnf(s1501,plain,
( spl7_27
| ~ spl7_98
| ~ spl7_207 ),
inference(sat_conversion,[],[f2843]) ).
cnf(s3215,plain,
( spl7_99
| ~ spl7_109
| ~ spl7_113 ),
inference(sat_conversion,[],[f5694]) ).
cnf(s3560,plain,
( spl7_99
| ~ spl7_109
| spl7_113 ),
inference(sat_conversion,[],[f6548]) ).
cnf(s3562,plain,
~ spl7_28,
inference(rat,[],[s253,s162]) ).
cnf(s3563,plain,
spl7_30,
inference(rat,[],[s205,s162]) ).
cnf(s3566,plain,
spl7_93,
inference(rat,[],[s585,s160]) ).
cnf(s3570,plain,
spl7_9,
inference(rat,[],[s142,s135]) ).
cnf(s3572,plain,
spl7_52,
inference(rat,[],[s314,s133]) ).
cnf(s3573,plain,
spl7_11,
inference(rat,[],[s146,s110]) ).
cnf(s3574,plain,
spl7_6,
inference(rat,[],[s131,s110]) ).
cnf(s3581,plain,
spl7_13,
inference(rat,[],[s153,s108]) ).
cnf(s3584,plain,
spl7_78,
inference(rat,[],[s453,s3574,s3581]) ).
cnf(s3587,plain,
spl7_86,
inference(rat,[],[s504,s106]) ).
cnf(s3595,plain,
spl7_17,
inference(rat,[],[s164,s104]) ).
cnf(s3596,plain,
spl7_18,
inference(rat,[],[s167,s3595]) ).
cnf(s3597,plain,
spl7_19,
inference(rat,[],[s170,s162,s3596]) ).
cnf(s3599,plain,
spl7_24,
inference(rat,[],[s184,s3597]) ).
cnf(s3600,plain,
spl7_23,
inference(rat,[],[s182,s3597]) ).
cnf(s3601,plain,
spl7_22,
inference(rat,[],[s180,s3597]) ).
cnf(s3604,plain,
spl7_31,
inference(rat,[],[s209,s104,s3563,s3599]) ).
cnf(s3606,plain,
spl7_29,
inference(rat,[],[s202,s3563,s104,s3600]) ).
cnf(s3608,plain,
~ spl7_27,
inference(rat,[],[s250,s3604,s3562,s106,s3601]) ).
cnf(s3614,plain,
~ spl7_103,
inference(rat,[],[s635,s160,s3606]) ).
cnf(s3615,plain,
spl7_94,
inference(rat,[],[s597,s3566,s3606]) ).
cnf(s3616,plain,
~ spl7_54,
inference(rat,[],[s327,s3606]) ).
cnf(s3619,plain,
spl7_115,
inference(rat,[],[s733,s3614]) ).
cnf(s3621,plain,
spl7_95,
inference(rat,[],[s718,s3619,s3584,s3615]) ).
cnf(s3622,plain,
spl7_107,
inference(rat,[],[s652,s3615]) ).
cnf(s3623,plain,
spl7_105,
inference(rat,[],[s638,s3615]) ).
cnf(s3624,plain,
spl7_102,
inference(rat,[],[s621,s3615]) ).
cnf(s3627,plain,
spl7_108,
inference(rat,[],[s743,s3573,s3619]) ).
cnf(s3630,plain,
spl7_104,
inference(rat,[],[s625,s3614,s3624]) ).
cnf(s3631,plain,
spl7_207,
inference(rat,[],[s1338,s3630]) ).
cnf(s3632,plain,
~ spl7_98,
inference(rat,[],[s1501,s3608,s3631]) ).
cnf(s3633,plain,
spl7_20,
inference(rat,[],[s1344,s3621,s3631]) ).
cnf(s3635,plain,
~ spl7_99,
inference(rat,[],[s616,s3615,s3587,s3632]) ).
cnf(s3637,plain,
~ spl7_36,
inference(rat,[],[s259,s3608,s3570,s3633]) ).
cnf(s3640,plain,
spl7_55,
inference(rat,[],[s320,s3616,s3572,s3637]) ).
cnf(s3643,plain,
spl7_63,
inference(rat,[],[s410,s3640]) ).
cnf(s3645,plain,
spl7_109,
inference(rat,[],[s655,s3630,s3627,s3622,s3623,s3614,s3643]) ).
cnf(s3647,plain,
spl7_113,
inference(rat,[],[s3560,s3635,s3645]) ).
cnf(s3648,plain,
$false,
inference(rat,[],[s3215,s3635,s3647,s3645]) ).
fof(f6549,plain,
$false,
inference(avatar_sat_refutation,[],[s3648]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET276-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n016.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 01:22:33 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 Running first-order theorem proving
% 0.12/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.05/2.59 % (3167300)Input is clausal, will run a generic CNF schedule.
% 12.05/2.59 % (3167306)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1929116693:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.05/2.59 % (3167308)lrs+10_1_sil=8000:sp=occurrence:random_seed=898802979:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.05/2.59 % (3167310)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2696820045:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.05/2.59 % (3167309)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2746729847:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.05/2.59 % (3167305)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=2812077110:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.05/2.59 % (3167311)dis-21_1_sil=8000:lcm=predicate:random_seed=1982087774: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)
% 12.05/2.59 % (3167307)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2512523512:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.05/2.59 % (3167308)Refutation not found, incomplete strategy
% 12.05/2.59 % (3167308)------------------------------
% 12.05/2.59 % (3167308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.05/2.59 % (3167308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.05/2.59 % (3167308)CaDiCaL version: 2.1.3
% 12.05/2.59 % (3167308)Termination reason: Refutation not found, incomplete strategy
% 12.05/2.59 % (3167308)Time elapsed: 0.003 s
% 12.05/2.59 % (3167308)Peak memory usage: 88 MB
% 12.05/2.59 % (3167308)Instructions burned: 2 (million)
% 12.05/2.59 % (3167309)Instruction limit reached!
% 12.05/2.59 % (3167309)------------------------------
% 12.05/2.59 % (3167309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.05/2.59 % (3167309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.05/2.59 % (3167309)CaDiCaL version: 2.1.3
% 12.05/2.59 % (3167309)Termination reason: Instruction limit
% 12.05/2.59 % (3167309)Termination phase: Saturation
% 12.05/2.59 % (3167309)Time elapsed: 0.068 s
% 12.05/2.59 % (3167309)Peak memory usage: 89 MB
% 12.05/2.59 % (3167309)Instructions burned: 115 (million)
% 12.05/2.59 % (3167311)Instruction limit reached!
% 12.05/2.59 % (3167311)------------------------------
% 12.05/2.59 % (3167311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.05/2.59 % (3167311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.05/2.59 % (3167311)CaDiCaL version: 2.1.3
% 12.05/2.59 % (3167311)Termination reason: Instruction limit
% 12.05/2.59 % (3167311)Termination phase: Saturation
% 12.05/2.59 % (3167311)Time elapsed: 0.071 s
% 12.05/2.59 % (3167311)Peak memory usage: 89 MB
% 12.05/2.59 % (3167311)Instructions burned: 117 (million)
% 12.05/2.59 % (3167310)Instruction limit reached!
% 12.05/2.59 % (3167310)------------------------------
% 12.05/2.59 % (3167310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.05/2.59 % (3167310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.05/2.59 % (3167310)CaDiCaL version: 2.1.3
% 12.05/2.59 % (3167310)Termination reason: Instruction limit
% 12.05/2.59 % (3167310)Termination phase: Saturation
% 12.05/2.59 % (3167310)Time elapsed: 0.137 s
% 12.05/2.59 % (3167310)Peak memory usage: 90 MB
% 12.05/2.59 % (3167310)Instructions burned: 181 (million)
% 12.05/2.59 % (3167319)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=4279347523:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.05/2.59 % (3167320)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2269212796: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)
% 12.05/2.59 % (3167319)Refutation not found, incomplete strategy
% 12.05/2.59 % (3167319)------------------------------
% 12.05/2.59 % (3167319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.05/2.59 % (3167319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.05/2.59 % (3167319)CaDiCaL version: 2.1.3
% 24.15/4.21 % (3167319)Termination reason: Refutation not found, incomplete strategy
% 24.15/4.21 % (3167319)Time elapsed: 0.003 s
% 24.15/4.21 % (3167319)Peak memory usage: 88 MB
% 24.15/4.21 % (3167319)Instructions burned: 3 (million)
% 24.15/4.21 % (3167308)------------------------------
% 24.15/4.21 % (3167308)------------------------------
% 24.15/4.21 % (3167321)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3083358513:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 24.15/4.21 % (3167320)Instruction limit reached!
% 24.15/4.21 % (3167320)------------------------------
% 24.15/4.21 % (3167320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/4.21 % (3167320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/4.21 % (3167320)CaDiCaL version: 2.1.3
% 24.15/4.21 % (3167320)Termination reason: Instruction limit
% 24.15/4.21 % (3167320)Termination phase: Saturation
% 24.15/4.21 % (3167320)Time elapsed: 0.105 s
% 24.15/4.21 % (3167320)Peak memory usage: 90 MB
% 24.15/4.21 % (3167320)Instructions burned: 189 (million)
% 24.15/4.21 % (3167324)lrs+10_64_to=lpo:sil=8000:random_seed=4007334144:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 24.15/4.21 % (3167321)Instruction limit reached!
% 24.15/4.21 % (3167321)------------------------------
% 24.15/4.21 % (3167321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/4.21 % (3167321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/4.21 % (3167321)CaDiCaL version: 2.1.3
% 24.15/4.21 % (3167321)Termination reason: Instruction limit
% 24.15/4.21 % (3167321)Termination phase: Saturation
% 24.15/4.21 % (3167321)Time elapsed: 0.127 s
% 24.15/4.21 % (3167321)Peak memory usage: 89 MB
% 24.15/4.21 % (3167321)Instructions burned: 221 (million)
% 24.15/4.21 % (3167319)------------------------------
% 24.15/4.21 % (3167319)------------------------------
% 24.15/4.21 % (3167324)Instruction limit reached!
% 24.15/4.21 % (3167324)------------------------------
% 24.15/4.21 % (3167324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/4.21 % (3167324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/4.21 % (3167324)CaDiCaL version: 2.1.3
% 24.15/4.21 % (3167324)Termination reason: Instruction limit
% 24.15/4.21 % (3167324)Termination phase: Saturation
% 24.15/4.21 % (3167324)Time elapsed: 0.081 s
% 24.15/4.21 % (3167324)Peak memory usage: 89 MB
% 24.15/4.21 % (3167324)Instructions burned: 126 (million)
% 24.15/4.21 % (3167326)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2003675200:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 24.15/4.21 % (3167328)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4172917679:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 24.15/4.21 % (3167326)Instruction limit reached!
% 24.15/4.21 % (3167326)------------------------------
% 24.15/4.21 % (3167326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/4.21 % (3167326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/4.21 % (3167326)CaDiCaL version: 2.1.3
% 24.15/4.21 % (3167326)Termination reason: Instruction limit
% 24.15/4.21 % (3167326)Termination phase: Saturation
% 24.15/4.21 % (3167326)Time elapsed: 0.125 s
% 24.15/4.21 % (3167326)Peak memory usage: 90 MB
% 24.15/4.21 % (3167326)Instructions burned: 194 (million)
% 24.15/4.21 % (3167330)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=2659050855:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 24.15/4.21 % (3167329)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=920728963:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 24.15/4.21 % (3167328)Instruction limit reached!
% 24.15/4.21 % (3167328)------------------------------
% 24.15/4.21 % (3167328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.15/4.21 % (3167328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.15/4.21 % (3167328)CaDiCaL version: 2.1.3
% 24.15/4.21 % (3167328)Termination reason: Instruction limit
% 24.15/4.21 % (3167328)Termination phase: Saturation
% 24.15/4.21 % (3167328)Time elapsed: 0.107 s
% 24.15/4.21 % (3167328)Peak memory usage: 91 MB
% 24.15/4.21 % (3167328)Instructions burned: 158 (million)
% 24.15/4.21 % (3167330)Instruction limit reached!
% 24.15/4.21 % (3167330)------------------------------
% 24.15/4.21 % (3167330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.98/5.69 % (3167330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.98/5.69 % (3167330)CaDiCaL version: 2.1.3
% 33.98/5.69 % (3167330)Termination reason: Instruction limit
% 33.98/5.69 % (3167330)Termination phase: Saturation
% 33.98/5.69 % (3167330)Time elapsed: 0.059 s
% 33.98/5.69 % (3167330)Peak memory usage: 89 MB
% 33.98/5.69 % (3167330)Instructions burned: 107 (million)
% 33.98/5.69 % (3167333)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1292177272:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 33.98/5.69 % (3167333)Instruction limit reached!
% 33.98/5.69 % (3167333)------------------------------
% 33.98/5.69 % (3167333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.98/5.69 % (3167333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.98/5.69 % (3167333)CaDiCaL version: 2.1.3
% 33.98/5.69 % (3167333)Termination reason: Instruction limit
% 33.98/5.69 % (3167333)Termination phase: Saturation
% 33.98/5.69 % (3167333)Time elapsed: 0.073 s
% 33.98/5.69 % (3167333)Peak memory usage: 89 MB
% 33.98/5.69 % (3167333)Instructions burned: 108 (million)
% 33.98/5.69 % (3167336)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3064307057:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 33.98/5.69 % (3167337)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3302255415:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 33.98/5.69 % (3167336)Instruction limit reached!
% 33.98/5.69 % (3167336)------------------------------
% 33.98/5.69 % (3167336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.98/5.69 % (3167336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.98/5.69 % (3167336)CaDiCaL version: 2.1.3
% 33.98/5.69 % (3167336)Termination reason: Instruction limit
% 33.98/5.69 % (3167336)Termination phase: Saturation
% 33.98/5.69 % (3167336)Time elapsed: 0.163 s
% 33.98/5.69 % (3167336)Peak memory usage: 90 MB
% 33.98/5.69 % (3167336)Instructions burned: 244 (million)
% 33.98/5.69 % (3167341)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=97093684:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 33.98/5.69 % (3167341)Instruction limit reached!
% 33.98/5.69 % (3167341)------------------------------
% 33.98/5.69 % (3167341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.98/5.69 % (3167341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.98/5.69 % (3167341)CaDiCaL version: 2.1.3
% 33.98/5.69 % (3167341)Termination reason: Instruction limit
% 33.98/5.69 % (3167341)Termination phase: Saturation
% 33.98/5.69 % (3167341)Time elapsed: 0.102 s
% 33.98/5.69 % (3167341)Peak memory usage: 90 MB
% 33.98/5.69 % (3167341)Instructions burned: 135 (million)
% 33.98/5.69 % (3167343)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=826192081:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 33.98/5.69 % (3167344)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2676824337:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 33.98/5.69 % (3167344)Instruction limit reached!
% 33.98/5.69 % (3167344)------------------------------
% 33.98/5.69 % (3167344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.98/5.69 % (3167344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.98/5.69 % (3167344)CaDiCaL version: 2.1.3
% 33.98/5.69 % (3167344)Termination reason: Instruction limit
% 33.98/5.69 % (3167344)Termination phase: Saturation
% 33.98/5.69 % (3167344)Time elapsed: 0.115 s
% 33.98/5.69 % (3167344)Peak memory usage: 89 MB
% 33.98/5.69 % (3167344)Instructions burned: 192 (million)
% 33.98/5.69 % (3167343)Instruction limit reached!
% 33.98/5.69 % (3167343)------------------------------
% 33.98/5.69 % (3167343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.98/5.69 % (3167343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.98/5.69 % (3167343)CaDiCaL version: 2.1.3
% 33.98/5.69 % (3167343)Termination reason: Instruction limit
% 33.98/5.69 % (3167343)Termination phase: Saturation
% 33.98/5.69 % (3167343)Time elapsed: 0.286 s
% 33.98/5.69 % (3167343)Peak memory usage: 93 MB
% 33.98/5.69 % (3167343)Instructions burned: 500 (million)
% 33.98/5.69 % (3167347)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4126450552:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 56.52/8.87 % (3167348)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2514409089:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 56.52/8.87 % (3167347)Instruction limit reached!
% 56.52/8.87 % (3167347)------------------------------
% 56.52/8.87 % (3167347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.52/8.87 % (3167347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.52/8.87 % (3167347)CaDiCaL version: 2.1.3
% 56.52/8.87 % (3167347)Termination reason: Instruction limit
% 56.52/8.87 % (3167347)Termination phase: Saturation
% 56.52/8.87 % (3167347)Time elapsed: 0.130 s
% 56.52/8.87 % (3167347)Peak memory usage: 90 MB
% 56.52/8.87 % (3167347)Instructions burned: 266 (million)
% 56.52/8.87 % (3167348)Instruction limit reached!
% 56.52/8.87 % (3167348)------------------------------
% 56.52/8.87 % (3167348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.52/8.87 % (3167348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.52/8.87 % (3167348)CaDiCaL version: 2.1.3
% 56.52/8.87 % (3167348)Termination reason: Instruction limit
% 56.52/8.87 % (3167348)Termination phase: Saturation
% 56.52/8.87 % (3167348)Time elapsed: 0.091 s
% 56.52/8.87 % (3167348)Peak memory usage: 90 MB
% 56.52/8.87 % (3167348)Instructions burned: 157 (million)
% 56.52/8.87 % (3167351)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=1925834577:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 56.52/8.87 % (3167352)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2187689170:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 56.52/8.87 % (3167352)Refutation not found, incomplete strategy
% 56.52/8.87 % (3167352)------------------------------
% 56.52/8.87 % (3167352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.52/8.87 % (3167352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.52/8.87 % (3167352)CaDiCaL version: 2.1.3
% 56.52/8.87 % (3167352)Termination reason: Refutation not found, incomplete strategy
% 56.52/8.87 % (3167352)Time elapsed: 0.004 s
% 56.52/8.87 % (3167352)Peak memory usage: 88 MB
% 56.52/8.87 % (3167352)Instructions burned: 5 (million)
% 56.52/8.87 % (3167352)------------------------------
% 56.52/8.87 % (3167352)------------------------------
% 56.52/8.87 % (3167355)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2215931187:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 56.52/8.87 % (3167355)Instruction limit reached!
% 56.52/8.87 % (3167355)------------------------------
% 56.52/8.87 % (3167355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.52/8.87 % (3167355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.52/8.87 % (3167355)CaDiCaL version: 2.1.3
% 56.52/8.87 % (3167355)Termination reason: Instruction limit
% 56.52/8.87 % (3167355)Termination phase: Saturation
% 56.52/8.87 % (3167355)Time elapsed: 0.099 s
% 56.52/8.87 % (3167355)Peak memory usage: 90 MB
% 56.52/8.87 % (3167355)Instructions burned: 181 (million)
% 56.52/8.87 % (3167357)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=442092842:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 56.52/8.87 % (3167329)Instruction limit reached!
% 56.52/8.87 % (3167329)------------------------------
% 56.52/8.87 % (3167329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.52/8.87 % (3167329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.52/8.87 % (3167329)CaDiCaL version: 2.1.3
% 56.52/8.87 % (3167329)Termination reason: Instruction limit
% 56.52/8.87 % (3167329)Termination phase: Saturation
% 56.52/8.87 % (3167329)Time elapsed: 2.205 s
% 56.52/8.87 % (3167329)Peak memory usage: 149 MB
% 56.52/8.87 % (3167329)Instructions burned: 3395 (million)
% 56.52/8.87 % (3167359)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=304365257:i=412:gtgl=4:gtg=exists_all_2969 on theBenchmark for (2969ds/412Mi)
% 56.52/8.87 % (3167359)Instruction limit reached!
% 56.52/8.87 % (3167359)------------------------------
% 56.52/8.87 % (3167359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.64/11.97 % (3167359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.64/11.97 % (3167359)CaDiCaL version: 2.1.3
% 78.64/11.97 % (3167359)Termination reason: Instruction limit
% 78.64/11.97 % (3167359)Termination phase: Saturation
% 78.64/11.97 % (3167359)Time elapsed: 0.182 s
% 78.64/11.97 % (3167359)Peak memory usage: 90 MB
% 78.64/11.97 % (3167359)Instructions burned: 414 (million)
% 78.64/11.97 % (3167361)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=3282730867:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi)
% 78.64/11.97 % (3167351)Instruction limit reached!
% 78.64/11.97 % (3167351)------------------------------
% 78.64/11.97 % (3167351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.64/11.97 % (3167351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.64/11.97 % (3167351)CaDiCaL version: 2.1.3
% 78.64/11.97 % (3167351)Termination reason: Instruction limit
% 78.64/11.97 % (3167351)Termination phase: Saturation
% 78.64/11.97 % (3167351)Time elapsed: 1.840 s
% 78.64/11.97 % (3167351)Peak memory usage: 150 MB
% 78.64/11.97 % (3167351)Instructions burned: 3257 (million)
% 78.64/11.97 % (3167363)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=1291703671:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2961 on theBenchmark for (2961ds/303Mi)
% 78.64/11.97 % (3167363)Refutation not found, incomplete strategy
% 78.64/11.97 % (3167363)------------------------------
% 78.64/11.97 % (3167363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.64/11.97 % (3167363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.64/11.97 % (3167363)CaDiCaL version: 2.1.3
% 78.64/11.97 % (3167363)Termination reason: Refutation not found, incomplete strategy
% 78.64/11.97 % (3167363)Time elapsed: 0.003 s
% 78.64/11.97 % (3167363)Peak memory usage: 88 MB
% 78.64/11.97 % (3167363)Instructions burned: 2 (million)
% 78.64/11.97 % (3167337)Instruction limit reached!
% 78.64/11.97 % (3167337)------------------------------
% 78.64/11.97 % (3167337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.64/11.97 % (3167337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.64/11.97 % (3167337)CaDiCaL version: 2.1.3
% 78.64/11.97 % (3167337)Termination reason: Instruction limit
% 78.64/11.97 % (3167337)Termination phase: Saturation
% 78.64/11.97 % (3167337)Time elapsed: 3.240 s
% 78.64/11.97 % (3167337)Peak memory usage: 154 MB
% 78.64/11.97 % (3167337)Instructions burned: 5208 (million)
% 78.64/11.97 % (3167363)------------------------------
% 78.64/11.97 % (3167363)------------------------------
% 78.64/11.97 % (3167365)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3038248042:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi)
% 78.64/11.97 % (3167365)Refutation not found, incomplete strategy
% 78.64/11.97 % (3167365)------------------------------
% 78.64/11.97 % (3167365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.64/11.97 % (3167365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.64/11.97 % (3167365)CaDiCaL version: 2.1.3
% 78.64/11.97 % (3167365)Termination reason: Refutation not found, incomplete strategy
% 78.64/11.97 % (3167365)Time elapsed: 0.004 s
% 78.64/11.97 % (3167365)Peak memory usage: 88 MB
% 78.64/11.97 % (3167365)Instructions burned: 4 (million)
% 78.64/11.97 % (3167366)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=886934989:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi)
% 78.64/11.97 % (3167366)Refutation not found, incomplete strategy
% 78.64/11.97 % (3167366)------------------------------
% 78.64/11.97 % (3167366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.64/11.97 % (3167366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.64/11.97 % (3167366)CaDiCaL version: 2.1.3
% 78.64/11.97 % (3167366)Termination reason: Refutation not found, incomplete strategy
% 78.64/11.97 % (3167366)Time elapsed: 0.005 s
% 78.64/11.97 % (3167366)Peak memory usage: 88 MB
% 78.64/11.97 % (3167366)Instructions burned: 5 (million)
% 78.64/11.97 % (3167365)------------------------------
% 78.64/11.97 % (3167365)------------------------------
% 78.64/11.97 % (3167366)------------------------------
% 78.64/11.97 % (3167366)------------------------------
% 78.64/11.97 % (3167369)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3313197243:i=2989:sd=3:ss=axioms:sgt=60_2953 on theBenchmark for (2953ds/2989Mi)
% 93.90/14.10 % (3167370)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=4283766137:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi)
% 93.90/14.10 % (3167370)Instruction limit reached!
% 93.90/14.10 % (3167370)------------------------------
% 93.90/14.10 % (3167370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167370)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167370)Termination reason: Instruction limit
% 93.90/14.10 % (3167370)Termination phase: Saturation
% 93.90/14.10 % (3167370)Time elapsed: 1.327 s
% 93.90/14.10 % (3167370)Peak memory usage: 137 MB
% 93.90/14.10 % (3167370)Instructions burned: 1997 (million)
% 93.90/14.10 % (3167373)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=954406677:i=2088:bd=preordered:av=off_2937 on theBenchmark for (2937ds/2088Mi)
% 93.90/14.10 % (3167369)Instruction limit reached!
% 93.90/14.10 % (3167369)------------------------------
% 93.90/14.10 % (3167369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167369)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167369)Termination reason: Instruction limit
% 93.90/14.10 % (3167369)Termination phase: Saturation
% 93.90/14.10 % (3167369)Time elapsed: 1.869 s
% 93.90/14.10 % (3167369)Peak memory usage: 143 MB
% 93.90/14.10 % (3167369)Instructions burned: 2990 (million)
% 93.90/14.10 % (3167375)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=544170203:i=1098:nicw=on_2932 on theBenchmark for (2932ds/1098Mi)
% 93.90/14.10 % (3167375)Instruction limit reached!
% 93.90/14.10 % (3167375)------------------------------
% 93.90/14.10 % (3167375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167375)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167375)Termination reason: Instruction limit
% 93.90/14.10 % (3167375)Termination phase: Saturation
% 93.90/14.10 % (3167375)Time elapsed: 0.647 s
% 93.90/14.10 % (3167375)Peak memory usage: 102 MB
% 93.90/14.10 % (3167375)Instructions burned: 1099 (million)
% 93.90/14.10 % (3167373)Instruction limit reached!
% 93.90/14.10 % (3167373)------------------------------
% 93.90/14.10 % (3167373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167373)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167373)Termination reason: Instruction limit
% 93.90/14.10 % (3167373)Termination phase: Saturation
% 93.90/14.10 % (3167373)Time elapsed: 1.303 s
% 93.90/14.10 % (3167373)Peak memory usage: 137 MB
% 93.90/14.10 % (3167373)Instructions burned: 2088 (million)
% 93.90/14.10 % (3167377)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3794678714:i=433:bd=preordered_2924 on theBenchmark for (2924ds/433Mi)
% 93.90/14.10 % (3167378)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1467939114:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2923 on theBenchmark for (2923ds/2942Mi)
% 93.90/14.10 % (3167377)Instruction limit reached!
% 93.90/14.10 % (3167377)------------------------------
% 93.90/14.10 % (3167377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167377)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167377)Termination reason: Instruction limit
% 93.90/14.10 % (3167377)Termination phase: Saturation
% 93.90/14.10 % (3167377)Time elapsed: 0.238 s
% 93.90/14.10 % (3167377)Peak memory usage: 93 MB
% 93.90/14.10 % (3167377)Instructions burned: 433 (million)
% 93.90/14.10 % (3167361)Instruction limit reached!
% 93.90/14.10 % (3167361)------------------------------
% 93.90/14.10 % (3167361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167361)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167361)Termination reason: Instruction limit
% 93.90/14.10 % (3167361)Termination phase: Saturation
% 93.90/14.10 % (3167361)Time elapsed: 4.505 s
% 93.90/14.10 % (3167361)Peak memory usage: 182 MB
% 93.90/14.10 % (3167361)Instructions burned: 8480 (million)
% 93.90/14.10 % (3167381)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1592030347:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2920 on theBenchmark for (2920ds/6922Mi)
% 93.90/14.10 % (3167382)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=3611554624:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2919 on theBenchmark for (2919ds/596Mi)
% 93.90/14.10 % (3167382)Instruction limit reached!
% 93.90/14.10 % (3167382)------------------------------
% 93.90/14.10 % (3167382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167382)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167382)Termination reason: Instruction limit
% 93.90/14.10 % (3167382)Termination phase: Saturation
% 93.90/14.10 % (3167382)Time elapsed: 0.327 s
% 93.90/14.10 % (3167382)Peak memory usage: 99 MB
% 93.90/14.10 % (3167382)Instructions burned: 597 (million)
% 93.90/14.10 % (3167385)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=523359592:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2914 on theBenchmark for (2914ds/4123Mi)
% 93.90/14.10 % (3167357)Instruction limit reached!
% 93.90/14.10 % (3167357)------------------------------
% 93.90/14.10 % (3167357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167357)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167357)Termination reason: Instruction limit
% 93.90/14.10 % (3167357)Termination phase: Saturation
% 93.90/14.10 % (3167357)Time elapsed: 6.679 s
% 93.90/14.10 % (3167357)Peak memory usage: 168 MB
% 93.90/14.10 % (3167357)Instructions burned: 10308 (million)
% 93.90/14.10 % (3167387)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2268101573:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2905 on theBenchmark for (2905ds/16411Mi)
% 93.90/14.10 % (3167378)Instruction limit reached!
% 93.90/14.10 % (3167378)------------------------------
% 93.90/14.10 % (3167378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167378)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167378)Termination reason: Instruction limit
% 93.90/14.10 % (3167378)Termination phase: Saturation
% 93.90/14.10 % (3167378)Time elapsed: 1.882 s
% 93.90/14.10 % (3167378)Peak memory usage: 146 MB
% 93.90/14.10 % (3167378)Instructions burned: 2942 (million)
% 93.90/14.10 % (3167389)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1842213970:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2902 on theBenchmark for (2902ds/1670Mi)
% 93.90/14.10 % (3167389)Instruction limit reached!
% 93.90/14.10 % (3167389)------------------------------
% 93.90/14.10 % (3167389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167389)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167389)Termination reason: Instruction limit
% 93.90/14.10 % (3167389)Termination phase: Saturation
% 93.90/14.10 % (3167389)Time elapsed: 1.064 s
% 93.90/14.10 % (3167389)Peak memory usage: 136 MB
% 93.90/14.10 % (3167389)Instructions burned: 1670 (million)
% 93.90/14.10 % (3167385)Instruction limit reached!
% 93.90/14.10 % (3167385)------------------------------
% 93.90/14.10 % (3167385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167385)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167385)Termination reason: Instruction limit
% 93.90/14.10 % (3167385)Termination phase: Saturation
% 93.90/14.10 % (3167385)Time elapsed: 2.281 s
% 93.90/14.10 % (3167385)Peak memory usage: 162 MB
% 93.90/14.10 % (3167385)Instructions burned: 4124 (million)
% 93.90/14.10 % (3167391)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=1791602619:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2890 on theBenchmark for (2890ds/1722Mi)
% 93.90/14.10 % (3167392)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=2306459402:cts=off:cond=on:i=9530:bs=on:fsd=on_2889 on theBenchmark for (2889ds/9530Mi)
% 93.90/14.10 % (3167381)Instruction limit reached!
% 93.90/14.10 % (3167381)------------------------------
% 93.90/14.10 % (3167381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167381)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167381)Termination reason: Instruction limit
% 93.90/14.10 % (3167381)Termination phase: Saturation
% 93.90/14.10 % (3167381)Time elapsed: 3.825 s
% 93.90/14.10 % (3167381)Peak memory usage: 190 MB
% 93.90/14.10 % (3167381)Instructions burned: 6923 (million)
% 93.90/14.10 % (3167395)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3628613290:st=2:i=4495:sd=10:ss=included_2880 on theBenchmark for (2880ds/4495Mi)
% 93.90/14.10 % (3167391)Instruction limit reached!
% 93.90/14.10 % (3167391)------------------------------
% 93.90/14.10 % (3167391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.90/14.10 % (3167391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.90/14.10 % (3167391)CaDiCaL version: 2.1.3
% 93.90/14.10 % (3167391)Termination reason: Instruction limit
% 93.90/14.10 % (3167391)Termination phase: Saturation
% 93.90/14.10 % (3167391)Time elapsed: 1.166 s
% 93.90/14.10 % (3167391)Peak memory usage: 136 MB
% 93.90/14.10 % (3167391)Instructions burned: 1722 (million)
% 93.90/14.10 % (3167397)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=2281149781:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2876 on theBenchmark for (2876ds/4920Mi)
% 93.90/14.10 % (3167392)First to succeed.
% 93.90/14.10 % (3167392)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3167300"
% 93.90/14.10 % (3167392)Refutation found. Thanks to Tanya!
% 93.90/14.10 % SZS status Unsatisfiable for theBenchmark
% 93.90/14.10 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/14.30 % (3167392)------------------------------
% 0.16/14.30 % (3167392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/14.30 % (3167392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/14.30 % (3167392)CaDiCaL version: 2.1.3
% 0.16/14.30 % (3167392)Termination reason: Refutation
% 0.16/14.30 % (3167392)Time elapsed: 1.758 s
% 0.16/14.30 % (3167392)Peak memory usage: 140 MB
% 0.16/14.30 % (3167392)Instructions burned: 2471 (million)
% 0.16/14.30 % (3167392)------------------------------
% 0.16/14.30 % (3167392)------------------------------
% 0.16/14.30 % (3167300)Success in time 13.259 s
% 0.16/14.30 % Vampire exiting
%------------------------------------------------------------------------------