%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET293-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 : n003.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:43 PM UTC 2026
% Result : Unsatisfiable 132.36s 33.84s
% Output : Refutation 234.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 70
% Syntax : Number of formulae : 324 ( 61 unt; 43 def)
% Number of atoms : 802 ( 110 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 880 ( 402 ~; 438 |; 0 &)
% ( 40 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 44 ( 42 usr; 41 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 5 con; 0-3 aty)
% Number of variables : 250 ( 0 sgn 250 !; 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(f6,axiom,
! [X0,X1] :
( X0 != X1
| subclass(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equal_implies_subclass2) ).
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(f10,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| member(X0,unordered_pair(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair3) ).
fof(f11,axiom,
! [X0,X1] : member(unordered_pair(X0,X1),universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pairs_in_universal) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f13,axiom,
! [X0,X1] : unordered_pair(singleton(X0),unordered_pair(X0,singleton(X1))) = ordered_pair(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f14,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f15,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(X2,X3))
| member(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product2) ).
fof(f16,axiom,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(X2,X3)
| member(ordered_pair(X0,X2),cross_product(X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product3) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement1) ).
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(f36,axiom,
! [X0] : subclass(flip(X0),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',flip1) ).
fof(f38,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(ordered_pair(X0,X1),X2),X3)
| ~ member(ordered_pair(ordered_pair(X1,X0),X2),cross_product(cross_product(universal_class,universal_class),universal_class))
| member(ordered_pair(ordered_pair(X1,X0),X2),flip(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',flip3) ).
fof(f39,axiom,
! [X0] : domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
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(f122,negated_conjecture,
inverse(universal_class) != cross_product(universal_class,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_inverse_of_universal_class_1) ).
fof(f123,plain,
cross_product(universal_class,universal_class) != inverse(universal_class),
inference(reorient_equations,[],[f122]) ).
fof(f128,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(f137,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f128]) ).
fof(f138,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f128]) ).
fof(f139,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,f128]) ).
fof(f140,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,f128]) ).
fof(f144,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(f145,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(f149,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X3)) ),
inference(definition_unfolding,[],[f38,f128,f128,f128,f128,f128,f128]) ).
fof(f186,plain,
cross_product(universal_class,universal_class) != domain_of(flip(cross_product(universal_class,universal_class))),
inference(definition_unfolding,[],[f123,f39]) ).
fof(f188,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f191,definition,
sF0 = cross_product(universal_class,universal_class),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f192,plain,
cross_product(universal_class,universal_class) = sF0,
inference(reorient_equations,[],[f191]) ).
fof(f193,definition,
sF1 = flip(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f194,plain,
flip(sF0) = sF1,
inference(reorient_equations,[],[f193]) ).
fof(f195,definition,
sF2 = domain_of(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f196,plain,
domain_of(sF1) = sF2,
inference(reorient_equations,[],[f195]) ).
fof(f197,plain,
sF0 != sF2,
inference(definition_folding,[],[f186,f196,f194,f192,f192]) ).
fof(f199,definition,
( spl3_1
<=> flip(sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f201,plain,
( flip(sF0) = sF1
| ~ spl3_1 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f202,plain,
spl3_1,
inference(avatar_split_clause,[],[f194,f199]) ).
fof(f208,definition,
( spl3_2
<=> sF0 = sF2 ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f210,plain,
( sF0 != sF2
| spl3_2 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f211,plain,
~ spl3_2,
inference(avatar_split_clause,[],[f197,f208]) ).
fof(f213,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| subclass(X0,X1)
| ~ subclass(X2,X1) ),
inference(resolution,[],[f3,f1]) ).
fof(f216,definition,
( spl3_3
<=> domain_of(sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f218,plain,
( domain_of(sF1) = sF2
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f219,plain,
spl3_3,
inference(avatar_split_clause,[],[f196,f216]) ).
fof(f225,definition,
( spl3_5
<=> cross_product(universal_class,universal_class) = sF0 ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f227,plain,
( cross_product(universal_class,universal_class) = sF0
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,plain,
spl3_5,
inference(avatar_split_clause,[],[f192,f225]) ).
fof(f240,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) )
| ~ spl3_5 ),
inference(superposition,[],[f139,f227]) ).
fof(f243,plain,
( subclass(sF1,cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ spl3_1 ),
inference(superposition,[],[f36,f201]) ).
fof(f245,plain,
( subclass(sF1,cross_product(sF0,universal_class))
| ~ spl3_1
| ~ spl3_5 ),
inference(forward_demodulation,[],[f243,f227]) ).
fof(f254,definition,
( spl3_7
<=> ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f255,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) )
| ~ spl3_7 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f256,plain,
( spl3_7
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f240,f225,f254]) ).
fof(f257,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f258,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f262,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X3))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),cross_product(universal_class,universal_class)) ),
inference(resolution,[],[f149,f139]) ).
fof(f268,plain,
( ! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X3))
| ~ member(X2,universal_class) )
| ~ spl3_5 ),
inference(forward_demodulation,[],[f262,f227]) ).
fof(f271,definition,
( spl3_8
<=> ! [X0,X3,X2,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X3))
| ~ member(X2,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition]) ).
fof(f272,plain,
( ! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X3))
| ~ member(X2,universal_class) )
| ~ spl3_8 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( spl3_8
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f268,f225,f271]) ).
fof(f284,plain,
( ! [X0] :
( ~ member(X0,sF0)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 )
| ~ spl3_5 ),
inference(superposition,[],[f140,f227]) ).
fof(f286,definition,
( spl3_9
<=> ! [X0] :
( ~ member(X0,sF0)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f287,plain,
( ! [X0] :
( ~ member(X0,sF0)
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 )
| ~ spl3_9 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f288,plain,
( spl3_9
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f284,f225,f286]) ).
fof(f290,plain,
( ! [X0] :
( not_subclass_element(sF0,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,X0)),first(not_subclass_element(sF0,X0))),unordered_pair(first(not_subclass_element(sF0,X0)),unordered_pair(second(not_subclass_element(sF0,X0)),second(not_subclass_element(sF0,X0)))))
| subclass(sF0,X0) )
| ~ spl3_9 ),
inference(resolution,[],[f287,f2]) ).
fof(f295,definition,
( spl3_10
<=> ! [X0] :
( not_subclass_element(sF0,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,X0)),first(not_subclass_element(sF0,X0))),unordered_pair(first(not_subclass_element(sF0,X0)),unordered_pair(second(not_subclass_element(sF0,X0)),second(not_subclass_element(sF0,X0)))))
| subclass(sF0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f296,plain,
( ! [X0] :
( subclass(sF0,X0)
| not_subclass_element(sF0,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,X0)),first(not_subclass_element(sF0,X0))),unordered_pair(first(not_subclass_element(sF0,X0)),unordered_pair(second(not_subclass_element(sF0,X0)),second(not_subclass_element(sF0,X0))))) )
| ~ spl3_10 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f297,plain,
( spl3_10
| ~ spl3_9 ),
inference(avatar_split_clause,[],[f290,f286,f295]) ).
fof(f298,plain,
( ! [X0] :
( not_subclass_element(sF0,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,X0)),first(not_subclass_element(sF0,X0))),unordered_pair(first(not_subclass_element(sF0,X0)),unordered_pair(second(not_subclass_element(sF0,X0)),second(not_subclass_element(sF0,X0)))))
| ~ subclass(X0,sF0)
| sF0 = X0 )
| ~ spl3_10 ),
inference(resolution,[],[f296,f7]) ).
fof(f307,definition,
( spl3_12
<=> subclass(sF1,cross_product(sF0,universal_class)) ),
introduced(definition,[new_symbols(definition,[spl3_12])],[avatar_definition]) ).
fof(f309,plain,
( subclass(sF1,cross_product(sF0,universal_class))
| ~ spl3_12 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,plain,
( spl3_12
| ~ spl3_1
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f245,f225,f199,f307]) ).
fof(f317,definition,
( spl3_13
<=> ! [X0] :
( not_subclass_element(sF0,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,X0)),first(not_subclass_element(sF0,X0))),unordered_pair(first(not_subclass_element(sF0,X0)),unordered_pair(second(not_subclass_element(sF0,X0)),second(not_subclass_element(sF0,X0)))))
| ~ subclass(X0,sF0)
| sF0 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl3_13])],[avatar_definition]) ).
fof(f318,plain,
( ! [X0] :
( ~ subclass(X0,sF0)
| not_subclass_element(sF0,X0) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,X0)),first(not_subclass_element(sF0,X0))),unordered_pair(first(not_subclass_element(sF0,X0)),unordered_pair(second(not_subclass_element(sF0,X0)),second(not_subclass_element(sF0,X0)))))
| sF0 = X0 )
| ~ spl3_13 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f319,plain,
( spl3_13
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f298,f295,f317]) ).
fof(f334,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,X2)
| ~ subclass(X2,universal_class) ),
inference(resolution,[],[f10,f1]) ).
fof(f337,plain,
! [X2,X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,X2) ),
inference(forward_subsumption_resolution,[],[f334,f4]) ).
fof(f338,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,[],[f145,f1]) ).
fof(f341,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,[],[f338,f4]) ).
fof(f376,plain,
! [X2,X3,X0,X1,X4] :
( ~ subclass(X3,cross_product(X4,X1))
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),X3)
| member(X0,X1) ),
inference(resolution,[],[f138,f1]) ).
fof(f377,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X1,universal_class) )
| ~ spl3_5 ),
inference(superposition,[],[f138,f227]) ).
fof(f380,plain,
! [X2,X3,X0,X1,X4] :
( ~ subclass(X3,cross_product(X1,X4))
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),X3)
| member(X0,X1) ),
inference(resolution,[],[f137,f1]) ).
fof(f398,plain,
( ! [X0,X1] :
( member(X0,sF2)
| null_class = intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl3_3 ),
inference(superposition,[],[f341,f218]) ).
fof(f400,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,[],[f257,f140]) ).
fof(f403,plain,
! [X0,X1] :
( ~ member(regular(intersection(X0,complement(X1))),X1)
| null_class = intersection(X0,complement(X1)) ),
inference(resolution,[],[f257,f24]) ).
fof(f418,definition,
( spl3_20
<=> ! [X0,X1] :
( member(X0,sF2)
| null_class = intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition]) ).
fof(f419,plain,
( ! [X0,X1] :
( member(X0,sF2)
| null_class = intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,X1) )
| ~ spl3_20 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( spl3_20
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f398,f216,f418]) ).
fof(f421,plain,
( ! [X0,X1] :
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(X0,sF2),not_subclass_element(X0,sF2)),universal_class))
| ~ member(not_subclass_element(X0,sF2),X1)
| subclass(X0,sF2) )
| ~ spl3_20 ),
inference(resolution,[],[f419,f3]) ).
fof(f434,definition,
( spl3_21
<=> ! [X0,X1] :
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(X0,sF2),not_subclass_element(X0,sF2)),universal_class))
| ~ member(not_subclass_element(X0,sF2),X1)
| subclass(X0,sF2) ) ),
introduced(definition,[new_symbols(definition,[spl3_21])],[avatar_definition]) ).
fof(f435,plain,
( ! [X0,X1] :
( subclass(X0,sF2)
| ~ member(not_subclass_element(X0,sF2),X1)
| null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(X0,sF2),not_subclass_element(X0,sF2)),universal_class)) )
| ~ spl3_21 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f436,plain,
( spl3_21
| ~ spl3_20 ),
inference(avatar_split_clause,[],[f421,f418,f434]) ).
fof(f437,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(X0,sF2),X1)
| null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(X0,sF2),not_subclass_element(X0,sF2)),universal_class))
| ~ subclass(sF2,X0)
| sF2 = X0 )
| ~ spl3_21 ),
inference(resolution,[],[f435,f7]) ).
fof(f536,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X1,universal_class) )
| ~ spl3_12 ),
inference(resolution,[],[f376,f309]) ).
fof(f543,definition,
( spl3_26
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X1,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl3_26])],[avatar_definition]) ).
fof(f544,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X1,universal_class) )
| ~ spl3_26 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f545,plain,
( spl3_26
| ~ spl3_12 ),
inference(avatar_split_clause,[],[f536,f307,f543]) ).
fof(f571,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X0,sF0) )
| ~ spl3_12 ),
inference(resolution,[],[f380,f309]) ).
fof(f1199,plain,
! [X0] :
( null_class = intersection(X0,complement(X0))
| null_class = intersection(X0,complement(X0)) ),
inference(resolution,[],[f403,f258]) ).
fof(f1208,plain,
! [X0] : null_class = intersection(X0,complement(X0)),
inference(duplicate_literal_removal,[],[f1199]) ).
fof(f1209,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1) ),
inference(superposition,[],[f21,f1208]) ).
fof(f1210,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,complement(X1)) ),
inference(superposition,[],[f22,f1208]) ).
fof(f1468,definition,
( spl3_64
<=> ! [X0,X1] :
( ~ member(not_subclass_element(X0,sF2),X1)
| null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(X0,sF2),not_subclass_element(X0,sF2)),universal_class))
| ~ subclass(sF2,X0)
| sF2 = X0 ) ),
introduced(definition,[new_symbols(definition,[spl3_64])],[avatar_definition]) ).
fof(f1469,plain,
( ! [X0,X1] :
( ~ subclass(sF2,X0)
| null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(X0,sF2),not_subclass_element(X0,sF2)),universal_class))
| ~ member(not_subclass_element(X0,sF2),X1)
| sF2 = X0 )
| ~ spl3_64 ),
inference(avatar_component_clause,[],[f1468]) ).
fof(f1470,plain,
( spl3_64
| ~ spl3_21 ),
inference(avatar_split_clause,[],[f437,f434,f1468]) ).
fof(f1645,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,[],[f144,f400]) ).
fof(f1668,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,[],[f1645]) ).
fof(f1683,plain,
( ! [X0] :
( ~ member(X0,sF2)
| regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl3_3 ),
inference(superposition,[],[f1668,f218]) ).
fof(f1778,definition,
( spl3_75
<=> ! [X0] :
( ~ member(X0,sF2)
| regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))))) ) ),
introduced(definition,[new_symbols(definition,[spl3_75])],[avatar_definition]) ).
fof(f1779,plain,
( ! [X0] :
( ~ member(X0,sF2)
| regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(X0,X0),universal_class))))))) )
| ~ spl3_75 ),
inference(avatar_component_clause,[],[f1778]) ).
fof(f1780,plain,
( spl3_75
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f1683,f216,f1778]) ).
fof(f1783,plain,
( ! [X0] :
( regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))))))
| subclass(sF2,X0) )
| ~ spl3_75 ),
inference(resolution,[],[f1779,f2]) ).
fof(f1959,definition,
( spl3_82
<=> ! [X0] :
( regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))))))
| subclass(sF2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_82])],[avatar_definition]) ).
fof(f1960,plain,
( ! [X0] :
( subclass(sF2,X0)
| regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,X0),not_subclass_element(sF2,X0)),universal_class))))))) )
| ~ spl3_82 ),
inference(avatar_component_clause,[],[f1959]) ).
fof(f1961,plain,
( spl3_82
| ~ spl3_75 ),
inference(avatar_split_clause,[],[f1783,f1778,f1959]) ).
fof(f1974,plain,
( regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))))))
| not_subclass_element(sF0,sF2) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))),unordered_pair(first(not_subclass_element(sF0,sF2)),unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2)))))
| sF0 = sF2
| ~ spl3_13
| ~ spl3_82 ),
inference(resolution,[],[f1960,f318]) ).
fof(f1977,plain,
( regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))))))
| not_subclass_element(sF0,sF2) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))),unordered_pair(first(not_subclass_element(sF0,sF2)),unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2)))))
| spl3_2
| ~ spl3_13
| ~ spl3_82 ),
inference(forward_subsumption_resolution,[],[f1974,f210]) ).
fof(f2037,plain,
! [X0] : ~ member(X0,null_class),
inference(global_subsumption,[],[f1209,f1210,f24]) ).
fof(f2046,definition,
( spl3_87
<=> not_subclass_element(sF0,sF2) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))),unordered_pair(first(not_subclass_element(sF0,sF2)),unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))))) ),
introduced(definition,[new_symbols(definition,[spl3_87])],[avatar_definition]) ).
fof(f2048,plain,
( not_subclass_element(sF0,sF2) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))),unordered_pair(first(not_subclass_element(sF0,sF2)),unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2)))))
| ~ spl3_87 ),
inference(avatar_component_clause,[],[f2046]) ).
fof(f2050,definition,
( spl3_88
<=> regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))))) ),
introduced(definition,[new_symbols(definition,[spl3_88])],[avatar_definition]) ).
fof(f2051,plain,
( regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))) != unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))))))
| spl3_88 ),
inference(avatar_component_clause,[],[f2050]) ).
fof(f2052,plain,
( regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))))))
| ~ spl3_88 ),
inference(avatar_component_clause,[],[f2050]) ).
fof(f2053,plain,
( spl3_87
| spl3_88
| spl3_2
| ~ spl3_13
| ~ spl3_82 ),
inference(avatar_split_clause,[],[f1977,f1959,f317,f208,f2050,f2046]) ).
fof(f2061,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),X0) )
| ~ spl3_88 ),
inference(superposition,[],[f137,f2052]) ).
fof(f2108,definition,
( spl3_93
<=> ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl3_93])],[avatar_definition]) ).
fof(f2109,plain,
( ! [X0,X1] :
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))),cross_product(X0,X1))
| member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),X0) )
| ~ spl3_93 ),
inference(avatar_component_clause,[],[f2108]) ).
fof(f2110,plain,
( spl3_93
| ~ spl3_88 ),
inference(avatar_split_clause,[],[f2061,f2050,f2108]) ).
fof(f2111,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)))
| null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))
| ~ spl3_93 ),
inference(resolution,[],[f2109,f257]) ).
fof(f2240,definition,
( spl3_99
<=> member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))),sF1) ),
introduced(definition,[new_symbols(definition,[spl3_99])],[avatar_definition]) ).
fof(f2241,plain,
( member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))),sF1)
| ~ spl3_99 ),
inference(avatar_component_clause,[],[f2240]) ).
fof(f2242,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))),sF1)
| spl3_99 ),
inference(avatar_component_clause,[],[f2240]) ).
fof(f2244,plain,
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))
| spl3_99 ),
inference(resolution,[],[f2242,f258]) ).
fof(f2296,definition,
( spl3_102
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X1,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl3_102])],[avatar_definition]) ).
fof(f2297,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X1,universal_class) )
| ~ spl3_102 ),
inference(avatar_component_clause,[],[f2296]) ).
fof(f2298,plain,
( spl3_102
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f377,f225,f2296]) ).
fof(f2421,definition,
( spl3_110
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X0,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl3_110])],[avatar_definition]) ).
fof(f2422,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| member(X0,sF0) )
| ~ spl3_110 ),
inference(avatar_component_clause,[],[f2421]) ).
fof(f2423,plain,
( spl3_110
| ~ spl3_12 ),
inference(avatar_split_clause,[],[f571,f307,f2421]) ).
fof(f2429,plain,
( ~ member(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))),sF1)
| member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),sF0)
| ~ spl3_88
| ~ spl3_110 ),
inference(superposition,[],[f2422,f2052]) ).
fof(f2741,definition,
( spl3_127
<=> null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl3_127])],[avatar_definition]) ).
fof(f2742,plain,
( null_class != intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))
| spl3_127 ),
inference(avatar_component_clause,[],[f2741]) ).
fof(f2743,plain,
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))
| ~ spl3_127 ),
inference(avatar_component_clause,[],[f2741]) ).
fof(f2744,plain,
( spl3_127
| spl3_99 ),
inference(avatar_split_clause,[],[f2244,f2240,f2741]) ).
fof(f2754,plain,
( null_class != null_class
| ~ member(not_subclass_element(sF2,sF0),domain_of(sF1))
| ~ spl3_127 ),
inference(superposition,[],[f144,f2743]) ).
fof(f2769,plain,
( ~ member(not_subclass_element(sF2,sF0),domain_of(sF1))
| ~ spl3_127 ),
inference(trivial_inequality_removal,[],[f2754]) ).
fof(f2772,plain,
( ~ member(not_subclass_element(sF2,sF0),sF2)
| ~ spl3_3
| ~ spl3_127 ),
inference(forward_demodulation,[],[f2769,f218]) ).
fof(f2775,definition,
( spl3_128
<=> member(not_subclass_element(sF2,sF0),sF2) ),
introduced(definition,[new_symbols(definition,[spl3_128])],[avatar_definition]) ).
fof(f2777,plain,
( ~ member(not_subclass_element(sF2,sF0),sF2)
| spl3_128 ),
inference(avatar_component_clause,[],[f2775]) ).
fof(f2778,plain,
( ~ spl3_128
| ~ spl3_3
| ~ spl3_127 ),
inference(avatar_split_clause,[],[f2772,f2741,f216,f2775]) ).
fof(f2779,plain,
( subclass(sF2,sF0)
| spl3_128 ),
inference(resolution,[],[f2777,f2]) ).
fof(f2783,definition,
( spl3_129
<=> subclass(sF2,sF0) ),
introduced(definition,[new_symbols(definition,[spl3_129])],[avatar_definition]) ).
fof(f2784,plain,
( ~ subclass(sF2,sF0)
| spl3_129 ),
inference(avatar_component_clause,[],[f2783]) ).
fof(f2785,plain,
( subclass(sF2,sF0)
| ~ spl3_129 ),
inference(avatar_component_clause,[],[f2783]) ).
fof(f2786,plain,
( spl3_129
| spl3_128 ),
inference(avatar_split_clause,[],[f2779,f2775,f2783]) ).
fof(f2787,plain,
( ! [X0] :
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class))
| ~ member(not_subclass_element(sF0,sF2),X0)
| sF0 = sF2 )
| ~ spl3_64
| ~ spl3_129 ),
inference(resolution,[],[f2785,f1469]) ).
fof(f2788,plain,
( not_subclass_element(sF0,sF2) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))),unordered_pair(first(not_subclass_element(sF0,sF2)),unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2)))))
| sF0 = sF2
| ~ spl3_13
| ~ spl3_129 ),
inference(resolution,[],[f2785,f318]) ).
fof(f2791,plain,
( ~ subclass(sF0,sF2)
| sF0 = sF2
| ~ spl3_129 ),
inference(resolution,[],[f2785,f7]) ).
fof(f2792,plain,
( ~ subclass(sF0,sF2)
| spl3_2
| ~ spl3_129 ),
inference(forward_subsumption_resolution,[],[f2791,f210]) ).
fof(f2793,plain,
( not_subclass_element(sF0,sF2) = unordered_pair(unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))),unordered_pair(first(not_subclass_element(sF0,sF2)),unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2)))))
| spl3_2
| ~ spl3_13
| ~ spl3_129 ),
inference(forward_subsumption_resolution,[],[f2788,f210]) ).
fof(f2794,plain,
( ! [X0] :
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class))
| ~ member(not_subclass_element(sF0,sF2),X0) )
| spl3_2
| ~ spl3_64
| ~ spl3_129 ),
inference(forward_subsumption_resolution,[],[f2787,f210]) ).
fof(f2795,plain,
( spl3_87
| spl3_2
| ~ spl3_13
| ~ spl3_129 ),
inference(avatar_split_clause,[],[f2793,f2783,f317,f208,f2046]) ).
fof(f2797,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),sF0)
| ~ spl3_88
| ~ spl3_99
| ~ spl3_110 ),
inference(forward_subsumption_resolution,[],[f2429,f2241]) ).
fof(f2802,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)))
| ~ spl3_93
| spl3_127 ),
inference(forward_subsumption_resolution,[],[f2111,f2742]) ).
fof(f2825,definition,
( spl3_130
<=> member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),sF0) ),
introduced(definition,[new_symbols(definition,[spl3_130])],[avatar_definition]) ).
fof(f2827,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),sF0)
| ~ spl3_130 ),
inference(avatar_component_clause,[],[f2825]) ).
fof(f2828,plain,
( spl3_130
| ~ spl3_88
| ~ spl3_99
| ~ spl3_110 ),
inference(avatar_split_clause,[],[f2797,f2421,f2240,f2050,f2825]) ).
fof(f2836,definition,
( spl3_131
<=> member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0))) ),
introduced(definition,[new_symbols(definition,[spl3_131])],[avatar_definition]) ).
fof(f2838,plain,
( member(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)))
| ~ spl3_131 ),
inference(avatar_component_clause,[],[f2836]) ).
fof(f2839,plain,
( spl3_131
| ~ spl3_93
| spl3_127 ),
inference(avatar_split_clause,[],[f2802,f2741,f2108,f2836]) ).
fof(f2840,plain,
( not_subclass_element(sF2,sF0) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))
| not_subclass_element(sF2,sF0) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))
| ~ spl3_131 ),
inference(resolution,[],[f2838,f8]) ).
fof(f2845,plain,
( not_subclass_element(sF2,sF0) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))
| ~ spl3_131 ),
inference(duplicate_literal_removal,[],[f2840]) ).
fof(f2853,plain,
( regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))) = unordered_pair(unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))),unordered_pair(first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),unordered_pair(second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))),second(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))))))
| ~ spl3_82
| spl3_129 ),
inference(resolution,[],[f2784,f1960]) ).
fof(f2878,definition,
( spl3_135
<=> not_subclass_element(sF2,sF0) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class)))) ),
introduced(definition,[new_symbols(definition,[spl3_135])],[avatar_definition]) ).
fof(f2880,plain,
( not_subclass_element(sF2,sF0) = first(regular(intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF2,sF0),not_subclass_element(sF2,sF0)),universal_class))))
| ~ spl3_135 ),
inference(avatar_component_clause,[],[f2878]) ).
fof(f2881,plain,
( spl3_135
| ~ spl3_131 ),
inference(avatar_split_clause,[],[f2845,f2836,f2878]) ).
fof(f2887,plain,
( member(not_subclass_element(sF2,sF0),sF0)
| ~ spl3_130
| ~ spl3_135 ),
inference(superposition,[],[f2827,f2880]) ).
fof(f2892,definition,
( spl3_136
<=> member(not_subclass_element(sF2,sF0),sF0) ),
introduced(definition,[new_symbols(definition,[spl3_136])],[avatar_definition]) ).
fof(f2894,plain,
( member(not_subclass_element(sF2,sF0),sF0)
| ~ spl3_136 ),
inference(avatar_component_clause,[],[f2892]) ).
fof(f2895,plain,
( spl3_136
| ~ spl3_130
| ~ spl3_135 ),
inference(avatar_split_clause,[],[f2887,f2878,f2825,f2892]) ).
fof(f2901,plain,
( subclass(sF2,sF0)
| ~ subclass(sF0,sF0)
| ~ spl3_136 ),
inference(resolution,[],[f2894,f213]) ).
fof(f2906,plain,
( ~ subclass(sF0,sF0)
| spl3_129
| ~ spl3_136 ),
inference(forward_subsumption_resolution,[],[f2901,f2784]) ).
fof(f2910,plain,
( $false
| spl3_129
| ~ spl3_136 ),
inference(forward_subsumption_resolution,[],[f2906,f188]) ).
fof(f2911,plain,
( spl3_129
| ~ spl3_136 ),
inference(avatar_contradiction_clause,[],[f2910]) ).
fof(f3399,plain,
( ! [X0,X1] :
( ~ member(not_subclass_element(sF0,sF2),sF0)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),X1)
| member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),flip(X1))
| ~ member(X0,universal_class) )
| ~ spl3_8
| ~ spl3_87 ),
inference(superposition,[],[f272,f2048]) ).
fof(f3415,plain,
( member(not_subclass_element(sF0,sF2),universal_class)
| ~ spl3_87 ),
inference(superposition,[],[f11,f2048]) ).
fof(f3532,plain,
( $false
| ~ spl3_82
| spl3_88
| spl3_129 ),
inference(forward_subsumption_resolution,[],[f2853,f2051]) ).
fof(f3533,plain,
( ~ spl3_82
| spl3_88
| spl3_129 ),
inference(avatar_contradiction_clause,[],[f3532]) ).
fof(f3554,definition,
( spl3_140
<=> member(not_subclass_element(sF0,sF2),sF0) ),
introduced(definition,[new_symbols(definition,[spl3_140])],[avatar_definition]) ).
fof(f3555,plain,
( member(not_subclass_element(sF0,sF2),sF0)
| ~ spl3_140 ),
inference(avatar_component_clause,[],[f3554]) ).
fof(f3556,plain,
( ~ member(not_subclass_element(sF0,sF2),sF0)
| spl3_140 ),
inference(avatar_component_clause,[],[f3554]) ).
fof(f3558,plain,
( subclass(sF0,sF2)
| spl3_140 ),
inference(resolution,[],[f3556,f2]) ).
fof(f3563,plain,
( $false
| spl3_2
| ~ spl3_129
| spl3_140 ),
inference(forward_subsumption_resolution,[],[f3558,f2792]) ).
fof(f3564,plain,
( spl3_2
| ~ spl3_129
| spl3_140 ),
inference(avatar_contradiction_clause,[],[f3563]) ).
fof(f3566,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),X1)
| member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),flip(X1))
| ~ member(X0,universal_class) )
| ~ spl3_8
| ~ spl3_87
| ~ spl3_140 ),
inference(forward_subsumption_resolution,[],[f3399,f3555]) ).
fof(f3661,definition,
( spl3_148
<=> member(not_subclass_element(sF0,sF2),universal_class) ),
introduced(definition,[new_symbols(definition,[spl3_148])],[avatar_definition]) ).
fof(f3663,plain,
( member(not_subclass_element(sF0,sF2),universal_class)
| ~ spl3_148 ),
inference(avatar_component_clause,[],[f3661]) ).
fof(f3664,plain,
( spl3_148
| ~ spl3_87 ),
inference(avatar_split_clause,[],[f3415,f2046,f3661]) ).
fof(f3735,definition,
( spl3_154
<=> ! [X0] : ~ member(not_subclass_element(sF0,sF2),X0) ),
introduced(definition,[new_symbols(definition,[spl3_154])],[avatar_definition]) ).
fof(f3736,plain,
( ! [X0] : ~ member(not_subclass_element(sF0,sF2),X0)
| ~ spl3_154 ),
inference(avatar_component_clause,[],[f3735]) ).
fof(f3738,definition,
( spl3_155
<=> null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class)) ),
introduced(definition,[new_symbols(definition,[spl3_155])],[avatar_definition]) ).
fof(f3740,plain,
( null_class = intersection(sF1,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class))
| ~ spl3_155 ),
inference(avatar_component_clause,[],[f3738]) ).
fof(f3741,plain,
( spl3_154
| spl3_155
| spl3_2
| ~ spl3_64
| ~ spl3_129 ),
inference(avatar_split_clause,[],[f2794,f2783,f1468,f208,f3738,f3735]) ).
fof(f3747,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class))
| ~ member(X0,sF1) )
| ~ spl3_155 ),
inference(superposition,[],[f23,f3740]) ).
fof(f3761,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class))
| ~ member(X0,sF1) )
| ~ spl3_155 ),
inference(forward_subsumption_resolution,[],[f3747,f2037]) ).
fof(f3930,definition,
( spl3_169
<=> ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class))
| ~ member(X0,sF1) ) ),
introduced(definition,[new_symbols(definition,[spl3_169])],[avatar_definition]) ).
fof(f3931,plain,
( ! [X0] :
( ~ member(X0,cross_product(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),universal_class))
| ~ member(X0,sF1) )
| ~ spl3_169 ),
inference(avatar_component_clause,[],[f3930]) ).
fof(f3932,plain,
( spl3_169
| ~ spl3_155 ),
inference(avatar_split_clause,[],[f3761,f3738,f3930]) ).
fof(f3936,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2))) )
| ~ spl3_169 ),
inference(resolution,[],[f3931,f139]) ).
fof(f3952,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2))) )
| ~ spl3_26
| ~ spl3_169 ),
inference(forward_subsumption_resolution,[],[f3936,f544]) ).
fof(f3964,definition,
( spl3_172
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2))) ) ),
introduced(definition,[new_symbols(definition,[spl3_172])],[avatar_definition]) ).
fof(f3965,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF1)
| ~ member(X0,unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2))) )
| ~ spl3_172 ),
inference(avatar_component_clause,[],[f3964]) ).
fof(f3966,plain,
( spl3_172
| ~ spl3_26
| ~ spl3_169 ),
inference(avatar_split_clause,[],[f3952,f3930,f543,f3964]) ).
fof(f4788,definition,
( spl3_217
<=> ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),X1)
| member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),flip(X1))
| ~ member(X0,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl3_217])],[avatar_definition]) ).
fof(f4789,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),flip(X1))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),X1)
| ~ member(X0,universal_class) )
| ~ spl3_217 ),
inference(avatar_component_clause,[],[f4788]) ).
fof(f4790,plain,
( spl3_217
| ~ spl3_8
| ~ spl3_87
| ~ spl3_140 ),
inference(avatar_split_clause,[],[f3566,f3554,f2046,f271,f4788]) ).
fof(f4799,plain,
( ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),sF0)
| ~ member(X0,universal_class) )
| ~ spl3_1
| ~ spl3_217 ),
inference(superposition,[],[f4789,f201]) ).
fof(f4804,plain,
( ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),sF0) )
| ~ spl3_1
| ~ spl3_102
| ~ spl3_217 ),
inference(forward_subsumption_resolution,[],[f4799,f2297]) ).
fof(f4806,definition,
( spl3_218
<=> ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),sF0) ) ),
introduced(definition,[new_symbols(definition,[spl3_218])],[avatar_definition]) ).
fof(f4807,plain,
( ! [X0] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2)))))),unordered_pair(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),unordered_pair(X0,X0))),sF0)
| member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1) )
| ~ spl3_218 ),
inference(avatar_component_clause,[],[f4806]) ).
fof(f4808,plain,
( spl3_218
| ~ spl3_1
| ~ spl3_102
| ~ spl3_217 ),
inference(avatar_split_clause,[],[f4804,f4788,f2296,f199,f4806]) ).
fof(f4812,plain,
( ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1)
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(second(not_subclass_element(sF0,sF2)),second(not_subclass_element(sF0,sF2))),unordered_pair(second(not_subclass_element(sF0,sF2)),unordered_pair(first(not_subclass_element(sF0,sF2)),first(not_subclass_element(sF0,sF2))))),universal_class) )
| ~ spl3_7
| ~ spl3_218 ),
inference(resolution,[],[f4807,f255]) ).
fof(f4829,plain,
( ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1)
| ~ member(X0,universal_class) )
| ~ spl3_7
| ~ spl3_218 ),
inference(forward_subsumption_resolution,[],[f4812,f11]) ).
fof(f4833,definition,
( spl3_219
<=> ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1)
| ~ member(X0,universal_class) ) ),
introduced(definition,[new_symbols(definition,[spl3_219])],[avatar_definition]) ).
fof(f4834,plain,
( ! [X0] :
( member(unordered_pair(unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)),unordered_pair(not_subclass_element(sF0,sF2),unordered_pair(X0,X0))),sF1)
| ~ member(X0,universal_class) )
| ~ spl3_219 ),
inference(avatar_component_clause,[],[f4833]) ).
fof(f4835,plain,
( spl3_219
| ~ spl3_7
| ~ spl3_218 ),
inference(avatar_split_clause,[],[f4829,f4806,f254,f4833]) ).
fof(f4836,plain,
( ! [X0] :
( ~ member(X0,universal_class)
| ~ member(not_subclass_element(sF0,sF2),unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2))) )
| ~ spl3_172
| ~ spl3_219 ),
inference(resolution,[],[f4834,f3965]) ).
fof(f4847,definition,
( spl3_220
<=> member(not_subclass_element(sF0,sF2),unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2))) ),
introduced(definition,[new_symbols(definition,[spl3_220])],[avatar_definition]) ).
fof(f4849,plain,
( ~ member(not_subclass_element(sF0,sF2),unordered_pair(not_subclass_element(sF0,sF2),not_subclass_element(sF0,sF2)))
| spl3_220 ),
inference(avatar_component_clause,[],[f4847]) ).
fof(f4851,definition,
( spl3_221
<=> ! [X0] : ~ member(X0,universal_class) ),
introduced(definition,[new_symbols(definition,[spl3_221])],[avatar_definition]) ).
fof(f4852,plain,
( ! [X0] : ~ member(X0,universal_class)
| ~ spl3_221 ),
inference(avatar_component_clause,[],[f4851]) ).
fof(f4853,plain,
( ~ spl3_220
| spl3_221
| ~ spl3_172
| ~ spl3_219 ),
inference(avatar_split_clause,[],[f4836,f4833,f3964,f4851,f4847]) ).
fof(f4855,plain,
( $false
| ~ spl3_148
| spl3_220 ),
inference(unit_resulting_resolution,[],[f337,f3663,f4849]) ).
fof(f4863,plain,
( ~ spl3_148
| spl3_220 ),
inference(avatar_contradiction_clause,[],[f4855]) ).
fof(f4931,plain,
( $false
| ~ spl3_221 ),
inference(resolution,[],[f4852,f11]) ).
fof(f4948,plain,
~ spl3_221,
inference(avatar_contradiction_clause,[],[f4931]) ).
fof(f4977,plain,
( $false
| ~ spl3_148
| ~ spl3_154 ),
inference(unit_resulting_resolution,[],[f3736,f3663]) ).
fof(f4984,plain,
( ~ spl3_148
| ~ spl3_154 ),
inference(avatar_contradiction_clause,[],[f4977]) ).
cnf(s97,plain,
spl3_1,
inference(sat_conversion,[],[f202]) ).
cnf(s102,plain,
~ spl3_2,
inference(sat_conversion,[],[f211]) ).
cnf(s105,plain,
spl3_3,
inference(sat_conversion,[],[f219]) ).
cnf(s109,plain,
spl3_5,
inference(sat_conversion,[],[f228]) ).
cnf(s126,plain,
( ~ spl3_5
| spl3_7 ),
inference(sat_conversion,[],[f256]) ).
cnf(s137,plain,
( ~ spl3_5
| spl3_8 ),
inference(sat_conversion,[],[f273]) ).
cnf(s150,plain,
( ~ spl3_5
| spl3_9 ),
inference(sat_conversion,[],[f288]) ).
cnf(s156,plain,
( ~ spl3_9
| spl3_10 ),
inference(sat_conversion,[],[f297]) ).
cnf(s163,plain,
( ~ spl3_1
| ~ spl3_5
| spl3_12 ),
inference(sat_conversion,[],[f310]) ).
cnf(s169,plain,
( ~ spl3_10
| spl3_13 ),
inference(sat_conversion,[],[f319]) ).
cnf(s226,plain,
( ~ spl3_3
| spl3_20 ),
inference(sat_conversion,[],[f420]) ).
cnf(s238,plain,
( ~ spl3_20
| spl3_21 ),
inference(sat_conversion,[],[f436]) ).
cnf(s294,plain,
( ~ spl3_12
| spl3_26 ),
inference(sat_conversion,[],[f545]) ).
cnf(s749,plain,
( ~ spl3_21
| spl3_64 ),
inference(sat_conversion,[],[f1470]) ).
cnf(s898,plain,
( ~ spl3_3
| spl3_75 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s985,plain,
( ~ spl3_75
| spl3_82 ),
inference(sat_conversion,[],[f1961]) ).
cnf(s1183,plain,
( spl3_2
| ~ spl3_13
| ~ spl3_82
| spl3_87
| spl3_88 ),
inference(sat_conversion,[],[f2053]) ).
cnf(s1214,plain,
( ~ spl3_88
| spl3_93 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s1283,plain,
( ~ spl3_5
| spl3_102 ),
inference(sat_conversion,[],[f2298]) ).
cnf(s1349,plain,
( ~ spl3_12
| spl3_110 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s1534,plain,
( spl3_99
| spl3_127 ),
inference(sat_conversion,[],[f2744]) ).
cnf(s1548,plain,
( ~ spl3_3
| ~ spl3_127
| ~ spl3_128 ),
inference(sat_conversion,[],[f2778]) ).
cnf(s1552,plain,
( spl3_128
| spl3_129 ),
inference(sat_conversion,[],[f2786]) ).
cnf(s1559,plain,
( spl3_2
| ~ spl3_13
| spl3_87
| ~ spl3_129 ),
inference(sat_conversion,[],[f2795]) ).
cnf(s1603,plain,
( ~ spl3_88
| ~ spl3_99
| ~ spl3_110
| spl3_130 ),
inference(sat_conversion,[],[f2828]) ).
cnf(s1608,plain,
( ~ spl3_93
| spl3_127
| spl3_131 ),
inference(sat_conversion,[],[f2839]) ).
cnf(s1621,plain,
( ~ spl3_131
| spl3_135 ),
inference(sat_conversion,[],[f2881]) ).
cnf(s1628,plain,
( ~ spl3_130
| ~ spl3_135
| spl3_136 ),
inference(sat_conversion,[],[f2895]) ).
cnf(s1635,plain,
( spl3_129
| ~ spl3_136 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s1858,plain,
( ~ spl3_82
| spl3_88
| spl3_129 ),
inference(sat_conversion,[],[f3533]) ).
cnf(s1950,plain,
( spl3_2
| ~ spl3_129
| spl3_140 ),
inference(sat_conversion,[],[f3564]) ).
cnf(s2001,plain,
( ~ spl3_87
| spl3_148 ),
inference(sat_conversion,[],[f3664]) ).
cnf(s2043,plain,
( spl3_2
| ~ spl3_64
| ~ spl3_129
| spl3_154
| spl3_155 ),
inference(sat_conversion,[],[f3741]) ).
cnf(s2146,plain,
( ~ spl3_155
| spl3_169 ),
inference(sat_conversion,[],[f3932]) ).
cnf(s2166,plain,
( ~ spl3_26
| ~ spl3_169
| spl3_172 ),
inference(sat_conversion,[],[f3966]) ).
cnf(s2647,plain,
( ~ spl3_8
| ~ spl3_87
| ~ spl3_140
| spl3_217 ),
inference(sat_conversion,[],[f4790]) ).
cnf(s2656,plain,
( ~ spl3_1
| ~ spl3_102
| ~ spl3_217
| spl3_218 ),
inference(sat_conversion,[],[f4808]) ).
cnf(s2671,plain,
( ~ spl3_7
| ~ spl3_218
| spl3_219 ),
inference(sat_conversion,[],[f4835]) ).
cnf(s2679,plain,
( ~ spl3_172
| ~ spl3_219
| ~ spl3_220
| spl3_221 ),
inference(sat_conversion,[],[f4853]) ).
cnf(s2682,plain,
( ~ spl3_148
| spl3_220 ),
inference(sat_conversion,[],[f4863]) ).
cnf(s2837,plain,
~ spl3_221,
inference(sat_conversion,[],[f4948]) ).
cnf(s3691,plain,
( ~ spl3_148
| ~ spl3_154 ),
inference(sat_conversion,[],[f4984]) ).
cnf(s3694,plain,
( ~ spl3_172
| ~ spl3_219
| ~ spl3_220 ),
inference(rat,[],[s2679,s2837]) ).
cnf(s3703,plain,
spl3_102,
inference(rat,[],[s1283,s109]) ).
cnf(s3711,plain,
spl3_9,
inference(rat,[],[s150,s109]) ).
cnf(s3712,plain,
spl3_8,
inference(rat,[],[s137,s109]) ).
cnf(s3713,plain,
spl3_7,
inference(rat,[],[s126,s109]) ).
cnf(s3718,plain,
spl3_10,
inference(rat,[],[s156,s3711]) ).
cnf(s3726,plain,
spl3_13,
inference(rat,[],[s169,s3718]) ).
cnf(s3733,plain,
spl3_75,
inference(rat,[],[s898,s105]) ).
cnf(s3734,plain,
spl3_20,
inference(rat,[],[s226,s105]) ).
cnf(s3735,plain,
spl3_82,
inference(rat,[],[s985,s3733]) ).
cnf(s3736,plain,
spl3_21,
inference(rat,[],[s238,s3734]) ).
cnf(s3737,plain,
spl3_64,
inference(rat,[],[s749,s3736]) ).
cnf(s3741,plain,
spl3_12,
inference(rat,[],[s163,s109,s97]) ).
cnf(s3743,plain,
spl3_110,
inference(rat,[],[s1349,s3741]) ).
cnf(s3745,plain,
spl3_26,
inference(rat,[],[s294,s3741]) ).
cnf(s3747,plain,
spl3_87,
inference(rat,[],[s1628,s1603,s1621,s1534,s1608,s1548,s1214,s1552,s1635,s1183,s1559,s3743,s105,s3726,s3735,s102]) ).
cnf(s3752,plain,
spl3_148,
inference(rat,[],[s2001,s3747]) ).
cnf(s3756,plain,
~ spl3_154,
inference(rat,[],[s3691,s3752]) ).
cnf(s3757,plain,
spl3_220,
inference(rat,[],[s2682,s3752]) ).
cnf(s3762,plain,
~ spl3_129,
inference(rat,[],[s3694,s2671,s2166,s2656,s2146,s2647,s2043,s1950,s3757,s3713,s3745,s3703,s97,s3712,s3747,s3737,s102,s3756]) ).
cnf(s3763,plain,
~ spl3_136,
inference(rat,[],[s1635,s3762]) ).
cnf(s3764,plain,
spl3_128,
inference(rat,[],[s1552,s3762]) ).
cnf(s3765,plain,
spl3_88,
inference(rat,[],[s1858,s3735,s3762]) ).
cnf(s3768,plain,
~ spl3_127,
inference(rat,[],[s1548,s105,s3764]) ).
cnf(s3773,plain,
spl3_93,
inference(rat,[],[s1214,s3765]) ).
cnf(s3775,plain,
spl3_131,
inference(rat,[],[s1608,s3773,s3768]) ).
cnf(s3776,plain,
spl3_99,
inference(rat,[],[s1534,s3768]) ).
cnf(s3778,plain,
spl3_135,
inference(rat,[],[s1621,s3775]) ).
cnf(s3779,plain,
spl3_130,
inference(rat,[],[s1603,s3765,s3743,s3776]) ).
cnf(s3782,plain,
$false,
inference(rat,[],[s1628,s3763,s3779,s3778]) ).
fof(f4988,plain,
$false,
inference(avatar_sat_refutation,[],[s3782]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET293-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 % Computer : n003.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Mon Sep 28 01:24:12 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.45 Running first-order theorem proving
% 0.14/0.46 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
% 13.20/2.83 % (1104327)Input is clausal, will run a generic CNF schedule.
% 13.20/2.83 % (1104344)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3542089951:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.20/2.83 % (1104345)dis-21_1_sil=8000:lcm=predicate:random_seed=4014331092: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)
% 13.20/2.83 % (1104339)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=1676485468:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.20/2.83 % (1104343)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3106343569:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.20/2.83 % (1104340)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3755430610:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.20/2.83 % (1104342)lrs+10_1_sil=8000:sp=occurrence:random_seed=3535487983:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.20/2.83 % (1104341)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1736229280:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.20/2.83 % (1104342)Refutation not found, incomplete strategy
% 13.20/2.83 % (1104342)------------------------------
% 13.20/2.83 % (1104342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.83 % (1104342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.83 % (1104342)CaDiCaL version: 2.1.3
% 13.20/2.83 % (1104342)Termination reason: Refutation not found, incomplete strategy
% 13.20/2.83 % (1104342)Time elapsed: 0.001 s
% 13.20/2.83 % (1104342)Peak memory usage: 87 MB
% 13.20/2.83 % (1104343)Refutation not found, incomplete strategy
% 13.20/2.83 % (1104343)------------------------------
% 13.20/2.83 % (1104343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.83 % (1104343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.83 % (1104343)CaDiCaL version: 2.1.3
% 13.20/2.83 % (1104343)Termination reason: Refutation not found, incomplete strategy
% 13.20/2.83 % (1104343)Time elapsed: 0.004 s
% 13.20/2.83 % (1104343)Peak memory usage: 88 MB
% 13.20/2.83 % (1104343)Instructions burned: 2 (million)
% 13.20/2.83 % (1104345)Instruction limit reached!
% 13.20/2.83 % (1104345)------------------------------
% 13.20/2.83 % (1104345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.83 % (1104345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.83 % (1104345)CaDiCaL version: 2.1.3
% 13.20/2.83 % (1104345)Termination reason: Instruction limit
% 13.20/2.83 % (1104345)Termination phase: Saturation
% 13.20/2.83 % (1104345)Time elapsed: 0.083 s
% 13.20/2.83 % (1104345)Peak memory usage: 89 MB
% 13.20/2.83 % (1104345)Instructions burned: 120 (million)
% 13.20/2.83 % (1104344)Instruction limit reached!
% 13.20/2.83 % (1104344)------------------------------
% 13.20/2.83 % (1104344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.83 % (1104344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.83 % (1104344)CaDiCaL version: 2.1.3
% 13.20/2.83 % (1104344)Termination reason: Instruction limit
% 13.20/2.83 % (1104344)Termination phase: Saturation
% 13.20/2.83 % (1104344)Time elapsed: 0.116 s
% 13.20/2.83 % (1104344)Peak memory usage: 91 MB
% 13.20/2.83 % (1104344)Instructions burned: 180 (million)
% 13.20/2.83 % (1104357)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3256651808: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)
% 13.20/2.83 % (1104356)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=1853756780:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 13.20/2.83 % (1104356)Refutation not found, incomplete strategy
% 13.20/2.83 % (1104356)------------------------------
% 13.20/2.83 % (1104356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.83 % (1104356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.83 % (1104356)CaDiCaL version: 2.1.3
% 13.20/2.83 % (1104356)Termination reason: Refutation not found, incomplete strategy
% 28.71/4.91 % (1104356)Time elapsed: 0.005 s
% 28.71/4.91 % (1104356)Peak memory usage: 88 MB
% 28.71/4.91 % (1104356)Instructions burned: 3 (million)
% 28.71/4.91 % (1104357)Instruction limit reached!
% 28.71/4.91 % (1104357)------------------------------
% 28.71/4.91 % (1104357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/4.91 % (1104357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.91 % (1104357)CaDiCaL version: 2.1.3
% 28.71/4.91 % (1104357)Termination reason: Instruction limit
% 28.71/4.91 % (1104357)Termination phase: Saturation
% 28.71/4.91 % (1104357)Time elapsed: 0.094 s
% 28.71/4.91 % (1104357)Peak memory usage: 91 MB
% 28.71/4.91 % (1104357)Instructions burned: 190 (million)
% 28.71/4.91 % (1104343)------------------------------
% 28.71/4.91 % (1104343)------------------------------
% 28.71/4.91 % (1104342)------------------------------
% 28.71/4.91 % (1104342)------------------------------
% 28.71/4.91 % (1104365)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3688050576:st=4:i=219:sd=3:ss=axioms_2994 on theBenchmark for (2994ds/219Mi)
% 28.71/4.91 % (1104365)Refutation not found, incomplete strategy
% 28.71/4.91 % (1104365)------------------------------
% 28.71/4.91 % (1104365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/4.91 % (1104365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.91 % (1104365)CaDiCaL version: 2.1.3
% 28.71/4.91 % (1104365)Termination reason: Refutation not found, incomplete strategy
% 28.71/4.91 % (1104365)Time elapsed: 0.003 s
% 28.71/4.91 % (1104365)Peak memory usage: 88 MB
% 28.71/4.91 % (1104365)Instructions burned: 3 (million)
% 28.71/4.91 % (1104368)lrs+10_64_to=lpo:sil=8000:random_seed=2362851897:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 28.71/4.91 % (1104369)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3744161965:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 28.71/4.91 % (1104368)Instruction limit reached!
% 28.71/4.91 % (1104368)------------------------------
% 28.71/4.91 % (1104368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/4.91 % (1104368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.91 % (1104368)CaDiCaL version: 2.1.3
% 28.71/4.91 % (1104368)Termination reason: Instruction limit
% 28.71/4.91 % (1104368)Termination phase: Saturation
% 28.71/4.91 % (1104368)Time elapsed: 0.135 s
% 28.71/4.91 % (1104356)------------------------------
% 28.71/4.91 % (1104356)------------------------------
% 28.71/4.91 % (1104368)Peak memory usage: 89 MB
% 28.71/4.91 % (1104368)Instructions burned: 126 (million)
% 28.71/4.91 % (1104365)------------------------------
% 28.71/4.91 % (1104365)------------------------------
% 28.71/4.91 % (1104377)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=139765610:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 28.71/4.91 % (1104369)Instruction limit reached!
% 28.71/4.91 % (1104369)------------------------------
% 28.71/4.91 % (1104369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/4.91 % (1104369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.91 % (1104369)CaDiCaL version: 2.1.3
% 28.71/4.91 % (1104369)Termination reason: Instruction limit
% 28.71/4.91 % (1104369)Termination phase: Saturation
% 28.71/4.91 % (1104369)Time elapsed: 0.193 s
% 28.71/4.91 % (1104369)Peak memory usage: 90 MB
% 28.71/4.91 % (1104369)Instructions burned: 198 (million)
% 28.71/4.91 % (1104377)Instruction limit reached!
% 28.71/4.91 % (1104377)------------------------------
% 28.71/4.91 % (1104377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/4.91 % (1104377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/4.91 % (1104377)CaDiCaL version: 2.1.3
% 28.71/4.91 % (1104377)Termination reason: Instruction limit
% 28.71/4.91 % (1104377)Termination phase: Saturation
% 28.71/4.91 % (1104377)Time elapsed: 0.044 s
% 28.71/4.91 % (1104377)Peak memory usage: 90 MB
% 28.71/4.91 % (1104377)Instructions burned: 107 (million)
% 28.71/4.91 % (1104375)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=979039801:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 28.71/4.91 % (1104376)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1652289031:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 28.71/4.91 % (1104382)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=20012635:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 47.25/7.53 % (1104381)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4095917871:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 47.25/7.53 % (1104381)Refutation not found, incomplete strategy
% 47.25/7.53 % (1104381)------------------------------
% 47.25/7.53 % (1104381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.25/7.53 % (1104381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.25/7.53 % (1104381)CaDiCaL version: 2.1.3
% 47.25/7.53 % (1104381)Termination reason: Refutation not found, incomplete strategy
% 47.25/7.53 % (1104381)Time elapsed: 0.006 s
% 47.25/7.53 % (1104381)Peak memory usage: 88 MB
% 47.25/7.53 % (1104381)Instructions burned: 8 (million)
% 47.25/7.53 % (1104375)Instruction limit reached!
% 47.25/7.53 % (1104375)------------------------------
% 47.25/7.53 % (1104375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.25/7.53 % (1104375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.25/7.53 % (1104375)CaDiCaL version: 2.1.3
% 47.25/7.53 % (1104375)Termination reason: Instruction limit
% 47.25/7.53 % (1104375)Termination phase: Saturation
% 47.25/7.53 % (1104375)Time elapsed: 0.170 s
% 47.25/7.53 % (1104375)Peak memory usage: 91 MB
% 47.25/7.53 % (1104375)Instructions burned: 157 (million)
% 47.25/7.53 % (1104382)Instruction limit reached!
% 47.25/7.53 % (1104382)------------------------------
% 47.25/7.53 % (1104382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.25/7.53 % (1104382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.25/7.53 % (1104382)CaDiCaL version: 2.1.3
% 47.25/7.53 % (1104382)Termination reason: Instruction limit
% 47.25/7.53 % (1104382)Termination phase: Saturation
% 47.25/7.53 % (1104382)Time elapsed: 0.134 s
% 47.25/7.53 % (1104382)Peak memory usage: 91 MB
% 47.25/7.53 % (1104382)Instructions burned: 243 (million)
% 47.25/7.53 % (1104390)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=676952095:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 47.25/7.53 % (1104390)Refutation not found, incomplete strategy
% 47.25/7.53 % (1104390)------------------------------
% 47.25/7.53 % (1104390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.25/7.53 % (1104390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.25/7.53 % (1104390)CaDiCaL version: 2.1.3
% 47.25/7.53 % (1104390)Termination reason: Refutation not found, incomplete strategy
% 47.25/7.53 % (1104390)Time elapsed: 0.001 s
% 47.25/7.53 % (1104390)Peak memory usage: 87 MB
% 47.25/7.53 % (1104388)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=850312142:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 47.25/7.53 % (1104381)------------------------------
% 47.25/7.53 % (1104381)------------------------------
% 47.25/7.53 % (1104390)------------------------------
% 47.25/7.53 % (1104390)------------------------------
% 47.25/7.53 % (1104395)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4000500616:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 47.25/7.53 % (1104398)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2018876329:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 47.25/7.53 % (1104395)Instruction limit reached!
% 47.25/7.53 % (1104395)------------------------------
% 47.25/7.53 % (1104395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.25/7.53 % (1104395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.25/7.53 % (1104395)CaDiCaL version: 2.1.3
% 47.25/7.53 % (1104395)Termination reason: Instruction limit
% 47.25/7.53 % (1104395)Termination phase: Saturation
% 47.25/7.53 % (1104395)Time elapsed: 0.233 s
% 47.25/7.53 % (1104395)Peak memory usage: 93 MB
% 47.25/7.53 % (1104395)Instructions burned: 499 (million)
% 47.25/7.53 % (1104398)Instruction limit reached!
% 47.25/7.53 % (1104398)------------------------------
% 47.25/7.53 % (1104398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.25/7.53 % (1104398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.25/7.53 % (1104398)CaDiCaL version: 2.1.3
% 47.25/7.53 % (1104398)Termination reason: Instruction limit
% 70.59/10.81 % (1104398)Termination phase: Saturation
% 70.59/10.81 % (1104398)Time elapsed: 0.167 s
% 70.59/10.81 % (1104398)Peak memory usage: 89 MB
% 70.59/10.81 % (1104398)Instructions burned: 192 (million)
% 70.59/10.81 % (1104404)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4218545380:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 70.59/10.81 % (1104405)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1801220913:cond=on:i=156:bs=on:gtg=exists_all:er=known_2979 on theBenchmark for (2979ds/156Mi)
% 70.59/10.81 % (1104405)Instruction limit reached!
% 70.59/10.81 % (1104405)------------------------------
% 70.59/10.81 % (1104405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.59/10.81 % (1104405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.59/10.81 % (1104405)CaDiCaL version: 2.1.3
% 70.59/10.81 % (1104405)Termination reason: Instruction limit
% 70.59/10.81 % (1104405)Termination phase: Saturation
% 70.59/10.81 % (1104405)Time elapsed: 0.093 s
% 70.59/10.81 % (1104405)Peak memory usage: 90 MB
% 70.59/10.81 % (1104405)Instructions burned: 157 (million)
% 70.59/10.81 % (1104404)Instruction limit reached!
% 70.59/10.81 % (1104404)------------------------------
% 70.59/10.81 % (1104404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.59/10.81 % (1104404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.59/10.81 % (1104404)CaDiCaL version: 2.1.3
% 70.59/10.81 % (1104404)Termination reason: Instruction limit
% 70.59/10.81 % (1104404)Termination phase: Saturation
% 70.59/10.81 % (1104404)Time elapsed: 0.272 s
% 70.59/10.81 % (1104404)Peak memory usage: 92 MB
% 70.59/10.81 % (1104404)Instructions burned: 264 (million)
% 70.59/10.81 % (1104411)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=3628444390:i=3256:kws=precedence:bd=preordered:av=off_2976 on theBenchmark for (2976ds/3256Mi)
% 70.59/10.81 % (1104413)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1463987120:i=537:av=off:ss=included_2975 on theBenchmark for (2975ds/537Mi)
% 70.59/10.81 % (1104413)Refutation not found, incomplete strategy
% 70.59/10.81 % (1104413)------------------------------
% 70.59/10.81 % (1104413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.59/10.81 % (1104413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.59/10.81 % (1104413)CaDiCaL version: 2.1.3
% 70.59/10.81 % (1104413)Termination reason: Refutation not found, incomplete strategy
% 70.59/10.81 % (1104413)Time elapsed: 0.001 s
% 70.59/10.81 % (1104413)Peak memory usage: 87 MB
% 70.59/10.81 % (1104413)------------------------------
% 70.59/10.81 % (1104413)------------------------------
% 70.59/10.81 % (1104417)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3556725778:i=180:bd=preordered:av=off_2969 on theBenchmark for (2969ds/180Mi)
% 70.59/10.81 % (1104417)Instruction limit reached!
% 70.59/10.81 % (1104417)------------------------------
% 70.59/10.81 % (1104417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.59/10.81 % (1104417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.59/10.81 % (1104417)CaDiCaL version: 2.1.3
% 70.59/10.81 % (1104417)Termination reason: Instruction limit
% 70.59/10.81 % (1104417)Termination phase: Saturation
% 70.59/10.81 % (1104417)Time elapsed: 0.161 s
% 70.59/10.81 % (1104417)Peak memory usage: 90 MB
% 70.59/10.81 % (1104417)Instructions burned: 180 (million)
% 70.59/10.81 % (1104421)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=3994907856:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 70.59/10.81 % (1104411)Instruction limit reached!
% 70.59/10.81 % (1104411)------------------------------
% 70.59/10.81 % (1104411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.59/10.81 % (1104411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.59/10.81 % (1104411)CaDiCaL version: 2.1.3
% 70.59/10.81 % (1104411)Termination reason: Instruction limit
% 70.59/10.81 % (1104411)Termination phase: Saturation
% 70.59/10.81 % (1104411)Time elapsed: 1.519 s
% 70.59/10.81 % (1104411)Peak memory usage: 140 MB
% 70.59/10.81 % (1104411)Instructions burned: 3259 (million)
% 70.59/10.81 % (1104424)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=3495191607:i=412:gtgl=4:gtg=exists_all_2960 on theBenchmark for (2960ds/412Mi)
% 112.48/16.71 % (1104424)Instruction limit reached!
% 112.48/16.71 % (1104424)------------------------------
% 112.48/16.71 % (1104424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.48/16.71 % (1104424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.48/16.71 % (1104424)CaDiCaL version: 2.1.3
% 112.48/16.71 % (1104424)Termination reason: Instruction limit
% 112.48/16.71 % (1104424)Termination phase: Saturation
% 112.48/16.71 % (1104424)Time elapsed: 0.156 s
% 112.48/16.71 % (1104424)Peak memory usage: 90 MB
% 112.48/16.71 % (1104424)Instructions burned: 413 (million)
% 112.48/16.71 % (1104427)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=2042814742:s2pl=no:i=8478:s2at=4:nm=6_2956 on theBenchmark for (2956ds/8478Mi)
% 112.48/16.71 % (1104376)Instruction limit reached!
% 112.48/16.71 % (1104376)------------------------------
% 112.48/16.71 % (1104376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.48/16.71 % (1104376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.48/16.71 % (1104376)CaDiCaL version: 2.1.3
% 112.48/16.71 % (1104376)Termination reason: Instruction limit
% 112.48/16.71 % (1104376)Termination phase: Saturation
% 112.48/16.71 % (1104376)Time elapsed: 3.559 s
% 112.48/16.71 % (1104376)Peak memory usage: 147 MB
% 112.48/16.71 % (1104376)Instructions burned: 3394 (million)
% 112.48/16.71 % (1104431)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=3003491398:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2953 on theBenchmark for (2953ds/303Mi)
% 112.48/16.71 % (1104431)Refutation not found, incomplete strategy
% 112.48/16.71 % (1104431)------------------------------
% 112.48/16.71 % (1104431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.48/16.71 % (1104431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.48/16.71 % (1104431)CaDiCaL version: 2.1.3
% 112.48/16.71 % (1104431)Termination reason: Refutation not found, incomplete strategy
% 112.48/16.71 % (1104431)Time elapsed: 0.002 s
% 112.48/16.71 % (1104431)Peak memory usage: 88 MB
% 112.48/16.71 % (1104431)Instructions burned: 1 (million)
% 112.48/16.71 % (1104431)------------------------------
% 112.48/16.71 % (1104431)------------------------------
% 112.48/16.71 % (1104434)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=605326859:st=4:i=720:sd=3:fsr=off:ss=axioms_2947 on theBenchmark for (2947ds/720Mi)
% 112.48/16.71 % (1104434)Instruction limit reached!
% 112.48/16.71 % (1104434)------------------------------
% 112.48/16.71 % (1104434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.48/16.71 % (1104434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.48/16.71 % (1104434)CaDiCaL version: 2.1.3
% 112.48/16.71 % (1104434)Termination reason: Instruction limit
% 112.48/16.71 % (1104434)Termination phase: Saturation
% 112.48/16.71 % (1104434)Time elapsed: 0.699 s
% 112.48/16.71 % (1104434)Peak memory usage: 96 MB
% 112.48/16.71 % (1104434)Instructions burned: 720 (million)
% 112.48/16.71 % (1104440)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2064005423:i=598:bs=on:bd=preordered:av=off:ss=axioms_2938 on theBenchmark for (2938ds/598Mi)
% 112.48/16.71 % (1104440)Refutation not found, incomplete strategy
% 112.48/16.71 % (1104440)------------------------------
% 112.48/16.71 % (1104440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.48/16.71 % (1104440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.48/16.71 % (1104440)CaDiCaL version: 2.1.3
% 112.48/16.71 % (1104440)Termination reason: Refutation not found, incomplete strategy
% 112.48/16.71 % (1104440)Time elapsed: 0.002 s
% 112.48/16.71 % (1104440)Peak memory usage: 88 MB
% 112.48/16.71 % (1104440)------------------------------
% 112.48/16.71 % (1104440)------------------------------
% 112.48/16.71 % (1104388)Instruction limit reached!
% 112.48/16.71 % (1104388)------------------------------
% 112.48/16.71 % (1104388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.48/16.71 % (1104388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.48/16.71 % (1104388)CaDiCaL version: 2.1.3
% 112.48/16.71 % (1104388)Termination reason: Instruction limit
% 112.48/16.71 % (1104388)Termination phase: Saturation
% 112.48/16.71 % (1104388)Time elapsed: 5.297 s
% 112.48/16.71 % (1104388)Peak memory usage: 153 MB
% 112.48/16.71 % (1104388)Instructions burned: 5208 (million)
% 150.90/22.06 % (1104444)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2060292363:i=2989:sd=3:ss=axioms:sgt=60_2932 on theBenchmark for (2932ds/2989Mi)
% 150.90/22.06 % (1104447)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=3722847892:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2932 on theBenchmark for (2932ds/1997Mi)
% 150.90/22.06 % (1104427)Instruction limit reached!
% 150.90/22.06 % (1104427)------------------------------
% 150.90/22.06 % (1104427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.90/22.06 % (1104427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/22.06 % (1104427)CaDiCaL version: 2.1.3
% 150.90/22.06 % (1104427)Termination reason: Instruction limit
% 150.90/22.06 % (1104427)Termination phase: Saturation
% 150.90/22.06 % (1104427)Time elapsed: 4.0000 s
% 150.90/22.06 % (1104427)Peak memory usage: 175 MB
% 150.90/22.06 % (1104427)Instructions burned: 8479 (million)
% 150.90/22.06 % (1104451)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=3488360763:i=2088:bd=preordered:av=off_2915 on theBenchmark for (2915ds/2088Mi)
% 150.90/22.06 % (1104447)Instruction limit reached!
% 150.90/22.06 % (1104447)------------------------------
% 150.90/22.06 % (1104447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.90/22.06 % (1104447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/22.06 % (1104447)CaDiCaL version: 2.1.3
% 150.90/22.06 % (1104447)Termination reason: Instruction limit
% 150.90/22.06 % (1104447)Termination phase: Saturation
% 150.90/22.06 % (1104447)Time elapsed: 1.784 s
% 150.90/22.06 % (1104447)Peak memory usage: 138 MB
% 150.90/22.06 % (1104447)Instructions burned: 1999 (million)
% 150.90/22.06 % (1104453)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3280309066:i=1098:nicw=on_2912 on theBenchmark for (2912ds/1098Mi)
% 150.90/22.06 % (1104453)Instruction limit reached!
% 150.90/22.06 % (1104453)------------------------------
% 150.90/22.06 % (1104453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.90/22.06 % (1104453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/22.06 % (1104453)CaDiCaL version: 2.1.3
% 150.90/22.06 % (1104453)Termination reason: Instruction limit
% 150.90/22.06 % (1104453)Termination phase: Saturation
% 150.90/22.06 % (1104453)Time elapsed: 0.538 s
% 150.90/22.06 % (1104453)Peak memory usage: 102 MB
% 150.90/22.06 % (1104453)Instructions burned: 1100 (million)
% 150.90/22.06 % (1104444)Instruction limit reached!
% 150.90/22.06 % (1104444)------------------------------
% 150.90/22.06 % (1104444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.90/22.06 % (1104444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/22.06 % (1104444)CaDiCaL version: 2.1.3
% 150.90/22.06 % (1104444)Termination reason: Instruction limit
% 150.90/22.06 % (1104444)Termination phase: Saturation
% 150.90/22.06 % (1104444)Time elapsed: 2.605 s
% 150.90/22.06 % (1104444)Peak memory usage: 136 MB
% 150.90/22.06 % (1104444)Instructions burned: 2989 (million)
% 150.90/22.06 % (1104459)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=488357346:i=433:bd=preordered_2905 on theBenchmark for (2905ds/433Mi)
% 150.90/22.06 % (1104459)Refutation not found, incomplete strategy
% 150.90/22.06 % (1104459)------------------------------
% 150.90/22.06 % (1104459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.90/22.06 % (1104459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/22.06 % (1104459)CaDiCaL version: 2.1.3
% 150.90/22.06 % (1104459)Termination reason: Refutation not found, incomplete strategy
% 150.90/22.06 % (1104459)Time elapsed: 0.008 s
% 150.90/22.06 % (1104459)Peak memory usage: 89 MB
% 150.90/22.06 % (1104459)Instructions burned: 16 (million)
% 150.90/22.06 % (1104460)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1853435132:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2904 on theBenchmark for (2904ds/2942Mi)
% 150.90/22.06 % (1104459)------------------------------
% 150.90/22.06 % (1104459)------------------------------
% 150.90/22.06 % (1104463)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4249602570:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2901 on theBenchmark for (2901ds/6922Mi)
% 160.61/23.43 % (1104451)Instruction limit reached!
% 160.61/23.43 % (1104451)------------------------------
% 160.61/23.43 % (1104451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.61/23.43 % (1104451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.61/23.43 % (1104451)CaDiCaL version: 2.1.3
% 160.61/23.43 % (1104451)Termination reason: Instruction limit
% 160.61/23.43 % (1104451)Termination phase: Saturation
% 160.61/23.43 % (1104451)Time elapsed: 2.053 s
% 160.61/23.43 % (1104451)Peak memory usage: 138 MB
% 160.61/23.43 % (1104451)Instructions burned: 2088 (million)
% 160.61/23.43 % (1104466)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=1607413509:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2892 on theBenchmark for (2892ds/596Mi)
% 160.61/23.43 % (1104466)Instruction limit reached!
% 160.61/23.43 % (1104466)------------------------------
% 160.61/23.43 % (1104466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.61/23.43 % (1104466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.61/23.43 % (1104466)CaDiCaL version: 2.1.3
% 160.61/23.43 % (1104466)Termination reason: Instruction limit
% 160.61/23.43 % (1104466)Termination phase: Saturation
% 160.61/23.43 % (1104466)Time elapsed: 0.537 s
% 160.61/23.43 % (1104466)Peak memory usage: 99 MB
% 160.61/23.43 % (1104466)Instructions burned: 596 (million)
% 160.61/23.43 % (1104471)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=433119043:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2885 on theBenchmark for (2885ds/4123Mi)
% 160.61/23.43 % (1104460)Instruction limit reached!
% 160.61/23.43 % (1104460)------------------------------
% 160.61/23.43 % (1104460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.61/23.43 % (1104460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.61/23.43 % (1104460)CaDiCaL version: 2.1.3
% 160.61/23.43 % (1104460)Termination reason: Instruction limit
% 160.61/23.43 % (1104460)Termination phase: Saturation
% 160.61/23.43 % (1104460)Time elapsed: 1.998 s
% 160.61/23.43 % (1104460)Peak memory usage: 140 MB
% 160.61/23.43 % (1104460)Instructions burned: 2944 (million)
% 160.61/23.43 % (1104475)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2233076195:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2882 on theBenchmark for (2882ds/16411Mi)
% 160.61/23.43 % (1104421)Instruction limit reached!
% 160.61/23.43 % (1104421)------------------------------
% 160.61/23.43 % (1104421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.61/23.43 % (1104421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.61/23.43 % (1104421)CaDiCaL version: 2.1.3
% 160.61/23.43 % (1104421)Termination reason: Instruction limit
% 160.61/23.43 % (1104421)Termination phase: Saturation
% 160.61/23.43 % (1104421)Time elapsed: 9.767 s
% 160.61/23.43 % (1104421)Peak memory usage: 165 MB
% 160.61/23.43 % (1104421)Instructions burned: 10307 (million)
% 160.61/23.43 % (1104480)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3455073049:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2866 on theBenchmark for (2866ds/1670Mi)
% 160.61/23.43 % (1104480)Instruction limit reached!
% 160.61/23.43 % (1104480)------------------------------
% 160.61/23.43 % (1104480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.61/23.43 % (1104480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.61/23.43 % (1104480)CaDiCaL version: 2.1.3
% 160.61/23.43 % (1104480)Termination reason: Instruction limit
% 160.61/23.43 % (1104480)Termination phase: Saturation
% 160.61/23.43 % (1104480)Time elapsed: 1.748 s
% 160.61/23.43 % (1104480)Peak memory usage: 136 MB
% 160.61/23.43 % (1104480)Instructions burned: 1671 (million)
% 160.61/23.43 % (1104487)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=2238339077:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2846 on theBenchmark for (2846ds/1722Mi)
% 160.61/23.43 % (1104471)Instruction limit reached!
% 160.61/23.43 % (1104471)------------------------------
% 160.61/23.43 % (1104471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.61/23.43 % (1104471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.25/27.09 % (1104471)CaDiCaL version: 2.1.3
% 186.25/27.09 % (1104471)Termination reason: Instruction limit
% 186.25/27.09 % (1104471)Termination phase: Saturation
% 186.25/27.09 % (1104471)Time elapsed: 4.274 s
% 186.25/27.09 % (1104471)Peak memory usage: 152 MB
% 186.25/27.09 % (1104471)Instructions burned: 4123 (million)
% 186.25/27.09 % (1104489)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=3159163648:cts=off:cond=on:i=9530:bs=on:fsd=on_2840 on theBenchmark for (2840ds/9530Mi)
% 186.25/27.09 % (1104463)Instruction limit reached!
% 186.25/27.09 % (1104463)------------------------------
% 186.25/27.09 % (1104463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.25/27.09 % (1104463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.25/27.09 % (1104463)CaDiCaL version: 2.1.3
% 186.25/27.09 % (1104463)Termination reason: Instruction limit
% 186.25/27.09 % (1104463)Termination phase: Saturation
% 186.25/27.09 % (1104463)Time elapsed: 6.320 s
% 186.25/27.09 % (1104463)Peak memory usage: 177 MB
% 186.25/27.09 % (1104463)Instructions burned: 6922 (million)
% 186.25/27.09 % (1104487)Refutation not found, incomplete strategy
% 186.25/27.09 % (1104487)------------------------------
% 186.25/27.09 % (1104487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.25/27.09 % (1104487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.25/27.09 % (1104487)CaDiCaL version: 2.1.3
% 186.25/27.09 % (1104487)Termination reason: Refutation not found, incomplete strategy
% 186.25/27.09 % (1104487)Time elapsed: 0.982 s
% 186.25/27.09 % (1104487)Peak memory usage: 128 MB
% 186.25/27.09 % (1104487)Instructions burned: 909 (million)
% 186.25/27.09 % (1104491)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1843847748:st=2:i=4495:sd=10:ss=included_2836 on theBenchmark for (2836ds/4495Mi)
% 186.25/27.09 % (1104487)------------------------------
% 186.25/27.09 % (1104487)------------------------------
% 186.25/27.09 % (1104495)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1927444573:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2830 on theBenchmark for (2830ds/4920Mi)
% 186.25/27.09 % (1104475)Instruction limit reached!
% 186.25/27.09 % (1104475)------------------------------
% 186.25/27.09 % (1104475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.25/27.09 % (1104475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.25/27.09 % (1104475)CaDiCaL version: 2.1.3
% 186.25/27.09 % (1104475)Termination reason: Instruction limit
% 186.25/27.09 % (1104475)Termination phase: Saturation
% 186.25/27.09 % (1104475)Time elapsed: 8.047 s
% 186.25/27.09 % (1104475)Peak memory usage: 211 MB
% 186.25/27.09 % (1104475)Instructions burned: 16413 (million)
% 186.25/27.09 % (1104503)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=290685207:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2799 on theBenchmark for (2799ds/2083Mi)
% 186.25/27.09 % (1104491)Instruction limit reached!
% 186.25/27.09 % (1104491)------------------------------
% 186.25/27.09 % (1104491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.25/27.09 % (1104491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.25/27.09 % (1104491)CaDiCaL version: 2.1.3
% 186.25/27.09 % (1104491)Termination reason: Instruction limit
% 186.25/27.09 % (1104491)Termination phase: Saturation
% 186.25/27.09 % (1104491)Time elapsed: 4.517 s
% 186.25/27.09 % (1104491)Peak memory usage: 156 MB
% 186.25/27.09 % (1104491)Instructions burned: 4495 (million)
% 186.25/27.09 % (1104503)Instruction limit reached!
% 186.25/27.09 % (1104503)------------------------------
% 186.25/27.09 % (1104503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.25/27.09 % (1104503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.25/27.09 % (1104503)CaDiCaL version: 2.1.3
% 186.25/27.09 % (1104503)Termination reason: Instruction limit
% 186.25/27.09 % (1104503)Termination phase: Saturation
% 186.25/27.09 % (1104503)Time elapsed: 1.138 s
% 186.25/27.09 % (1104503)Peak memory usage: 136 MB
% 186.25/27.09 % (1104503)Instructions burned: 2083 (million)
% 186.25/27.09 % (1104505)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2378247710:i=4629:av=off:gsp=on_2788 on theBenchmark for (2788ds/4629Mi)
% 189.22/27.68 % (1104507)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3553195189:i=1258:av=off_2786 on theBenchmark for (2786ds/1258Mi)
% 189.22/27.68 % (1104505)Refutation not found, incomplete strategy
% 189.22/27.68 % (1104505)------------------------------
% 189.22/27.68 % (1104505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.22/27.68 % (1104505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.22/27.68 % (1104505)CaDiCaL version: 2.1.3
% 189.22/27.68 % (1104505)Termination reason: Refutation not found, incomplete strategy
% 189.22/27.68 % (1104505)Time elapsed: 0.492 s
% 189.22/27.68 % (1104505)Peak memory usage: 129 MB
% 189.22/27.68 % (1104505)Instructions burned: 879 (million)
% 189.22/27.68 % (1104505)------------------------------
% 189.22/27.68 % (1104505)------------------------------
% 189.22/27.68 % (1104495)Instruction limit reached!
% 189.22/27.68 % (1104495)------------------------------
% 189.22/27.68 % (1104495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.22/27.68 % (1104495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.22/27.68 % (1104495)CaDiCaL version: 2.1.3
% 189.22/27.68 % (1104495)Termination reason: Instruction limit
% 189.22/27.68 % (1104495)Termination phase: Saturation
% 189.22/27.68 % (1104495)Time elapsed: 4.969 s
% 189.22/27.68 % (1104495)Peak memory usage: 153 MB
% 189.22/27.68 % (1104495)Instructions burned: 4920 (million)
% 189.22/27.68 % (1104509)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3791852937:i=7343:av=off:ss=included_2779 on theBenchmark for (2779ds/7343Mi)
% 189.22/27.68 % (1104510)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=617948047:i=1325:sd=2:ss=axioms:sgt=16_2778 on theBenchmark for (2778ds/1325Mi)
% 189.22/27.68 % (1104510)Refutation not found, incomplete strategy
% 189.22/27.68 % (1104510)------------------------------
% 189.22/27.68 % (1104510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 189.22/27.68 % (1104510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 189.22/27.68 % (1104510)CaDiCaL version: 2.1.3
% 189.22/27.68 % (1104510)Termination reason: Refutation not found, incomplete strategy
% 189.22/27.68 % (1104510)Time elapsed: 0.006 s
% 189.22/27.68 % (1104510)Peak memory usage: 88 MB
% 189.22/27.68 % (1104510)Instructions burned: 4 (million)
% 189.22/27.68 [W928 01:24:35.514489939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 189.22/27.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 189.22/27.68 [W928 01:24:35.514531650 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 189.22/27.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 189.22/27.68 [W928 01:24:35.514558800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 189.22/27.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 189.22/27.68 [W928 01:24:35.514568066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 189.22/27.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 189.22/27.68 [W928 01:24:35.514588705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 189.22/27.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 189.22/27.68 [W928 01:24:35.514598653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 189.22/27.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 189.22/27.68 % (1104509)Refutation not found, incomplete strategy
% 204.32/29.64 % (1104509)------------------------------
% 204.32/29.64 % (1104509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 204.32/29.64 % (1104509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.32/29.64 % (1104509)CaDiCaL version: 2.1.3
% 204.32/29.64 % (1104509)Termination reason: Refutation not found, incomplete strategy
% 204.32/29.64 % (1104509)Time elapsed: 0.480 s
% 204.32/29.64 % (1104509)Peak memory usage: 127 MB
% 204.32/29.64 % (1104509)Instructions burned: 856 (million)
% 204.32/29.64 % (1104507)Instruction limit reached!
% 204.32/29.64 % (1104507)------------------------------
% 204.32/29.64 % (1104507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 204.32/29.64 % (1104507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.32/29.64 % (1104507)CaDiCaL version: 2.1.3
% 204.32/29.64 % (1104507)Termination reason: Instruction limit
% 204.32/29.64 % (1104507)Termination phase: Saturation
% 204.32/29.64 % (1104507)Time elapsed: 1.179 s
% 204.32/29.64 % (1104507)Peak memory usage: 96 MB
% 204.32/29.64 % (1104507)Instructions burned: 1258 (million)
% 204.32/29.64 % (1104510)------------------------------
% 204.32/29.64 % (1104510)------------------------------
% 204.32/29.64 % (1104509)------------------------------
% 204.32/29.64 % (1104509)------------------------------
% 204.32/29.64 % (1104514)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1598818168:i=1489:sd=2:ep=R:ss=axioms_2772 on theBenchmark for (2772ds/1489Mi)
% 204.32/29.64 % (1104513)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=3649975048:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2773 on theBenchmark for (2773ds/2646Mi)
% 204.32/29.64 % (1104517)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=1129901642:i=1503_2770 on theBenchmark for (2770ds/1503Mi)
% 204.32/29.64 % (1104514)Refutation not found, incomplete strategy
% 204.32/29.64 % (1104514)------------------------------
% 204.32/29.64 % (1104514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 204.32/29.64 % (1104514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.32/29.64 % (1104514)CaDiCaL version: 2.1.3
% 204.32/29.64 % (1104514)Termination reason: Refutation not found, incomplete strategy
% 204.32/29.64 % (1104514)Time elapsed: 0.873 s
% 204.32/29.64 % (1104514)Peak memory usage: 127 MB
% 204.32/29.64 % (1104514)Instructions burned: 857 (million)
% 204.32/29.64 % (1104514)------------------------------
% 204.32/29.64 % (1104514)------------------------------
% 204.32/29.64 % (1104513)Instruction limit reached!
% 204.32/29.64 % (1104513)------------------------------
% 204.32/29.64 % (1104513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 204.32/29.64 % (1104513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.32/29.64 % (1104513)CaDiCaL version: 2.1.3
% 204.32/29.64 % (1104513)Termination reason: Instruction limit
% 204.32/29.64 % (1104513)Termination phase: Saturation
% 204.32/29.64 % (1104513)Time elapsed: 1.432 s
% 204.32/29.64 % (1104513)Peak memory usage: 140 MB
% 204.32/29.64 % (1104513)Instructions burned: 2654 (million)
% 204.32/29.64 % (1104523)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3453742809:i=13942:kws=frequency_2758 on theBenchmark for (2758ds/13942Mi)
% 204.32/29.64 % (1104524)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=1080931479:i=3604:fsr=off:er=filter_2756 on theBenchmark for (2756ds/3604Mi)
% 204.32/29.64 % (1104517)Instruction limit reached!
% 204.32/29.64 % (1104517)------------------------------
% 204.32/29.64 % (1104517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 204.32/29.64 % (1104517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 204.32/29.64 % (1104517)CaDiCaL version: 2.1.3
% 204.32/29.64 % (1104517)Termination reason: Instruction limit
% 204.32/29.64 % (1104517)Termination phase: Saturation
% 204.32/29.64 % (1104517)Time elapsed: 1.632 s
% 204.32/29.64 % (1104517)Peak memory usage: 133 MB
% 204.32/29.64 % (1104517)Instructions burned: 1503 (million)
% 204.32/29.64 % (1104527)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2837800616:i=1876:sd=1:ss=included:sgt=32_2752 on theBenchmark for (2752ds/1876Mi)
% 204.32/29.64 % (1104524)Instruction limit reached!
% 132.36/33.84 % (1104524)------------------------------
% 132.36/33.84 % (1104524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104524)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104524)Termination reason: Instruction limit
% 132.36/33.84 % (1104524)Termination phase: Saturation
% 132.36/33.84 % (1104524)Time elapsed: 1.857 s
% 132.36/33.84 % (1104524)Peak memory usage: 142 MB
% 132.36/33.84 % (1104524)Instructions burned: 3604 (million)
% 132.36/33.84 % (1104489)Instruction limit reached!
% 132.36/33.84 % (1104489)------------------------------
% 132.36/33.84 % (1104489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104489)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104489)Termination reason: Instruction limit
% 132.36/33.84 % (1104489)Termination phase: Saturation
% 132.36/33.84 % (1104489)Time elapsed: 10.223 s
% 132.36/33.84 % (1104489)Peak memory usage: 173 MB
% 132.36/33.84 % (1104489)Instructions burned: 9530 (million)
% 132.36/33.84 % (1104533)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3982484767:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2736 on theBenchmark for (2736ds/1932Mi)
% 132.36/33.84 % (1104535)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=1450758555:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2736 on theBenchmark for (2736ds/1980Mi)
% 132.36/33.84 % (1104527)Instruction limit reached!
% 132.36/33.84 % (1104527)------------------------------
% 132.36/33.84 % (1104527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104527)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104527)Termination reason: Instruction limit
% 132.36/33.84 % (1104527)Termination phase: Saturation
% 132.36/33.84 % (1104527)Time elapsed: 1.748 s
% 132.36/33.84 % (1104527)Peak memory usage: 133 MB
% 132.36/33.84 % (1104527)Instructions burned: 1877 (million)
% 132.36/33.84 [W928 01:24:39.800587338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:39.800615119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:39.800642688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:39.800653398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:39.800674707 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:39.800683632 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 % (1104539)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=2478502199:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2733 on theBenchmark for (2733ds/3902Mi)
% 132.36/33.84 % (1104533)Refutation not found, incomplete strategy
% 132.36/33.84 % (1104533)------------------------------
% 132.36/33.84 % (1104533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104533)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104533)Termination reason: Refutation not found, incomplete strategy
% 132.36/33.84 % (1104533)Time elapsed: 0.494 s
% 132.36/33.84 % (1104533)Peak memory usage: 127 MB
% 132.36/33.84 % (1104533)Instructions burned: 850 (million)
% 132.36/33.84 % (1104533)------------------------------
% 132.36/33.84 % (1104533)------------------------------
% 132.36/33.84 % (1104542)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2218818274:avsq=on:i=3916:aac=none:amm=off_2727 on theBenchmark for (2727ds/3916Mi)
% 132.36/33.84 [W928 01:24:40.549079244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:40.549132441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:40.549194478 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:40.549212679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:40.549255932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 [W928 01:24:40.549272976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 132.36/33.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 132.36/33.84 % (1104539)Refutation not found, incomplete strategy
% 132.36/33.84 % (1104539)------------------------------
% 132.36/33.84 % (1104539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104539)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104539)Termination reason: Refutation not found, incomplete strategy
% 132.36/33.84 % (1104539)Time elapsed: 0.901 s
% 132.36/33.84 % (1104539)Peak memory usage: 127 MB
% 132.36/33.84 % (1104539)Instructions burned: 855 (million)
% 132.36/33.84 % (1104539)------------------------------
% 132.36/33.84 % (1104539)------------------------------
% 132.36/33.84 % (1104548)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3914996352:cond=on:i=3940:av=off:er=known_2717 on theBenchmark for (2717ds/3940Mi)
% 132.36/33.84 % (1104535)Instruction limit reached!
% 132.36/33.84 % (1104535)------------------------------
% 132.36/33.84 % (1104535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104535)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104535)Termination reason: Instruction limit
% 132.36/33.84 % (1104535)Termination phase: Saturation
% 132.36/33.84 % (1104535)Time elapsed: 2.040 s
% 132.36/33.84 % (1104535)Peak memory usage: 137 MB
% 132.36/33.84 % (1104535)Instructions burned: 1980 (million)
% 132.36/33.84 % (1104551)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1599488005:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2713 on theBenchmark for (2713ds/3980Mi)
% 132.36/33.84 % (1104542)Instruction limit reached!
% 132.36/33.84 % (1104542)------------------------------
% 132.36/33.84 % (1104542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104542)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104542)Termination reason: Instruction limit
% 132.36/33.84 % (1104542)Termination phase: Saturation
% 132.36/33.84 % (1104542)Time elapsed: 1.921 s
% 132.36/33.84 % (1104542)Peak memory usage: 117 MB
% 132.36/33.84 % (1104542)Instructions burned: 3918 (million)
% 132.36/33.84 % (1104555)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1586040726:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2707 on theBenchmark for (2707ds/2087Mi)
% 132.36/33.84 % (1104548)Instruction limit reached!
% 132.36/33.84 % (1104548)------------------------------
% 132.36/33.84 % (1104548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104548)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104548)Termination reason: Instruction limit
% 132.36/33.84 % (1104548)Termination phase: Saturation
% 132.36/33.84 % (1104548)Time elapsed: 2.539 s
% 132.36/33.84 % (1104548)Peak memory usage: 149 MB
% 132.36/33.84 % (1104548)Instructions burned: 3940 (million)
% 132.36/33.84 % (1104563)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=571610666:cts=off:cond=on:i=4272:bs=on:fsd=on_2689 on theBenchmark for (2689ds/4272Mi)
% 132.36/33.84 % (1104555)Instruction limit reached!
% 132.36/33.84 % (1104555)------------------------------
% 132.36/33.84 % (1104555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104555)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104555)Termination reason: Instruction limit
% 132.36/33.84 % (1104555)Termination phase: Saturation
% 132.36/33.84 % (1104555)Time elapsed: 2.233 s
% 132.36/33.84 % (1104555)Peak memory usage: 140 MB
% 132.36/33.84 % (1104555)Instructions burned: 2087 (million)
% 132.36/33.84 % (1104565)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=3926225561:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2682 on theBenchmark for (2682ds/2197Mi)
% 132.36/33.84 % (1104563)First to succeed.
% 132.36/33.84 % (1104563)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1104327"
% 132.36/33.84 % (1104551)Instruction limit reached!
% 132.36/33.84 % (1104551)------------------------------
% 132.36/33.84 % (1104551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.36/33.84 % (1104551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.36/33.84 % (1104551)CaDiCaL version: 2.1.3
% 132.36/33.84 % (1104551)Termination reason: Instruction limit
% 132.36/33.84 % (1104551)Termination phase: Saturation
% 132.36/33.84 % (1104551)Time elapsed: 3.976 s
% 132.36/33.84 % (1104551)Peak memory usage: 150 MB
% 132.36/33.84 % (1104551)Instructions burned: 3980 (million)
% 132.36/33.84 % (1104563)Refutation found. Thanks to Tanya!
% 132.36/33.84 % SZS status Unsatisfiable for theBenchmark
% 132.36/33.84 % SZS output start Proof for theBenchmark
% See solution above
% 234.61/34.08 % (1104563)------------------------------
% 234.61/34.08 % (1104563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 234.61/34.08 % (1104563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 234.61/34.08 % (1104563)CaDiCaL version: 2.1.3
% 234.61/34.08 % (1104563)Termination reason: Refutation
% 234.61/34.08 % (1104563)Time elapsed: 1.634 s
% 234.61/34.08 % (1104563)Peak memory usage: 142 MB
% 234.61/34.08 % (1104563)Instructions burned: 2965 (million)
% 234.61/34.08 % (1104563)------------------------------
% 234.61/34.08 % (1104563)------------------------------
% 234.61/34.08 % (1104327)Success in time 33.075 s
% 234.61/34.08 % Vampire exiting
%------------------------------------------------------------------------------