%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET537-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 : n007.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:41:07 PM UTC 2026
% Result : Unsatisfiable 212.73s 30.90s
% Output : Refutation 213.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 43
% Syntax : Number of formulae : 171 ( 61 unt; 14 def)
% Number of atoms : 452 ( 52 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 560 ( 279 ~; 281 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 38 ( 38 usr; 20 con; 0-3 aty)
% Number of variables : 244 ( 244 !; 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(f9,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f10,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
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(f20,axiom,
! [X0,X1] :
( ~ member(ordered_pair(X0,X1),cross_product(universal_class,universal_class))
| ~ member(X0,X1)
| member(ordered_pair(X0,X1),element_relation) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_relation3) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
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(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(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(f40,axiom,
! [X0] : domain_of(inverse(X0)) = range_of(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_of) ).
fof(f43,axiom,
! [X0,X1] : range_of(restrict(X0,X1,universal_class)) = image(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',image) ).
fof(f54,axiom,
! [X0] : domain_of(restrict(element_relation,universal_class,X0)) = sum_class(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_class_definition) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f71,axiom,
! [X0,X1] : sum_class(image(X0,singleton(X1))) = apply(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apply) ).
fof(f122,negated_conjecture,
member(ordered_pair(x,y),xf),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_2_to_application_property3_1) ).
fof(f123,negated_conjecture,
member(ordered_pair(x,y),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_2_to_application_property3_2) ).
fof(f124,negated_conjecture,
~ subclass(y,apply(xf,x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_2_to_application_property3_3) ).
fof(f125,plain,
! [X0] : sum_class(X0) = domain_of(intersection(element_relation,cross_product(universal_class,X0))),
inference(definition_unfolding,[],[f54,f28]) ).
fof(f126,plain,
! [X0] : range_of(X0) = domain_of(domain_of(flip(cross_product(X0,universal_class)))),
inference(definition_unfolding,[],[f40,f39]) ).
fof(f127,plain,
! [X0,X1] : image(X0,X1) = domain_of(domain_of(flip(cross_product(intersection(X0,cross_product(X1,universal_class)),universal_class)))),
inference(definition_unfolding,[],[f43,f126,f28]) ).
fof(f128,plain,
! [X0,X1] : apply(X0,X1) = domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class)),universal_class))))))),
inference(definition_unfolding,[],[f71,f125,f127,f12]) ).
fof(f129,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(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(X0,X2) ),
inference(definition_unfolding,[],[f14,f129]) ).
fof(f139,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X1,X3) ),
inference(definition_unfolding,[],[f15,f129]) ).
fof(f140,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,f129]) ).
fof(f141,plain,
! [X2,X0,X1] :
( unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0
| ~ member(X0,cross_product(X1,X2)) ),
inference(definition_unfolding,[],[f17,f129]) ).
fof(f143,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ member(X0,X1)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),element_relation) ),
inference(definition_unfolding,[],[f20,f129,f129]) ).
fof(f146,plain,
! [X0,X1] :
( null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,domain_of(X1)) ),
inference(definition_unfolding,[],[f32,f28,f12]) ).
fof(f150,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,f129,f129,f129,f129,f129,f129]) ).
fof(f187,plain,
member(unordered_pair(unordered_pair(x,x),unordered_pair(x,unordered_pair(y,y))),xf),
inference(definition_unfolding,[],[f122,f129]) ).
fof(f188,plain,
member(unordered_pair(unordered_pair(x,x),unordered_pair(x,unordered_pair(y,y))),cross_product(universal_class,universal_class)),
inference(definition_unfolding,[],[f123,f129]) ).
fof(f189,plain,
~ subclass(y,domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(xf,cross_product(unordered_pair(x,x),universal_class)),universal_class)))))))),
inference(definition_unfolding,[],[f124,f128]) ).
fof(f196,definition,
sF1 = unordered_pair(x,x),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f197,plain,
unordered_pair(x,x) = sF1,
inference(reorient_equations,[],[f196]) ).
fof(f198,definition,
sF2 = unordered_pair(y,y),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f199,plain,
unordered_pair(y,y) = sF2,
inference(reorient_equations,[],[f198]) ).
fof(f200,definition,
sF3 = unordered_pair(x,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f201,plain,
unordered_pair(x,sF2) = sF3,
inference(reorient_equations,[],[f200]) ).
fof(f202,definition,
sF4 = unordered_pair(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f203,plain,
unordered_pair(sF1,sF3) = sF4,
inference(reorient_equations,[],[f202]) ).
fof(f204,plain,
member(sF4,xf),
inference(definition_folding,[],[f187,f203,f201,f199,f197]) ).
fof(f205,definition,
sF5 = cross_product(universal_class,universal_class),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f206,plain,
cross_product(universal_class,universal_class) = sF5,
inference(reorient_equations,[],[f205]) ).
fof(f207,plain,
member(sF4,sF5),
inference(definition_folding,[],[f188,f206,f203,f201,f199,f197]) ).
fof(f208,definition,
sF6 = cross_product(sF1,universal_class),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f209,plain,
cross_product(sF1,universal_class) = sF6,
inference(reorient_equations,[],[f208]) ).
fof(f210,definition,
sF7 = intersection(xf,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f211,plain,
intersection(xf,sF6) = sF7,
inference(reorient_equations,[],[f210]) ).
fof(f212,definition,
sF8 = cross_product(sF7,universal_class),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f213,plain,
cross_product(sF7,universal_class) = sF8,
inference(reorient_equations,[],[f212]) ).
fof(f214,definition,
sF9 = flip(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f215,plain,
flip(sF8) = sF9,
inference(reorient_equations,[],[f214]) ).
fof(f216,definition,
sF10 = domain_of(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f217,plain,
domain_of(sF9) = sF10,
inference(reorient_equations,[],[f216]) ).
fof(f218,definition,
sF11 = domain_of(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f219,plain,
domain_of(sF10) = sF11,
inference(reorient_equations,[],[f218]) ).
fof(f220,definition,
sF12 = cross_product(universal_class,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f221,plain,
cross_product(universal_class,sF11) = sF12,
inference(reorient_equations,[],[f220]) ).
fof(f222,definition,
sF13 = intersection(element_relation,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f223,plain,
intersection(element_relation,sF12) = sF13,
inference(reorient_equations,[],[f222]) ).
fof(f224,definition,
sF14 = domain_of(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f225,plain,
domain_of(sF13) = sF14,
inference(reorient_equations,[],[f224]) ).
fof(f226,plain,
~ subclass(y,sF14),
inference(definition_folding,[],[f189,f225,f223,f221,f219,f217,f215,f213,f211,f209,f197]) ).
fof(f233,plain,
( member(y,sF2)
| ~ member(y,universal_class) ),
inference(superposition,[],[f9,f199]) ).
fof(f271,plain,
( member(x,sF1)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f197]) ).
fof(f283,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X0,X0))),unordered_pair(X2,X2))),cross_product(sF5,universal_class))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X3,X3))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X3,X3)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X3,X3))),unordered_pair(X2,X2))),X1)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X0,X0))),unordered_pair(X2,X2))),flip(X1)) ),
inference(superposition,[],[f150,f206]) ).
fof(f286,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| member(X0,universal_class) ),
inference(superposition,[],[f138,f206]) ).
fof(f287,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| member(X1,universal_class) ),
inference(superposition,[],[f139,f206]) ).
fof(f290,plain,
! [X0] :
( member(X0,sF7)
| ~ member(X0,sF6)
| ~ member(X0,xf) ),
inference(superposition,[],[f23,f211]) ).
fof(f324,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(superposition,[],[f140,f206]) ).
fof(f325,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF6)
| ~ member(X1,universal_class)
| ~ member(X0,sF1) ),
inference(superposition,[],[f140,f209]) ).
fof(f326,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF8)
| ~ member(X1,universal_class)
| ~ member(X0,sF7) ),
inference(superposition,[],[f140,f213]) ).
fof(f327,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF12)
| ~ member(X1,sF11)
| ~ member(X0,universal_class) ),
inference(superposition,[],[f140,f221]) ).
fof(f345,plain,
! [X0] :
( member(X0,sF13)
| ~ member(X0,sF12)
| ~ member(X0,element_relation) ),
inference(superposition,[],[f23,f223]) ).
fof(f373,plain,
! [X0,X1] :
( member(X1,X0)
| ~ member(X1,null_class)
| null_class = X0 ),
inference(superposition,[],[f21,f70]) ).
fof(f402,plain,
! [X0] :
( member(unordered_pair(sF2,unordered_pair(y,unordered_pair(X0,X0))),sF5)
| ~ member(X0,universal_class)
| ~ member(y,universal_class) ),
inference(superposition,[],[f324,f199]) ).
fof(f404,plain,
! [X0] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF5)
| ~ member(y,universal_class)
| ~ member(X0,universal_class) ),
inference(superposition,[],[f324,f199]) ).
fof(f509,plain,
! [X2,X0,X1] :
( ~ member(X2,cross_product(unordered_pair(X0,X0),universal_class))
| member(X2,null_class)
| ~ member(X2,X1)
| ~ member(X0,universal_class)
| member(X0,domain_of(X1)) ),
inference(superposition,[],[f23,f146]) ).
fof(f534,plain,
! [X2,X3,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X3,universal_class)
| member(X3,domain_of(X2))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X3,X3)) ),
inference(resolution,[],[f509,f140]) ).
fof(f543,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(y,y))),X2)
| ~ member(X1,universal_class)
| member(X1,domain_of(X2))
| ~ member(y,universal_class)
| ~ member(X0,unordered_pair(X1,X1)) ),
inference(superposition,[],[f534,f199]) ).
fof(f545,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),X2)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),null_class)
| ~ member(X1,universal_class)
| member(X1,domain_of(X2))
| ~ member(y,universal_class)
| ~ member(X0,unordered_pair(X1,X1)) ),
inference(forward_demodulation,[],[f543,f199]) ).
fof(f560,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))),flip(X3))
| ~ 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(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF5) ),
inference(resolution,[],[f283,f140]) ).
fof(f590,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),sF2)),flip(X1))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),unordered_pair(y,y))),X1)
| ~ member(y,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),sF5) ),
inference(superposition,[],[f560,f199]) ).
fof(f593,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),sF2)),X1)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),sF2)),flip(X1))
| ~ member(y,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),sF5) ),
inference(forward_demodulation,[],[f590,f199]) ).
fof(f664,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(X0,universal_class) ),
inference(superposition,[],[f11,f141]) ).
fof(f679,plain,
! [X0] :
( member(X0,universal_class)
| ~ member(X0,sF5) ),
inference(superposition,[],[f664,f206]) ).
fof(f713,plain,
! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF5)
| member(y,universal_class) ),
inference(superposition,[],[f287,f199]) ).
fof(f720,plain,
! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF5)
| member(X0,universal_class) ),
inference(superposition,[],[f286,f199]) ).
fof(f723,plain,
( ~ member(unordered_pair(sF1,unordered_pair(x,sF2)),sF5)
| member(x,universal_class) ),
inference(superposition,[],[f720,f197]) ).
fof(f725,plain,
( ~ member(unordered_pair(sF1,sF3),sF5)
| member(x,universal_class) ),
inference(forward_demodulation,[],[f723,f201]) ).
fof(f726,plain,
( ~ member(sF4,sF5)
| member(x,universal_class) ),
inference(forward_demodulation,[],[f725,f203]) ).
fof(f727,plain,
member(x,universal_class),
inference(forward_subsumption_resolution,[],[f726,f207]) ).
fof(f728,plain,
member(x,sF1),
inference(backward_subsumption_resolution,[],[f271,f727]) ).
fof(f913,plain,
! [X0] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF8)
| ~ member(y,universal_class)
| ~ member(X0,sF7) ),
inference(superposition,[],[f326,f199]) ).
fof(f1052,plain,
( ~ member(unordered_pair(sF1,unordered_pair(x,sF2)),sF5)
| member(y,universal_class) ),
inference(superposition,[],[f713,f197]) ).
fof(f1054,plain,
( ~ member(unordered_pair(sF1,sF3),sF5)
| member(y,universal_class) ),
inference(forward_demodulation,[],[f1052,f201]) ).
fof(f1055,plain,
( ~ member(sF4,sF5)
| member(y,universal_class) ),
inference(forward_demodulation,[],[f1054,f203]) ).
fof(f1056,plain,
member(y,universal_class),
inference(forward_subsumption_resolution,[],[f1055,f207]) ).
fof(f1057,plain,
member(y,sF2),
inference(backward_subsumption_resolution,[],[f233,f1056]) ).
fof(f1058,plain,
! [X0] :
( member(unordered_pair(sF2,unordered_pair(y,unordered_pair(X0,X0))),sF5)
| ~ member(X0,universal_class) ),
inference(backward_subsumption_resolution,[],[f402,f1056]) ).
fof(f1059,plain,
! [X0] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF5)
| ~ member(X0,universal_class) ),
inference(backward_subsumption_resolution,[],[f404,f1056]) ).
fof(f1062,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),null_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),X2)
| ~ member(X1,universal_class)
| member(X1,domain_of(X2))
| ~ member(X0,unordered_pair(X1,X1)) ),
inference(backward_subsumption_resolution,[],[f545,f1056]) ).
fof(f1063,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),sF2)),flip(X1))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X2,X2))),sF2)),X1)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X0,X0))),sF5) ),
inference(backward_subsumption_resolution,[],[f593,f1056]) ).
fof(f1068,plain,
! [X0] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF8)
| ~ member(X0,sF7) ),
inference(backward_subsumption_resolution,[],[f913,f1056]) ).
fof(f1265,plain,
! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),cross_product(universal_class,universal_class))
| ~ member(X0,y)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(y,y))),element_relation) ),
inference(superposition,[],[f143,f199]) ).
fof(f1269,plain,
! [X0] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF5)
| ~ member(X0,y)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(y,y))),element_relation) ),
inference(forward_demodulation,[],[f1265,f206]) ).
fof(f1274,plain,
! [X0] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),element_relation)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),sF5)
| ~ member(X0,y) ),
inference(forward_demodulation,[],[f1269,f199]) ).
fof(f1278,plain,
! [X0] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),element_relation)
| ~ member(X0,universal_class)
| ~ member(X0,y) ),
inference(forward_literal_rewriting,[],[f1274,f1059]) ).
fof(f1592,plain,
! [X0,X1] :
( complement(X1) = null_class
| ~ member(X0,null_class)
| ~ member(X0,X1) ),
inference(resolution,[],[f373,f24]) ).
fof(f1641,plain,
! [X2,X0,X1] :
( ~ member(X2,null_class)
| ~ member(X0,X1)
| ~ member(X0,null_class)
| ~ member(X2,X1) ),
inference(superposition,[],[f24,f1592]) ).
fof(f1679,plain,
! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,null_class)
| ~ member(X0,null_class) ),
inference(factoring,[],[f1641]) ).
fof(f1684,plain,
! [X0] : ~ member(X0,null_class),
inference(duplicate_literal_removal,[],[f1679]) ).
fof(f1719,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X2)
| ~ member(X3,universal_class)
| member(X3,domain_of(X2))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X3,X3)) ),
inference(backward_subsumption_resolution,[],[f534,f1684]) ).
fof(f1721,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),X2)
| ~ member(X1,universal_class)
| member(X1,domain_of(X2))
| ~ member(X0,unordered_pair(X1,X1)) ),
inference(backward_subsumption_resolution,[],[f1062,f1684]) ).
fof(f1819,plain,
! [X2,X0,X1] :
( ~ member(X0,universal_class)
| member(X0,domain_of(sF13))
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF12)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation) ),
inference(resolution,[],[f1719,f345]) ).
fof(f1831,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF12)
| ~ member(X0,universal_class)
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| member(X0,sF14)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation) ),
inference(forward_demodulation,[],[f1819,f225]) ).
fof(f1912,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X2,X2))),sF2)),X1)
| member(X0,domain_of(flip(X1)))
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3))),unordered_pair(X0,X0))
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3))),sF5) ),
inference(resolution,[],[f1721,f1063]) ).
fof(f1946,plain,
! [X2,X0,X1] :
( member(X0,domain_of(flip(sF8)))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X0,X0))
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF5)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF7) ),
inference(resolution,[],[f1912,f1068]) ).
fof(f1974,plain,
! [X2,X0,X1] :
( member(X0,domain_of(sF9))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X0,X0))
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF5)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF7) ),
inference(forward_demodulation,[],[f1946,f215]) ).
fof(f1981,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X0,X0))
| member(X0,sF10)
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF5)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF7) ),
inference(forward_demodulation,[],[f1974,f217]) ).
fof(f1988,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF10)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF7)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),universal_class) ),
inference(resolution,[],[f1981,f10]) ).
fof(f1998,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF10)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF7) ),
inference(duplicate_literal_removal,[],[f1988]) ).
fof(f2006,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF10)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF7) ),
inference(forward_subsumption_resolution,[],[f1998,f679]) ).
fof(f2276,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation)
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| member(X0,sF14)
| ~ member(X0,universal_class)
| ~ member(X1,sF11)
| ~ member(X2,universal_class) ),
inference(resolution,[],[f1831,f327]) ).
fof(f2300,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),element_relation)
| ~ member(y,universal_class)
| ~ member(X0,unordered_pair(X1,X1))
| member(X1,sF14)
| ~ member(X1,universal_class)
| ~ member(y,sF11)
| ~ member(X0,universal_class) ),
inference(superposition,[],[f2276,f199]) ).
fof(f2302,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),element_relation)
| ~ member(X0,unordered_pair(X1,X1))
| member(X1,sF14)
| ~ member(X1,universal_class)
| ~ member(y,sF11)
| ~ member(X0,universal_class) ),
inference(forward_subsumption_resolution,[],[f2300,f1056]) ).
fof(f2659,plain,
! [X0,X1] :
( ~ member(X0,unordered_pair(X1,X1))
| member(X1,sF14)
| ~ member(X1,universal_class)
| ~ member(y,sF11)
| ~ member(X0,universal_class)
| ~ member(X0,universal_class)
| ~ member(X0,y) ),
inference(resolution,[],[f2302,f1278]) ).
fof(f2665,plain,
! [X0,X1] :
( ~ member(X0,unordered_pair(X1,X1))
| member(X1,sF14)
| ~ member(X1,universal_class)
| ~ member(y,sF11)
| ~ member(X0,universal_class)
| ~ member(X0,y) ),
inference(duplicate_literal_removal,[],[f2659]) ).
fof(f2672,plain,
! [X0] :
( member(X0,sF14)
| ~ member(X0,universal_class)
| ~ member(y,sF11)
| ~ member(X0,universal_class)
| ~ member(X0,y)
| ~ member(X0,universal_class) ),
inference(resolution,[],[f2665,f10]) ).
fof(f2685,plain,
! [X0] :
( member(X0,sF14)
| ~ member(X0,universal_class)
| ~ member(y,sF11)
| ~ member(X0,y) ),
inference(duplicate_literal_removal,[],[f2672]) ).
fof(f2689,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF14),y)
| ~ member(y,sF11)
| ~ member(not_subclass_element(X0,sF14),universal_class)
| subclass(X0,sF14) ),
inference(resolution,[],[f2685,f3]) ).
fof(f2747,plain,
( ~ member(y,sF11)
| ~ member(not_subclass_element(y,sF14),universal_class)
| subclass(y,sF14)
| subclass(y,sF14) ),
inference(resolution,[],[f2689,f2]) ).
fof(f2758,plain,
( ~ member(y,sF11)
| ~ member(not_subclass_element(y,sF14),universal_class)
| subclass(y,sF14) ),
inference(duplicate_literal_removal,[],[f2747]) ).
fof(f2759,plain,
( ~ member(not_subclass_element(y,sF14),universal_class)
| ~ member(y,sF11) ),
inference(forward_subsumption_resolution,[],[f2758,f226]) ).
fof(f2800,plain,
! [X0] :
( ~ member(y,sF11)
| ~ member(not_subclass_element(y,sF14),X0)
| ~ subclass(X0,universal_class) ),
inference(resolution,[],[f2759,f1]) ).
fof(f2801,plain,
! [X0] :
( ~ member(y,sF11)
| ~ member(not_subclass_element(y,sF14),X0) ),
inference(forward_subsumption_resolution,[],[f2800,f4]) ).
fof(f3247,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF7)
| ~ member(X2,universal_class)
| member(X2,domain_of(sF10))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X2,X2)) ),
inference(resolution,[],[f2006,f1719]) ).
fof(f3258,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF7)
| ~ member(X2,universal_class)
| member(X2,domain_of(sF10))
| ~ member(X0,unordered_pair(X2,X2)) ),
inference(forward_subsumption_resolution,[],[f3247,f287]) ).
fof(f3264,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF7)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| member(X2,sF11)
| ~ member(X2,universal_class)
| ~ member(X0,unordered_pair(X2,X2)) ),
inference(forward_demodulation,[],[f3258,f219]) ).
fof(f3270,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF6)
| member(X2,sF11)
| ~ member(X2,universal_class)
| ~ member(X0,unordered_pair(X2,X2))
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF5)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),xf) ),
inference(resolution,[],[f3264,f290]) ).
fof(f3286,plain,
! [X2,X0,X1] :
( member(X0,sF11)
| ~ member(X0,universal_class)
| ~ member(X1,unordered_pair(X0,X0))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF5)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),xf)
| ~ member(X1,universal_class)
| ~ member(X2,sF1) ),
inference(resolution,[],[f3270,f325]) ).
fof(f3299,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),xf)
| ~ member(X0,universal_class)
| ~ member(X1,unordered_pair(X0,X0))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF5)
| member(X0,sF11)
| ~ member(X2,sF1) ),
inference(forward_subsumption_resolution,[],[f3286,f286]) ).
fof(f3315,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),xf)
| ~ member(X1,universal_class)
| ~ member(y,unordered_pair(X1,X1))
| ~ member(unordered_pair(unordered_pair(y,y),unordered_pair(y,unordered_pair(X0,X0))),sF5)
| member(X1,sF11)
| ~ member(X0,sF1) ),
inference(superposition,[],[f3299,f199]) ).
fof(f3317,plain,
! [X0,X1] :
( ~ member(unordered_pair(sF2,unordered_pair(y,unordered_pair(X0,X0))),sF5)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),xf)
| ~ member(X1,universal_class)
| ~ member(y,unordered_pair(X1,X1))
| member(X1,sF11)
| ~ member(X0,sF1) ),
inference(forward_demodulation,[],[f3315,f199]) ).
fof(f3321,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,sF2)),xf)
| ~ member(X0,universal_class)
| ~ member(X1,universal_class)
| ~ member(y,unordered_pair(X1,X1))
| member(X1,sF11)
| ~ member(X0,sF1) ),
inference(forward_literal_rewriting,[],[f3317,f1058]) ).
fof(f3337,plain,
! [X0] :
( ~ member(unordered_pair(sF1,unordered_pair(x,sF2)),xf)
| ~ member(x,universal_class)
| ~ member(X0,universal_class)
| ~ member(y,unordered_pair(X0,X0))
| member(X0,sF11)
| ~ member(x,sF1) ),
inference(superposition,[],[f3321,f197]) ).
fof(f3340,plain,
! [X0] :
( ~ member(unordered_pair(sF1,unordered_pair(x,sF2)),xf)
| ~ member(X0,universal_class)
| ~ member(y,unordered_pair(X0,X0))
| member(X0,sF11)
| ~ member(x,sF1) ),
inference(forward_subsumption_resolution,[],[f3337,f727]) ).
fof(f3341,plain,
! [X0] :
( ~ member(unordered_pair(sF1,unordered_pair(x,sF2)),xf)
| ~ member(X0,universal_class)
| ~ member(y,unordered_pair(X0,X0))
| member(X0,sF11) ),
inference(forward_subsumption_resolution,[],[f3340,f728]) ).
fof(f3342,plain,
! [X0] :
( ~ member(unordered_pair(sF1,sF3),xf)
| ~ member(X0,universal_class)
| ~ member(y,unordered_pair(X0,X0))
| member(X0,sF11) ),
inference(forward_demodulation,[],[f3341,f201]) ).
fof(f3343,plain,
! [X0] :
( ~ member(sF4,xf)
| ~ member(X0,universal_class)
| ~ member(y,unordered_pair(X0,X0))
| member(X0,sF11) ),
inference(forward_demodulation,[],[f3342,f203]) ).
fof(f3344,plain,
! [X0] :
( ~ member(y,unordered_pair(X0,X0))
| ~ member(X0,universal_class)
| member(X0,sF11) ),
inference(forward_subsumption_resolution,[],[f3343,f204]) ).
fof(f3348,plain,
( ~ member(y,sF2)
| ~ member(y,universal_class)
| member(y,sF11) ),
inference(superposition,[],[f3344,f199]) ).
fof(f3349,plain,
( ~ member(y,universal_class)
| member(y,sF11) ),
inference(forward_subsumption_resolution,[],[f3348,f1057]) ).
fof(f3351,plain,
member(y,sF11),
inference(forward_subsumption_resolution,[],[f3349,f1056]) ).
fof(f3414,plain,
! [X0] : ~ member(not_subclass_element(y,sF14),X0),
inference(backward_subsumption_resolution,[],[f2801,f3351]) ).
fof(f3422,plain,
subclass(y,sF14),
inference(resolution,[],[f3414,f2]) ).
fof(f3445,plain,
$false,
inference(forward_subsumption_resolution,[],[f3422,f226]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET537-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.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 28 02:04:25 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.39 Running first-order theorem proving
% 0.15/0.39 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
% 10.00/2.27 % (1959640)Input is clausal, will run a generic CNF schedule.
% 10.00/2.27 % (1959647)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=91602558:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.00/2.27 % (1959648)lrs+10_1_sil=8000:sp=occurrence:random_seed=3753257200:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.00/2.27 % (1959649)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4068643651:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.00/2.27 % (1959645)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=2837122136:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.00/2.27 % (1959646)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4227759536:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.00/2.27 % (1959650)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1966324862:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.00/2.27 % (1959651)dis-21_1_sil=8000:lcm=predicate:random_seed=3574478709:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.00/2.27 % (1959649)Instruction limit reached!
% 10.00/2.27 % (1959649)------------------------------
% 10.00/2.27 % (1959649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.27 % (1959649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.27 % (1959649)CaDiCaL version: 2.1.3
% 10.00/2.27 % (1959649)Termination reason: Instruction limit
% 10.00/2.27 % (1959649)Termination phase: Saturation
% 10.00/2.27 % (1959649)Time elapsed: 0.064 s
% 10.00/2.27 % (1959649)Peak memory usage: 88 MB
% 10.00/2.27 % (1959649)Instructions burned: 114 (million)
% 10.00/2.27 % (1959651)Instruction limit reached!
% 10.00/2.27 % (1959651)------------------------------
% 10.00/2.27 % (1959651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.27 % (1959651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.27 % (1959651)CaDiCaL version: 2.1.3
% 10.00/2.27 % (1959651)Termination reason: Instruction limit
% 10.00/2.27 % (1959651)Termination phase: Saturation
% 10.00/2.27 % (1959651)Time elapsed: 0.059 s
% 10.00/2.27 % (1959651)Peak memory usage: 89 MB
% 10.00/2.27 % (1959651)Instructions burned: 118 (million)
% 10.00/2.27 % (1959648)Instruction limit reached!
% 10.00/2.27 % (1959648)------------------------------
% 10.00/2.27 % (1959648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.27 % (1959648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.27 % (1959648)CaDiCaL version: 2.1.3
% 10.00/2.27 % (1959648)Termination reason: Instruction limit
% 10.00/2.27 % (1959648)Termination phase: Saturation
% 10.00/2.27 % (1959648)Time elapsed: 0.068 s
% 10.00/2.27 % (1959648)Peak memory usage: 90 MB
% 10.00/2.27 % (1959648)Instructions burned: 109 (million)
% 10.00/2.27 % (1959650)Instruction limit reached!
% 10.00/2.27 % (1959650)------------------------------
% 10.00/2.27 % (1959650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/2.27 % (1959650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/2.27 % (1959650)CaDiCaL version: 2.1.3
% 10.00/2.27 % (1959650)Termination reason: Instruction limit
% 10.00/2.27 % (1959650)Termination phase: Saturation
% 10.00/2.27 % (1959650)Time elapsed: 0.138 s
% 10.00/2.27 % (1959650)Peak memory usage: 90 MB
% 10.00/2.27 % (1959650)Instructions burned: 180 (million)
% 10.00/2.27 % (1959659)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=219301407:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.00/2.27 % (1959661)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4119526384:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.00/2.27 % (1959660)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=220821812: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)
% 10.00/2.27 % (1959661)Refutation not found, incomplete strategy
% 10.00/2.27 % (1959661)------------------------------
% 10.00/2.27 % (1959661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.21/3.68 % (1959661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.21/3.68 % (1959661)CaDiCaL version: 2.1.3
% 19.21/3.68 % (1959661)Termination reason: Refutation not found, incomplete strategy
% 19.21/3.68 % (1959661)Time elapsed: 0.008 s
% 19.21/3.68 % (1959661)Peak memory usage: 88 MB
% 19.21/3.68 % (1959661)Instructions burned: 9 (million)
% 19.21/3.68 % (1959662)lrs+10_64_to=lpo:sil=8000:random_seed=3339252597:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 19.21/3.68 % (1959659)Instruction limit reached!
% 19.21/3.68 % (1959659)------------------------------
% 19.21/3.68 % (1959659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.21/3.68 % (1959659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.21/3.68 % (1959659)CaDiCaL version: 2.1.3
% 19.21/3.68 % (1959659)Termination reason: Instruction limit
% 19.21/3.68 % (1959659)Termination phase: Saturation
% 19.21/3.68 % (1959659)Time elapsed: 0.089 s
% 19.21/3.68 % (1959659)Peak memory usage: 88 MB
% 19.21/3.68 % (1959659)Instructions burned: 143 (million)
% 19.21/3.68 % (1959660)Instruction limit reached!
% 19.21/3.68 % (1959660)------------------------------
% 19.21/3.68 % (1959660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.21/3.68 % (1959660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.21/3.68 % (1959660)CaDiCaL version: 2.1.3
% 19.21/3.68 % (1959660)Termination reason: Instruction limit
% 19.21/3.68 % (1959660)Termination phase: Saturation
% 19.21/3.68 % (1959660)Time elapsed: 0.092 s
% 19.21/3.68 % (1959660)Peak memory usage: 90 MB
% 19.21/3.68 % (1959660)Instructions burned: 190 (million)
% 19.21/3.68 % (1959662)Instruction limit reached!
% 19.21/3.68 % (1959662)------------------------------
% 19.21/3.68 % (1959662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.21/3.68 % (1959662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.21/3.68 % (1959662)CaDiCaL version: 2.1.3
% 19.21/3.68 % (1959662)Termination reason: Instruction limit
% 19.21/3.68 % (1959662)Termination phase: Saturation
% 19.21/3.68 % (1959662)Time elapsed: 0.079 s
% 19.21/3.68 % (1959662)Peak memory usage: 89 MB
% 19.21/3.68 % (1959662)Instructions burned: 127 (million)
% 19.21/3.68 % (1959668)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1490188275:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 19.21/3.68 % (1959667)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1878899686:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 19.21/3.68 % (1959661)------------------------------
% 19.21/3.68 % (1959661)------------------------------
% 19.21/3.68 % (1959669)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1814309780:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 19.21/3.68 % (1959668)Instruction limit reached!
% 19.21/3.68 % (1959668)------------------------------
% 19.21/3.68 % (1959668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.21/3.68 % (1959668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.21/3.68 % (1959668)CaDiCaL version: 2.1.3
% 19.21/3.68 % (1959668)Termination reason: Instruction limit
% 19.21/3.68 % (1959668)Termination phase: Saturation
% 19.21/3.68 % (1959668)Time elapsed: 0.106 s
% 19.21/3.68 % (1959668)Peak memory usage: 91 MB
% 19.21/3.68 % (1959668)Instructions burned: 157 (million)
% 19.21/3.68 % (1959667)Instruction limit reached!
% 19.21/3.68 % (1959667)------------------------------
% 19.21/3.68 % (1959667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.21/3.68 % (1959667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.21/3.68 % (1959667)CaDiCaL version: 2.1.3
% 19.21/3.68 % (1959667)Termination reason: Instruction limit
% 19.21/3.68 % (1959667)Termination phase: Saturation
% 19.21/3.68 % (1959667)Time elapsed: 0.128 s
% 19.21/3.68 % (1959667)Peak memory usage: 90 MB
% 19.21/3.68 % (1959667)Instructions burned: 195 (million)
% 19.21/3.68 % (1959672)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=108343544:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.21/3.68 % (1959672)Instruction limit reached!
% 19.21/3.68 % (1959672)------------------------------
% 19.21/3.68 % (1959672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.21/3.68 % (1959672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.69/5.63 % (1959672)CaDiCaL version: 2.1.3
% 33.69/5.63 % (1959672)Termination reason: Instruction limit
% 33.69/5.63 % (1959672)Termination phase: Saturation
% 33.69/5.63 % (1959672)Time elapsed: 0.058 s
% 33.69/5.63 % (1959672)Peak memory usage: 90 MB
% 33.69/5.63 % (1959672)Instructions burned: 107 (million)
% 33.69/5.63 % (1959674)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2419041374:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 33.69/5.63 % (1959675)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1184866301:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 33.69/5.63 % (1959674)Instruction limit reached!
% 33.69/5.63 % (1959674)------------------------------
% 33.69/5.63 % (1959674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.69/5.63 % (1959674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.69/5.63 % (1959674)CaDiCaL version: 2.1.3
% 33.69/5.63 % (1959674)Termination reason: Instruction limit
% 33.69/5.63 % (1959674)Termination phase: Saturation
% 33.69/5.63 % (1959674)Time elapsed: 0.074 s
% 33.69/5.63 % (1959674)Peak memory usage: 89 MB
% 33.69/5.63 % (1959674)Instructions burned: 108 (million)
% 33.69/5.63 % (1959677)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2955053708:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 33.69/5.63 % (1959675)Instruction limit reached!
% 33.69/5.63 % (1959675)------------------------------
% 33.69/5.63 % (1959675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.69/5.63 % (1959675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.69/5.63 % (1959675)CaDiCaL version: 2.1.3
% 33.69/5.63 % (1959675)Termination reason: Instruction limit
% 33.69/5.63 % (1959675)Termination phase: Saturation
% 33.69/5.63 % (1959675)Time elapsed: 0.167 s
% 33.69/5.63 % (1959675)Peak memory usage: 90 MB
% 33.69/5.63 % (1959675)Instructions burned: 242 (million)
% 33.69/5.63 % (1959680)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=28624905:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 33.69/5.63 % (1959680)Instruction limit reached!
% 33.69/5.63 % (1959680)------------------------------
% 33.69/5.63 % (1959680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.69/5.63 % (1959680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.69/5.63 % (1959680)CaDiCaL version: 2.1.3
% 33.69/5.63 % (1959680)Termination reason: Instruction limit
% 33.69/5.63 % (1959680)Termination phase: Saturation
% 33.69/5.63 % (1959680)Time elapsed: 0.067 s
% 33.69/5.63 % (1959680)Peak memory usage: 90 MB
% 33.69/5.63 % (1959680)Instructions burned: 135 (million)
% 33.69/5.63 % (1959682)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4025682046:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 33.69/5.63 % (1959684)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3372961672:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 33.69/5.63 % (1959684)Instruction limit reached!
% 33.69/5.63 % (1959684)------------------------------
% 33.69/5.63 % (1959684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.69/5.63 % (1959684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.69/5.63 % (1959684)CaDiCaL version: 2.1.3
% 33.69/5.63 % (1959684)Termination reason: Instruction limit
% 33.69/5.63 % (1959684)Termination phase: Saturation
% 33.69/5.63 % (1959684)Time elapsed: 0.103 s
% 33.69/5.63 % (1959684)Peak memory usage: 89 MB
% 33.69/5.63 % (1959684)Instructions burned: 191 (million)
% 33.69/5.63 % (1959682)Instruction limit reached!
% 33.69/5.63 % (1959682)------------------------------
% 33.69/5.63 % (1959682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.69/5.63 % (1959682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.69/5.63 % (1959682)CaDiCaL version: 2.1.3
% 33.69/5.63 % (1959682)Termination reason: Instruction limit
% 33.69/5.63 % (1959682)Termination phase: Saturation
% 33.69/5.63 % (1959682)Time elapsed: 0.257 s
% 33.69/5.63 % (1959682)Peak memory usage: 94 MB
% 33.69/5.63 % (1959682)Instructions burned: 500 (million)
% 33.69/5.63 % (1959687)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1688488913:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 52.97/8.33 % (1959688)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1058008938:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 52.97/8.33 % (1959687)Instruction limit reached!
% 52.97/8.33 % (1959687)------------------------------
% 52.97/8.33 % (1959687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.33 % (1959687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.33 % (1959687)CaDiCaL version: 2.1.3
% 52.97/8.33 % (1959687)Termination reason: Instruction limit
% 52.97/8.33 % (1959687)Termination phase: Saturation
% 52.97/8.33 % (1959687)Time elapsed: 0.137 s
% 52.97/8.33 % (1959687)Peak memory usage: 90 MB
% 52.97/8.33 % (1959687)Instructions burned: 265 (million)
% 52.97/8.33 % (1959688)Instruction limit reached!
% 52.97/8.33 % (1959688)------------------------------
% 52.97/8.33 % (1959688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.33 % (1959688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.33 % (1959688)CaDiCaL version: 2.1.3
% 52.97/8.33 % (1959688)Termination reason: Instruction limit
% 52.97/8.33 % (1959688)Termination phase: Saturation
% 52.97/8.33 % (1959688)Time elapsed: 0.109 s
% 52.97/8.33 % (1959688)Peak memory usage: 90 MB
% 52.97/8.33 % (1959688)Instructions burned: 157 (million)
% 52.97/8.33 % (1959691)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=4175203466:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 52.97/8.33 % (1959692)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=853403028:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 52.97/8.33 % (1959692)Instruction limit reached!
% 52.97/8.33 % (1959692)------------------------------
% 52.97/8.33 % (1959692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.33 % (1959692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.33 % (1959692)CaDiCaL version: 2.1.3
% 52.97/8.33 % (1959692)Termination reason: Instruction limit
% 52.97/8.33 % (1959692)Termination phase: Saturation
% 52.97/8.33 % (1959692)Time elapsed: 0.249 s
% 52.97/8.33 % (1959692)Peak memory usage: 88 MB
% 52.97/8.33 % (1959692)Instructions burned: 538 (million)
% 52.97/8.33 % (1959695)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1974780091:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 52.97/8.33 % (1959695)Instruction limit reached!
% 52.97/8.33 % (1959695)------------------------------
% 52.97/8.33 % (1959695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.33 % (1959695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.33 % (1959695)CaDiCaL version: 2.1.3
% 52.97/8.33 % (1959695)Termination reason: Instruction limit
% 52.97/8.33 % (1959695)Termination phase: Saturation
% 52.97/8.33 % (1959695)Time elapsed: 0.092 s
% 52.97/8.33 % (1959695)Peak memory usage: 90 MB
% 52.97/8.33 % (1959695)Instructions burned: 181 (million)
% 52.97/8.33 % (1959697)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=1989523389:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2977 on theBenchmark for (2977ds/10307Mi)
% 52.97/8.33 % (1959669)Instruction limit reached!
% 52.97/8.33 % (1959669)------------------------------
% 52.97/8.33 % (1959669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.33 % (1959669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.33 % (1959669)CaDiCaL version: 2.1.3
% 52.97/8.33 % (1959669)Termination reason: Instruction limit
% 52.97/8.33 % (1959669)Termination phase: Saturation
% 52.97/8.33 % (1959669)Time elapsed: 1.893 s
% 52.97/8.33 % (1959669)Peak memory usage: 150 MB
% 52.97/8.33 % (1959669)Instructions burned: 3395 (million)
% 52.97/8.33 % (1959699)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=3200619124:i=412:gtgl=4:gtg=exists_all_2974 on theBenchmark for (2974ds/412Mi)
% 52.97/8.33 % (1959699)Instruction limit reached!
% 52.97/8.33 % (1959699)------------------------------
% 52.97/8.33 % (1959699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.97/8.33 % (1959699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.97/8.33 % (1959699)CaDiCaL version: 2.1.3
% 74.32/11.30 % (1959699)Termination reason: Instruction limit
% 74.32/11.30 % (1959699)Termination phase: Saturation
% 74.32/11.30 % (1959699)Time elapsed: 0.182 s
% 74.32/11.30 % (1959699)Peak memory usage: 90 MB
% 74.32/11.30 % (1959699)Instructions burned: 413 (million)
% 74.32/11.30 % (1959701)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=2521797435:s2pl=no:i=8478:s2at=4:nm=6_2971 on theBenchmark for (2971ds/8478Mi)
% 74.32/11.30 % (1959691)Instruction limit reached!
% 74.32/11.30 % (1959691)------------------------------
% 74.32/11.30 % (1959691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.32/11.30 % (1959691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.32/11.30 % (1959691)CaDiCaL version: 2.1.3
% 74.32/11.30 % (1959691)Termination reason: Instruction limit
% 74.32/11.30 % (1959691)Termination phase: Saturation
% 74.32/11.30 % (1959691)Time elapsed: 1.840 s
% 74.32/11.30 % (1959691)Peak memory usage: 150 MB
% 74.32/11.30 % (1959691)Instructions burned: 3258 (million)
% 74.32/11.30 % (1959703)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=2390587872:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi)
% 74.32/11.30 % (1959703)Instruction limit reached!
% 74.32/11.30 % (1959703)------------------------------
% 74.32/11.30 % (1959703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.32/11.30 % (1959703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.32/11.30 % (1959703)CaDiCaL version: 2.1.3
% 74.32/11.30 % (1959703)Termination reason: Instruction limit
% 74.32/11.30 % (1959703)Termination phase: Saturation
% 74.32/11.30 % (1959703)Time elapsed: 0.153 s
% 74.32/11.30 % (1959703)Peak memory usage: 93 MB
% 74.32/11.30 % (1959703)Instructions burned: 304 (million)
% 74.32/11.30 % (1959705)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2713877693:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi)
% 74.32/11.30 % (1959677)Instruction limit reached!
% 74.32/11.30 % (1959677)------------------------------
% 74.32/11.30 % (1959677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.32/11.30 % (1959677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.32/11.30 % (1959677)CaDiCaL version: 2.1.3
% 74.32/11.30 % (1959677)Termination reason: Instruction limit
% 74.32/11.30 % (1959677)Termination phase: Saturation
% 74.32/11.30 % (1959677)Time elapsed: 3.303 s
% 74.32/11.30 % (1959677)Peak memory usage: 157 MB
% 74.32/11.30 % (1959677)Instructions burned: 5208 (million)
% 74.32/11.30 % (1959705)Instruction limit reached!
% 74.32/11.30 % (1959705)------------------------------
% 74.32/11.30 % (1959705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.32/11.30 % (1959705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.32/11.30 % (1959705)CaDiCaL version: 2.1.3
% 74.32/11.30 % (1959705)Termination reason: Instruction limit
% 74.32/11.30 % (1959705)Termination phase: Saturation
% 74.32/11.30 % (1959705)Time elapsed: 0.388 s
% 74.32/11.30 % (1959705)Peak memory usage: 98 MB
% 74.32/11.30 % (1959705)Instructions burned: 721 (million)
% 74.32/11.30 % (1959707)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=537325967:i=598:bs=on:bd=preordered:av=off:ss=axioms_2957 on theBenchmark for (2957ds/598Mi)
% 74.32/11.30 % (1959709)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=359956998:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 74.32/11.30 % (1959707)Instruction limit reached!
% 74.32/11.30 % (1959707)------------------------------
% 74.32/11.30 % (1959707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.32/11.30 % (1959707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.32/11.30 % (1959707)CaDiCaL version: 2.1.3
% 74.32/11.30 % (1959707)Termination reason: Instruction limit
% 74.32/11.30 % (1959707)Termination phase: Saturation
% 74.32/11.30 % (1959707)Time elapsed: 0.300 s
% 74.32/11.30 % (1959707)Peak memory usage: 94 MB
% 74.32/11.30 % (1959707)Instructions burned: 598 (million)
% 74.32/11.30 % (1959711)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=1232572629:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi)
% 115.15/17.04 % (1959711)Instruction limit reached!
% 115.15/17.04 % (1959711)------------------------------
% 115.15/17.04 % (1959711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.15/17.04 % (1959711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/17.04 % (1959711)CaDiCaL version: 2.1.3
% 115.15/17.04 % (1959711)Termination reason: Instruction limit
% 115.15/17.04 % (1959711)Termination phase: Saturation
% 115.15/17.04 % (1959711)Time elapsed: 1.318 s
% 115.15/17.04 % (1959711)Peak memory usage: 137 MB
% 115.15/17.04 % (1959711)Instructions burned: 1998 (million)
% 115.15/17.04 % (1959713)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=2079346134:i=2088:bd=preordered:av=off_2938 on theBenchmark for (2938ds/2088Mi)
% 115.15/17.04 % (1959709)Instruction limit reached!
% 115.15/17.04 % (1959709)------------------------------
% 115.15/17.04 % (1959709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.15/17.04 % (1959709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/17.04 % (1959709)CaDiCaL version: 2.1.3
% 115.15/17.04 % (1959709)Termination reason: Instruction limit
% 115.15/17.04 % (1959709)Termination phase: Saturation
% 115.15/17.04 % (1959709)Time elapsed: 1.910 s
% 115.15/17.04 % (1959709)Peak memory usage: 143 MB
% 115.15/17.04 % (1959709)Instructions burned: 2989 (million)
% 115.15/17.04 % (1959715)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2484265987:i=1098:nicw=on_2935 on theBenchmark for (2935ds/1098Mi)
% 115.15/17.04 % (1959701)Instruction limit reached!
% 115.15/17.04 % (1959701)------------------------------
% 115.15/17.04 % (1959701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.15/17.04 % (1959701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/17.04 % (1959701)CaDiCaL version: 2.1.3
% 115.15/17.04 % (1959701)Termination reason: Instruction limit
% 115.15/17.04 % (1959701)Termination phase: Saturation
% 115.15/17.04 % (1959701)Time elapsed: 3.992 s
% 115.15/17.04 % (1959701)Peak memory usage: 184 MB
% 115.15/17.04 % (1959701)Instructions burned: 8479 (million)
% 115.15/17.04 % (1959717)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3419340893:i=433:bd=preordered_2930 on theBenchmark for (2930ds/433Mi)
% 115.15/17.04 % (1959715)Instruction limit reached!
% 115.15/17.04 % (1959715)------------------------------
% 115.15/17.04 % (1959715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.15/17.04 % (1959715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/17.04 % (1959715)CaDiCaL version: 2.1.3
% 115.15/17.04 % (1959715)Termination reason: Instruction limit
% 115.15/17.04 % (1959715)Termination phase: Saturation
% 115.15/17.04 % (1959715)Time elapsed: 0.643 s
% 115.15/17.04 % (1959715)Peak memory usage: 104 MB
% 115.15/17.04 % (1959715)Instructions burned: 1098 (million)
% 115.15/17.04 % (1959719)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2128379309:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2928 on theBenchmark for (2928ds/2942Mi)
% 115.15/17.04 % (1959717)Instruction limit reached!
% 115.15/17.04 % (1959717)------------------------------
% 115.15/17.04 % (1959717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.15/17.04 % (1959717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/17.04 % (1959717)CaDiCaL version: 2.1.3
% 115.15/17.04 % (1959717)Termination reason: Instruction limit
% 115.15/17.04 % (1959717)Termination phase: Saturation
% 115.15/17.04 % (1959717)Time elapsed: 0.252 s
% 115.15/17.04 % (1959717)Peak memory usage: 93 MB
% 115.15/17.04 % (1959717)Instructions burned: 433 (million)
% 115.15/17.04 % (1959713)Instruction limit reached!
% 115.15/17.04 % (1959713)------------------------------
% 115.15/17.04 % (1959713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.15/17.04 % (1959713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.15/17.04 % (1959713)CaDiCaL version: 2.1.3
% 115.15/17.04 % (1959713)Termination reason: Instruction limit
% 115.15/17.04 % (1959713)Termination phase: Saturation
% 115.15/17.04 % (1959713)Time elapsed: 1.234 s
% 115.15/17.04 % (1959713)Peak memory usage: 136 MB
% 115.15/17.04 % (1959713)Instructions burned: 2088 (million)
% 115.15/17.04 % (1959721)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3550090621:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2926 on theBenchmark for (2926ds/6922Mi)
% 134.68/19.88 % (1959723)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=2584950409:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2924 on theBenchmark for (2924ds/596Mi)
% 134.68/19.88 % (1959723)Instruction limit reached!
% 134.68/19.88 % (1959723)------------------------------
% 134.68/19.88 % (1959723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.68/19.88 % (1959723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.68/19.88 % (1959723)CaDiCaL version: 2.1.3
% 134.68/19.88 % (1959723)Termination reason: Instruction limit
% 134.68/19.88 % (1959723)Termination phase: Saturation
% 134.68/19.88 % (1959723)Time elapsed: 0.311 s
% 134.68/19.88 % (1959723)Peak memory usage: 99 MB
% 134.68/19.88 % (1959723)Instructions burned: 597 (million)
% 134.68/19.88 % (1959725)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=827757471:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2920 on theBenchmark for (2920ds/4123Mi)
% 134.68/19.88 % (1959697)Instruction limit reached!
% 134.68/19.88 % (1959697)------------------------------
% 134.68/19.88 % (1959697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.68/19.88 % (1959697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.68/19.88 % (1959697)CaDiCaL version: 2.1.3
% 134.68/19.88 % (1959697)Termination reason: Instruction limit
% 134.68/19.88 % (1959697)Termination phase: Saturation
% 134.68/19.88 % (1959697)Time elapsed: 5.772 s
% 134.68/19.88 % (1959697)Peak memory usage: 163 MB
% 134.68/19.88 % (1959697)Instructions burned: 10308 (million)
% 134.68/19.88 % (1959727)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=182222891:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2918 on theBenchmark for (2918ds/16411Mi)
% 134.68/19.88 % (1959719)Instruction limit reached!
% 134.68/19.88 % (1959719)------------------------------
% 134.68/19.88 % (1959719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.68/19.88 % (1959719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.68/19.88 % (1959719)CaDiCaL version: 2.1.3
% 134.68/19.88 % (1959719)Termination reason: Instruction limit
% 134.68/19.88 % (1959719)Termination phase: Saturation
% 134.68/19.88 % (1959719)Time elapsed: 1.790 s
% 134.68/19.88 % (1959719)Peak memory usage: 139 MB
% 134.68/19.88 % (1959719)Instructions burned: 2942 (million)
% 134.68/19.88 % (1959729)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=82822869:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2909 on theBenchmark for (2909ds/1670Mi)
% 134.68/19.88 % (1959729)Instruction limit reached!
% 134.68/19.88 % (1959729)------------------------------
% 134.68/19.88 % (1959729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.68/19.88 % (1959729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.68/19.88 % (1959729)CaDiCaL version: 2.1.3
% 134.68/19.88 % (1959729)Termination reason: Instruction limit
% 134.68/19.88 % (1959729)Termination phase: Saturation
% 134.68/19.88 % (1959729)Time elapsed: 1.045 s
% 134.68/19.88 % (1959729)Peak memory usage: 137 MB
% 134.68/19.88 % (1959729)Instructions burned: 1671 (million)
% 134.68/19.88 % (1959725)Instruction limit reached!
% 134.68/19.88 % (1959725)------------------------------
% 134.68/19.88 % (1959725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.68/19.88 % (1959725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.68/19.88 % (1959725)CaDiCaL version: 2.1.3
% 134.68/19.88 % (1959725)Termination reason: Instruction limit
% 134.68/19.88 % (1959725)Termination phase: Saturation
% 134.68/19.88 % (1959725)Time elapsed: 2.262 s
% 134.68/19.88 % (1959725)Peak memory usage: 161 MB
% 134.68/19.88 % (1959725)Instructions burned: 4124 (million)
% 134.68/19.88 % (1959731)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=176441674:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2897 on theBenchmark for (2897ds/1722Mi)
% 134.68/19.88 % (1959732)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=2344733964:cts=off:cond=on:i=9530:bs=on:fsd=on_2896 on theBenchmark for (2896ds/9530Mi)
% 152.91/22.48 % (1959721)Instruction limit reached!
% 152.91/22.48 % (1959721)------------------------------
% 152.91/22.48 % (1959721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.91/22.48 % (1959721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.91/22.48 % (1959721)CaDiCaL version: 2.1.3
% 152.91/22.48 % (1959721)Termination reason: Instruction limit
% 152.91/22.48 % (1959721)Termination phase: Saturation
% 152.91/22.48 % (1959721)Time elapsed: 3.526 s
% 152.91/22.48 % (1959721)Peak memory usage: 178 MB
% 152.91/22.48 % (1959721)Instructions burned: 6922 (million)
% 152.91/22.48 % (1959735)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3310547550:st=2:i=4495:sd=10:ss=included_2889 on theBenchmark for (2889ds/4495Mi)
% 152.91/22.48 % (1959731)Instruction limit reached!
% 152.91/22.48 % (1959731)------------------------------
% 152.91/22.48 % (1959731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.91/22.48 % (1959731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.91/22.48 % (1959731)CaDiCaL version: 2.1.3
% 152.91/22.48 % (1959731)Termination reason: Instruction limit
% 152.91/22.48 % (1959731)Termination phase: Saturation
% 152.91/22.48 % (1959731)Time elapsed: 1.199 s
% 152.91/22.48 % (1959731)Peak memory usage: 134 MB
% 152.91/22.48 % (1959731)Instructions burned: 1723 (million)
% 152.91/22.48 % (1959737)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=4143830776:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2883 on theBenchmark for (2883ds/4920Mi)
% 152.91/22.48 % (1959735)Instruction limit reached!
% 152.91/22.48 % (1959735)------------------------------
% 152.91/22.48 % (1959735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.91/22.48 % (1959735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.91/22.48 % (1959735)CaDiCaL version: 2.1.3
% 152.91/22.48 % (1959735)Termination reason: Instruction limit
% 152.91/22.48 % (1959735)Termination phase: Saturation
% 152.91/22.48 % (1959735)Time elapsed: 2.817 s
% 152.91/22.48 % (1959735)Peak memory usage: 158 MB
% 152.91/22.48 % (1959735)Instructions burned: 4495 (million)
% 152.91/22.48 % (1959739)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=1398202835:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2859 on theBenchmark for (2859ds/2083Mi)
% 152.91/22.48 % (1959737)Instruction limit reached!
% 152.91/22.48 % (1959737)------------------------------
% 152.91/22.48 % (1959737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.91/22.48 % (1959737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.91/22.48 % (1959737)CaDiCaL version: 2.1.3
% 152.91/22.48 % (1959737)Termination reason: Instruction limit
% 152.91/22.48 % (1959737)Termination phase: Saturation
% 152.91/22.48 % (1959737)Time elapsed: 3.135 s
% 152.91/22.48 % (1959737)Peak memory usage: 147 MB
% 152.91/22.48 % (1959737)Instructions burned: 4920 (million)
% 152.91/22.48 % (1959741)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=1826415500:i=4629:av=off:gsp=on_2851 on theBenchmark for (2851ds/4629Mi)
% 152.91/22.48 % (1959739)Instruction limit reached!
% 152.91/22.48 % (1959739)------------------------------
% 152.91/22.48 % (1959739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.91/22.48 % (1959739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.91/22.48 % (1959739)CaDiCaL version: 2.1.3
% 152.91/22.48 % (1959739)Termination reason: Instruction limit
% 152.91/22.48 % (1959739)Termination phase: Saturation
% 152.91/22.48 % (1959739)Time elapsed: 1.258 s
% 152.91/22.48 % (1959739)Peak memory usage: 136 MB
% 152.91/22.48 % (1959739)Instructions burned: 2084 (million)
% 152.91/22.48 % (1959743)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1352519645:i=1258:av=off_2845 on theBenchmark for (2845ds/1258Mi)
% 152.91/22.48 % (1959743)Instruction limit reached!
% 152.91/22.48 % (1959743)------------------------------
% 152.91/22.48 % (1959743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.91/22.48 % (1959743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.91/22.48 % (1959743)CaDiCaL version: 2.1.3
% 152.91/22.48 % (1959743)Termination reason: Instruction limit
% 152.91/22.48 % (1959743)Termination phase: Saturation
% 186.12/27.11 % (1959743)Time elapsed: 0.678 s
% 186.12/27.11 % (1959743)Peak memory usage: 97 MB
% 186.12/27.11 % (1959743)Instructions burned: 1258 (million)
% 186.12/27.11 % (1959745)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2522959480:i=7343:av=off:ss=included_2837 on theBenchmark for (2837ds/7343Mi)
% 186.12/27.11 % (1959732)Instruction limit reached!
% 186.12/27.11 % (1959732)------------------------------
% 186.12/27.11 % (1959732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.12/27.11 % (1959732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.12/27.11 % (1959732)CaDiCaL version: 2.1.3
% 186.12/27.11 % (1959732)Termination reason: Instruction limit
% 186.12/27.11 % (1959732)Termination phase: Saturation
% 186.12/27.11 % (1959732)Time elapsed: 5.955 s
% 186.12/27.11 % (1959732)Peak memory usage: 162 MB
% 186.12/27.11 % (1959732)Instructions burned: 9530 (million)
% 186.12/27.11 % (1959747)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4099692887:i=1325:sd=2:ss=axioms:sgt=16_2835 on theBenchmark for (2835ds/1325Mi)
% 186.12/27.11 % (1959747)Instruction limit reached!
% 186.12/27.11 % (1959747)------------------------------
% 186.12/27.11 % (1959747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.12/27.11 % (1959747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.12/27.11 % (1959747)CaDiCaL version: 2.1.3
% 186.12/27.11 % (1959747)Termination reason: Instruction limit
% 186.12/27.11 % (1959747)Termination phase: Saturation
% 186.12/27.11 % (1959747)Time elapsed: 0.641 s
% 186.12/27.11 % (1959747)Peak memory usage: 103 MB
% 186.12/27.11 % (1959747)Instructions burned: 1326 (million)
% 186.12/27.11 % (1959749)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=2202897853:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2827 on theBenchmark for (2827ds/2646Mi)
% 186.12/27.11 % (1959741)Instruction limit reached!
% 186.12/27.11 % (1959741)------------------------------
% 186.12/27.11 % (1959741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.12/27.11 % (1959741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.12/27.11 % (1959741)CaDiCaL version: 2.1.3
% 186.12/27.11 % (1959741)Termination reason: Instruction limit
% 186.12/27.11 % (1959741)Termination phase: Saturation
% 186.12/27.11 % (1959741)Time elapsed: 2.816 s
% 186.12/27.11 % (1959741)Peak memory usage: 167 MB
% 186.12/27.11 % (1959741)Instructions burned: 4630 (million)
% 186.12/27.11 % (1959751)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3170323666:i=1489:sd=2:ep=R:ss=axioms_2821 on theBenchmark for (2821ds/1489Mi)
% 186.12/27.11 % (1959727)Instruction limit reached!
% 186.12/27.11 % (1959727)------------------------------
% 186.12/27.11 % (1959727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.12/27.11 % (1959727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.12/27.11 % (1959727)CaDiCaL version: 2.1.3
% 186.12/27.11 % (1959727)Termination reason: Instruction limit
% 186.12/27.11 % (1959727)Termination phase: Saturation
% 186.12/27.11 % (1959727)Time elapsed: 9.864 s
% 186.12/27.11 % (1959727)Peak memory usage: 199 MB
% 186.12/27.11 % (1959727)Instructions burned: 16412 (million)
% 186.12/27.11 % (1959753)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=2820927312:i=1503_2818 on theBenchmark for (2818ds/1503Mi)
% 186.12/27.11 % (1959751)Instruction limit reached!
% 186.12/27.11 % (1959751)------------------------------
% 186.12/27.11 % (1959751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.12/27.11 % (1959751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.12/27.11 % (1959751)CaDiCaL version: 2.1.3
% 186.12/27.11 % (1959751)Termination reason: Instruction limit
% 186.12/27.11 % (1959751)Termination phase: Saturation
% 186.12/27.11 % (1959751)Time elapsed: 0.891 s
% 186.12/27.11 % (1959751)Peak memory usage: 135 MB
% 186.12/27.11 % (1959751)Instructions burned: 1490 (million)
% 186.12/27.11 % (1959755)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=184262964:i=13942:kws=frequency_2811 on theBenchmark for (2811ds/13942Mi)
% 186.12/27.11 % (1959749)Instruction limit reached!
% 186.12/27.11 % (1959749)------------------------------
% 186.12/27.11 % (1959749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.12/27.11 % (1959749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.80 % (1959749)CaDiCaL version: 2.1.3
% 212.73/30.80 % (1959749)Termination reason: Instruction limit
% 212.73/30.80 % (1959749)Termination phase: Saturation
% 212.73/30.80 % (1959749)Time elapsed: 1.710 s
% 212.73/30.80 % (1959749)Peak memory usage: 141 MB
% 212.73/30.80 % (1959749)Instructions burned: 2646 (million)
% 212.73/30.80 % (1959753)Instruction limit reached!
% 212.73/30.80 % (1959753)------------------------------
% 212.73/30.80 % (1959753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.80 % (1959753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.80 % (1959753)CaDiCaL version: 2.1.3
% 212.73/30.80 % (1959753)Termination reason: Instruction limit
% 212.73/30.80 % (1959753)Termination phase: Saturation
% 212.73/30.80 % (1959753)Time elapsed: 0.908 s
% 212.73/30.80 % (1959753)Peak memory usage: 135 MB
% 212.73/30.80 % (1959753)Instructions burned: 1504 (million)
% 212.73/30.80 % (1959757)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=3043654369:i=3604:fsr=off:er=filter_2809 on theBenchmark for (2809ds/3604Mi)
% 212.73/30.80 % (1959758)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=4194249824:i=1876:sd=1:ss=included:sgt=32_2808 on theBenchmark for (2808ds/1876Mi)
% 212.73/30.80 % (1959745)Instruction limit reached!
% 212.73/30.80 % (1959745)------------------------------
% 212.73/30.80 % (1959745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.80 % (1959745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.80 % (1959745)CaDiCaL version: 2.1.3
% 212.73/30.80 % (1959745)Termination reason: Instruction limit
% 212.73/30.80 % (1959745)Termination phase: Saturation
% 212.73/30.80 % (1959745)Time elapsed: 3.918 s
% 212.73/30.80 % (1959745)Peak memory usage: 197 MB
% 212.73/30.80 % (1959745)Instructions burned: 7344 (million)
% 212.73/30.80 % (1959761)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3307684234:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2797 on theBenchmark for (2797ds/1932Mi)
% 212.73/30.80 % (1959758)Instruction limit reached!
% 212.73/30.80 % (1959758)------------------------------
% 212.73/30.80 % (1959758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.80 % (1959758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.80 % (1959758)CaDiCaL version: 2.1.3
% 212.73/30.80 % (1959758)Termination reason: Instruction limit
% 212.73/30.80 % (1959758)Termination phase: Saturation
% 212.73/30.80 % (1959758)Time elapsed: 1.235 s
% 212.73/30.80 % (1959758)Peak memory usage: 137 MB
% 212.73/30.80 % (1959758)Instructions burned: 1876 (million)
% 212.73/30.80 % (1959763)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=395536360:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2794 on theBenchmark for (2794ds/1980Mi)
% 212.73/30.80 % (1959757)Instruction limit reached!
% 212.73/30.80 % (1959757)------------------------------
% 212.73/30.80 % (1959757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.80 % (1959757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.80 % (1959757)CaDiCaL version: 2.1.3
% 212.73/30.80 % (1959757)Termination reason: Instruction limit
% 212.73/30.80 % (1959757)Termination phase: Saturation
% 212.73/30.80 % (1959757)Time elapsed: 2.068 s
% 212.73/30.80 % (1959757)Peak memory usage: 156 MB
% 212.73/30.80 % (1959757)Instructions burned: 3605 (million)
% 212.73/30.80 % (1959765)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=2782166476:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2787 on theBenchmark for (2787ds/3902Mi)
% 212.73/30.80 % (1959761)Instruction limit reached!
% 212.73/30.80 % (1959761)------------------------------
% 212.73/30.80 % (1959761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.80 % (1959761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.80 % (1959761)CaDiCaL version: 2.1.3
% 212.73/30.80 % (1959761)Termination reason: Instruction limit
% 212.73/30.80 % (1959761)Termination phase: Saturation
% 212.73/30.80 % (1959761)Time elapsed: 1.117 s
% 212.73/30.80 % (1959761)Peak memory usage: 142 MB
% 212.73/30.80 % (1959761)Instructions burned: 1933 (million)
% 212.73/30.90 % (1959767)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=3642085345:avsq=on:i=3916:aac=none:amm=off_2784 on theBenchmark for (2784ds/3916Mi)
% 212.73/30.90 % (1959763)Instruction limit reached!
% 212.73/30.90 % (1959763)------------------------------
% 212.73/30.90 % (1959763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959763)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959763)Termination reason: Instruction limit
% 212.73/30.90 % (1959763)Termination phase: Saturation
% 212.73/30.90 % (1959763)Time elapsed: 1.262 s
% 212.73/30.90 % (1959763)Peak memory usage: 137 MB
% 212.73/30.90 % (1959763)Instructions burned: 1981 (million)
% 212.73/30.90 % (1959769)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=802951422:cond=on:i=3940:av=off:er=known_2780 on theBenchmark for (2780ds/3940Mi)
% 212.73/30.90 % (1959765)Instruction limit reached!
% 212.73/30.90 % (1959765)------------------------------
% 212.73/30.90 % (1959765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959765)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959765)Termination reason: Instruction limit
% 212.73/30.90 % (1959765)Termination phase: Saturation
% 212.73/30.90 % (1959765)Time elapsed: 2.201 s
% 212.73/30.90 % (1959765)Peak memory usage: 157 MB
% 212.73/30.90 % (1959765)Instructions burned: 3902 (million)
% 212.73/30.90 % (1959771)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=2955544105:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2763 on theBenchmark for (2763ds/3980Mi)
% 212.73/30.90 % (1959767)Instruction limit reached!
% 212.73/30.90 % (1959767)------------------------------
% 212.73/30.90 % (1959767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959767)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959767)Termination reason: Instruction limit
% 212.73/30.90 % (1959767)Termination phase: Saturation
% 212.73/30.90 % (1959767)Time elapsed: 2.219 s
% 212.73/30.90 % (1959767)Peak memory usage: 110 MB
% 212.73/30.90 % (1959767)Instructions burned: 3917 (million)
% 212.73/30.90 % (1959773)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=3054827535:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2761 on theBenchmark for (2761ds/2087Mi)
% 212.73/30.90 % (1959769)Instruction limit reached!
% 212.73/30.90 % (1959769)------------------------------
% 212.73/30.90 % (1959769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959769)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959769)Termination reason: Instruction limit
% 212.73/30.90 % (1959769)Termination phase: Saturation
% 212.73/30.90 % (1959769)Time elapsed: 2.400 s
% 212.73/30.90 % (1959769)Peak memory usage: 151 MB
% 212.73/30.90 % (1959769)Instructions burned: 3941 (million)
% 212.73/30.90 % (1959775)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=3046456119:cts=off:cond=on:i=4272:bs=on:fsd=on_2755 on theBenchmark for (2755ds/4272Mi)
% 212.73/30.90 % (1959773)Instruction limit reached!
% 212.73/30.90 % (1959773)------------------------------
% 212.73/30.90 % (1959773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959773)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959773)Termination reason: Instruction limit
% 212.73/30.90 % (1959773)Termination phase: Saturation
% 212.73/30.90 % (1959773)Time elapsed: 1.413 s
% 212.73/30.90 % (1959773)Peak memory usage: 139 MB
% 212.73/30.90 % (1959773)Instructions burned: 2088 (million)
% 212.73/30.90 % (1959777)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=890121339:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2745 on theBenchmark for (2745ds/2197Mi)
% 212.73/30.90 % (1959771)Instruction limit reached!
% 212.73/30.90 % (1959771)------------------------------
% 212.73/30.90 % (1959771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959771)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959771)Termination reason: Instruction limit
% 212.73/30.90 % (1959771)Termination phase: Saturation
% 212.73/30.90 % (1959771)Time elapsed: 2.547 s
% 212.73/30.90 % (1959771)Peak memory usage: 157 MB
% 212.73/30.90 % (1959771)Instructions burned: 3981 (million)
% 212.73/30.90 % (1959779)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1570392508:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2737 on theBenchmark for (2737ds/6508Mi)
% 212.73/30.90 % (1959777)Instruction limit reached!
% 212.73/30.90 % (1959777)------------------------------
% 212.73/30.90 % (1959777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959777)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959777)Termination reason: Instruction limit
% 212.73/30.90 % (1959777)Termination phase: Saturation
% 212.73/30.90 % (1959777)Time elapsed: 1.287 s
% 212.73/30.90 % (1959777)Peak memory usage: 141 MB
% 212.73/30.90 % (1959777)Instructions burned: 2198 (million)
% 212.73/30.90 % (1959781)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=1785433642:i=2330:fgj=on:av=off:fsr=off_2731 on theBenchmark for (2731ds/2330Mi)
% 212.73/30.90 % (1959775)Instruction limit reached!
% 212.73/30.90 % (1959775)------------------------------
% 212.73/30.90 % (1959775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959775)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959775)Termination reason: Instruction limit
% 212.73/30.90 % (1959775)Termination phase: Saturation
% 212.73/30.90 % (1959775)Time elapsed: 2.843 s
% 212.73/30.90 % (1959775)Peak memory usage: 149 MB
% 212.73/30.90 % (1959775)Instructions burned: 4273 (million)
% 212.73/30.90 % (1959783)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2853124983:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2725 on theBenchmark for (2725ds/7592Mi)
% 212.73/30.90 % (1959781)Instruction limit reached!
% 212.73/30.90 % (1959781)------------------------------
% 212.73/30.90 % (1959781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959781)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959781)Termination reason: Instruction limit
% 212.73/30.90 % (1959781)Termination phase: Saturation
% 212.73/30.90 % (1959781)Time elapsed: 1.351 s
% 212.73/30.90 % (1959781)Peak memory usage: 137 MB
% 212.73/30.90 % (1959781)Instructions burned: 2330 (million)
% 212.73/30.90 % (1959755)Instruction limit reached!
% 212.73/30.90 % (1959755)------------------------------
% 212.73/30.90 % (1959755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959755)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959755)Termination reason: Instruction limit
% 212.73/30.90 % (1959755)Termination phase: Saturation
% 212.73/30.90 % (1959755)Time elapsed: 9.378 s
% 212.73/30.90 % (1959755)Peak memory usage: 234 MB
% 212.73/30.90 % (1959755)Instructions burned: 13942 (million)
% 212.73/30.90 % (1959785)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=571555719:i=2693:kws=precedence:ins=1:av=off_2716 on theBenchmark for (2716ds/2693Mi)
% 212.73/30.90 % (1959786)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=1508969904:i=28651:sd=4:ss=included:sgt=64_2716 on theBenchmark for (2716ds/28651Mi)
% 212.73/30.90 % (1959785)First to succeed.
% 212.73/30.90 % (1959785)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1959640"
% 212.73/30.90 % (1959779)Instruction limit reached!
% 212.73/30.90 % (1959779)------------------------------
% 212.73/30.90 % (1959779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 212.73/30.90 % (1959779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 212.73/30.90 % (1959779)CaDiCaL version: 2.1.3
% 212.73/30.90 % (1959779)Termination reason: Instruction limit
% 212.73/30.90 % (1959779)Termination phase: Saturation
% 212.73/30.90 % (1959779)Time elapsed: 3.402 s
% 212.73/30.90 % (1959779)Peak memory usage: 131 MB
% 212.73/30.90 % (1959779)Instructions burned: 6510 (million)
% 212.73/30.90 % (1959789)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1044547290:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2701 on theBenchmark for (2701ds/2700Mi)
% 212.73/30.90 % (1959785)Refutation found. Thanks to Tanya!
% 212.73/30.90 % SZS status Unsatisfiable for theBenchmark
% 212.73/30.90 % SZS output start Proof for theBenchmark
% See solution above
% 213.48/31.10 % (1959785)------------------------------
% 213.48/31.10 % (1959785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 213.48/31.10 % (1959785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.48/31.10 % (1959785)CaDiCaL version: 2.1.3
% 213.48/31.10 % (1959785)Termination reason: Refutation
% 213.48/31.10 % (1959785)Time elapsed: 1.297 s
% 213.48/31.10 % (1959785)Peak memory usage: 139 MB
% 213.48/31.10 % (1959785)Instructions burned: 1992 (million)
% 213.48/31.10 % (1959785)------------------------------
% 213.48/31.10 % (1959785)------------------------------
% 213.48/31.10 % (1959640)Success in time 30.067 s
% 213.48/31.10 % Vampire exiting
%------------------------------------------------------------------------------