%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET368-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:40:52 PM UTC 2026
% Result : Unsatisfiable 10.52s 2.61s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 41
% Syntax : Number of formulae : 202 ( 63 unt; 15 def)
% Number of atoms : 395 ( 116 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 329 ( 136 ~; 186 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 11 con; 0-3 aty)
% Number of variables : 233 ( 0 sgn 233 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| ~ subclass(X0,X1)
| member(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f6,axiom,
! [X0,X1] :
( X0 != X1
| subclass(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_implies_subclass2) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',cartesian_product1) ).
fof(f17,axiom,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| ordered_pair(first(X0),second(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cartesian_product4) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,complement(X1))
| ~ member(X0,universal_class)
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement2) ).
fof(f28,axiom,
! [X2,X0,X1] : intersection(X0,cross_product(X1,X2)) = restrict(X0,X1,X2),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f36,axiom,
! [X0] : subclass(flip(X0),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',flip1) ).
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/sandbox/benchmark/theBenchmark.p',flip2) ).
fof(f39,axiom,
! [X0] : domain_of(flip(cross_product(X0,universal_class))) = inverse(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inverse) ).
fof(f40,axiom,
! [X0] : domain_of(inverse(X0)) = range_of(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_of) ).
fof(f43,axiom,
! [X0,X1] : range_of(restrict(X0,X1,universal_class)) = image(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',image) ).
fof(f56,axiom,
! [X0] : complement(image(element_relation,complement(X0))) = power_class(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',power_class_definition) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f122,negated_conjecture,
power_class(universal_class) != universal_class,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_power_class_of_universal_class_1) ).
fof(f123,plain,
universal_class != power_class(universal_class),
inference(reorient_equations,[],[f122]) ).
fof(f125,plain,
! [X0] : range_of(X0) = domain_of(domain_of(flip(cross_product(X0,universal_class)))),
inference(definition_unfolding,[],[f40,f39]) ).
fof(f126,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,f125,f28]) ).
fof(f128,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),
inference(definition_unfolding,[],[f13,f12,f12]) ).
fof(f135,plain,
! [X0] : power_class(X0) = complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(X0),universal_class)),universal_class))))),
inference(definition_unfolding,[],[f56,f126]) ).
fof(f137,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X0,X0),unordered_pair(X0,unordered_pair(X1,X1))),cross_product(X2,X3))
| member(X0,X2) ),
inference(definition_unfolding,[],[f14,f128]) ).
fof(f140,plain,
! [X2,X0,X1] :
( ~ member(X0,cross_product(X1,X2))
| unordered_pair(unordered_pair(first(X0),first(X0)),unordered_pair(first(X0),unordered_pair(second(X0),second(X0)))) = X0 ),
inference(definition_unfolding,[],[f17,f128]) ).
fof(f144,plain,
! [X0,X1] :
( null_class != intersection(X0,cross_product(unordered_pair(X1,X1),universal_class))
| ~ member(X1,domain_of(X0)) ),
inference(definition_unfolding,[],[f30,f28,f12]) ).
fof(f148,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,f128,f128,f128,f128]) ).
fof(f186,plain,
universal_class != complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(universal_class),universal_class)),universal_class))))),
inference(definition_unfolding,[],[f123,f135]) ).
fof(f188,plain,
! [X1] : subclass(X1,X1),
inference(equality_resolution,[],[f6]) ).
fof(f191,definition,
sF0 = complement(universal_class),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f192,plain,
complement(universal_class) = sF0,
inference(reorient_equations,[],[f191]) ).
fof(f193,definition,
sF1 = cross_product(sF0,universal_class),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f194,plain,
cross_product(sF0,universal_class) = sF1,
inference(reorient_equations,[],[f193]) ).
fof(f195,definition,
sF2 = intersection(element_relation,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f196,plain,
intersection(element_relation,sF1) = sF2,
inference(reorient_equations,[],[f195]) ).
fof(f197,definition,
sF3 = cross_product(sF2,universal_class),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f198,plain,
cross_product(sF2,universal_class) = sF3,
inference(reorient_equations,[],[f197]) ).
fof(f199,definition,
sF4 = flip(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f200,plain,
flip(sF3) = sF4,
inference(reorient_equations,[],[f199]) ).
fof(f201,definition,
sF5 = domain_of(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f202,plain,
domain_of(sF4) = sF5,
inference(reorient_equations,[],[f201]) ).
fof(f203,definition,
sF6 = domain_of(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f204,plain,
domain_of(sF5) = sF6,
inference(reorient_equations,[],[f203]) ).
fof(f205,definition,
sF7 = complement(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f206,plain,
complement(sF6) = sF7,
inference(reorient_equations,[],[f205]) ).
fof(f207,plain,
universal_class != sF7,
inference(definition_folding,[],[f186,f206,f204,f202,f200,f198,f196,f194,f192]) ).
fof(f212,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF7)
| member(X0,sF6) ),
inference(superposition,[],[f25,f206]) ).
fof(f213,plain,
! [X0] :
( ~ subclass(universal_class,X0)
| universal_class = X0 ),
inference(resolution,[],[f4,f7]) ).
fof(f223,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X1),X2)
| ~ subclass(X0,X2)
| subclass(X0,X1) ),
inference(resolution,[],[f2,f1]) ).
fof(f226,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f22]) ).
fof(f227,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f228,plain,
! [X0,X1] :
( ~ member(not_subclass_element(complement(X0),X1),X0)
| subclass(complement(X0),X1) ),
inference(resolution,[],[f2,f24]) ).
fof(f234,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,complement(X1)),universal_class)
| subclass(X0,complement(X1))
| member(not_subclass_element(X0,complement(X1)),X1) ),
inference(resolution,[],[f3,f25]) ).
fof(f238,plain,
! [X2,X3,X0,X1] :
( ~ subclass(intersection(X2,X1),X3)
| ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,X3) ),
inference(resolution,[],[f23,f1]) ).
fof(f239,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X2)
| ~ member(not_subclass_element(X0,intersection(X1,X2)),X1)
| subclass(X0,intersection(X1,X2)) ),
inference(resolution,[],[f23,f3]) ).
fof(f245,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF7)
| member(not_subclass_element(X0,X1),sF6) ),
inference(resolution,[],[f223,f212]) ).
fof(f257,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF7)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF6) ),
inference(forward_subsumption_resolution,[],[f245,f4]) ).
fof(f266,plain,
! [X0] :
( subclass(X0,sF7)
| member(not_subclass_element(X0,sF7),sF6)
| subclass(X0,sF7) ),
inference(resolution,[],[f257,f3]) ).
fof(f269,plain,
! [X0] :
( member(not_subclass_element(X0,sF7),sF6)
| subclass(X0,sF7) ),
inference(duplicate_literal_removal,[],[f266]) ).
fof(f279,plain,
! [X2,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))),sF4)
| 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))),sF3) ),
inference(superposition,[],[f148,f200]) ).
fof(f290,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f227,f3]) ).
fof(f304,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f290]) ).
fof(f309,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[],[f226,f3]) ).
fof(f315,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(intersection(X0,complement(X1)),X2),X1)
| subclass(intersection(X0,complement(X1)),X2) ),
inference(resolution,[],[f226,f24]) ).
fof(f324,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literal_removal,[],[f309]) ).
fof(f331,plain,
! [X0,X1] :
( subclass(X0,complement(X1))
| member(not_subclass_element(X0,complement(X1)),X1)
| ~ subclass(X0,universal_class)
| subclass(X0,complement(X1)) ),
inference(resolution,[],[f234,f223]) ).
fof(f338,plain,
! [X0,X1] :
( subclass(X0,complement(X1))
| member(not_subclass_element(X0,complement(X1)),X1)
| ~ subclass(X0,universal_class) ),
inference(duplicate_literal_removal,[],[f331]) ).
fof(f340,plain,
! [X0,X1] :
( member(not_subclass_element(X0,complement(X1)),X1)
| subclass(X0,complement(X1)) ),
inference(forward_subsumption_resolution,[],[f338,f4]) ).
fof(f348,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,complement(complement(X1))),X1)
| subclass(X0,complement(complement(X1))) ),
inference(resolution,[],[f340,f24]) ).
fof(f363,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f304,f70]) ).
fof(f364,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f363,f7]) ).
fof(f365,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f364]) ).
fof(f366,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f365,f304]) ).
fof(f373,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1) ),
inference(superposition,[],[f22,f366]) ).
fof(f375,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f144,f366]) ).
fof(f376,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f375]) ).
fof(f383,plain,
subclass(sF2,sF1),
inference(superposition,[],[f324,f196]) ).
fof(f386,plain,
! [X0,X1] :
( member(regular(X0),X1)
| ~ subclass(X0,X1)
| null_class = X0 ),
inference(resolution,[],[f68,f1]) ).
fof(f389,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f413,definition,
( spl8_6
<=> null_class = sF3 ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
fof(f415,plain,
( null_class = sF3
| ~ spl8_6 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f422,definition,
( spl8_8
<=> null_class = sF2 ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
fof(f423,plain,
( null_class != sF2
| spl8_8 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f424,plain,
( null_class = sF2
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f454,definition,
( spl8_15
<=> null_class = sF0 ),
introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition]) ).
fof(f456,plain,
( null_class = sF0
| ~ spl8_15 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f477,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f376,f68]) ).
fof(f485,plain,
! [X0] : ~ member(X0,null_class),
inference(superposition,[],[f376,f477]) ).
fof(f516,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,universal_class) ),
inference(resolution,[],[f238,f4]) ).
fof(f527,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(resolution,[],[f516,f2]) ).
fof(f530,plain,
! [X0,X1] :
( ~ member(not_subclass_element(X0,sF7),X1)
| member(not_subclass_element(X0,sF7),universal_class)
| subclass(X0,sF7) ),
inference(resolution,[],[f516,f269]) ).
fof(f540,plain,
! [X0] :
( member(not_subclass_element(X0,sF7),universal_class)
| subclass(X0,sF7)
| subclass(X0,sF7) ),
inference(resolution,[],[f530,f2]) ).
fof(f552,plain,
! [X0] :
( member(not_subclass_element(X0,sF7),universal_class)
| subclass(X0,sF7) ),
inference(duplicate_literal_removal,[],[f540]) ).
fof(f563,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1)
| subclass(X0,X1) ),
inference(resolution,[],[f527,f2]) ).
fof(f581,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f563]) ).
fof(f584,plain,
! [X0] :
( subclass(complement(universal_class),X0)
| subclass(complement(universal_class),X0) ),
inference(resolution,[],[f581,f228]) ).
fof(f594,plain,
! [X0] : subclass(complement(universal_class),X0),
inference(duplicate_literal_removal,[],[f584]) ).
fof(f596,plain,
! [X0] : subclass(sF0,X0),
inference(forward_demodulation,[],[f594,f192]) ).
fof(f598,plain,
null_class = sF0,
inference(resolution,[],[f596,f365]) ).
fof(f599,plain,
spl8_15,
inference(avatar_split_clause,[],[f598,f454]) ).
fof(f614,plain,
! [X2,X0,X1] :
( ~ subclass(X0,cross_product(X1,X2))
| null_class = X0
| regular(X0) = unordered_pair(unordered_pair(first(regular(X0)),first(regular(X0))),unordered_pair(first(regular(X0)),unordered_pair(second(regular(X0)),second(regular(X0))))) ),
inference(resolution,[],[f386,f140]) ).
fof(f698,plain,
! [X2,X0,X1] :
( regular(intersection(X0,cross_product(X1,X2))) = unordered_pair(unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),first(regular(intersection(X0,cross_product(X1,X2))))),unordered_pair(first(regular(intersection(X0,cross_product(X1,X2)))),unordered_pair(second(regular(intersection(X0,cross_product(X1,X2)))),second(regular(intersection(X0,cross_product(X1,X2)))))))
| intersection(X0,cross_product(X1,X2)) = null_class ),
inference(resolution,[],[f389,f140]) ).
fof(f915,plain,
! [X0] :
( subclass(X0,complement(complement(X0)))
| subclass(X0,complement(complement(X0))) ),
inference(resolution,[],[f348,f2]) ).
fof(f931,plain,
! [X0] : subclass(X0,complement(complement(X0))),
inference(duplicate_literal_removal,[],[f915]) ).
fof(f966,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X1)
| subclass(X0,intersection(X1,X2))
| ~ subclass(X0,X2)
| subclass(X0,intersection(X1,X2)) ),
inference(resolution,[],[f239,f223]) ).
fof(f988,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X1)
| subclass(X0,intersection(X1,X2))
| ~ subclass(X0,X2) ),
inference(duplicate_literal_removal,[],[f966]) ).
fof(f993,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f988,f2]) ).
fof(f1017,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f993]) ).
fof(f1023,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f1017,f7]) ).
fof(f1038,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1023,f304]) ).
fof(f1040,plain,
! [X0] : intersection(X0,X0) = X0,
inference(resolution,[],[f1038,f188]) ).
fof(f1218,definition,
( spl8_24
<=> ! [X0] : subclass(X0,sF7) ),
introduced(definition,[new_symbols(definition,[spl8_24])],[avatar_definition]) ).
fof(f1219,plain,
( ! [X0] : subclass(X0,sF7)
| ~ spl8_24 ),
inference(avatar_component_clause,[],[f1218]) ).
fof(f1251,definition,
( spl8_29
<=> null_class = complement(sF7) ),
introduced(definition,[new_symbols(definition,[spl8_29])],[avatar_definition]) ).
fof(f1252,plain,
( null_class != complement(sF7)
| spl8_29 ),
inference(avatar_component_clause,[],[f1251]) ).
fof(f1253,plain,
( null_class = complement(sF7)
| ~ spl8_29 ),
inference(avatar_component_clause,[],[f1251]) ).
fof(f1538,plain,
! [X2,X3,X0,X1,X4] :
( ~ member(regular(intersection(X0,cross_product(X1,X2))),cross_product(X3,X4))
| member(first(regular(intersection(X0,cross_product(X1,X2)))),X3)
| intersection(X0,cross_product(X1,X2)) = null_class ),
inference(superposition,[],[f137,f698]) ).
fof(f1583,plain,
! [X2,X0,X1] :
( member(first(regular(intersection(X0,cross_product(X1,X2)))),X1)
| intersection(X0,cross_product(X1,X2)) = null_class
| intersection(X0,cross_product(X1,X2)) = null_class ),
inference(resolution,[],[f1538,f389]) ).
fof(f1593,plain,
! [X2,X0,X1] :
( member(first(regular(intersection(X0,cross_product(X1,X2)))),X1)
| intersection(X0,cross_product(X1,X2)) = null_class ),
inference(duplicate_literal_removal,[],[f1583]) ).
fof(f1675,plain,
! [X0] :
( member(first(regular(intersection(X0,sF1))),sF0)
| null_class = intersection(X0,sF1) ),
inference(superposition,[],[f1593,f194]) ).
fof(f1676,plain,
! [X0] :
( member(first(regular(intersection(X0,sF3))),sF2)
| null_class = intersection(X0,sF3) ),
inference(superposition,[],[f1593,f198]) ).
fof(f1680,plain,
( ! [X0] :
( member(first(regular(intersection(X0,sF3))),null_class)
| null_class = intersection(X0,sF3) )
| ~ spl8_8 ),
inference(forward_demodulation,[],[f1676,f424]) ).
fof(f1681,plain,
( ! [X0] :
( member(first(regular(intersection(X0,sF1))),null_class)
| null_class = intersection(X0,sF1) )
| ~ spl8_15 ),
inference(forward_demodulation,[],[f1675,f456]) ).
fof(f1688,plain,
( ! [X0] : null_class = intersection(X0,sF3)
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f1680,f485]) ).
fof(f1689,plain,
( ! [X0] : null_class = intersection(X0,sF1)
| ~ spl8_15 ),
inference(forward_subsumption_resolution,[],[f1681,f485]) ).
fof(f1695,plain,
( null_class = sF3
| ~ spl8_8 ),
inference(superposition,[],[f1040,f1688]) ).
fof(f1714,plain,
( spl8_6
| ~ spl8_8 ),
inference(avatar_split_clause,[],[f1695,f422,f413]) ).
fof(f2104,plain,
sF2 = intersection(sF2,sF1),
inference(resolution,[],[f383,f1038]) ).
fof(f3071,plain,
( ! [X0] :
( member(X0,null_class)
| ~ member(X0,universal_class)
| member(X0,sF7) )
| ~ spl8_29 ),
inference(superposition,[],[f25,f1253]) ).
fof(f3110,plain,
( ! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF7) )
| ~ spl8_29 ),
inference(forward_subsumption_resolution,[],[f3071,f373]) ).
fof(f3122,plain,
( ! [X0] :
( member(not_subclass_element(X0,sF7),sF7)
| subclass(X0,sF7) )
| ~ spl8_29 ),
inference(resolution,[],[f3110,f552]) ).
fof(f3155,plain,
( ! [X0] : subclass(X0,sF7)
| ~ spl8_29 ),
inference(forward_subsumption_resolution,[],[f3122,f3]) ).
fof(f3165,plain,
( spl8_24
| ~ spl8_29 ),
inference(avatar_split_clause,[],[f3155,f1251,f1218]) ).
fof(f3178,plain,
( universal_class = sF7
| ~ spl8_24 ),
inference(resolution,[],[f1219,f213]) ).
fof(f3183,plain,
( $false
| ~ spl8_24 ),
inference(forward_subsumption_resolution,[],[f3178,f207]) ).
fof(f3184,plain,
~ spl8_24,
inference(avatar_contradiction_clause,[],[f3183]) ).
fof(f3847,plain,
! [X2,X0,X1] :
( subclass(intersection(X0,complement(complement(X1))),X2)
| ~ member(not_subclass_element(intersection(X0,complement(complement(X1))),X2),universal_class)
| member(not_subclass_element(intersection(X0,complement(complement(X1))),X2),X1) ),
inference(resolution,[],[f315,f25]) ).
fof(f3876,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,complement(complement(X1))),X2),X1)
| subclass(intersection(X0,complement(complement(X1))),X2) ),
inference(forward_subsumption_resolution,[],[f3847,f581]) ).
fof(f3911,plain,
! [X0,X1] :
( subclass(intersection(X0,complement(complement(X1))),X1)
| subclass(intersection(X0,complement(complement(X1))),X1) ),
inference(resolution,[],[f3876,f3]) ).
fof(f3970,plain,
! [X0,X1] : subclass(intersection(X0,complement(complement(X1))),X1),
inference(duplicate_literal_removal,[],[f3911]) ).
fof(f4062,plain,
! [X0] : subclass(complement(complement(X0)),X0),
inference(superposition,[],[f3970,f1040]) ).
fof(f4074,plain,
! [X0] :
( ~ subclass(X0,complement(complement(X0)))
| complement(complement(X0)) = X0 ),
inference(resolution,[],[f4062,f7]) ).
fof(f4082,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f4074,f931]) ).
fof(f4086,plain,
sF6 = complement(sF7),
inference(superposition,[],[f4082,f206]) ).
fof(f4171,definition,
( spl8_74
<=> null_class = sF6 ),
introduced(definition,[new_symbols(definition,[spl8_74])],[avatar_definition]) ).
fof(f4172,plain,
( null_class != sF6
| spl8_74 ),
inference(avatar_component_clause,[],[f4171]) ).
fof(f6139,plain,
( null_class != sF6
| spl8_29 ),
inference(superposition,[],[f1252,f4086]) ).
fof(f6318,plain,
! [X0] :
( regular(flip(X0)) = unordered_pair(unordered_pair(first(regular(flip(X0))),first(regular(flip(X0)))),unordered_pair(first(regular(flip(X0))),unordered_pair(second(regular(flip(X0))),second(regular(flip(X0))))))
| null_class = flip(X0) ),
inference(resolution,[],[f36,f614]) ).
fof(f6580,plain,
( ~ spl8_74
| spl8_29 ),
inference(avatar_split_clause,[],[f6139,f1251,f4171]) ).
fof(f6595,plain,
! [X2,X0,X1] :
( ~ member(regular(flip(X0)),cross_product(X1,X2))
| member(first(regular(flip(X0))),X1)
| null_class = flip(X0) ),
inference(superposition,[],[f137,f6318]) ).
fof(f6659,plain,
! [X2,X0,X1] :
( member(first(regular(flip(X0))),X1)
| null_class = flip(X0)
| ~ subclass(flip(X0),cross_product(X1,X2))
| null_class = flip(X0) ),
inference(resolution,[],[f6595,f386]) ).
fof(f6666,plain,
! [X2,X0,X1] :
( ~ subclass(flip(X0),cross_product(X1,X2))
| null_class = flip(X0)
| member(first(regular(flip(X0))),X1) ),
inference(duplicate_literal_removal,[],[f6659]) ).
fof(f6800,plain,
! [X0] :
( member(first(regular(flip(X0))),cross_product(universal_class,universal_class))
| null_class = flip(X0) ),
inference(resolution,[],[f6666,f36]) ).
fof(f6817,plain,
! [X0] :
( first(regular(flip(X0))) = unordered_pair(unordered_pair(first(first(regular(flip(X0)))),first(first(regular(flip(X0))))),unordered_pair(first(first(regular(flip(X0)))),unordered_pair(second(first(regular(flip(X0)))),second(first(regular(flip(X0)))))))
| null_class = flip(X0) ),
inference(resolution,[],[f6800,f140]) ).
fof(f6844,plain,
! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(first(regular(flip(X0))),first(regular(flip(X0)))),unordered_pair(first(regular(flip(X0))),unordered_pair(X1,X1))),sF4)
| member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(first(regular(flip(X0)))),second(first(regular(flip(X0))))),unordered_pair(second(first(regular(flip(X0)))),unordered_pair(first(first(regular(flip(X0)))),first(first(regular(flip(X0))))))),unordered_pair(unordered_pair(second(first(regular(flip(X0)))),second(first(regular(flip(X0))))),unordered_pair(second(first(regular(flip(X0)))),unordered_pair(first(first(regular(flip(X0)))),first(first(regular(flip(X0)))))))),unordered_pair(unordered_pair(unordered_pair(second(first(regular(flip(X0)))),second(first(regular(flip(X0))))),unordered_pair(second(first(regular(flip(X0)))),unordered_pair(first(first(regular(flip(X0)))),first(first(regular(flip(X0))))))),unordered_pair(X1,X1))),sF3)
| null_class = flip(X0) ),
inference(superposition,[],[f279,f6817]) ).
fof(f7738,plain,
( null_class = sF2
| ~ spl8_15 ),
inference(forward_demodulation,[],[f2104,f1689]) ).
fof(f7802,plain,
( $false
| spl8_8
| ~ spl8_15 ),
inference(forward_subsumption_resolution,[],[f7738,f423]) ).
fof(f7803,plain,
( spl8_8
| ~ spl8_15 ),
inference(avatar_contradiction_clause,[],[f7802]) ).
fof(f7932,plain,
( sF4 = flip(null_class)
| ~ spl8_6 ),
inference(superposition,[],[f200,f415]) ).
fof(f7946,definition,
( spl8_147
<=> null_class = sF4 ),
introduced(definition,[new_symbols(definition,[spl8_147])],[avatar_definition]) ).
fof(f7947,plain,
( null_class != sF4
| spl8_147 ),
inference(avatar_component_clause,[],[f7946]) ).
fof(f7948,plain,
( null_class = sF4
| ~ spl8_147 ),
inference(avatar_component_clause,[],[f7946]) ).
fof(f8066,plain,
( sF5 = domain_of(null_class)
| ~ spl8_147 ),
inference(superposition,[],[f202,f7948]) ).
fof(f8069,plain,
( null_class = sF5
| ~ spl8_147 ),
inference(forward_demodulation,[],[f8066,f477]) ).
fof(f8071,plain,
( sF6 = domain_of(null_class)
| ~ spl8_147 ),
inference(superposition,[],[f204,f8069]) ).
fof(f8072,plain,
( null_class = sF6
| ~ spl8_147 ),
inference(forward_demodulation,[],[f8071,f477]) ).
fof(f8074,plain,
( $false
| spl8_74
| ~ spl8_147 ),
inference(forward_subsumption_resolution,[],[f8072,f4172]) ).
fof(f8075,plain,
( spl8_74
| ~ spl8_147 ),
inference(avatar_contradiction_clause,[],[f8074]) ).
fof(f8083,plain,
( ! [X0,X1] :
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(second(first(regular(flip(X0)))),second(first(regular(flip(X0))))),unordered_pair(second(first(regular(flip(X0)))),unordered_pair(first(first(regular(flip(X0)))),first(first(regular(flip(X0))))))),unordered_pair(unordered_pair(second(first(regular(flip(X0)))),second(first(regular(flip(X0))))),unordered_pair(second(first(regular(flip(X0)))),unordered_pair(first(first(regular(flip(X0)))),first(first(regular(flip(X0)))))))),unordered_pair(unordered_pair(unordered_pair(second(first(regular(flip(X0)))),second(first(regular(flip(X0))))),unordered_pair(second(first(regular(flip(X0)))),unordered_pair(first(first(regular(flip(X0)))),first(first(regular(flip(X0))))))),unordered_pair(X1,X1))),null_class)
| ~ member(unordered_pair(unordered_pair(first(regular(flip(X0))),first(regular(flip(X0)))),unordered_pair(first(regular(flip(X0))),unordered_pair(X1,X1))),sF4)
| null_class = flip(X0) )
| ~ spl8_6 ),
inference(forward_demodulation,[],[f6844,f415]) ).
fof(f8105,plain,
( ! [X0,X1] :
( ~ member(unordered_pair(unordered_pair(first(regular(flip(X0))),first(regular(flip(X0)))),unordered_pair(first(regular(flip(X0))),unordered_pair(X1,X1))),sF4)
| null_class = flip(X0) )
| ~ spl8_6 ),
inference(forward_subsumption_resolution,[],[f8083,f485]) ).
fof(f8171,plain,
( ! [X0] :
( ~ member(regular(flip(X0)),sF4)
| null_class = flip(X0)
| null_class = flip(X0) )
| ~ spl8_6 ),
inference(superposition,[],[f8105,f6318]) ).
fof(f8172,plain,
( ! [X0] :
( ~ member(regular(flip(X0)),sF4)
| null_class = flip(X0) )
| ~ spl8_6 ),
inference(duplicate_literal_removal,[],[f8171]) ).
fof(f8176,plain,
( ~ member(regular(sF4),sF4)
| null_class = sF4
| ~ spl8_6 ),
inference(superposition,[],[f8172,f7932]) ).
fof(f8180,plain,
( null_class = sF4
| ~ spl8_6 ),
inference(forward_subsumption_resolution,[],[f8176,f68]) ).
fof(f8183,plain,
( $false
| ~ spl8_6
| spl8_147 ),
inference(forward_subsumption_resolution,[],[f8180,f7947]) ).
fof(f8184,plain,
( ~ spl8_6
| spl8_147 ),
inference(avatar_contradiction_clause,[],[f8183]) ).
cnf(s10,plain,
spl8_15,
inference(sat_conversion,[],[f599]) ).
cnf(s17,plain,
( spl8_6
| ~ spl8_8 ),
inference(sat_conversion,[],[f1714]) ).
cnf(s61,plain,
( spl8_24
| ~ spl8_29 ),
inference(sat_conversion,[],[f3165]) ).
cnf(s63,plain,
~ spl8_24,
inference(sat_conversion,[],[f3184]) ).
cnf(s118,plain,
( spl8_29
| ~ spl8_74 ),
inference(sat_conversion,[],[f6580]) ).
cnf(s160,plain,
( spl8_8
| ~ spl8_15 ),
inference(sat_conversion,[],[f7803]) ).
cnf(s185,plain,
( spl8_74
| ~ spl8_147 ),
inference(sat_conversion,[],[f8075]) ).
cnf(s188,plain,
( ~ spl8_6
| spl8_147 ),
inference(sat_conversion,[],[f8184]) ).
cnf(s190,plain,
~ spl8_29,
inference(rat,[],[s61,s63]) ).
cnf(s191,plain,
~ spl8_74,
inference(rat,[],[s118,s190]) ).
cnf(s192,plain,
~ spl8_147,
inference(rat,[],[s185,s191]) ).
cnf(s194,plain,
~ spl8_6,
inference(rat,[],[s188,s192]) ).
cnf(s209,plain,
~ spl8_8,
inference(rat,[],[s17,s194]) ).
cnf(s210,plain,
~ spl8_15,
inference(rat,[],[s160,s209]) ).
cnf(s215,plain,
$false,
inference(rat,[],[s10,s210]) ).
fof(f8185,plain,
$false,
inference(avatar_sat_refutation,[],[s215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET368-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n009.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 01:35:30 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.23/2.41 % (2586783)Input is clausal, will run a generic CNF schedule.
% 11.23/2.41 % (2586792)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=525369358:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.23/2.41 % (2586789)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2333513614:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.23/2.41 % (2586790)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=71965848:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.23/2.41 % (2586788)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=3308241466:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.23/2.41 % (2586791)lrs+10_1_sil=8000:sp=occurrence:random_seed=1162567917:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.23/2.41 % (2586792)Instruction limit reached!
% 11.23/2.41 % (2586792)------------------------------
% 11.23/2.41 % (2586792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.41 % (2586792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.41 % (2586792)CaDiCaL version: 2.1.3
% 11.23/2.41 % (2586792)Termination reason: Instruction limit
% 11.23/2.41 % (2586792)Termination phase: Saturation
% 11.23/2.41 % (2586792)Time elapsed: 0.037 s
% 11.23/2.41 % (2586792)Peak memory usage: 89 MB
% 11.23/2.41 % (2586792)Instructions burned: 117 (million)
% 11.23/2.41 % (2586793)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3003695439:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.23/2.41 % (2586794)dis-21_1_sil=8000:lcm=predicate:random_seed=3603482951:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.23/2.41 % (2586791)Instruction limit reached!
% 11.23/2.41 % (2586791)------------------------------
% 11.23/2.41 % (2586791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.41 % (2586791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.41 % (2586791)CaDiCaL version: 2.1.3
% 11.23/2.41 % (2586791)Termination reason: Instruction limit
% 11.23/2.41 % (2586791)Termination phase: Saturation
% 11.23/2.41 % (2586791)Time elapsed: 0.070 s
% 11.23/2.41 % (2586791)Peak memory usage: 89 MB
% 11.23/2.41 % (2586791)Instructions burned: 107 (million)
% 11.23/2.41 % (2586794)Instruction limit reached!
% 11.23/2.41 % (2586794)------------------------------
% 11.23/2.41 % (2586794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.41 % (2586794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.41 % (2586794)CaDiCaL version: 2.1.3
% 11.23/2.41 % (2586794)Termination reason: Instruction limit
% 11.23/2.41 % (2586794)Termination phase: Saturation
% 11.23/2.41 % (2586794)Time elapsed: 0.063 s
% 11.23/2.41 % (2586794)Peak memory usage: 89 MB
% 11.23/2.41 % (2586794)Instructions burned: 118 (million)
% 11.23/2.41 % (2586800)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=3315793464:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.23/2.41 % (2586800)Refutation not found, incomplete strategy
% 11.23/2.41 % (2586800)------------------------------
% 11.23/2.41 % (2586800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.41 % (2586800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.41 % (2586800)CaDiCaL version: 2.1.3
% 11.23/2.41 % (2586800)Termination reason: Refutation not found, incomplete strategy
% 11.23/2.41 % (2586800)Time elapsed: 0.001 s
% 11.23/2.41 % (2586800)Peak memory usage: 88 MB
% 11.23/2.41 % (2586800)Instructions burned: 1 (million)
% 11.23/2.41 % (2586793)Instruction limit reached!
% 11.23/2.41 % (2586793)------------------------------
% 11.23/2.41 % (2586793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.41 % (2586793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.41 % (2586793)CaDiCaL version: 2.1.3
% 11.23/2.41 % (2586793)Termination reason: Instruction limit
% 11.23/2.41 % (2586793)Termination phase: Saturation
% 11.23/2.41 % (2586793)Time elapsed: 0.134 s
% 11.23/2.41 % (2586793)Peak memory usage: 90 MB
% 11.23/2.41 % (2586793)Instructions burned: 181 (million)
% 11.23/2.41 % (2586803)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3547516076: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.52/2.61 % (2586804)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3427266503:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.52/2.61 % (2586804)Refutation not found, incomplete strategy
% 10.52/2.61 % (2586804)------------------------------
% 10.52/2.61 % (2586804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586804)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586804)Termination reason: Refutation not found, incomplete strategy
% 10.52/2.61 % (2586804)Time elapsed: 0.003 s
% 10.52/2.61 % (2586804)Peak memory usage: 88 MB
% 10.52/2.61 % (2586804)Instructions burned: 3 (million)
% 10.52/2.61 % (2586800)------------------------------
% 10.52/2.61 % (2586800)------------------------------
% 10.52/2.61 % (2586806)lrs+10_64_to=lpo:sil=8000:random_seed=3129313272:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 10.52/2.61 % (2586803)Instruction limit reached!
% 10.52/2.61 % (2586803)------------------------------
% 10.52/2.61 % (2586803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586803)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586803)Termination reason: Instruction limit
% 10.52/2.61 % (2586803)Termination phase: Saturation
% 10.52/2.61 % (2586803)Time elapsed: 0.100 s
% 10.52/2.61 % (2586803)Peak memory usage: 90 MB
% 10.52/2.61 % (2586803)Instructions burned: 190 (million)
% 10.52/2.61 % (2586806)Instruction limit reached!
% 10.52/2.61 % (2586806)------------------------------
% 10.52/2.61 % (2586806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586806)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586806)Termination reason: Instruction limit
% 10.52/2.61 % (2586806)Termination phase: Saturation
% 10.52/2.61 % (2586806)Time elapsed: 0.081 s
% 10.52/2.61 % (2586806)Peak memory usage: 89 MB
% 10.52/2.61 % (2586806)Instructions burned: 126 (million)
% 10.52/2.61 % (2586809)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=321568795:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 10.52/2.61 % (2586804)------------------------------
% 10.52/2.61 % (2586804)------------------------------
% 10.52/2.61 % (2586809)Instruction limit reached!
% 10.52/2.61 % (2586809)------------------------------
% 10.52/2.61 % (2586809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586809)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586809)Termination reason: Instruction limit
% 10.52/2.61 % (2586809)Termination phase: Saturation
% 10.52/2.61 % (2586809)Time elapsed: 0.066 s
% 10.52/2.61 % (2586809)Peak memory usage: 89 MB
% 10.52/2.61 % (2586809)Instructions burned: 194 (million)
% 10.52/2.61 % (2586811)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1269758394:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 10.52/2.61 % (2586812)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2710908221:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 10.52/2.61 % (2586811)Instruction limit reached!
% 10.52/2.61 % (2586811)------------------------------
% 10.52/2.61 % (2586811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586811)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586811)Termination reason: Instruction limit
% 10.52/2.61 % (2586811)Termination phase: Saturation
% 10.52/2.61 % (2586811)Time elapsed: 0.110 s
% 10.52/2.61 % (2586811)Peak memory usage: 91 MB
% 10.52/2.61 % (2586811)Instructions burned: 158 (million)
% 10.52/2.61 % (2586816)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=225979145:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 10.52/2.61 % (2586816)Refutation not found, incomplete strategy
% 10.52/2.61 % (2586816)------------------------------
% 10.52/2.61 % (2586816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586816)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586816)Termination reason: Refutation not found, incomplete strategy
% 10.52/2.61 % (2586816)Time elapsed: 0.003 s
% 10.52/2.61 % (2586816)Peak memory usage: 88 MB
% 10.52/2.61 % (2586816)Instructions burned: 8 (million)
% 10.52/2.61 % (2586815)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=3643307733:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 10.52/2.61 % (2586815)Instruction limit reached!
% 10.52/2.61 % (2586815)------------------------------
% 10.52/2.61 % (2586815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586815)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586815)Termination reason: Instruction limit
% 10.52/2.61 % (2586815)Termination phase: Saturation
% 10.52/2.61 % (2586815)Time elapsed: 0.050 s
% 10.52/2.61 % (2586815)Peak memory usage: 94 MB
% 10.52/2.61 % (2586815)Instructions burned: 107 (million)
% 10.52/2.61 % (2586816)------------------------------
% 10.52/2.61 % (2586816)------------------------------
% 10.52/2.61 % (2586819)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1644564197:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 10.52/2.61 % (2586821)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4170440208:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 10.52/2.61 % (2586822)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2640174994:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 10.52/2.61 % (2586822)Refutation not found, incomplete strategy
% 10.52/2.61 % (2586822)------------------------------
% 10.52/2.61 % (2586822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586822)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586822)Termination reason: Refutation not found, incomplete strategy
% 10.52/2.61 % (2586822)Time elapsed: 0.001 s
% 10.52/2.61 % (2586822)Peak memory usage: 88 MB
% 10.52/2.61 % (2586822)Instructions burned: 1 (million)
% 10.52/2.61 % (2586819)Instruction limit reached!
% 10.52/2.61 % (2586819)------------------------------
% 10.52/2.61 % (2586819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586819)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586819)Termination reason: Instruction limit
% 10.52/2.61 % (2586819)Termination phase: Saturation
% 10.52/2.61 % (2586819)Time elapsed: 0.163 s
% 10.52/2.61 % (2586819)Peak memory usage: 90 MB
% 10.52/2.61 % (2586819)Instructions burned: 243 (million)
% 10.52/2.61 % (2586822)------------------------------
% 10.52/2.61 % (2586822)------------------------------
% 10.52/2.61 % (2586826)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=402859858:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 10.52/2.61 % (2586827)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2612089337:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 10.52/2.61 % (2586827)Instruction limit reached!
% 10.52/2.61 % (2586827)------------------------------
% 10.52/2.61 % (2586827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586827)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586827)Termination reason: Instruction limit
% 10.52/2.61 % (2586827)Termination phase: Saturation
% 10.52/2.61 % (2586827)Time elapsed: 0.111 s
% 10.52/2.61 % (2586827)Peak memory usage: 89 MB
% 10.52/2.61 % (2586827)Instructions burned: 193 (million)
% 10.52/2.61 % (2586788)First to succeed.
% 10.52/2.61 % (2586788)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2586783"
% 10.52/2.61 % (2586826)Instruction limit reached!
% 10.52/2.61 % (2586826)------------------------------
% 10.52/2.61 % (2586826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.52/2.61 % (2586826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.52/2.61 % (2586826)CaDiCaL version: 2.1.3
% 10.52/2.61 % (2586826)Termination reason: Instruction limit
% 10.52/2.61 % (2586826)Termination phase: Saturation
% 10.52/2.61 % (2586826)Time elapsed: 0.291 s
% 10.52/2.61 % (2586826)Peak memory usage: 93 MB
% 10.52/2.61 % (2586826)Instructions burned: 503 (million)
% 10.52/2.61 % (2586830)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3860313466:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 10.52/2.61 % (2586832)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1842666723:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 10.52/2.61 % (2586788)Refutation found. Thanks to Tanya!
% 10.52/2.61 % SZS status Unsatisfiable for theBenchmark
% 10.52/2.61 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/2.81 % (2586788)------------------------------
% 0.16/2.81 % (2586788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/2.81 % (2586788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/2.81 % (2586788)CaDiCaL version: 2.1.3
% 0.16/2.81 % (2586788)Termination reason: Refutation
% 0.16/2.81 % (2586788)Time elapsed: 1.328 s
% 0.16/2.81 % (2586788)Peak memory usage: 137 MB
% 0.16/2.81 % (2586788)Instructions burned: 2024 (million)
% 0.16/2.81 % (2586788)------------------------------
% 0.16/2.81 % (2586788)------------------------------
% 0.16/2.81 % (2586783)Success in time 1.752 s
% 0.16/2.81 % Vampire exiting
%------------------------------------------------------------------------------