%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM038-1 : 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 : n026.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:11:38 PM UTC 2026
% Result : Unsatisfiable 132.07s 19.70s
% Output : Refutation 132.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 45
% Syntax : Number of formulae : 224 ( 52 unt; 16 def)
% Number of atoms : 662 ( 73 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 846 ( 408 ~; 434 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 5 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 15 con; 0-3 aty)
% Number of variables : 422 ( 0 sgn 422 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(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(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,complement(X1))
| ~ member(X0,universal_class)
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement2) ).
fof(f26,axiom,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',restriction1) ).
fof(f30,axiom,
! [X0,X1] :
( restrict(X0,singleton(X1),universal_class) != null_class
| ~ member(X1,domain_of(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f31,axiom,
! [X0,X1] :
( ~ member(X0,universal_class)
| restrict(X1,singleton(X0),universal_class) = null_class
| member(X0,domain_of(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f32,plain,
! [X0,X1] :
( ~ member(X0,universal_class)
| null_class = restrict(X1,singleton(X0),universal_class)
| member(X0,domain_of(X1)) ),
inference(reorient_equations,[],[f31]) ).
fof(f37,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(ordered_pair(X0,X1),X2),flip(X3))
| member(ordered_pair(ordered_pair(X1,X0),X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',flip2) ).
fof(f38,axiom,
! [X2,X3,X0,X1] :
( ~ member(ordered_pair(ordered_pair(X0,X1),X2),X3)
| ~ member(ordered_pair(ordered_pair(X1,X0),X2),cross_product(cross_product(universal_class,universal_class),universal_class))
| member(ordered_pair(ordered_pair(X1,X0),X2),flip(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',flip3) ).
fof(f39,axiom,
! [X0] : domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f122,axiom,
! [X0] : union(X0,inverse(X0)) = symmetrization_of(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetrization) ).
fof(f176,negated_conjecture,
restrict(x,universal_class,universal_class) != restrict(x,domain_of(symmetrization_of(x)),domain_of(symmetrization_of(x))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_symmetrization_property9_1) ).
fof(f177,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(f190,plain,
! [X0] : symmetrization_of(X0) = complement(intersection(complement(X0),complement(domain_of(flip(cross_product(X0,universal_class)))))),
inference(definition_unfolding,[],[f122,f26,f39]) ).
fof(f194,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,f177]) ).
fof(f195,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,f177]) ).
fof(f196,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,f177]) ).
fof(f197,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,f177]) ).
fof(f201,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f202,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(f205,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),flip(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))),X3) ),
inference(definition_unfolding,[],[f37,f177,f177,f177,f177]) ).
fof(f206,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X2,X2))),X3)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X2,X2))),cross_product(cross_product(universal_class,universal_class),universal_class))
| 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,f177,f177,f177,f177,f177,f177]) ).
fof(f267,plain,
intersection(x,cross_product(universal_class,universal_class)) != intersection(x,cross_product(domain_of(complement(intersection(complement(x),complement(domain_of(flip(cross_product(x,universal_class))))))),domain_of(complement(intersection(complement(x),complement(domain_of(flip(cross_product(x,universal_class))))))))),
inference(definition_unfolding,[],[f176,f28,f28,f190,f190]) ).
fof(f274,definition,
sF0 = cross_product(universal_class,universal_class),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f275,plain,
cross_product(universal_class,universal_class) = sF0,
inference(reorient_equations,[],[f274]) ).
fof(f276,definition,
sF1 = intersection(x,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f277,plain,
intersection(x,sF0) = sF1,
inference(reorient_equations,[],[f276]) ).
fof(f278,definition,
sF2 = complement(x),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f279,plain,
complement(x) = sF2,
inference(reorient_equations,[],[f278]) ).
fof(f280,definition,
sF3 = cross_product(x,universal_class),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f281,plain,
cross_product(x,universal_class) = sF3,
inference(reorient_equations,[],[f280]) ).
fof(f282,definition,
sF4 = flip(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f283,plain,
flip(sF3) = sF4,
inference(reorient_equations,[],[f282]) ).
fof(f284,definition,
sF5 = domain_of(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f285,plain,
domain_of(sF4) = sF5,
inference(reorient_equations,[],[f284]) ).
fof(f286,definition,
sF6 = complement(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f287,plain,
complement(sF5) = sF6,
inference(reorient_equations,[],[f286]) ).
fof(f288,definition,
sF7 = intersection(sF2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f289,plain,
intersection(sF2,sF6) = sF7,
inference(reorient_equations,[],[f288]) ).
fof(f290,definition,
sF8 = complement(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f291,plain,
complement(sF7) = sF8,
inference(reorient_equations,[],[f290]) ).
fof(f292,definition,
sF9 = domain_of(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f293,plain,
domain_of(sF8) = sF9,
inference(reorient_equations,[],[f292]) ).
fof(f294,definition,
sF10 = cross_product(sF9,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f295,plain,
cross_product(sF9,sF9) = sF10,
inference(reorient_equations,[],[f294]) ).
fof(f296,definition,
sF11 = intersection(x,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f297,plain,
intersection(x,sF10) = sF11,
inference(reorient_equations,[],[f296]) ).
fof(f298,plain,
sF1 != sF11,
inference(definition_folding,[],[f267,f297,f295,f293,f291,f289,f287,f285,f283,f281,f279,f293,f291,f289,f287,f285,f283,f281,f279,f277,f275]) ).
fof(f314,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(sF0,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(backward_demodulation,[],[f206,f275]) ).
fof(f325,plain,
! [X0] :
( member(X0,sF2)
| ~ member(X0,sF7) ),
inference(superposition,[],[f21,f289]) ).
fof(f328,plain,
! [X0] :
( member(X0,sF6)
| ~ member(X0,sF7) ),
inference(superposition,[],[f22,f289]) ).
fof(f331,plain,
! [X0] :
( ~ member(X0,sF2)
| ~ member(X0,x) ),
inference(superposition,[],[f24,f279]) ).
fof(f333,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f22]) ).
fof(f334,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f336,plain,
! [X0] :
( ~ member(X0,sF6)
| ~ member(X0,sF5) ),
inference(superposition,[],[f24,f287]) ).
fof(f338,plain,
! [X0] :
( member(X0,sF8)
| ~ member(X0,universal_class)
| member(X0,sF7) ),
inference(superposition,[],[f25,f291]) ).
fof(f354,plain,
! [X0] :
( ~ member(X0,sF7)
| ~ member(X0,sF5) ),
inference(resolution,[],[f328,f336]) ).
fof(f357,plain,
! [X0] :
( ~ member(X0,sF7)
| ~ member(X0,x) ),
inference(resolution,[],[f325,f331]) ).
fof(f363,plain,
! [X0] :
( member(X0,sF1)
| ~ member(X0,sF0)
| ~ member(X0,x) ),
inference(superposition,[],[f23,f277]) ).
fof(f364,plain,
! [X0] :
( member(X0,sF11)
| ~ member(X0,sF10)
| ~ member(X0,x) ),
inference(superposition,[],[f23,f297]) ).
fof(f366,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF11),sF10)
| ~ member(not_subclass_element(X0,sF11),x)
| subclass(X0,sF11) ),
inference(resolution,[],[f364,f3]) ).
fof(f379,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF1),sF0)
| ~ member(not_subclass_element(X0,sF1),x)
| subclass(X0,sF1) ),
inference(resolution,[],[f363,f3]) ).
fof(f397,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| member(X0,universal_class) ),
inference(superposition,[],[f194,f275]) ).
fof(f403,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X3,X4))
| member(second(X0),X2)
| ~ member(X0,cross_product(X1,X2)) ),
inference(superposition,[],[f195,f197]) ).
fof(f404,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,cross_product(X3,X4))
| member(first(X0),X1)
| ~ member(X0,cross_product(X1,X2)) ),
inference(superposition,[],[f194,f197]) ).
fof(f406,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(first(X0),X1)
| ~ member(X0,sF10) ),
inference(superposition,[],[f404,f295]) ).
fof(f408,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(first(X0),X1)
| ~ member(X0,sF0) ),
inference(superposition,[],[f404,f275]) ).
fof(f410,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X2,X1))
| member(second(X0),X1)
| ~ member(X0,sF10) ),
inference(superposition,[],[f403,f295]) ).
fof(f412,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X2,X1))
| member(second(X0),X1)
| ~ member(X0,sF0) ),
inference(superposition,[],[f403,f275]) ).
fof(f429,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(unordered_pair(X2,X2),universal_class))
| member(X0,null_class)
| ~ member(X0,X1)
| ~ member(X2,universal_class)
| member(X2,domain_of(X1)) ),
inference(superposition,[],[f23,f202]) ).
fof(f436,plain,
! [X2,X3,X0,X1,X4] :
( member(X0,cross_product(X1,X2))
| ~ member(second(X0),X2)
| ~ member(first(X0),X1)
| ~ member(X0,cross_product(X3,X4)) ),
inference(superposition,[],[f196,f197]) ).
fof(f439,plain,
! [X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X1,universal_class)
| ~ member(X0,universal_class) ),
inference(superposition,[],[f196,f275]) ).
fof(f443,plain,
! [X0] :
( ~ member(X0,sF10)
| member(second(X0),sF9)
| ~ member(X0,sF10) ),
inference(superposition,[],[f410,f295]) ).
fof(f446,plain,
! [X0] :
( member(second(X0),sF9)
| ~ member(X0,sF10) ),
inference(duplicate_literal_removal,[],[f443]) ).
fof(f453,plain,
! [X0] :
( ~ member(X0,sF10)
| member(first(X0),sF9)
| ~ member(X0,sF10) ),
inference(superposition,[],[f406,f295]) ).
fof(f456,plain,
! [X0] :
( member(first(X0),sF9)
| ~ member(X0,sF10) ),
inference(duplicate_literal_removal,[],[f453]) ).
fof(f464,plain,
! [X0] :
( ~ member(X0,sF0)
| member(second(X0),universal_class)
| ~ member(X0,sF0) ),
inference(superposition,[],[f412,f275]) ).
fof(f465,plain,
! [X0] :
( member(second(X0),universal_class)
| ~ member(X0,sF0) ),
inference(duplicate_literal_removal,[],[f464]) ).
fof(f474,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ~ member(second(X0),sF9)
| ~ member(first(X0),sF9)
| member(X0,sF10) ),
inference(superposition,[],[f436,f295]) ).
fof(f476,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ~ member(second(X0),universal_class)
| ~ member(first(X0),universal_class)
| member(X0,sF0) ),
inference(superposition,[],[f436,f275]) ).
fof(f491,plain,
! [X0] :
( ~ member(X0,sF0)
| member(first(X0),universal_class)
| ~ member(X0,sF0) ),
inference(superposition,[],[f408,f275]) ).
fof(f492,plain,
! [X0] :
( member(first(X0),universal_class)
| ~ member(X0,sF0) ),
inference(duplicate_literal_removal,[],[f491]) ).
fof(f571,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f572,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f679,plain,
! [X0] :
( ~ member(second(X0),sF9)
| ~ member(X0,sF0)
| ~ member(first(X0),sF9)
| member(X0,sF10) ),
inference(superposition,[],[f474,f275]) ).
fof(f680,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(first(X0),unordered_pair(X2,X2))
| ~ member(X0,X1)
| ~ member(X2,universal_class)
| member(X2,domain_of(X1))
| ~ member(second(X0),universal_class)
| member(X0,null_class)
| ~ member(X0,cross_product(X3,X4)) ),
inference(resolution,[],[f429,f436]) ).
fof(f683,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,[],[f429,f196]) ).
fof(f687,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f334,f3]) ).
fof(f717,plain,
! [X0] :
( member(not_subclass_element(sF1,X0),x)
| subclass(sF1,X0) ),
inference(superposition,[],[f334,f277]) ).
fof(f718,plain,
! [X0] :
( member(not_subclass_element(sF11,X0),x)
| subclass(sF11,X0) ),
inference(superposition,[],[f334,f297]) ).
fof(f725,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f687]) ).
fof(f772,plain,
! [X0] :
( member(not_subclass_element(sF1,X0),sF0)
| subclass(sF1,X0) ),
inference(superposition,[],[f333,f277]) ).
fof(f773,plain,
! [X0] :
( member(not_subclass_element(sF11,X0),sF10)
| subclass(sF11,X0) ),
inference(superposition,[],[f333,f297]) ).
fof(f792,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f725,f70]) ).
fof(f803,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f792,f7]) ).
fof(f804,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f803]) ).
fof(f805,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f804,f725]) ).
fof(f814,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f201,f805]) ).
fof(f815,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f814]) ).
fof(f821,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f815,f68]) ).
fof(f822,plain,
! [X0] : ~ member(X0,null_class),
inference(backward_demodulation,[],[f815,f821]) ).
fof(f833,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(resolution,[],[f822,f683]) ).
fof(f1062,definition,
( spl12_31
<=> ! [X0] : ~ member(X0,universal_class) ),
introduced(definition,[new_symbols(definition,[spl12_31])],[avatar_definition]) ).
fof(f1063,plain,
( ! [X0] : ~ member(X0,universal_class)
| ~ spl12_31 ),
inference(avatar_component_clause,[],[f1062]) ).
fof(f1533,plain,
! [X2,X0,X1] :
( null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),null_class)
| ~ member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),X2)
| ~ member(X1,universal_class)
| member(X1,domain_of(X2)) ),
inference(resolution,[],[f571,f429]) ).
fof(f1551,plain,
! [X2,X0,X1] :
( ~ member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),X2)
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,universal_class)
| member(X1,domain_of(X2)) ),
inference(forward_subsumption_resolution,[],[f1533,f822]) ).
fof(f1603,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))),sF0) ),
inference(resolution,[],[f314,f196]) ).
fof(f1650,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0)))),unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0))))),unordered_pair(unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0)))),unordered_pair(X1,X1))),X2)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),flip(X2))
| ~ member(X1,universal_class)
| ~ member(X0,sF0)
| ~ member(X0,cross_product(X3,X4)) ),
inference(superposition,[],[f1603,f197]) ).
fof(f1775,plain,
! [X0] :
( ~ member(second(X0),universal_class)
| ~ member(X0,sF10)
| ~ member(first(X0),universal_class)
| member(X0,sF0) ),
inference(superposition,[],[f476,f295]) ).
fof(f1944,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ member(unordered_pair(unordered_pair(second(X0),second(X0)),unordered_pair(second(X0),unordered_pair(first(X0),first(X0)))),X2)
| ~ member(X1,universal_class)
| ~ member(X0,sF0)
| ~ member(X0,cross_product(X4,X5))
| ~ member(X1,X3)
| member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),flip(cross_product(X2,X3))) ),
inference(resolution,[],[f1650,f196]) ).
fof(f2166,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(X0,universal_class) ),
inference(superposition,[],[f11,f197]) ).
fof(f2179,plain,
! [X2,X0,X1] :
( member(regular(intersection(X0,cross_product(X1,X2))),universal_class)
| intersection(X0,cross_product(X1,X2)) = null_class ),
inference(resolution,[],[f2166,f571]) ).
fof(f2247,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,universal_class)
| ~ member(X1,sF0)
| ~ member(X1,cross_product(X2,X3))
| ~ member(X0,X4)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),flip(cross_product(sF0,X4)))
| ~ member(first(X1),universal_class)
| ~ member(second(X1),universal_class) ),
inference(resolution,[],[f1944,f439]) ).
fof(f2279,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,universal_class)
| ~ member(X1,sF0)
| ~ member(X1,cross_product(X2,X3))
| ~ member(X0,X4)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),flip(cross_product(sF0,X4)))
| ~ member(second(X1),universal_class) ),
inference(forward_subsumption_resolution,[],[f2247,f492]) ).
fof(f2281,plain,
! [X2,X3,X0,X1,X4] :
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),flip(cross_product(sF0,X4)))
| ~ member(X1,sF0)
| ~ member(X1,cross_product(X2,X3))
| ~ member(X0,X4)
| ~ member(X0,universal_class) ),
inference(forward_subsumption_resolution,[],[f2279,f465]) ).
fof(f2283,plain,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(first(X0),universal_class)
| member(first(X0),domain_of(X1))
| ~ member(second(X0),universal_class)
| member(X0,null_class)
| ~ member(X0,cross_product(X2,X3))
| ~ member(first(X0),universal_class) ),
inference(resolution,[],[f680,f10]) ).
fof(f2287,plain,
! [X2,X3,X0,X1] :
( ~ member(X0,X1)
| ~ member(first(X0),universal_class)
| member(first(X0),domain_of(X1))
| ~ member(second(X0),universal_class)
| member(X0,null_class)
| ~ member(X0,cross_product(X2,X3)) ),
inference(duplicate_literal_removal,[],[f2283]) ).
fof(f2290,plain,
! [X2,X3,X0,X1] :
( member(first(X0),domain_of(X1))
| ~ member(first(X0),universal_class)
| ~ member(X0,X1)
| ~ member(second(X0),universal_class)
| ~ member(X0,cross_product(X2,X3)) ),
inference(forward_subsumption_resolution,[],[f2287,f822]) ).
fof(f2292,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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(X4,X4))),cross_product(sF0,X5))
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| ~ member(X4,X5)
| ~ member(X4,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0) ),
inference(resolution,[],[f2281,f205]) ).
fof(f2311,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| ~ member(X4,universal_class)
| ~ member(X4,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X4,X4))),X5)
| 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(X4,X4))),flip(X5)) ),
inference(resolution,[],[f2292,f314]) ).
fof(f2337,plain,
! [X2,X3,X0,X1,X4,X5] :
( 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(X4,X4))),flip(X5))
| ~ member(X4,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),unordered_pair(X4,X4))),X5)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3)) ),
inference(duplicate_literal_removal,[],[f2311]) ).
fof(f2373,definition,
( spl12_88
<=> universal_class = null_class ),
introduced(definition,[new_symbols(definition,[spl12_88])],[avatar_definition]) ).
fof(f2375,plain,
( universal_class = null_class
| ~ spl12_88 ),
inference(avatar_component_clause,[],[f2373]) ).
fof(f2925,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ member(X0,universal_class)
| member(X0,domain_of(flip(X1)))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X4,X4))),unordered_pair(X0,X0))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),sF0)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3)))),unordered_pair(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),unordered_pair(X2,X2))),X1)
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),cross_product(X5,X6)) ),
inference(resolution,[],[f833,f2337]) ).
fof(f2960,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3)))),unordered_pair(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),unordered_pair(X2,X2))),X1)
| member(X0,domain_of(flip(X1)))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X4,X4))),unordered_pair(X0,X0))
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),sF0)
| ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X3,X3))),cross_product(X5,X6)) ),
inference(duplicate_literal_removal,[],[f2925]) ).
fof(f3046,plain,
( universal_class = null_class
| ~ spl12_31 ),
inference(resolution,[],[f1063,f68]) ).
fof(f3053,plain,
( spl12_88
| ~ spl12_31 ),
inference(avatar_split_clause,[],[f3046,f1062,f2373]) ).
fof(f3143,plain,
! [X2,X0,X1] :
( ~ 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))),sF7)
| ~ member(X2,universal_class)
| member(X2,domain_of(sF8))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X2,X2)) ),
inference(resolution,[],[f338,f833]) ).
fof(f3148,plain,
! [X0,X1] :
( ~ member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),universal_class)
| member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),sF7)
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,universal_class)
| member(X1,domain_of(sF8)) ),
inference(resolution,[],[f338,f1551]) ).
fof(f3150,plain,
! [X0,X1] :
( member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),sF7)
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,universal_class)
| member(X1,domain_of(sF8)) ),
inference(forward_subsumption_resolution,[],[f3148,f2179]) ).
fof(f3151,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF7)
| ~ member(X2,universal_class)
| member(X2,domain_of(sF8))
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X2,X2)) ),
inference(forward_subsumption_resolution,[],[f3143,f11]) ).
fof(f3157,plain,
! [X0,X1] :
( member(regular(intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))),sF7)
| member(X1,sF9)
| null_class = intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,universal_class) ),
inference(forward_demodulation,[],[f3150,f293]) ).
fof(f3158,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF7)
| member(X2,sF9)
| ~ member(X2,universal_class)
| ~ member(X1,universal_class)
| ~ member(X0,unordered_pair(X2,X2)) ),
inference(forward_demodulation,[],[f3151,f293]) ).
fof(f3258,plain,
! [X0,X1] :
( ~ member(regular(intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))),x)
| null_class = intersection(X1,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,sF9) ),
inference(resolution,[],[f3157,f357]) ).
fof(f3321,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),sF5)
| ~ member(X0,universal_class)
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| member(X0,sF9) ),
inference(resolution,[],[f3158,f354]) ).
fof(f3354,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ member(unordered_pair(unordered_pair(X5,X5),unordered_pair(X5,unordered_pair(X4,X4))),cross_product(X6,X7))
| ~ member(X3,universal_class)
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X5,X5))),unordered_pair(X0,X0))
| ~ member(unordered_pair(unordered_pair(X5,X5),unordered_pair(X5,unordered_pair(X4,X4))),sF0)
| ~ member(X0,universal_class)
| member(X0,domain_of(flip(cross_product(X1,X2))))
| ~ member(X3,X2)
| ~ member(unordered_pair(unordered_pair(X5,X5),unordered_pair(X5,unordered_pair(X4,X4))),X1) ),
inference(resolution,[],[f2960,f196]) ).
fof(f3458,plain,
( ! [X0,X1] : member(unordered_pair(X0,X1),null_class)
| ~ spl12_88 ),
inference(backward_demodulation,[],[f11,f2375]) ).
fof(f4197,plain,
( $false
| ~ spl12_88 ),
inference(forward_subsumption_resolution,[],[f3458,f822]) ).
fof(f4198,plain,
~ spl12_88,
inference(avatar_contradiction_clause,[],[f4197]) ).
fof(f6142,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X3,X3))
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X3,universal_class)
| member(X3,domain_of(flip(cross_product(X4,X5))))
| ~ member(X2,X5)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X4) ),
inference(superposition,[],[f3354,f275]) ).
fof(f6143,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),unordered_pair(X3,X3))
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),sF0)
| ~ member(X3,universal_class)
| member(X3,domain_of(flip(cross_product(X4,X5))))
| ~ member(X2,X5)
| ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),X4) ),
inference(duplicate_literal_removal,[],[f6142]) ).
fof(f6147,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF0)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),universal_class)
| member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),domain_of(flip(cross_product(X3,X4))))
| ~ member(X0,X4)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),X3)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),universal_class) ),
inference(resolution,[],[f6143,f10]) ).
fof(f6152,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(X0,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF0)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),universal_class)
| member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),domain_of(flip(cross_product(X3,X4))))
| ~ member(X0,X4)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),X3) ),
inference(duplicate_literal_removal,[],[f6147]) ).
fof(f6154,plain,
! [X2,X3,X0,X1,X4] :
( member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),domain_of(flip(cross_product(X3,X4))))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF0)
| ~ member(X0,universal_class)
| ~ member(X0,X4)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),X3) ),
inference(forward_subsumption_resolution,[],[f6152,f11]) ).
fof(f6190,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),domain_of(flip(sF3)))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0)
| ~ member(X2,universal_class)
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x) ),
inference(superposition,[],[f6154,f281]) ).
fof(f6193,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),domain_of(flip(sF3)))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0)
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x) ),
inference(duplicate_literal_removal,[],[f6190]) ).
fof(f10253,plain,
! [X0] :
( null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,sF9)
| null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class)) ),
inference(resolution,[],[f3258,f572]) ).
fof(f10260,plain,
! [X0] :
( null_class = intersection(x,cross_product(unordered_pair(X0,X0),universal_class))
| ~ member(X0,universal_class)
| member(X0,sF9) ),
inference(duplicate_literal_removal,[],[f10253]) ).
fof(f10795,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(x))
| ~ member(X0,universal_class)
| member(X0,sF9) ),
inference(superposition,[],[f201,f10260]) ).
fof(f10804,plain,
! [X0] :
( ~ member(X0,domain_of(x))
| ~ member(X0,universal_class)
| member(X0,sF9) ),
inference(trivial_inequality_removal,[],[f10795]) ).
fof(f10815,plain,
! [X2,X0,X1] :
( ~ member(first(X0),universal_class)
| member(first(X0),sF9)
| ~ member(first(X0),universal_class)
| ~ member(X0,x)
| ~ member(second(X0),universal_class)
| ~ member(X0,cross_product(X1,X2)) ),
inference(resolution,[],[f10804,f2290]) ).
fof(f10819,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(first(X0),sF9)
| ~ member(X0,x)
| ~ member(second(X0),universal_class)
| ~ member(first(X0),universal_class) ),
inference(duplicate_literal_removal,[],[f10815]) ).
fof(f10857,plain,
! [X0] :
( ~ member(X0,sF0)
| member(first(X0),sF9)
| ~ member(X0,x)
| ~ member(second(X0),universal_class)
| ~ member(first(X0),universal_class) ),
inference(superposition,[],[f10819,f275]) ).
fof(f10858,plain,
! [X0] :
( ~ member(X0,sF0)
| member(first(X0),sF9)
| ~ member(X0,x)
| ~ member(first(X0),universal_class) ),
inference(forward_subsumption_resolution,[],[f10857,f465]) ).
fof(f10862,plain,
! [X0] :
( member(first(X0),sF9)
| ~ member(X0,sF0)
| ~ member(X0,x) ),
inference(forward_subsumption_resolution,[],[f10858,f492]) ).
fof(f11298,plain,
! [X0,X1] :
( ~ member(X0,sF10)
| ~ member(first(X0),universal_class)
| member(X0,sF0)
| ~ member(second(X0),X1)
| ~ subclass(X1,universal_class) ),
inference(resolution,[],[f1775,f1]) ).
fof(f11304,plain,
! [X0,X1] :
( ~ member(second(X0),X1)
| ~ member(first(X0),universal_class)
| member(X0,sF0)
| ~ member(X0,sF10) ),
inference(forward_subsumption_resolution,[],[f11298,f4]) ).
fof(f11325,plain,
! [X0] :
( ~ member(first(X0),universal_class)
| member(X0,sF0)
| ~ member(X0,sF10)
| ~ member(X0,sF10) ),
inference(resolution,[],[f11304,f446]) ).
fof(f11360,plain,
! [X0] :
( ~ member(first(X0),universal_class)
| member(X0,sF0)
| ~ member(X0,sF10) ),
inference(duplicate_literal_removal,[],[f11325]) ).
fof(f11368,plain,
! [X0,X1] :
( member(X0,sF0)
| ~ member(X0,sF10)
| ~ member(first(X0),X1)
| ~ subclass(X1,universal_class) ),
inference(resolution,[],[f11360,f1]) ).
fof(f11370,plain,
! [X0,X1] :
( ~ member(first(X0),X1)
| ~ member(X0,sF10)
| member(X0,sF0) ),
inference(forward_subsumption_resolution,[],[f11368,f4]) ).
fof(f11383,plain,
! [X0] :
( ~ member(X0,sF10)
| member(X0,sF0)
| ~ member(X0,sF10) ),
inference(resolution,[],[f11370,f456]) ).
fof(f11406,plain,
! [X0] :
( member(X0,sF0)
| ~ member(X0,sF10) ),
inference(duplicate_literal_removal,[],[f11383]) ).
fof(f11451,plain,
! [X2,X0,X1] :
( member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),domain_of(sF4))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0)
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x) ),
inference(forward_demodulation,[],[f6193,f283]) ).
fof(f11460,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))),sF0)
| ~ member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),x) ),
inference(forward_demodulation,[],[f11451,f285]) ).
fof(f11464,definition,
( spl12_200
<=> ! [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))),x)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0) ) ),
introduced(definition,[new_symbols(definition,[spl12_200])],[avatar_definition]) ).
fof(f11465,plain,
( ! [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))),x)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X0,X0))),sF0) )
| ~ spl12_200 ),
inference(avatar_component_clause,[],[f11464]) ).
fof(f11466,plain,
( spl12_31
| spl12_200 ),
inference(avatar_split_clause,[],[f11460,f11464,f1062]) ).
fof(f11482,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF1),sF10)
| subclass(X0,sF1)
| ~ member(not_subclass_element(X0,sF1),x) ),
inference(resolution,[],[f379,f11406]) ).
fof(f11612,plain,
( subclass(sF11,sF1)
| ~ member(not_subclass_element(sF11,sF1),x)
| subclass(sF11,sF1) ),
inference(resolution,[],[f11482,f773]) ).
fof(f11623,plain,
( subclass(sF11,sF1)
| ~ member(not_subclass_element(sF11,sF1),x) ),
inference(duplicate_literal_removal,[],[f11612]) ).
fof(f11634,plain,
subclass(sF11,sF1),
inference(forward_subsumption_resolution,[],[f11623,f718]) ).
fof(f11635,plain,
( ~ subclass(sF1,sF11)
| sF1 = sF11 ),
inference(resolution,[],[f11634,f7]) ).
fof(f11636,plain,
~ subclass(sF1,sF11),
inference(forward_subsumption_resolution,[],[f11635,f298]) ).
fof(f12206,definition,
( spl12_246
<=> ! [X2,X1,X3] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF0)
| ~ member(X2,unordered_pair(X3,X3))
| member(X3,sF9)
| ~ member(X3,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),x) ) ),
introduced(definition,[new_symbols(definition,[spl12_246])],[avatar_definition]) ).
fof(f12207,plain,
( ! [X2,X3,X1] :
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF0)
| ~ member(X2,unordered_pair(X3,X3))
| member(X3,sF9)
| ~ member(X3,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),x) )
| ~ spl12_246 ),
inference(avatar_component_clause,[],[f12206]) ).
fof(f72533,plain,
( ! [X2,X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X1,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| member(X0,sF9)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),x)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF0) )
| ~ spl12_200 ),
inference(resolution,[],[f3321,f11465]) ).
fof(f72547,plain,
( ! [X2,X0,X1] :
( ~ member(X0,universal_class)
| ~ member(X2,unordered_pair(X0,X0))
| member(X0,sF9)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),x)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),sF0) )
| ~ spl12_200 ),
inference(forward_subsumption_resolution,[],[f72533,f397]) ).
fof(f72552,plain,
( spl12_246
| ~ spl12_200 ),
inference(avatar_split_clause,[],[f72547,f11464,f12206]) ).
fof(f72576,plain,
( ! [X2,X3,X0,X1] :
( ~ member(second(X0),unordered_pair(X1,X1))
| ~ member(X0,sF0)
| member(X1,sF9)
| ~ member(X1,universal_class)
| ~ member(X0,x)
| ~ member(X0,cross_product(X2,X3)) )
| ~ spl12_246 ),
inference(superposition,[],[f12207,f197]) ).
fof(f72579,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sF0)
| member(second(X0),sF9)
| ~ member(second(X0),universal_class)
| ~ member(X0,x)
| ~ member(X0,cross_product(X1,X2))
| ~ member(second(X0),universal_class) )
| ~ spl12_246 ),
inference(resolution,[],[f72576,f10]) ).
fof(f72583,plain,
( ! [X2,X0,X1] :
( ~ member(X0,sF0)
| member(second(X0),sF9)
| ~ member(second(X0),universal_class)
| ~ member(X0,x)
| ~ member(X0,cross_product(X1,X2)) )
| ~ spl12_246 ),
inference(duplicate_literal_removal,[],[f72579]) ).
fof(f72585,plain,
( ! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| member(second(X0),sF9)
| ~ member(X0,x)
| ~ member(X0,sF0) )
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f72583,f465]) ).
fof(f72618,plain,
( ! [X0] :
( ~ member(X0,sF0)
| member(second(X0),sF9)
| ~ member(X0,x)
| ~ member(X0,sF0) )
| ~ spl12_246 ),
inference(superposition,[],[f72585,f275]) ).
fof(f72622,plain,
( ! [X0] :
( member(second(X0),sF9)
| ~ member(X0,sF0)
| ~ member(X0,x) )
| ~ spl12_246 ),
inference(duplicate_literal_removal,[],[f72618]) ).
fof(f72625,plain,
( ! [X0] :
( ~ member(X0,sF0)
| ~ member(X0,x)
| ~ member(X0,sF0)
| ~ member(first(X0),sF9)
| member(X0,sF10) )
| ~ spl12_246 ),
inference(resolution,[],[f72622,f679]) ).
fof(f72629,plain,
( ! [X0] :
( ~ member(X0,sF0)
| ~ member(X0,x)
| ~ member(first(X0),sF9)
| member(X0,sF10) )
| ~ spl12_246 ),
inference(duplicate_literal_removal,[],[f72625]) ).
fof(f72630,plain,
( ! [X0] :
( member(X0,sF10)
| ~ member(X0,x)
| ~ member(X0,sF0) )
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f72629,f10862]) ).
fof(f72635,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF11),x)
| ~ member(not_subclass_element(X0,sF11),sF0)
| ~ member(not_subclass_element(X0,sF11),x)
| subclass(X0,sF11) )
| ~ spl12_246 ),
inference(resolution,[],[f72630,f366]) ).
fof(f72714,plain,
( ! [X0] :
( ~ member(not_subclass_element(X0,sF11),sF0)
| ~ member(not_subclass_element(X0,sF11),x)
| subclass(X0,sF11) )
| ~ spl12_246 ),
inference(duplicate_literal_removal,[],[f72635]) ).
fof(f72727,plain,
( ~ member(not_subclass_element(sF1,sF11),x)
| subclass(sF1,sF11)
| subclass(sF1,sF11)
| ~ spl12_246 ),
inference(resolution,[],[f72714,f772]) ).
fof(f72746,plain,
( ~ member(not_subclass_element(sF1,sF11),x)
| subclass(sF1,sF11)
| ~ spl12_246 ),
inference(duplicate_literal_removal,[],[f72727]) ).
fof(f72748,plain,
( subclass(sF1,sF11)
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f72746,f717]) ).
fof(f72749,plain,
( $false
| ~ spl12_246 ),
inference(forward_subsumption_resolution,[],[f72748,f11636]) ).
fof(f72750,plain,
~ spl12_246,
inference(avatar_contradiction_clause,[],[f72749]) ).
cnf(s84,plain,
( ~ spl12_31
| spl12_88 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s108,plain,
~ spl12_88,
inference(sat_conversion,[],[f4198]) ).
cnf(s371,plain,
( spl12_31
| spl12_200 ),
inference(sat_conversion,[],[f11466]) ).
cnf(s1607,plain,
( ~ spl12_200
| spl12_246 ),
inference(sat_conversion,[],[f72552]) ).
cnf(s1609,plain,
~ spl12_246,
inference(sat_conversion,[],[f72750]) ).
cnf(s1610,plain,
~ spl12_200,
inference(rat,[],[s1607,s1609]) ).
cnf(s1633,plain,
spl12_31,
inference(rat,[],[s371,s1610]) ).
cnf(s1702,plain,
$false,
inference(rat,[],[s84,s108,s1633]) ).
fof(f72751,plain,
$false,
inference(avatar_sat_refutation,[],[s1702]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM038-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 % Computer : n026.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 27 18:43:11 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 Running first-order theorem proving
% 0.23/0.48 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.49/3.02 % (3136648)Input is clausal, will run a generic CNF schedule.
% 12.49/3.02 % (3136657)lrs+10_1_sil=8000:sp=occurrence:random_seed=3560096859:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.49/3.02 % (3136657)Instruction limit reached!
% 12.49/3.02 % (3136657)------------------------------
% 12.49/3.02 % (3136657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/3.02 % (3136657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/3.02 % (3136657)CaDiCaL version: 2.1.3
% 12.49/3.02 % (3136657)Termination reason: Instruction limit
% 12.49/3.02 % (3136657)Termination phase: Saturation
% 12.49/3.02 % (3136657)Time elapsed: 0.052 s
% 12.49/3.02 % (3136657)Peak memory usage: 89 MB
% 12.49/3.02 % (3136657)Instructions burned: 107 (million)
% 12.49/3.02 % (3136655)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1522317900:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.49/3.02 % (3136654)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=1236384812:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.49/3.02 % (3136659)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1887422576:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.49/3.02 % (3136658)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1492467079:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.49/3.02 % (3136656)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3355771117:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.49/3.02 % (3136660)dis-21_1_sil=8000:lcm=predicate:random_seed=233477144:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 12.49/3.02 % (3136658)Instruction limit reached!
% 12.49/3.02 % (3136658)------------------------------
% 12.49/3.02 % (3136658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/3.02 % (3136658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/3.02 % (3136658)CaDiCaL version: 2.1.3
% 12.49/3.02 % (3136658)Termination reason: Instruction limit
% 12.49/3.02 % (3136658)Termination phase: Saturation
% 12.49/3.02 % (3136658)Time elapsed: 0.112 s
% 12.49/3.02 % (3136658)Peak memory usage: 89 MB
% 12.49/3.02 % (3136658)Instructions burned: 114 (million)
% 12.49/3.02 % (3136662)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=3628273404:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 12.49/3.02 % (3136662)Refutation not found, incomplete strategy
% 12.49/3.02 % (3136662)------------------------------
% 12.49/3.02 % (3136662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/3.02 % (3136662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/3.02 % (3136662)CaDiCaL version: 2.1.3
% 12.49/3.02 % (3136662)Termination reason: Refutation not found, incomplete strategy
% 12.49/3.02 % (3136662)Time elapsed: 0.002 s
% 12.49/3.02 % (3136662)Peak memory usage: 88 MB
% 12.49/3.02 % (3136662)Instructions burned: 2 (million)
% 12.49/3.02 % (3136660)Instruction limit reached!
% 12.49/3.02 % (3136660)------------------------------
% 12.49/3.02 % (3136660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/3.02 % (3136660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/3.02 % (3136660)CaDiCaL version: 2.1.3
% 12.49/3.02 % (3136660)Termination reason: Instruction limit
% 12.49/3.02 % (3136660)Termination phase: Saturation
% 12.49/3.02 % (3136660)Time elapsed: 0.095 s
% 12.49/3.02 % (3136660)Peak memory usage: 89 MB
% 12.49/3.02 % (3136660)Instructions burned: 117 (million)
% 12.49/3.02 % (3136659)Instruction limit reached!
% 12.49/3.02 % (3136659)------------------------------
% 12.49/3.02 % (3136659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.49/3.02 % (3136659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.49/3.02 % (3136659)CaDiCaL version: 2.1.3
% 12.49/3.02 % (3136659)Termination reason: Instruction limit
% 12.49/3.02 % (3136659)Termination phase: Saturation
% 12.49/3.02 % (3136659)Time elapsed: 0.209 s
% 12.49/3.02 % (3136659)Peak memory usage: 90 MB
% 12.49/3.02 % (3136659)Instructions burned: 180 (million)
% 12.49/3.02 % (3136670)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2567306339:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 32.04/5.53 % (3136671)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1581617204:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 32.04/5.53 % (3136672)lrs+10_64_to=lpo:sil=8000:random_seed=3957523747:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 32.04/5.53 % (3136670)Instruction limit reached!
% 32.04/5.53 % (3136670)------------------------------
% 32.04/5.53 % (3136670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.04/5.53 % (3136670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.53 % (3136670)CaDiCaL version: 2.1.3
% 32.04/5.53 % (3136670)Termination reason: Instruction limit
% 32.04/5.53 % (3136670)Termination phase: Saturation
% 32.04/5.53 % (3136670)Time elapsed: 0.096 s
% 32.04/5.53 % (3136670)Peak memory usage: 91 MB
% 32.04/5.53 % (3136670)Instructions burned: 189 (million)
% 32.04/5.53 % (3136672)Instruction limit reached!
% 32.04/5.53 % (3136672)------------------------------
% 32.04/5.53 % (3136672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.04/5.53 % (3136672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.53 % (3136672)CaDiCaL version: 2.1.3
% 32.04/5.53 % (3136672)Termination reason: Instruction limit
% 32.04/5.53 % (3136672)Termination phase: Saturation
% 32.04/5.53 % (3136672)Time elapsed: 0.103 s
% 32.04/5.53 % (3136672)Peak memory usage: 89 MB
% 32.04/5.53 % (3136672)Instructions burned: 126 (million)
% 32.04/5.53 % (3136662)------------------------------
% 32.04/5.53 % (3136662)------------------------------
% 32.04/5.53 % (3136676)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2944994642:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 32.04/5.53 % (3136671)Instruction limit reached!
% 32.04/5.53 % (3136671)------------------------------
% 32.04/5.53 % (3136671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.04/5.53 % (3136671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.53 % (3136671)CaDiCaL version: 2.1.3
% 32.04/5.53 % (3136671)Termination reason: Instruction limit
% 32.04/5.53 % (3136671)Termination phase: Saturation
% 32.04/5.53 % (3136671)Time elapsed: 0.198 s
% 32.04/5.53 % (3136671)Peak memory usage: 89 MB
% 32.04/5.53 % (3136671)Instructions burned: 220 (million)
% 32.04/5.53 % (3136676)Instruction limit reached!
% 32.04/5.53 % (3136676)------------------------------
% 32.04/5.53 % (3136676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.04/5.53 % (3136676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.53 % (3136676)CaDiCaL version: 2.1.3
% 32.04/5.53 % (3136676)Termination reason: Instruction limit
% 32.04/5.53 % (3136676)Termination phase: Saturation
% 32.04/5.53 % (3136676)Time elapsed: 0.108 s
% 32.04/5.53 % (3136676)Peak memory usage: 90 MB
% 32.04/5.53 % (3136676)Instructions burned: 195 (million)
% 32.04/5.53 % (3136678)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2611485215:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 32.04/5.53 % (3136677)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=685698403:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 32.04/5.53 % (3136680)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=1711288422:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 32.04/5.53 % (3136681)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3669510756:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 32.04/5.53 % (3136681)Refutation not found, incomplete strategy
% 32.04/5.53 % (3136681)------------------------------
% 32.04/5.53 % (3136681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.04/5.53 % (3136681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.04/5.53 % (3136681)CaDiCaL version: 2.1.3
% 32.04/5.53 % (3136681)Termination reason: Refutation not found, incomplete strategy
% 32.04/5.53 % (3136681)Time elapsed: 0.006 s
% 32.04/5.53 % (3136681)Peak memory usage: 88 MB
% 32.04/5.53 % (3136681)Instructions burned: 11 (million)
% 32.04/5.53 % (3136677)Instruction limit reached!
% 32.04/5.53 % (3136677)------------------------------
% 43.24/7.08 % (3136677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.24/7.08 % (3136677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.24/7.08 % (3136677)CaDiCaL version: 2.1.3
% 43.24/7.08 % (3136677)Termination reason: Instruction limit
% 43.24/7.08 % (3136677)Termination phase: Saturation
% 43.24/7.08 % (3136677)Time elapsed: 0.170 s
% 43.24/7.08 % (3136677)Peak memory usage: 91 MB
% 43.24/7.08 % (3136677)Instructions burned: 157 (million)
% 43.24/7.08 % (3136680)Instruction limit reached!
% 43.24/7.08 % (3136680)------------------------------
% 43.24/7.08 % (3136680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.24/7.08 % (3136680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.24/7.08 % (3136680)CaDiCaL version: 2.1.3
% 43.24/7.08 % (3136680)Termination reason: Instruction limit
% 43.24/7.08 % (3136680)Termination phase: Saturation
% 43.24/7.08 % (3136680)Time elapsed: 0.110 s
% 43.24/7.08 % (3136680)Peak memory usage: 89 MB
% 43.24/7.08 % (3136680)Instructions burned: 106 (million)
% 43.24/7.08 % (3136681)------------------------------
% 43.24/7.08 % (3136681)------------------------------
% 43.24/7.08 % (3136686)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1793144798:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 43.24/7.08 % (3136687)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2916902341:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 43.24/7.08 % (3136688)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=266254213:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 43.24/7.08 % (3136688)Refutation not found, incomplete strategy
% 43.24/7.08 % (3136688)------------------------------
% 43.24/7.08 % (3136688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.24/7.08 % (3136688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.24/7.08 % (3136688)CaDiCaL version: 2.1.3
% 43.24/7.08 % (3136688)Termination reason: Refutation not found, incomplete strategy
% 43.24/7.08 % (3136688)Time elapsed: 0.002 s
% 43.24/7.08 % (3136688)Peak memory usage: 88 MB
% 43.24/7.08 % (3136688)Instructions burned: 2 (million)
% 43.24/7.08 % (3136686)Instruction limit reached!
% 43.24/7.08 % (3136686)------------------------------
% 43.24/7.08 % (3136686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.24/7.08 % (3136686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.24/7.08 % (3136686)CaDiCaL version: 2.1.3
% 43.24/7.08 % (3136686)Termination reason: Instruction limit
% 43.24/7.08 % (3136686)Termination phase: Saturation
% 43.24/7.08 % (3136686)Time elapsed: 0.262 s
% 43.24/7.08 % (3136686)Peak memory usage: 91 MB
% 43.24/7.08 % (3136686)Instructions burned: 242 (million)
% 43.24/7.08 % (3136688)------------------------------
% 43.24/7.08 % (3136688)------------------------------
% 43.24/7.08 % (3136692)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1695961806:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 43.24/7.08 % (3136693)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3954127454:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 43.24/7.08 % (3136692)Instruction limit reached!
% 43.24/7.08 % (3136692)------------------------------
% 43.24/7.08 % (3136692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.24/7.08 % (3136692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.24/7.08 % (3136692)CaDiCaL version: 2.1.3
% 43.24/7.08 % (3136692)Termination reason: Instruction limit
% 43.24/7.08 % (3136692)Termination phase: Saturation
% 43.24/7.08 % (3136692)Time elapsed: 0.266 s
% 43.24/7.08 % (3136692)Peak memory usage: 94 MB
% 43.24/7.08 % (3136692)Instructions burned: 500 (million)
% 43.24/7.08 % (3136693)Instruction limit reached!
% 43.24/7.08 % (3136693)------------------------------
% 43.24/7.08 % (3136693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.24/7.08 % (3136693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.24/7.08 % (3136693)CaDiCaL version: 2.1.3
% 43.24/7.08 % (3136693)Termination reason: Instruction limit
% 43.24/7.08 % (3136693)Termination phase: Saturation
% 43.24/7.08 % (3136693)Time elapsed: 0.172 s
% 43.24/7.08 % (3136693)Peak memory usage: 89 MB
% 43.24/7.08 % (3136693)Instructions burned: 191 (million)
% 77.53/12.07 % (3136697)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1796759510:cond=on:i=156:bs=on:gtg=exists_all:er=known_2979 on theBenchmark for (2979ds/156Mi)
% 77.53/12.07 % (3136696)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2824431330:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 77.53/12.07 % (3136697)Instruction limit reached!
% 77.53/12.07 % (3136697)------------------------------
% 77.53/12.07 % (3136697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.53/12.07 % (3136697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.53/12.07 % (3136697)CaDiCaL version: 2.1.3
% 77.53/12.07 % (3136697)Termination reason: Instruction limit
% 77.53/12.07 % (3136697)Termination phase: Saturation
% 77.53/12.07 % (3136697)Time elapsed: 0.173 s
% 77.53/12.07 % (3136697)Peak memory usage: 90 MB
% 77.53/12.07 % (3136697)Instructions burned: 156 (million)
% 77.53/12.07 % (3136696)Instruction limit reached!
% 77.53/12.07 % (3136696)------------------------------
% 77.53/12.07 % (3136696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.53/12.07 % (3136696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.53/12.07 % (3136696)CaDiCaL version: 2.1.3
% 77.53/12.07 % (3136696)Termination reason: Instruction limit
% 77.53/12.07 % (3136696)Termination phase: Saturation
% 77.53/12.07 % (3136696)Time elapsed: 0.261 s
% 77.53/12.07 % (3136696)Peak memory usage: 92 MB
% 77.53/12.07 % (3136696)Instructions burned: 265 (million)
% 77.53/12.07 % (3136700)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=265987704:i=3256:kws=precedence:bd=preordered:av=off_2975 on theBenchmark for (2975ds/3256Mi)
% 77.53/12.07 % (3136701)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=364521101:i=537:av=off:ss=included_2974 on theBenchmark for (2974ds/537Mi)
% 77.53/12.07 % (3136701)Instruction limit reached!
% 77.53/12.07 % (3136701)------------------------------
% 77.53/12.07 % (3136701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.53/12.07 % (3136701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.53/12.07 % (3136701)CaDiCaL version: 2.1.3
% 77.53/12.07 % (3136701)Termination reason: Instruction limit
% 77.53/12.07 % (3136701)Termination phase: Saturation
% 77.53/12.07 % (3136701)Time elapsed: 0.429 s
% 77.53/12.07 % (3136701)Peak memory usage: 89 MB
% 77.53/12.07 % (3136701)Instructions burned: 538 (million)
% 77.53/12.07 % (3136704)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2704606099:i=180:bd=preordered:av=off_2968 on theBenchmark for (2968ds/180Mi)
% 77.53/12.07 % (3136704)Instruction limit reached!
% 77.53/12.07 % (3136704)------------------------------
% 77.53/12.07 % (3136704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.53/12.07 % (3136704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.53/12.07 % (3136704)CaDiCaL version: 2.1.3
% 77.53/12.07 % (3136704)Termination reason: Instruction limit
% 77.53/12.07 % (3136704)Termination phase: Saturation
% 77.53/12.07 % (3136704)Time elapsed: 0.174 s
% 77.53/12.07 % (3136704)Peak memory usage: 90 MB
% 77.53/12.07 % (3136704)Instructions burned: 181 (million)
% 77.53/12.07 % (3136706)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=2678953178:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 77.53/12.07 % (3136678)Instruction limit reached!
% 77.53/12.07 % (3136678)------------------------------
% 77.53/12.07 % (3136678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.53/12.07 % (3136678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.53/12.07 % (3136678)CaDiCaL version: 2.1.3
% 77.53/12.07 % (3136678)Termination reason: Instruction limit
% 77.53/12.07 % (3136678)Termination phase: Saturation
% 77.53/12.07 % (3136678)Time elapsed: 3.423 s
% 77.53/12.07 % (3136678)Peak memory usage: 149 MB
% 77.53/12.07 % (3136678)Instructions burned: 3394 (million)
% 77.53/12.07 % (3136710)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=3165370255:i=412:gtgl=4:gtg=exists_all_2956 on theBenchmark for (2956ds/412Mi)
% 77.53/12.07 % (3136687)Instruction limit reached!
% 77.53/12.07 % (3136687)------------------------------
% 77.53/12.07 % (3136687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.03/16.24 % (3136687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.03/16.24 % (3136687)CaDiCaL version: 2.1.3
% 108.03/16.24 % (3136687)Termination reason: Instruction limit
% 108.03/16.24 % (3136687)Termination phase: Saturation
% 108.03/16.24 % (3136687)Time elapsed: 3.218 s
% 108.03/16.24 % (3136687)Peak memory usage: 157 MB
% 108.03/16.24 % (3136687)Instructions burned: 5209 (million)
% 108.03/16.24 % (3136710)Instruction limit reached!
% 108.03/16.24 % (3136710)------------------------------
% 108.03/16.24 % (3136710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.03/16.24 % (3136710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.03/16.24 % (3136710)CaDiCaL version: 2.1.3
% 108.03/16.24 % (3136710)Termination reason: Instruction limit
% 108.03/16.24 % (3136710)Termination phase: Saturation
% 108.03/16.24 % (3136710)Time elapsed: 0.193 s
% 108.03/16.24 % (3136710)Peak memory usage: 90 MB
% 108.03/16.24 % (3136710)Instructions burned: 413 (million)
% 108.03/16.24 % (3136712)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=1769920262:s2pl=no:i=8478:s2at=4:nm=6_2954 on theBenchmark for (2954ds/8478Mi)
% 108.03/16.24 % (3136713)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=1870846911:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2953 on theBenchmark for (2953ds/303Mi)
% 108.03/16.24 % (3136713)Refutation not found, incomplete strategy
% 108.03/16.24 % (3136713)------------------------------
% 108.03/16.24 % (3136713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.03/16.24 % (3136713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.03/16.24 % (3136713)CaDiCaL version: 2.1.3
% 108.03/16.24 % (3136713)Termination reason: Refutation not found, incomplete strategy
% 108.03/16.24 % (3136713)Time elapsed: 0.002 s
% 108.03/16.24 % (3136713)Peak memory usage: 88 MB
% 108.03/16.24 % (3136713)Instructions burned: 1 (million)
% 108.03/16.24 % (3136713)------------------------------
% 108.03/16.24 % (3136713)------------------------------
% 108.03/16.24 % (3136716)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1925996489:st=4:i=720:sd=3:fsr=off:ss=axioms_2949 on theBenchmark for (2949ds/720Mi)
% 108.03/16.24 % (3136716)Instruction limit reached!
% 108.03/16.24 % (3136716)------------------------------
% 108.03/16.24 % (3136716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.03/16.24 % (3136716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.03/16.24 % (3136716)CaDiCaL version: 2.1.3
% 108.03/16.24 % (3136716)Termination reason: Instruction limit
% 108.03/16.24 % (3136716)Termination phase: Saturation
% 108.03/16.24 % (3136716)Time elapsed: 0.403 s
% 108.03/16.24 % (3136716)Peak memory usage: 95 MB
% 108.03/16.24 % (3136716)Instructions burned: 720 (million)
% 108.03/16.24 % (3136700)Instruction limit reached!
% 108.03/16.24 % (3136700)------------------------------
% 108.03/16.24 % (3136700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.03/16.24 % (3136700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.03/16.24 % (3136700)CaDiCaL version: 2.1.3
% 108.03/16.24 % (3136700)Termination reason: Instruction limit
% 108.03/16.24 % (3136700)Termination phase: Saturation
% 108.03/16.24 % (3136700)Time elapsed: 3.141 s
% 108.03/16.24 % (3136700)Peak memory usage: 148 MB
% 108.03/16.24 % (3136700)Instructions burned: 3257 (million)
% 108.03/16.24 % (3136718)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3719377494:i=598:bs=on:bd=preordered:av=off:ss=axioms_2943 on theBenchmark for (2943ds/598Mi)
% 108.03/16.24 % (3136719)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1353114262:i=2989:sd=3:ss=axioms:sgt=60_2942 on theBenchmark for (2942ds/2989Mi)
% 108.03/16.24 % (3136718)Instruction limit reached!
% 108.03/16.24 % (3136718)------------------------------
% 108.03/16.24 % (3136718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 108.03/16.24 % (3136718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.03/16.24 % (3136718)CaDiCaL version: 2.1.3
% 108.03/16.24 % (3136718)Termination reason: Instruction limit
% 108.03/16.24 % (3136718)Termination phase: Saturation
% 108.03/16.24 % (3136718)Time elapsed: 0.312 s
% 108.03/16.24 % (3136718)Peak memory usage: 91 MB
% 108.03/16.24 % (3136718)Instructions burned: 600 (million)
% 132.07/19.69 % (3136722)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=1728311208:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2939 on theBenchmark for (2939ds/1997Mi)
% 132.07/19.69 % (3136722)Instruction limit reached!
% 132.07/19.69 % (3136722)------------------------------
% 132.07/19.69 % (3136722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136722)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136722)Termination reason: Instruction limit
% 132.07/19.69 % (3136722)Termination phase: Saturation
% 132.07/19.69 % (3136722)Time elapsed: 1.286 s
% 132.07/19.69 % (3136722)Peak memory usage: 137 MB
% 132.07/19.69 % (3136722)Instructions burned: 1998 (million)
% 132.07/19.69 % (3136724)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=129048212:i=2088:bd=preordered:av=off_2924 on theBenchmark for (2924ds/2088Mi)
% 132.07/19.69 % (3136719)Instruction limit reached!
% 132.07/19.69 % (3136719)------------------------------
% 132.07/19.69 % (3136719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136719)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136719)Termination reason: Instruction limit
% 132.07/19.69 % (3136719)Termination phase: Saturation
% 132.07/19.69 % (3136719)Time elapsed: 2.709 s
% 132.07/19.69 % (3136719)Peak memory usage: 145 MB
% 132.07/19.69 % (3136719)Instructions burned: 2990 (million)
% 132.07/19.69 % (3136724)Instruction limit reached!
% 132.07/19.69 % (3136724)------------------------------
% 132.07/19.69 % (3136724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136724)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136724)Termination reason: Instruction limit
% 132.07/19.69 % (3136724)Termination phase: Saturation
% 132.07/19.69 % (3136724)Time elapsed: 1.132 s
% 132.07/19.69 % (3136724)Peak memory usage: 138 MB
% 132.07/19.69 % (3136724)Instructions burned: 2088 (million)
% 132.07/19.69 % (3136726)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2862356818:i=1098:nicw=on_2912 on theBenchmark for (2912ds/1098Mi)
% 132.07/19.69 % (3136727)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1315758220:i=433:bd=preordered_2911 on theBenchmark for (2911ds/433Mi)
% 132.07/19.69 % (3136727)Refutation not found, incomplete strategy
% 132.07/19.69 % (3136727)------------------------------
% 132.07/19.69 % (3136727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136727)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136727)Termination reason: Refutation not found, incomplete strategy
% 132.07/19.69 % (3136727)Time elapsed: 0.038 s
% 132.07/19.69 % (3136727)Peak memory usage: 89 MB
% 132.07/19.69 % (3136727)Instructions burned: 21 (million)
% 132.07/19.69 % (3136727)------------------------------
% 132.07/19.69 % (3136727)------------------------------
% 132.07/19.69 % (3136730)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4009200081:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2906 on theBenchmark for (2906ds/2942Mi)
% 132.07/19.69 % (3136726)Instruction limit reached!
% 132.07/19.69 % (3136726)------------------------------
% 132.07/19.69 % (3136726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136726)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136726)Termination reason: Instruction limit
% 132.07/19.69 % (3136726)Termination phase: Saturation
% 132.07/19.69 % (3136726)Time elapsed: 1.077 s
% 132.07/19.69 % (3136726)Peak memory usage: 102 MB
% 132.07/19.69 % (3136726)Instructions burned: 1098 (million)
% 132.07/19.69 % (3136732)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=332188732:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2900 on theBenchmark for (2900ds/6922Mi)
% 132.07/19.69 % (3136730)Instruction limit reached!
% 132.07/19.69 % (3136730)------------------------------
% 132.07/19.69 % (3136730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136730)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136730)Termination reason: Instruction limit
% 132.07/19.69 % (3136730)Termination phase: Saturation
% 132.07/19.69 % (3136730)Time elapsed: 1.615 s
% 132.07/19.69 % (3136730)Peak memory usage: 147 MB
% 132.07/19.69 % (3136730)Instructions burned: 2943 (million)
% 132.07/19.69 % (3136734)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=942733554:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2889 on theBenchmark for (2889ds/596Mi)
% 132.07/19.69 % (3136734)Instruction limit reached!
% 132.07/19.69 % (3136734)------------------------------
% 132.07/19.69 % (3136734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136734)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136734)Termination reason: Instruction limit
% 132.07/19.69 % (3136734)Termination phase: Saturation
% 132.07/19.69 % (3136734)Time elapsed: 0.537 s
% 132.07/19.69 % (3136734)Peak memory usage: 99 MB
% 132.07/19.69 % (3136734)Instructions burned: 596 (million)
% 132.07/19.69 % (3136736)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=322819533:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2881 on theBenchmark for (2881ds/4123Mi)
% 132.07/19.69 % (3136712)Instruction limit reached!
% 132.07/19.69 % (3136712)------------------------------
% 132.07/19.69 % (3136712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136712)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136712)Termination reason: Instruction limit
% 132.07/19.69 % (3136712)Termination phase: Saturation
% 132.07/19.69 % (3136712)Time elapsed: 7.949 s
% 132.07/19.69 % (3136712)Peak memory usage: 160 MB
% 132.07/19.69 % (3136712)Instructions burned: 8478 (million)
% 132.07/19.69 % (3136738)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3929331325:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2872 on theBenchmark for (2872ds/16411Mi)
% 132.07/19.69 % (3136732)Instruction limit reached!
% 132.07/19.69 % (3136732)------------------------------
% 132.07/19.69 % (3136732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136732)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136732)Termination reason: Instruction limit
% 132.07/19.69 % (3136732)Termination phase: Saturation
% 132.07/19.69 % (3136732)Time elapsed: 3.961 s
% 132.07/19.69 % (3136732)Peak memory usage: 178 MB
% 132.07/19.69 % (3136732)Instructions burned: 6923 (million)
% 132.07/19.69 % (3136740)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2819683297:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2858 on theBenchmark for (2858ds/1670Mi)
% 132.07/19.69 % (3136706)Instruction limit reached!
% 132.07/19.69 % (3136706)------------------------------
% 132.07/19.69 % (3136706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136706)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136706)Termination reason: Instruction limit
% 132.07/19.69 % (3136706)Termination phase: Saturation
% 132.07/19.69 % (3136706)Time elapsed: 10.627 s
% 132.07/19.69 % (3136706)Peak memory usage: 165 MB
% 132.07/19.69 % (3136706)Instructions burned: 10307 (million)
% 132.07/19.69 % (3136742)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=2269088571:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2856 on theBenchmark for (2856ds/1722Mi)
% 132.07/19.69 % (3136740)Instruction limit reached!
% 132.07/19.69 % (3136740)------------------------------
% 132.07/19.69 % (3136740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.69 % (3136740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.69 % (3136740)CaDiCaL version: 2.1.3
% 132.07/19.69 % (3136740)Termination reason: Instruction limit
% 132.07/19.69 % (3136740)Termination phase: Saturation
% 132.07/19.69 % (3136740)Time elapsed: 0.915 s
% 132.07/19.69 % (3136740)Peak memory usage: 136 MB
% 132.07/19.70 % (3136740)Instructions burned: 1671 (million)
% 132.07/19.70 % (3136744)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=3614818479:cts=off:cond=on:i=9530:bs=on:fsd=on_2847 on theBenchmark for (2847ds/9530Mi)
% 132.07/19.70 % (3136742)Refutation not found, incomplete strategy
% 132.07/19.70 % (3136742)------------------------------
% 132.07/19.70 % (3136742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.70 % (3136742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.70 % (3136742)CaDiCaL version: 2.1.3
% 132.07/19.70 % (3136742)Termination reason: Refutation not found, incomplete strategy
% 132.07/19.70 % (3136742)Time elapsed: 0.946 s
% 132.07/19.70 % (3136742)Peak memory usage: 129 MB
% 132.07/19.70 % (3136742)Instructions burned: 925 (million)
% 132.07/19.70 % (3136742)------------------------------
% 132.07/19.70 % (3136742)------------------------------
% 132.07/19.70 % (3136746)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2400986964:st=2:i=4495:sd=10:ss=included_2841 on theBenchmark for (2841ds/4495Mi)
% 132.07/19.70 % (3136736)Instruction limit reached!
% 132.07/19.70 % (3136736)------------------------------
% 132.07/19.70 % (3136736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.07/19.70 % (3136736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.07/19.70 % (3136736)CaDiCaL version: 2.1.3
% 132.07/19.70 % (3136736)Termination reason: Instruction limit
% 132.07/19.70 % (3136736)Termination phase: Saturation
% 132.07/19.70 % (3136736)Time elapsed: 4.323 s
% 132.07/19.70 % (3136736)Peak memory usage: 148 MB
% 132.07/19.70 % (3136736)Instructions burned: 4123 (million)
% 132.07/19.70 % (3136750)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=150816561:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2835 on theBenchmark for (2835ds/4920Mi)
% 132.07/19.70 % (3136656)First to succeed.
% 132.07/19.70 % (3136656)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3136648"
% 132.07/19.70 % (3136656)Refutation found. Thanks to Tanya!
% 132.07/19.70 % SZS status Unsatisfiable for theBenchmark
% 132.07/19.70 % SZS output start Proof for theBenchmark
% See solution above
% 132.79/19.84 % (3136656)------------------------------
% 132.79/19.84 % (3136656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.79/19.84 % (3136656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.79/19.84 % (3136656)CaDiCaL version: 2.1.3
% 132.79/19.84 % (3136656)Termination reason: Refutation
% 132.79/19.84 % (3136656)Time elapsed: 18.005 s
% 132.79/19.84 % (3136656)Peak memory usage: 200 MB
% 132.79/19.84 % (3136656)Instructions burned: 18162 (million)
% 132.79/19.84 % (3136656)------------------------------
% 132.79/19.84 % (3136656)------------------------------
% 132.79/19.84 % (3136648)Success in time 18.698 s
% 132.79/19.84 % Vampire exiting
%------------------------------------------------------------------------------