%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET270-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 : n013.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:39 PM UTC 2026
% Result : Unsatisfiable 73.66s 11.29s
% Output : Refutation 74.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 64
% Syntax : Number of formulae : 293 ( 50 unt; 41 def)
% Number of atoms : 769 ( 110 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 862 ( 386 ~; 437 |; 0 &)
% ( 39 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 43 ( 41 usr; 40 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 214 ( 0 sgn 214 !; 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(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
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(f9,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair2) ).
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(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,
domain_of(cross_product(x,y)) != x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_domain_property2_1) ).
fof(f123,plain,
x != domain_of(cross_product(x,y)),
inference(reorient_equations,[],[f122]) ).
fof(f124,negated_conjecture,
y != null_class,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_domain_property2_2) ).
fof(f125,plain,
null_class != y,
inference(reorient_equations,[],[f124]) ).
fof(f130,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(f139,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,f130]) ).
fof(f141,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,f130]) ).
fof(f142,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,f130]) ).
fof(f146,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(f147,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(f192,definition,
sF0 = cross_product(x,y),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f193,plain,
cross_product(x,y) = sF0,
inference(reorient_equations,[],[f192]) ).
fof(f194,definition,
sF1 = domain_of(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f195,plain,
domain_of(sF0) = sF1,
inference(reorient_equations,[],[f194]) ).
fof(f196,plain,
x != sF1,
inference(definition_folding,[],[f123,f195,f193]) ).
fof(f199,definition,
( spl2_1
<=> cross_product(x,y) = sF0 ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f201,plain,
( cross_product(x,y) = sF0
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f202,plain,
spl2_1,
inference(avatar_split_clause,[],[f193,f199]) ).
fof(f206,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,x) )
| ~ spl2_1 ),
inference(superposition,[],[f139,f201]) ).
fof(f208,definition,
( spl2_2
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f209,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,x) )
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f210,plain,
( spl2_2
| ~ spl2_1 ),
inference(avatar_split_clause,[],[f206,f199,f208]) ).
fof(f226,definition,
( spl2_4
<=> domain_of(sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f228,plain,
( domain_of(sF0) = sF1
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
spl2_4,
inference(avatar_split_clause,[],[f195,f226]) ).
fof(f231,definition,
( spl2_5
<=> x = sF1 ),
introduced(definition,[new_symbols(definition,[spl2_5])],[avatar_definition]) ).
fof(f233,plain,
( x != sF1
| spl2_5 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f234,plain,
~ spl2_5,
inference(avatar_split_clause,[],[f196,f231]) ).
fof(f238,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,y)
| ~ member(X0,x) )
| ~ spl2_1 ),
inference(superposition,[],[f141,f201]) ).
fof(f240,definition,
( spl2_6
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,y)
| ~ member(X0,x) ) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f241,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,y)
| ~ member(X0,x) )
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f242,plain,
( spl2_6
| ~ spl2_1 ),
inference(avatar_split_clause,[],[f238,f199,f240]) ).
fof(f253,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f21,f68]) ).
fof(f256,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f258,definition,
( spl2_7
<=> null_class = y ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f260,plain,
( null_class != y
| spl2_7 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f261,plain,
~ spl2_7,
inference(avatar_split_clause,[],[f125,f258]) ).
fof(f262,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f22,f68]) ).
fof(f286,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,[],[f147,f1]) ).
fof(f287,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,[],[f286,f4]) ).
fof(f297,plain,
( ! [X0,X1] :
( member(X0,sF1)
| null_class = intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl2_4 ),
inference(superposition,[],[f287,f228]) ).
fof(f299,definition,
( spl2_11
<=> ! [X0,X1] :
( member(X0,sF1)
| null_class = intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f300,plain,
( ! [X0,X1] :
( member(X0,sF1)
| null_class = intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl2_11 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f301,plain,
( spl2_11
| ~ spl2_4 ),
inference(avatar_split_clause,[],[f297,f226,f299]) ).
fof(f302,plain,
( ! [X0,X1] :
( null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| ~ member(not_subclass_element(X0,sF1),X1)
| subclass(X0,sF1) )
| ~ spl2_11 ),
inference(resolution,[],[f300,f3]) ).
fof(f304,definition,
( spl2_12
<=> ! [X0,X1] :
( null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| ~ member(not_subclass_element(X0,sF1),X1)
| subclass(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f305,plain,
( ! [X0,X1] :
( subclass(X0,sF1)
| ~ member(not_subclass_element(X0,sF1),X1)
| null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class)) )
| ~ spl2_12 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( spl2_12
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f302,f299,f304]) ).
fof(f307,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(X0,sF1),X1)
| null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| ~ subclass(sF1,X0)
| sF1 = X0 )
| ~ spl2_12 ),
inference(resolution,[],[f305,f7]) ).
fof(f348,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,[],[f262,f142]) ).
fof(f360,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,[],[f146,f348]) ).
fof(f368,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,[],[f360]) ).
fof(f377,plain,
( ! [X0] :
( ~ member(X0,sF1)
| regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl2_4 ),
inference(superposition,[],[f368,f228]) ).
fof(f379,definition,
( spl2_14
<=> ! [X0] :
( ~ member(X0,sF1)
| regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl2_14])],[avatar_definition]) ).
fof(f380,plain,
( ! [X0] :
( ~ member(X0,sF1)
| regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl2_14 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f381,plain,
( spl2_14
| ~ spl2_4 ),
inference(avatar_split_clause,[],[f377,f226,f379]) ).
fof(f385,plain,
( ! [X0] :
( regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))))))
| subclass(sF1,X0) )
| ~ spl2_14 ),
inference(resolution,[],[f380,f2]) ).
fof(f389,definition,
( spl2_15
<=> ! [X0] :
( regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))))))
| subclass(sF1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition]) ).
fof(f390,plain,
( ! [X0] :
( subclass(sF1,X0)
| regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,X0),not_subclass_element(sF1,X0)),universal_class))))))) )
| ~ spl2_15 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f391,plain,
( spl2_15
| ~ spl2_14 ),
inference(avatar_split_clause,[],[f385,f379,f389]) ).
fof(f410,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,X2)
| ~ subclass(X2,universal_class) ),
inference(resolution,[],[f9,f1]) ).
fof(f412,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,X2) ),
inference(forward_subsumption_resolution,[],[f410,f4]) ).
fof(f434,definition,
( spl2_16
<=> ! [X0,X1] :
( ~ member(not_subclass_element(X0,sF1),X1)
| null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| ~ subclass(sF1,X0)
| sF1 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition]) ).
fof(f435,plain,
( ! [X0,X1] :
( ~ subclass(sF1,X0)
| null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(X0,sF1),not_subclass_element(X0,sF1)),universal_class))
| ~ member(not_subclass_element(X0,sF1),X1)
| sF1 = X0 )
| ~ spl2_16 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f436,plain,
( spl2_16
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f307,f304,f434]) ).
fof(f1302,definition,
( spl2_52
<=> ! [X2] : ~ member(not_subclass_element(x,sF1),X2) ),
introduced(definition,[new_symbols(definition,[spl2_52])],[avatar_definition]) ).
fof(f1303,plain,
( ! [X2] : ~ member(not_subclass_element(x,sF1),X2)
| ~ spl2_52 ),
inference(avatar_component_clause,[],[f1302]) ).
fof(f1305,definition,
( spl2_53
<=> null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl2_53])],[avatar_definition]) ).
fof(f1306,plain,
( null_class != intersection(sF0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class))
| spl2_53 ),
inference(avatar_component_clause,[],[f1305]) ).
fof(f1307,plain,
( null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class))
| ~ spl2_53 ),
inference(avatar_component_clause,[],[f1305]) ).
fof(f1362,definition,
( spl2_56
<=> member(not_subclass_element(sF1,x),x) ),
introduced(definition,[new_symbols(definition,[spl2_56])],[avatar_definition]) ).
fof(f1363,plain,
( member(not_subclass_element(sF1,x),x)
| ~ spl2_56 ),
inference(avatar_component_clause,[],[f1362]) ).
fof(f1501,definition,
( spl2_69
<=> null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl2_69])],[avatar_definition]) ).
fof(f1503,plain,
( null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))
| ~ spl2_69 ),
inference(avatar_component_clause,[],[f1501]) ).
fof(f1505,definition,
( spl2_70
<=> subclass(sF1,x) ),
introduced(definition,[new_symbols(definition,[spl2_70])],[avatar_definition]) ).
fof(f1506,plain,
( subclass(sF1,x)
| ~ spl2_70 ),
inference(avatar_component_clause,[],[f1505]) ).
fof(f1507,plain,
( ~ subclass(sF1,x)
| spl2_70 ),
inference(avatar_component_clause,[],[f1505]) ).
fof(f1509,plain,
( regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))))))
| ~ spl2_15
| spl2_70 ),
inference(resolution,[],[f1507,f390]) ).
fof(f1511,definition,
( spl2_71
<=> regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl2_71])],[avatar_definition]) ).
fof(f1513,plain,
( regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))),unordered_pair(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),unordered_pair(second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),second(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))))))
| ~ spl2_71 ),
inference(avatar_component_clause,[],[f1511]) ).
fof(f1514,plain,
( spl2_71
| ~ spl2_15
| spl2_70 ),
inference(avatar_split_clause,[],[f1509,f1505,f389,f1511]) ).
fof(f1519,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),X0) )
| ~ spl2_71 ),
inference(superposition,[],[f139,f1513]) ).
fof(f1522,plain,
( ~ member(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))),sF0)
| member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),x)
| ~ spl2_2
| ~ spl2_71 ),
inference(superposition,[],[f209,f1513]) ).
fof(f1527,definition,
( spl2_72
<=> member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),x) ),
introduced(definition,[new_symbols(definition,[spl2_72])],[avatar_definition]) ).
fof(f1531,definition,
( spl2_73
<=> member(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))),sF0) ),
introduced(definition,[new_symbols(definition,[spl2_73])],[avatar_definition]) ).
fof(f1533,plain,
( ~ member(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))),sF0)
| spl2_73 ),
inference(avatar_component_clause,[],[f1531]) ).
fof(f1534,plain,
( spl2_72
| ~ spl2_73
| ~ spl2_2
| ~ spl2_71 ),
inference(avatar_split_clause,[],[f1522,f1511,f208,f1531,f1527]) ).
fof(f1535,plain,
( null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))
| spl2_73 ),
inference(resolution,[],[f1533,f253]) ).
fof(f1541,definition,
( spl2_74
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_74])],[avatar_definition]) ).
fof(f1542,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),X0) )
| ~ spl2_74 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1543,plain,
( spl2_74
| ~ spl2_71 ),
inference(avatar_split_clause,[],[f1519,f1511,f1541]) ).
fof(f1546,plain,
( spl2_69
| spl2_73 ),
inference(avatar_split_clause,[],[f1535,f1531,f1501]) ).
fof(f1552,plain,
( member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)))
| null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))
| ~ spl2_74 ),
inference(resolution,[],[f1542,f262]) ).
fof(f1572,definition,
( spl2_76
<=> member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x))) ),
introduced(definition,[new_symbols(definition,[spl2_76])],[avatar_definition]) ).
fof(f1574,plain,
( member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)))
| ~ spl2_76 ),
inference(avatar_component_clause,[],[f1572]) ).
fof(f1575,plain,
( spl2_69
| spl2_76
| ~ spl2_74 ),
inference(avatar_split_clause,[],[f1552,f1541,f1572,f1501]) ).
fof(f1633,plain,
( not_subclass_element(sF1,x) = first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))
| not_subclass_element(sF1,x) = first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))
| ~ spl2_76 ),
inference(resolution,[],[f8,f1574]) ).
fof(f1642,plain,
( not_subclass_element(sF1,x) = first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))
| ~ spl2_76 ),
inference(duplicate_literal_removal,[],[f1633]) ).
fof(f1644,definition,
( spl2_84
<=> not_subclass_element(sF1,x) = first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl2_84])],[avatar_definition]) ).
fof(f1647,plain,
( spl2_84
| ~ spl2_76 ),
inference(avatar_split_clause,[],[f1642,f1572,f1644]) ).
fof(f1648,plain,
( not_subclass_element(sF1,x) != first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class))))
| member(not_subclass_element(sF1,x),x)
| ~ member(first(regular(intersection(sF0,cross_product(unordered_pair(not_subclass_element(sF1,x),not_subclass_element(sF1,x)),universal_class)))),x) ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
fof(f1655,plain,
( subclass(sF1,x)
| ~ spl2_56 ),
inference(resolution,[],[f1363,f3]) ).
fof(f1656,plain,
( subclass(x,sF1)
| ~ spl2_52 ),
inference(resolution,[],[f1303,f2]) ).
fof(f1667,plain,
( ! [X0] :
( null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class))
| ~ member(not_subclass_element(x,sF1),X0)
| x = sF1 )
| ~ spl2_16
| ~ spl2_70 ),
inference(resolution,[],[f1506,f435]) ).
fof(f1668,plain,
( ~ subclass(x,sF1)
| x = sF1
| ~ spl2_70 ),
inference(resolution,[],[f1506,f7]) ).
fof(f1669,plain,
( ~ subclass(x,sF1)
| spl2_5
| ~ spl2_70 ),
inference(forward_subsumption_resolution,[],[f1668,f233]) ).
fof(f1674,plain,
( ! [X0] :
( null_class = intersection(sF0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class))
| ~ member(not_subclass_element(x,sF1),X0) )
| spl2_5
| ~ spl2_16
| ~ spl2_70 ),
inference(forward_subsumption_resolution,[],[f1667,f233]) ).
fof(f1686,plain,
( null_class != null_class
| ~ member(not_subclass_element(sF1,x),domain_of(sF0))
| ~ spl2_69 ),
inference(superposition,[],[f146,f1503]) ).
fof(f1692,plain,
( ~ member(not_subclass_element(sF1,x),domain_of(sF0))
| ~ spl2_69 ),
inference(trivial_inequality_removal,[],[f1686]) ).
fof(f1696,plain,
( ~ member(not_subclass_element(sF1,x),sF1)
| ~ spl2_4
| ~ spl2_69 ),
inference(forward_demodulation,[],[f1692,f228]) ).
fof(f1923,plain,
( spl2_70
| ~ spl2_56 ),
inference(avatar_split_clause,[],[f1655,f1362,f1505]) ).
fof(f1926,plain,
( null_class != null_class
| ~ member(not_subclass_element(x,sF1),domain_of(sF0))
| ~ spl2_53 ),
inference(superposition,[],[f146,f1307]) ).
fof(f1932,plain,
( ~ member(not_subclass_element(x,sF1),domain_of(sF0))
| ~ spl2_53 ),
inference(trivial_inequality_removal,[],[f1926]) ).
fof(f1934,plain,
( ~ member(not_subclass_element(x,sF1),sF1)
| ~ spl2_4
| ~ spl2_53 ),
inference(forward_demodulation,[],[f1932,f228]) ).
fof(f1938,definition,
( spl2_91
<=> member(not_subclass_element(sF1,x),sF1) ),
introduced(definition,[new_symbols(definition,[spl2_91])],[avatar_definition]) ).
fof(f1940,plain,
( ~ member(not_subclass_element(sF1,x),sF1)
| spl2_91 ),
inference(avatar_component_clause,[],[f1938]) ).
fof(f1941,plain,
( ~ spl2_91
| ~ spl2_4
| ~ spl2_69 ),
inference(avatar_split_clause,[],[f1696,f1501,f226,f1938]) ).
fof(f2012,definition,
( spl2_93
<=> member(not_subclass_element(x,sF1),sF1) ),
introduced(definition,[new_symbols(definition,[spl2_93])],[avatar_definition]) ).
fof(f2014,plain,
( ~ member(not_subclass_element(x,sF1),sF1)
| spl2_93 ),
inference(avatar_component_clause,[],[f2012]) ).
fof(f2015,plain,
( ~ spl2_93
| ~ spl2_4
| ~ spl2_53 ),
inference(avatar_split_clause,[],[f1934,f1305,f226,f2012]) ).
fof(f2019,plain,
( $false
| spl2_5
| ~ spl2_52
| ~ spl2_70 ),
inference(forward_subsumption_resolution,[],[f1656,f1669]) ).
fof(f2020,plain,
( spl2_5
| ~ spl2_52
| ~ spl2_70 ),
inference(avatar_contradiction_clause,[],[f2019]) ).
fof(f2032,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class))
| ~ member(X0,sF0) )
| ~ spl2_53 ),
inference(superposition,[],[f23,f1307]) ).
fof(f2052,definition,
( spl2_95
<=> ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class))
| ~ member(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl2_95])],[avatar_definition]) ).
fof(f2053,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),universal_class))
| member(X0,null_class)
| ~ member(X0,sF0) )
| ~ spl2_95 ),
inference(avatar_component_clause,[],[f2052]) ).
fof(f2054,plain,
( spl2_95
| ~ spl2_53 ),
inference(avatar_split_clause,[],[f2032,f1305,f2052]) ).
fof(f2055,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) )
| ~ spl2_95 ),
inference(resolution,[],[f2053,f141]) ).
fof(f2064,definition,
( spl2_96
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_96])],[avatar_definition]) ).
fof(f2065,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) )
| ~ spl2_96 ),
inference(avatar_component_clause,[],[f2064]) ).
fof(f2066,plain,
( spl2_96
| ~ spl2_95 ),
inference(avatar_split_clause,[],[f2055,f2052,f2064]) ).
fof(f2175,definition,
( spl2_105
<=> ! [X1] :
( ~ member(X1,universal_class)
| ~ member(X1,y) ) ),
introduced(definition,[new_symbols(definition,[spl2_105])],[avatar_definition]) ).
fof(f2176,plain,
( ! [X1] :
( ~ member(X1,y)
| ~ member(X1,universal_class) )
| ~ spl2_105 ),
inference(avatar_component_clause,[],[f2175]) ).
fof(f2540,plain,
( ! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| null_class = X2
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) )
| ~ spl2_96 ),
inference(resolution,[],[f256,f2065]) ).
fof(f2620,definition,
( spl2_138
<=> ! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| null_class = X2
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_138])],[avatar_definition]) ).
fof(f2621,plain,
( ! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| null_class = X2
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) )
| ~ spl2_138 ),
inference(avatar_component_clause,[],[f2620]) ).
fof(f2622,plain,
( spl2_138
| ~ spl2_96 ),
inference(avatar_split_clause,[],[f2540,f2064,f2620]) ).
fof(f2623,plain,
( ! [X2,X0,X1] :
( null_class = X0
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),X0)
| ~ member(X2,universal_class)
| ~ member(X1,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)))
| ~ member(X2,y)
| ~ member(X1,x) )
| ~ spl2_6
| ~ spl2_138 ),
inference(resolution,[],[f2621,f241]) ).
fof(f3187,definition,
( spl2_160
<=> member(not_subclass_element(x,sF1),x) ),
introduced(definition,[new_symbols(definition,[spl2_160])],[avatar_definition]) ).
fof(f3188,plain,
( member(not_subclass_element(x,sF1),x)
| ~ spl2_160 ),
inference(avatar_component_clause,[],[f3187]) ).
fof(f3189,plain,
( ~ member(not_subclass_element(x,sF1),x)
| spl2_160 ),
inference(avatar_component_clause,[],[f3187]) ).
fof(f3335,plain,
( subclass(sF1,x)
| spl2_91 ),
inference(resolution,[],[f1940,f2]) ).
fof(f3337,plain,
( $false
| spl2_70
| spl2_91 ),
inference(forward_subsumption_resolution,[],[f3335,f1507]) ).
fof(f3338,plain,
( spl2_70
| spl2_91 ),
inference(avatar_contradiction_clause,[],[f3337]) ).
fof(f3340,plain,
( ! [X0] : ~ member(not_subclass_element(x,sF1),X0)
| spl2_5
| ~ spl2_16
| spl2_53
| ~ spl2_70 ),
inference(forward_subsumption_resolution,[],[f1674,f1306]) ).
fof(f3347,plain,
( spl2_52
| spl2_5
| ~ spl2_16
| spl2_53
| ~ spl2_70 ),
inference(avatar_split_clause,[],[f3340,f1505,f1305,f434,f231,f1302]) ).
fof(f3431,plain,
( subclass(x,sF1)
| spl2_160 ),
inference(resolution,[],[f3189,f2]) ).
fof(f3433,plain,
( $false
| spl2_5
| ~ spl2_70
| spl2_160 ),
inference(forward_subsumption_resolution,[],[f3431,f1669]) ).
fof(f3434,plain,
( spl2_5
| ~ spl2_70
| spl2_160 ),
inference(avatar_contradiction_clause,[],[f3433]) ).
fof(f3559,plain,
( ~ member(regular(y),universal_class)
| null_class = y
| ~ spl2_105 ),
inference(resolution,[],[f2176,f68]) ).
fof(f3563,plain,
( ~ member(regular(y),universal_class)
| spl2_7
| ~ spl2_105 ),
inference(forward_subsumption_resolution,[],[f3559,f260]) ).
fof(f3903,definition,
( spl2_180
<=> ! [X2,X0,X1] :
( null_class = X0
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),X0)
| ~ member(X2,universal_class)
| ~ member(X1,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)))
| ~ member(X2,y)
| ~ member(X1,x) ) ),
introduced(definition,[new_symbols(definition,[spl2_180])],[avatar_definition]) ).
fof(f3904,plain,
( ! [X2,X0,X1] :
( ~ member(X1,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)))
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),X0)
| ~ member(X2,universal_class)
| null_class = X0
| ~ member(X2,y)
| ~ member(X1,x) )
| ~ spl2_180 ),
inference(avatar_component_clause,[],[f3903]) ).
fof(f3905,plain,
( spl2_180
| ~ spl2_6
| ~ spl2_138 ),
inference(avatar_split_clause,[],[f2623,f2620,f240,f3903]) ).
fof(f3906,plain,
( ! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(X0,X0))),X1)
| ~ member(X0,universal_class)
| null_class = X1
| ~ member(X0,y)
| ~ member(not_subclass_element(x,sF1),x)
| ~ member(not_subclass_element(x,sF1),X2) )
| ~ spl2_180 ),
inference(resolution,[],[f3904,f412]) ).
fof(f3916,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(x,sF1),x)
| member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(X0,X0))),X1)
| ~ member(X0,universal_class)
| null_class = X1
| ~ member(X0,y) )
| ~ spl2_180 ),
inference(condensation,[],[f3906]) ).
fof(f3917,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(X0,X0))),X1)
| ~ member(X0,universal_class)
| null_class = X1
| ~ member(X0,y) )
| ~ spl2_160
| ~ spl2_180 ),
inference(forward_subsumption_resolution,[],[f3916,f3188]) ).
fof(f3919,definition,
( spl2_181
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(X0,X0))),X1)
| ~ member(X0,universal_class)
| null_class = X1
| ~ member(X0,y) ) ),
introduced(definition,[new_symbols(definition,[spl2_181])],[avatar_definition]) ).
fof(f3920,plain,
( ! [X0,X1] :
( ~ member(X0,y)
| ~ member(X0,universal_class)
| null_class = X1
| member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(X0,X0))),X1) )
| ~ spl2_181 ),
inference(avatar_component_clause,[],[f3919]) ).
fof(f3921,plain,
( spl2_181
| ~ spl2_160
| ~ spl2_180 ),
inference(avatar_split_clause,[],[f3917,f3903,f3187,f3919]) ).
fof(f3927,plain,
( ! [X0] :
( ~ member(regular(y),universal_class)
| null_class = X0
| member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(regular(y),regular(y)))),X0)
| null_class = y )
| ~ spl2_181 ),
inference(resolution,[],[f3920,f68]) ).
fof(f3933,plain,
( ! [X0] :
( ~ member(regular(y),universal_class)
| null_class = X0
| member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(regular(y),regular(y)))),X0) )
| spl2_7
| ~ spl2_181 ),
inference(forward_subsumption_resolution,[],[f3927,f260]) ).
fof(f3969,definition,
( spl2_183
<=> ! [X0,X1] :
( cross_product(X0,X1) = null_class
| member(not_subclass_element(x,sF1),X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_183])],[avatar_definition]) ).
fof(f3970,plain,
( ! [X0,X1] :
( member(not_subclass_element(x,sF1),X0)
| cross_product(X0,X1) = null_class )
| ~ spl2_183 ),
inference(avatar_component_clause,[],[f3969]) ).
fof(f3976,plain,
( ! [X0] : null_class = cross_product(sF1,X0)
| spl2_93
| ~ spl2_183 ),
inference(resolution,[],[f3970,f2014]) ).
fof(f3993,definition,
( spl2_184
<=> ! [X0] : null_class = cross_product(sF1,X0) ),
introduced(definition,[new_symbols(definition,[spl2_184])],[avatar_definition]) ).
fof(f3994,plain,
( ! [X0] : null_class = cross_product(sF1,X0)
| ~ spl2_184 ),
inference(avatar_component_clause,[],[f3993]) ).
fof(f3995,plain,
( spl2_184
| spl2_93
| ~ spl2_183 ),
inference(avatar_split_clause,[],[f3976,f3969,f2012,f3993]) ).
fof(f4720,definition,
( spl2_218
<=> ! [X0] :
( null_class = X0
| member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(regular(y),regular(y)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_218])],[avatar_definition]) ).
fof(f4721,plain,
( ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)),unordered_pair(not_subclass_element(x,sF1),unordered_pair(regular(y),regular(y)))),X0)
| null_class = X0 )
| ~ spl2_218 ),
inference(avatar_component_clause,[],[f4720]) ).
fof(f4723,definition,
( spl2_219
<=> member(regular(y),universal_class) ),
introduced(definition,[new_symbols(definition,[spl2_219])],[avatar_definition]) ).
fof(f4724,plain,
( member(regular(y),universal_class)
| ~ spl2_219 ),
inference(avatar_component_clause,[],[f4723]) ).
fof(f4725,plain,
( ~ member(regular(y),universal_class)
| spl2_219 ),
inference(avatar_component_clause,[],[f4723]) ).
fof(f4726,plain,
( spl2_218
| ~ spl2_219
| spl2_7
| ~ spl2_181 ),
inference(avatar_split_clause,[],[f3933,f3919,f258,f4723,f4720]) ).
fof(f4727,plain,
( ! [X0] :
( ~ member(regular(y),X0)
| ~ subclass(X0,universal_class) )
| spl2_219 ),
inference(resolution,[],[f4725,f1]) ).
fof(f4728,plain,
( ! [X0] : ~ member(regular(y),X0)
| spl2_219 ),
inference(forward_subsumption_resolution,[],[f4727,f4]) ).
fof(f4730,definition,
( spl2_220
<=> ! [X0] : ~ member(regular(y),X0) ),
introduced(definition,[new_symbols(definition,[spl2_220])],[avatar_definition]) ).
fof(f4731,plain,
( ! [X0] : ~ member(regular(y),X0)
| ~ spl2_220 ),
inference(avatar_component_clause,[],[f4730]) ).
fof(f4732,plain,
( spl2_220
| spl2_219 ),
inference(avatar_split_clause,[],[f4728,f4723,f4730]) ).
fof(f4734,plain,
( null_class = y
| ~ spl2_220 ),
inference(resolution,[],[f4731,f68]) ).
fof(f4745,plain,
( $false
| spl2_7
| ~ spl2_220 ),
inference(forward_subsumption_resolution,[],[f4734,f260]) ).
fof(f4746,plain,
( spl2_7
| ~ spl2_220 ),
inference(avatar_contradiction_clause,[],[f4745]) ).
fof(f4751,plain,
( ! [X0,X1] :
( cross_product(X0,X1) = null_class
| member(not_subclass_element(x,sF1),X0) )
| ~ spl2_218 ),
inference(resolution,[],[f4721,f139]) ).
fof(f4888,plain,
( spl2_183
| ~ spl2_218 ),
inference(avatar_split_clause,[],[f4751,f4720,f3969]) ).
fof(f4946,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X0,sF1) )
| ~ spl2_184 ),
inference(superposition,[],[f139,f3994]) ).
fof(f5034,plain,
( $false
| spl2_7
| ~ spl2_105
| ~ spl2_219 ),
inference(forward_subsumption_resolution,[],[f3563,f4724]) ).
fof(f5035,plain,
( spl2_7
| ~ spl2_105
| ~ spl2_219 ),
inference(avatar_contradiction_clause,[],[f5034]) ).
fof(f5773,definition,
( spl2_256
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl2_256])],[avatar_definition]) ).
fof(f5774,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| member(X0,sF1) )
| ~ spl2_256 ),
inference(avatar_component_clause,[],[f5773]) ).
fof(f5775,plain,
( spl2_256
| ~ spl2_184 ),
inference(avatar_split_clause,[],[f4946,f3993,f5773]) ).
fof(f5778,plain,
( ! [X0,X1] :
( member(X0,sF1)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) )
| ~ spl2_96
| ~ spl2_256 ),
inference(resolution,[],[f5774,f2065]) ).
fof(f5869,definition,
( spl2_264
<=> ! [X0,X1] :
( member(X0,sF1)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_264])],[avatar_definition]) ).
fof(f5870,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,sF1)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) )
| ~ spl2_264 ),
inference(avatar_component_clause,[],[f5869]) ).
fof(f5871,plain,
( spl2_264
| ~ spl2_96
| ~ spl2_256 ),
inference(avatar_split_clause,[],[f5778,f5773,f2064,f5869]) ).
fof(f5872,plain,
( ! [X0,X1] :
( member(X0,sF1)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)))
| ~ member(X1,y)
| ~ member(X0,x) )
| ~ spl2_6
| ~ spl2_264 ),
inference(resolution,[],[f5870,f241]) ).
fof(f5896,definition,
( spl2_265
<=> ! [X0] :
( member(X0,sF1)
| ~ member(X0,x)
| ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1))) ) ),
introduced(definition,[new_symbols(definition,[spl2_265])],[avatar_definition]) ).
fof(f5897,plain,
( ! [X0] :
( ~ member(X0,unordered_pair(not_subclass_element(x,sF1),not_subclass_element(x,sF1)))
| ~ member(X0,x)
| member(X0,sF1) )
| ~ spl2_265 ),
inference(avatar_component_clause,[],[f5896]) ).
fof(f5898,plain,
( spl2_105
| spl2_265
| ~ spl2_6
| ~ spl2_264 ),
inference(avatar_split_clause,[],[f5872,f5869,f240,f5896,f2175]) ).
fof(f5899,plain,
( ! [X0] :
( ~ member(not_subclass_element(x,sF1),x)
| member(not_subclass_element(x,sF1),sF1)
| ~ member(not_subclass_element(x,sF1),X0) )
| ~ spl2_265 ),
inference(resolution,[],[f5897,f412]) ).
fof(f5911,plain,
( ~ member(not_subclass_element(x,sF1),x)
| member(not_subclass_element(x,sF1),sF1)
| ~ spl2_265 ),
inference(condensation,[],[f5899]) ).
fof(f5915,plain,
( member(not_subclass_element(x,sF1),sF1)
| ~ spl2_160
| ~ spl2_265 ),
inference(forward_subsumption_resolution,[],[f5911,f3188]) ).
fof(f5918,plain,
( $false
| spl2_93
| ~ spl2_160
| ~ spl2_265 ),
inference(forward_subsumption_resolution,[],[f5915,f2014]) ).
fof(f5919,plain,
( spl2_93
| ~ spl2_160
| ~ spl2_265 ),
inference(avatar_contradiction_clause,[],[f5918]) ).
cnf(s97,plain,
spl2_1,
inference(sat_conversion,[],[f202]) ).
cnf(s103,plain,
( ~ spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f210]) ).
cnf(s115,plain,
spl2_4,
inference(sat_conversion,[],[f229]) ).
cnf(s117,plain,
~ spl2_5,
inference(sat_conversion,[],[f234]) ).
cnf(s121,plain,
( ~ spl2_1
| spl2_6 ),
inference(sat_conversion,[],[f242]) ).
cnf(s133,plain,
~ spl2_7,
inference(sat_conversion,[],[f261]) ).
cnf(s160,plain,
( ~ spl2_4
| spl2_11 ),
inference(sat_conversion,[],[f301]) ).
cnf(s163,plain,
( ~ spl2_11
| spl2_12 ),
inference(sat_conversion,[],[f306]) ).
cnf(s197,plain,
( ~ spl2_4
| spl2_14 ),
inference(sat_conversion,[],[f381]) ).
cnf(s204,plain,
( ~ spl2_14
| spl2_15 ),
inference(sat_conversion,[],[f391]) ).
cnf(s242,plain,
( ~ spl2_12
| spl2_16 ),
inference(sat_conversion,[],[f436]) ).
cnf(s983,plain,
( ~ spl2_15
| spl2_70
| spl2_71 ),
inference(sat_conversion,[],[f1514]) ).
cnf(s992,plain,
( ~ spl2_2
| ~ spl2_71
| spl2_72
| ~ spl2_73 ),
inference(sat_conversion,[],[f1534]) ).
cnf(s997,plain,
( ~ spl2_71
| spl2_74 ),
inference(sat_conversion,[],[f1543]) ).
cnf(s999,plain,
( spl2_69
| spl2_73 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s1013,plain,
( spl2_69
| ~ spl2_74
| spl2_76 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s1033,plain,
( ~ spl2_76
| spl2_84 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s1034,plain,
( spl2_56
| ~ spl2_72
| ~ spl2_84 ),
inference(sat_conversion,[],[f1648]) ).
cnf(s1199,plain,
( ~ spl2_56
| spl2_70 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s1204,plain,
( ~ spl2_4
| ~ spl2_69
| ~ spl2_91 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s1321,plain,
( ~ spl2_4
| ~ spl2_53
| ~ spl2_93 ),
inference(sat_conversion,[],[f2015]) ).
cnf(s1341,plain,
( spl2_5
| ~ spl2_52
| ~ spl2_70 ),
inference(sat_conversion,[],[f2020]) ).
cnf(s1392,plain,
( ~ spl2_53
| spl2_95 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s1400,plain,
( ~ spl2_95
| spl2_96 ),
inference(sat_conversion,[],[f2066]) ).
cnf(s1636,plain,
( ~ spl2_96
| spl2_138 ),
inference(sat_conversion,[],[f2622]) ).
cnf(s1938,plain,
( spl2_70
| spl2_91 ),
inference(sat_conversion,[],[f3338]) ).
cnf(s1943,plain,
( spl2_5
| ~ spl2_16
| spl2_52
| spl2_53
| ~ spl2_70 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s2043,plain,
( spl2_5
| ~ spl2_70
| spl2_160 ),
inference(sat_conversion,[],[f3434]) ).
cnf(s2339,plain,
( ~ spl2_6
| ~ spl2_138
| spl2_180 ),
inference(sat_conversion,[],[f3905]) ).
cnf(s2350,plain,
( ~ spl2_160
| ~ spl2_180
| spl2_181 ),
inference(sat_conversion,[],[f3921]) ).
cnf(s2398,plain,
( spl2_93
| ~ spl2_183
| spl2_184 ),
inference(sat_conversion,[],[f3995]) ).
cnf(s2646,plain,
( spl2_7
| ~ spl2_181
| spl2_218
| ~ spl2_219 ),
inference(sat_conversion,[],[f4726]) ).
cnf(s2649,plain,
( spl2_219
| spl2_220 ),
inference(sat_conversion,[],[f4732]) ).
cnf(s2654,plain,
( spl2_7
| ~ spl2_220 ),
inference(sat_conversion,[],[f4746]) ).
cnf(s2755,plain,
( spl2_183
| ~ spl2_218 ),
inference(sat_conversion,[],[f4888]) ).
cnf(s2857,plain,
( spl2_7
| ~ spl2_105
| ~ spl2_219 ),
inference(sat_conversion,[],[f5035]) ).
cnf(s3222,plain,
( ~ spl2_184
| spl2_256 ),
inference(sat_conversion,[],[f5775]) ).
cnf(s3264,plain,
( ~ spl2_96
| ~ spl2_256
| spl2_264 ),
inference(sat_conversion,[],[f5871]) ).
cnf(s3273,plain,
( ~ spl2_6
| spl2_105
| ~ spl2_264
| spl2_265 ),
inference(sat_conversion,[],[f5898]) ).
cnf(s3283,plain,
( spl2_93
| ~ spl2_160
| ~ spl2_265 ),
inference(sat_conversion,[],[f5919]) ).
cnf(s3292,plain,
~ spl2_220,
inference(rat,[],[s2654,s133]) ).
cnf(s3294,plain,
spl2_219,
inference(rat,[],[s2649,s3292]) ).
cnf(s3295,plain,
~ spl2_105,
inference(rat,[],[s2857,s133,s3294]) ).
cnf(s3296,plain,
spl2_14,
inference(rat,[],[s197,s115]) ).
cnf(s3297,plain,
spl2_11,
inference(rat,[],[s160,s115]) ).
cnf(s3298,plain,
spl2_15,
inference(rat,[],[s204,s3296]) ).
cnf(s3299,plain,
spl2_12,
inference(rat,[],[s163,s3297]) ).
cnf(s3300,plain,
spl2_16,
inference(rat,[],[s242,s3299]) ).
cnf(s3303,plain,
spl2_6,
inference(rat,[],[s121,s97]) ).
cnf(s3305,plain,
spl2_2,
inference(rat,[],[s103,s97]) ).
cnf(s3312,plain,
spl2_70,
inference(rat,[],[s1034,s1033,s992,s1013,s999,s997,s1204,s983,s1199,s1938,s3305,s115,s3298]) ).
cnf(s3313,plain,
spl2_160,
inference(rat,[],[s2043,s117,s3312]) ).
cnf(s3315,plain,
~ spl2_52,
inference(rat,[],[s1341,s117,s3312]) ).
cnf(s3316,plain,
spl2_53,
inference(rat,[],[s1943,s3315,s3300,s117,s3312]) ).
cnf(s3321,plain,
spl2_95,
inference(rat,[],[s1392,s3316]) ).
cnf(s3322,plain,
~ spl2_93,
inference(rat,[],[s1321,s115,s3316]) ).
cnf(s3329,plain,
spl2_96,
inference(rat,[],[s1400,s3321]) ).
cnf(s3330,plain,
~ spl2_265,
inference(rat,[],[s3283,s3313,s3322]) ).
cnf(s3333,plain,
spl2_138,
inference(rat,[],[s1636,s3329]) ).
cnf(s3334,plain,
~ spl2_264,
inference(rat,[],[s3273,s3303,s3295,s3330]) ).
cnf(s3338,plain,
spl2_180,
inference(rat,[],[s2339,s3303,s3333]) ).
cnf(s3339,plain,
~ spl2_256,
inference(rat,[],[s3264,s3329,s3334]) ).
cnf(s3342,plain,
spl2_181,
inference(rat,[],[s2350,s3313,s3338]) ).
cnf(s3343,plain,
~ spl2_184,
inference(rat,[],[s3222,s3339]) ).
cnf(s3344,plain,
spl2_218,
inference(rat,[],[s2646,s3294,s133,s3342]) ).
cnf(s3345,plain,
~ spl2_183,
inference(rat,[],[s2398,s3322,s3343]) ).
cnf(s3346,plain,
$false,
inference(rat,[],[s2755,s3344,s3345]) ).
fof(f5920,plain,
$false,
inference(avatar_sat_refutation,[],[s3346]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET270-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n013.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 01:15:37 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.20/2.46 % (721609)Input is clausal, will run a generic CNF schedule.
% 11.20/2.46 % (721620)dis-21_1_sil=8000:lcm=predicate:random_seed=704822998:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.20/2.46 % (721620)Instruction limit reached!
% 11.20/2.46 % (721620)------------------------------
% 11.20/2.46 % (721620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.20/2.46 % (721620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.20/2.46 % (721620)CaDiCaL version: 2.1.3
% 11.20/2.46 % (721620)Termination reason: Instruction limit
% 11.20/2.46 % (721620)Termination phase: Saturation
% 11.20/2.46 % (721620)Time elapsed: 0.041 s
% 11.20/2.46 % (721620)Peak memory usage: 89 MB
% 11.20/2.46 % (721620)Instructions burned: 125 (million)
% 11.20/2.46 % (721614)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=3155343003:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.20/2.46 % (721615)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4138261584:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.20/2.46 % (721618)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3657169989:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.20/2.46 % (721616)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3759899339:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.20/2.46 % (721617)lrs+10_1_sil=8000:sp=occurrence:random_seed=1273628339:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.20/2.46 % (721619)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3150242913:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.20/2.46 % (721617)Refutation not found, incomplete strategy
% 11.20/2.46 % (721617)------------------------------
% 11.20/2.46 % (721617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.20/2.46 % (721617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.20/2.46 % (721617)CaDiCaL version: 2.1.3
% 11.20/2.46 % (721617)Termination reason: Refutation not found, incomplete strategy
% 11.20/2.46 % (721617)Time elapsed: 0.001 s
% 11.20/2.46 % (721617)Peak memory usage: 87 MB
% 11.20/2.46 % (721618)Instruction limit reached!
% 11.20/2.46 % (721618)------------------------------
% 11.20/2.46 % (721618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.20/2.46 % (721618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.20/2.46 % (721618)CaDiCaL version: 2.1.3
% 11.20/2.46 % (721618)Termination reason: Instruction limit
% 11.20/2.46 % (721618)Termination phase: Saturation
% 11.20/2.46 % (721618)Time elapsed: 0.068 s
% 11.20/2.46 % (721618)Peak memory usage: 88 MB
% 11.20/2.46 % (721618)Instructions burned: 116 (million)
% 11.20/2.46 % (721628)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=1742630301:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.20/2.46 % (721628)Refutation not found, incomplete strategy
% 11.20/2.46 % (721628)------------------------------
% 11.20/2.46 % (721628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.20/2.46 % (721628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.20/2.46 % (721628)CaDiCaL version: 2.1.3
% 11.20/2.46 % (721628)Termination reason: Refutation not found, incomplete strategy
% 11.20/2.46 % (721628)Time elapsed: 0.001 s
% 11.20/2.46 % (721628)Peak memory usage: 88 MB
% 11.20/2.46 % (721628)Instructions burned: 2 (million)
% 11.20/2.46 % (721619)Instruction limit reached!
% 11.20/2.46 % (721619)------------------------------
% 11.20/2.46 % (721619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.20/2.46 % (721619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.20/2.46 % (721619)CaDiCaL version: 2.1.3
% 11.20/2.46 % (721619)Termination reason: Instruction limit
% 11.20/2.46 % (721619)Termination phase: Saturation
% 11.20/2.46 % (721619)Time elapsed: 0.137 s
% 11.20/2.46 % (721619)Peak memory usage: 90 MB
% 11.20/2.46 % (721619)Instructions burned: 180 (million)
% 11.20/2.46 % (721629)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3941863876: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)
% 17.40/3.32 % (721628)------------------------------
% 17.40/3.32 % (721628)------------------------------
% 17.40/3.32 % (721617)------------------------------
% 17.40/3.32 % (721617)------------------------------
% 17.40/3.32 % (721631)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1931924756:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 17.40/3.32 % (721631)Refutation not found, incomplete strategy
% 17.40/3.32 % (721631)------------------------------
% 17.40/3.32 % (721631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.32 % (721631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.32 % (721631)CaDiCaL version: 2.1.3
% 17.40/3.32 % (721631)Termination reason: Refutation not found, incomplete strategy
% 17.40/3.32 % (721631)Time elapsed: 0.003 s
% 17.40/3.32 % (721631)Peak memory usage: 88 MB
% 17.40/3.32 % (721631)Instructions burned: 4 (million)
% 17.40/3.32 % (721629)Instruction limit reached!
% 17.40/3.32 % (721629)------------------------------
% 17.40/3.32 % (721629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.32 % (721629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.32 % (721629)CaDiCaL version: 2.1.3
% 17.40/3.32 % (721629)Termination reason: Instruction limit
% 17.40/3.32 % (721629)Termination phase: Saturation
% 17.40/3.32 % (721629)Time elapsed: 0.109 s
% 17.40/3.32 % (721629)Peak memory usage: 91 MB
% 17.40/3.32 % (721629)Instructions burned: 189 (million)
% 17.40/3.32 % (721633)lrs+10_64_to=lpo:sil=8000:random_seed=4243985657:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 17.40/3.32 % (721633)Instruction limit reached!
% 17.40/3.32 % (721633)------------------------------
% 17.40/3.32 % (721633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.32 % (721633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.32 % (721633)CaDiCaL version: 2.1.3
% 17.40/3.32 % (721633)Termination reason: Instruction limit
% 17.40/3.32 % (721633)Termination phase: Saturation
% 17.40/3.32 % (721633)Time elapsed: 0.044 s
% 17.40/3.32 % (721633)Peak memory usage: 89 MB
% 17.40/3.32 % (721633)Instructions burned: 127 (million)
% 17.40/3.32 % (721634)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=423484481:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 17.40/3.32 % (721636)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1473751320:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 17.40/3.32 % (721638)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2340319654:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 17.40/3.32 % (721631)------------------------------
% 17.40/3.32 % (721631)------------------------------
% 17.40/3.32 % (721634)Instruction limit reached!
% 17.40/3.32 % (721634)------------------------------
% 17.40/3.32 % (721634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.32 % (721634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.32 % (721634)CaDiCaL version: 2.1.3
% 17.40/3.32 % (721634)Termination reason: Instruction limit
% 17.40/3.32 % (721634)Termination phase: Saturation
% 17.40/3.32 % (721634)Time elapsed: 0.124 s
% 17.40/3.32 % (721634)Peak memory usage: 89 MB
% 17.40/3.32 % (721634)Instructions burned: 196 (million)
% 17.40/3.32 % (721636)Instruction limit reached!
% 17.40/3.32 % (721636)------------------------------
% 17.40/3.32 % (721636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.40/3.32 % (721636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.40/3.32 % (721636)CaDiCaL version: 2.1.3
% 17.40/3.32 % (721636)Termination reason: Instruction limit
% 17.40/3.32 % (721636)Termination phase: Saturation
% 17.40/3.32 % (721636)Time elapsed: 0.107 s
% 17.40/3.32 % (721636)Peak memory usage: 91 MB
% 17.40/3.32 % (721636)Instructions burned: 158 (million)
% 17.40/3.32 % (721643)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2581847720:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 17.40/3.32 % (721642)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=483016833:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 17.40/3.32 % (721643)Refutation not found, incomplete strategy
% 17.40/3.32 % (721643)------------------------------
% 33.86/5.67 % (721643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.86/5.67 % (721643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.86/5.67 % (721643)CaDiCaL version: 2.1.3
% 33.86/5.67 % (721643)Termination reason: Refutation not found, incomplete strategy
% 33.86/5.67 % (721643)Time elapsed: 0.005 s
% 33.86/5.67 % (721643)Peak memory usage: 88 MB
% 33.86/5.67 % (721643)Instructions burned: 8 (million)
% 33.86/5.67 % (721644)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1736941979:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 33.86/5.67 % (721642)Instruction limit reached!
% 33.86/5.67 % (721642)------------------------------
% 33.86/5.67 % (721642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.86/5.67 % (721642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.86/5.67 % (721642)CaDiCaL version: 2.1.3
% 33.86/5.67 % (721642)Termination reason: Instruction limit
% 33.86/5.67 % (721642)Termination phase: Saturation
% 33.86/5.67 % (721642)Time elapsed: 0.063 s
% 33.86/5.67 % (721642)Peak memory usage: 89 MB
% 33.86/5.67 % (721642)Instructions burned: 107 (million)
% 33.86/5.67 % (721644)Instruction limit reached!
% 33.86/5.67 % (721644)------------------------------
% 33.86/5.67 % (721644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.86/5.67 % (721644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.86/5.67 % (721644)CaDiCaL version: 2.1.3
% 33.86/5.67 % (721644)Termination reason: Instruction limit
% 33.86/5.67 % (721644)Termination phase: Saturation
% 33.86/5.67 % (721644)Time elapsed: 0.162 s
% 33.86/5.67 % (721644)Peak memory usage: 90 MB
% 33.86/5.67 % (721644)Instructions burned: 242 (million)
% 33.86/5.67 % (721648)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3622243570:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 33.86/5.67 % (721643)------------------------------
% 33.86/5.67 % (721643)------------------------------
% 33.86/5.67 % (721650)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4009094041:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 33.86/5.67 % (721651)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2367512150:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 33.86/5.67 % (721650)Instruction limit reached!
% 33.86/5.67 % (721650)------------------------------
% 33.86/5.67 % (721650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.86/5.67 % (721650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.86/5.67 % (721650)CaDiCaL version: 2.1.3
% 33.86/5.67 % (721650)Termination reason: Instruction limit
% 33.86/5.67 % (721650)Termination phase: Saturation
% 33.86/5.67 % (721650)Time elapsed: 0.098 s
% 33.86/5.67 % (721650)Peak memory usage: 90 MB
% 33.86/5.67 % (721650)Instructions burned: 134 (million)
% 33.86/5.67 % (721654)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4175521295:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 33.86/5.67 % (721651)Instruction limit reached!
% 33.86/5.67 % (721651)------------------------------
% 33.86/5.67 % (721651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.86/5.67 % (721651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.86/5.67 % (721651)CaDiCaL version: 2.1.3
% 33.86/5.67 % (721651)Termination reason: Instruction limit
% 33.86/5.67 % (721651)Termination phase: Saturation
% 33.86/5.67 % (721651)Time elapsed: 0.295 s
% 33.86/5.67 % (721651)Peak memory usage: 94 MB
% 33.86/5.67 % (721651)Instructions burned: 499 (million)
% 33.86/5.67 % (721654)Instruction limit reached!
% 33.86/5.67 % (721654)------------------------------
% 33.86/5.67 % (721654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.86/5.67 % (721654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.86/5.67 % (721654)CaDiCaL version: 2.1.3
% 33.86/5.67 % (721654)Termination reason: Instruction limit
% 33.86/5.67 % (721654)Termination phase: Saturation
% 33.86/5.67 % (721654)Time elapsed: 0.110 s
% 33.86/5.67 % (721654)Peak memory usage: 89 MB
% 33.86/5.67 % (721654)Instructions burned: 191 (million)
% 33.86/5.67 % (721656)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3546867040:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 48.34/7.74 % (721657)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2415329082:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 48.34/7.74 % (721657)Instruction limit reached!
% 48.34/7.74 % (721657)------------------------------
% 48.34/7.74 % (721657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.74 % (721657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.74 % (721657)CaDiCaL version: 2.1.3
% 48.34/7.74 % (721657)Termination reason: Instruction limit
% 48.34/7.74 % (721657)Termination phase: Saturation
% 48.34/7.74 % (721657)Time elapsed: 0.106 s
% 48.34/7.74 % (721657)Peak memory usage: 89 MB
% 48.34/7.74 % (721657)Instructions burned: 157 (million)
% 48.34/7.74 % (721656)Instruction limit reached!
% 48.34/7.74 % (721656)------------------------------
% 48.34/7.74 % (721656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.74 % (721656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.74 % (721656)CaDiCaL version: 2.1.3
% 48.34/7.74 % (721656)Termination reason: Instruction limit
% 48.34/7.74 % (721656)Termination phase: Saturation
% 48.34/7.74 % (721656)Time elapsed: 0.167 s
% 48.34/7.74 % (721656)Peak memory usage: 92 MB
% 48.34/7.74 % (721656)Instructions burned: 265 (million)
% 48.34/7.74 % (721660)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=3131069912:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 48.34/7.74 % (721638)Instruction limit reached!
% 48.34/7.74 % (721638)------------------------------
% 48.34/7.74 % (721638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.74 % (721638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.74 % (721638)CaDiCaL version: 2.1.3
% 48.34/7.74 % (721638)Termination reason: Instruction limit
% 48.34/7.74 % (721638)Termination phase: Saturation
% 48.34/7.74 % (721638)Time elapsed: 1.253 s
% 48.34/7.74 % (721638)Peak memory usage: 149 MB
% 48.34/7.74 % (721638)Instructions burned: 3396 (million)
% 48.34/7.74 % (721661)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=4063050042:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 48.34/7.74 % (721661)Refutation not found, incomplete strategy
% 48.34/7.74 % (721661)------------------------------
% 48.34/7.74 % (721661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.74 % (721661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.74 % (721661)CaDiCaL version: 2.1.3
% 48.34/7.74 % (721661)Termination reason: Refutation not found, incomplete strategy
% 48.34/7.74 % (721661)Time elapsed: 0.001 s
% 48.34/7.74 % (721661)Peak memory usage: 87 MB
% 48.34/7.74 % (721663)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2775524919:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 48.34/7.74 % (721663)Instruction limit reached!
% 48.34/7.74 % (721663)------------------------------
% 48.34/7.74 % (721663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.74 % (721663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.74 % (721663)CaDiCaL version: 2.1.3
% 48.34/7.74 % (721663)Termination reason: Instruction limit
% 48.34/7.74 % (721663)Termination phase: Saturation
% 48.34/7.74 % (721663)Time elapsed: 0.050 s
% 48.34/7.74 % (721663)Peak memory usage: 90 MB
% 48.34/7.74 % (721663)Instructions burned: 183 (million)
% 48.34/7.74 % (721666)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=4160854584:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi)
% 48.34/7.74 % (721661)------------------------------
% 48.34/7.74 % (721661)------------------------------
% 48.34/7.74 % (721668)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=2499963839:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi)
% 48.34/7.74 % (721668)Instruction limit reached!
% 48.34/7.74 % (721668)------------------------------
% 48.34/7.74 % (721668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.34/7.74 % (721668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.34/7.74 % (721668)CaDiCaL version: 2.1.3
% 65.39/10.10 % (721668)Termination reason: Instruction limit
% 65.39/10.10 % (721668)Termination phase: Saturation
% 65.39/10.10 % (721668)Time elapsed: 0.182 s
% 65.39/10.10 % (721668)Peak memory usage: 90 MB
% 65.39/10.10 % (721668)Instructions burned: 413 (million)
% 65.39/10.10 % (721670)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=2997673036:s2pl=no:i=8478:s2at=4:nm=6_2975 on theBenchmark for (2975ds/8478Mi)
% 65.39/10.10 % (721660)Instruction limit reached!
% 65.39/10.10 % (721660)------------------------------
% 65.39/10.10 % (721660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.39/10.10 % (721660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.39/10.10 % (721660)CaDiCaL version: 2.1.3
% 65.39/10.10 % (721660)Termination reason: Instruction limit
% 65.39/10.10 % (721660)Termination phase: Saturation
% 65.39/10.10 % (721660)Time elapsed: 1.843 s
% 65.39/10.10 % (721660)Peak memory usage: 152 MB
% 65.39/10.10 % (721660)Instructions burned: 3256 (million)
% 65.39/10.10 % (721672)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=4098064259:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2962 on theBenchmark for (2962ds/303Mi)
% 65.39/10.10 % (721672)Refutation not found, incomplete strategy
% 65.39/10.10 % (721672)------------------------------
% 65.39/10.10 % (721672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.39/10.10 % (721672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.39/10.10 % (721672)CaDiCaL version: 2.1.3
% 65.39/10.10 % (721672)Termination reason: Refutation not found, incomplete strategy
% 65.39/10.10 % (721672)Time elapsed: 0.001 s
% 65.39/10.10 % (721672)Peak memory usage: 88 MB
% 65.39/10.10 % (721672)Instructions burned: 1 (million)
% 65.39/10.10 % (721672)------------------------------
% 65.39/10.10 % (721672)------------------------------
% 65.39/10.10 % (721674)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3023796873:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi)
% 65.39/10.10 % (721648)Instruction limit reached!
% 65.39/10.10 % (721648)------------------------------
% 65.39/10.10 % (721648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.39/10.10 % (721648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.39/10.10 % (721648)CaDiCaL version: 2.1.3
% 65.39/10.10 % (721648)Termination reason: Instruction limit
% 65.39/10.10 % (721648)Termination phase: Saturation
% 65.39/10.10 % (721648)Time elapsed: 3.263 s
% 65.39/10.10 % (721648)Peak memory usage: 158 MB
% 65.39/10.10 % (721648)Instructions burned: 5209 (million)
% 65.39/10.10 % (721676)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3845217618:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi)
% 65.39/10.10 % (721676)Refutation not found, incomplete strategy
% 65.39/10.10 % (721676)------------------------------
% 65.39/10.10 % (721676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.39/10.10 % (721676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.39/10.10 % (721676)CaDiCaL version: 2.1.3
% 65.39/10.10 % (721676)Termination reason: Refutation not found, incomplete strategy
% 65.39/10.10 % (721676)Time elapsed: 0.001 s
% 65.39/10.10 % (721676)Peak memory usage: 87 MB
% 65.39/10.10 % (721676)------------------------------
% 65.39/10.10 % (721676)------------------------------
% 65.39/10.10 % (721674)Instruction limit reached!
% 65.39/10.10 % (721674)------------------------------
% 65.39/10.10 % (721674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.39/10.10 % (721674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.39/10.10 % (721674)CaDiCaL version: 2.1.3
% 65.39/10.10 % (721674)Termination reason: Instruction limit
% 65.39/10.10 % (721674)Termination phase: Saturation
% 65.39/10.10 % (721674)Time elapsed: 0.462 s
% 65.39/10.10 % (721674)Peak memory usage: 96 MB
% 65.39/10.10 % (721674)Instructions burned: 721 (million)
% 65.39/10.10 % (721678)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=980001216:i=2989:sd=3:ss=axioms:sgt=60_2953 on theBenchmark for (2953ds/2989Mi)
% 65.39/10.10 % (721679)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=988731504:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi)
% 73.66/11.28 % (721666)Instruction limit reached!
% 73.66/11.28 % (721666)------------------------------
% 73.66/11.28 % (721666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721666)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721666)Termination reason: Instruction limit
% 73.66/11.28 % (721666)Termination phase: Saturation
% 73.66/11.28 % (721666)Time elapsed: 3.518 s
% 73.66/11.28 % (721666)Peak memory usage: 172 MB
% 73.66/11.28 % (721666)Instructions burned: 10310 (million)
% 73.66/11.28 % (721682)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=1335012165:i=2088:bd=preordered:av=off_2943 on theBenchmark for (2943ds/2088Mi)
% 73.66/11.28 % (721679)Instruction limit reached!
% 73.66/11.28 % (721679)------------------------------
% 73.66/11.28 % (721679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721679)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721679)Termination reason: Instruction limit
% 73.66/11.28 % (721679)Termination phase: Saturation
% 73.66/11.28 % (721679)Time elapsed: 1.283 s
% 73.66/11.28 % (721679)Peak memory usage: 137 MB
% 73.66/11.28 % (721679)Instructions burned: 1998 (million)
% 73.66/11.28 % (721684)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=919783160:i=1098:nicw=on_2938 on theBenchmark for (2938ds/1098Mi)
% 73.66/11.28 % (721682)Instruction limit reached!
% 73.66/11.28 % (721682)------------------------------
% 73.66/11.28 % (721682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721682)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721682)Termination reason: Instruction limit
% 73.66/11.28 % (721682)Termination phase: Saturation
% 73.66/11.28 % (721682)Time elapsed: 0.722 s
% 73.66/11.28 % (721682)Peak memory usage: 138 MB
% 73.66/11.28 % (721682)Instructions burned: 2089 (million)
% 73.66/11.28 % (721678)Instruction limit reached!
% 73.66/11.28 % (721678)------------------------------
% 73.66/11.28 % (721678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721678)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721678)Termination reason: Instruction limit
% 73.66/11.28 % (721678)Termination phase: Saturation
% 73.66/11.28 % (721678)Time elapsed: 1.635 s
% 73.66/11.28 % (721678)Peak memory usage: 138 MB
% 73.66/11.28 % (721678)Instructions burned: 2989 (million)
% 73.66/11.28 % (721686)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1015490548:i=433:bd=preordered_2935 on theBenchmark for (2935ds/433Mi)
% 73.66/11.28 % (721686)Refutation not found, incomplete strategy
% 73.66/11.28 % (721686)------------------------------
% 73.66/11.28 % (721686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721686)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721686)Termination reason: Refutation not found, incomplete strategy
% 73.66/11.28 % (721686)Time elapsed: 0.005 s
% 73.66/11.28 % (721686)Peak memory usage: 89 MB
% 73.66/11.28 % (721686)Instructions burned: 16 (million)
% 73.66/11.28 % (721687)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2094842600:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2935 on theBenchmark for (2935ds/2942Mi)
% 73.66/11.28 % (721686)------------------------------
% 73.66/11.28 % (721686)------------------------------
% 73.66/11.28 % (721690)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2823176029:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2933 on theBenchmark for (2933ds/6922Mi)
% 73.66/11.28 % (721684)Instruction limit reached!
% 73.66/11.28 % (721684)------------------------------
% 73.66/11.28 % (721684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721684)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721684)Termination reason: Instruction limit
% 73.66/11.28 % (721684)Termination phase: Saturation
% 73.66/11.28 % (721684)Time elapsed: 0.652 s
% 73.66/11.28 % (721684)Peak memory usage: 102 MB
% 73.66/11.28 % (721684)Instructions burned: 1098 (million)
% 73.66/11.28 % (721692)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=115654372:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2931 on theBenchmark for (2931ds/596Mi)
% 73.66/11.28 % (721692)Instruction limit reached!
% 73.66/11.28 % (721692)------------------------------
% 73.66/11.28 % (721692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721692)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721692)Termination reason: Instruction limit
% 73.66/11.28 % (721692)Termination phase: Saturation
% 73.66/11.28 % (721692)Time elapsed: 0.319 s
% 73.66/11.28 % (721692)Peak memory usage: 99 MB
% 73.66/11.28 % (721692)Instructions burned: 596 (million)
% 73.66/11.28 % (721694)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=93149757:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2926 on theBenchmark for (2926ds/4123Mi)
% 73.66/11.28 % (721670)Instruction limit reached!
% 73.66/11.28 % (721670)------------------------------
% 73.66/11.28 % (721670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721670)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721670)Termination reason: Instruction limit
% 73.66/11.28 % (721670)Termination phase: Saturation
% 73.66/11.28 % (721670)Time elapsed: 4.938 s
% 73.66/11.28 % (721670)Peak memory usage: 160 MB
% 73.66/11.28 % (721670)Instructions burned: 8479 (million)
% 73.66/11.28 % (721696)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=230207116:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi)
% 73.66/11.28 % (721687)Instruction limit reached!
% 73.66/11.28 % (721687)------------------------------
% 73.66/11.28 % (721687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721687)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721687)Termination reason: Instruction limit
% 73.66/11.28 % (721687)Termination phase: Saturation
% 73.66/11.28 % (721687)Time elapsed: 1.168 s
% 73.66/11.28 % (721687)Peak memory usage: 140 MB
% 73.66/11.28 % (721687)Instructions burned: 2947 (million)
% 73.66/11.28 % (721698)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3696952732:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2922 on theBenchmark for (2922ds/1670Mi)
% 73.66/11.28 % (721698)Instruction limit reached!
% 73.66/11.28 % (721698)------------------------------
% 73.66/11.28 % (721698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721698)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721698)Termination reason: Instruction limit
% 73.66/11.28 % (721698)Termination phase: Saturation
% 73.66/11.28 % (721698)Time elapsed: 0.566 s
% 73.66/11.28 % (721698)Peak memory usage: 137 MB
% 73.66/11.28 % (721698)Instructions burned: 1674 (million)
% 73.66/11.28 % (721700)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=2336021024:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2915 on theBenchmark for (2915ds/1722Mi)
% 73.66/11.28 % (721700)Instruction limit reached!
% 73.66/11.28 % (721700)------------------------------
% 73.66/11.28 % (721700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.28 % (721700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.28 % (721700)CaDiCaL version: 2.1.3
% 73.66/11.28 % (721700)Termination reason: Instruction limit
% 73.66/11.28 % (721700)Termination phase: Saturation
% 73.66/11.28 % (721700)Time elapsed: 0.654 s
% 73.66/11.28 % (721700)Peak memory usage: 135 MB
% 73.66/11.28 % (721700)Instructions burned: 1723 (million)
% 73.66/11.28 % (721702)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=282609313:cts=off:cond=on:i=9530:bs=on:fsd=on_2908 on theBenchmark for (2908ds/9530Mi)
% 73.66/11.29 % (721694)Instruction limit reached!
% 73.66/11.29 % (721694)------------------------------
% 73.66/11.29 % (721694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.66/11.29 % (721694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.66/11.29 % (721694)CaDiCaL version: 2.1.3
% 73.66/11.29 % (721694)Termination reason: Instruction limit
% 73.66/11.29 % (721694)Termination phase: Saturation
% 73.66/11.29 % (721694)Time elapsed: 2.612 s
% 73.66/11.29 % (721694)Peak memory usage: 156 MB
% 73.66/11.29 % (721694)Instructions burned: 4123 (million)
% 73.66/11.29 % (721702)First to succeed.
% 73.66/11.29 % (721704)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2422327262:st=2:i=4495:sd=10:ss=included_2898 on theBenchmark for (2898ds/4495Mi)
% 73.66/11.29 % (721702)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-721609"
% 73.66/11.29 % (721702)Refutation found. Thanks to Tanya!
% 73.66/11.29 % SZS status Unsatisfiable for theBenchmark
% 73.66/11.29 % SZS output start Proof for theBenchmark
% See solution above
% 74.34/11.48 % (721702)------------------------------
% 74.34/11.48 % (721702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.34/11.48 % (721702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.34/11.48 % (721702)CaDiCaL version: 2.1.3
% 74.34/11.48 % (721702)Termination reason: Refutation
% 74.34/11.48 % (721702)Time elapsed: 0.990 s
% 74.34/11.48 % (721702)Peak memory usage: 140 MB
% 74.34/11.48 % (721702)Instructions burned: 2437 (million)
% 74.34/11.48 % (721702)------------------------------
% 74.34/11.48 % (721702)------------------------------
% 74.34/11.48 % (721609)Success in time 10.429 s
% 74.34/11.48 % Vampire exiting
%------------------------------------------------------------------------------