%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET508-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 : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:41:04 PM UTC 2026
% Result : Unsatisfiable 4.31s 1.58s
% Output : Refutation 5.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 26
% Syntax : Number of formulae : 155 ( 30 unt; 11 def)
% Number of atoms : 349 ( 85 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 326 ( 132 ~; 185 |; 0 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-3 aty)
% Number of variables : 100 ( 0 sgn 100 !; 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(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
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(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(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,
unordered_pair(x,universal_class) != singleton(x),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_corollary_1_to_singleton_in_unordered_pair_1) ).
fof(f143,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(f185,plain,
unordered_pair(x,universal_class) != unordered_pair(x,x),
inference(definition_unfolding,[],[f122,f12]) ).
fof(f190,definition,
sF0 = unordered_pair(x,universal_class),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f191,plain,
unordered_pair(x,universal_class) = sF0,
inference(reorient_equations,[],[f190]) ).
fof(f192,definition,
sF1 = unordered_pair(x,x),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f193,plain,
unordered_pair(x,x) = sF1,
inference(reorient_equations,[],[f192]) ).
fof(f194,plain,
sF0 != sF1,
inference(definition_folding,[],[f185,f193,f191]) ).
fof(f195,plain,
( member(x,sF1)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f193]) ).
fof(f196,plain,
( member(x,sF0)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f191]) ).
fof(f198,definition,
( spl2_1
<=> member(x,universal_class) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f200,plain,
( ~ member(x,universal_class)
| spl2_1 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f202,definition,
( spl2_2
<=> member(x,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f204,plain,
( member(x,sF0)
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,plain,
( ~ spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f196,f202,f198]) ).
fof(f207,definition,
( spl2_3
<=> member(x,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f209,plain,
( member(x,sF1)
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f210,plain,
( ~ spl2_1
| spl2_3 ),
inference(avatar_split_clause,[],[f195,f207,f198]) ).
fof(f214,definition,
( spl2_4
<=> member(universal_class,universal_class) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f215,plain,
( member(universal_class,universal_class)
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f216,plain,
( ~ member(universal_class,universal_class)
| spl2_4 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f224,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0
| x = X0 ),
inference(superposition,[],[f8,f193]) ).
fof(f225,plain,
! [X0] :
( ~ member(X0,sF0)
| x = X0
| universal_class = X0 ),
inference(superposition,[],[f8,f191]) ).
fof(f226,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0 ),
inference(duplicate_literal_removal,[],[f224]) ).
fof(f228,plain,
! [X0] :
( subclass(sF1,X0)
| x = not_subclass_element(sF1,X0) ),
inference(resolution,[],[f2,f226]) ).
fof(f229,plain,
! [X0] :
( ~ subclass(X0,sF1)
| x = not_subclass_element(sF1,X0)
| sF1 = X0 ),
inference(resolution,[],[f228,f7]) ).
fof(f235,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X2),X1)
| ~ subclass(X0,X1)
| subclass(X0,X2) ),
inference(resolution,[],[f1,f2]) ).
fof(f239,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f21,f2]) ).
fof(f243,plain,
! [X0] :
( subclass(sF0,X0)
| universal_class = not_subclass_element(sF0,X0)
| x = not_subclass_element(sF0,X0) ),
inference(resolution,[],[f225,f2]) ).
fof(f244,plain,
! [X0] :
( ~ subclass(X0,sF0)
| x = not_subclass_element(sF0,X0)
| universal_class = not_subclass_element(sF0,X0)
| sF0 = X0 ),
inference(resolution,[],[f243,f7]) ).
fof(f245,plain,
( universal_class = not_subclass_element(sF0,sF1)
| x = not_subclass_element(sF0,sF1)
| x = not_subclass_element(sF1,sF0)
| sF0 = sF1 ),
inference(resolution,[],[f243,f229]) ).
fof(f246,plain,
( universal_class = not_subclass_element(sF0,sF1)
| x = not_subclass_element(sF0,sF1)
| x = not_subclass_element(sF1,sF0) ),
inference(forward_subsumption_resolution,[],[f245,f194]) ).
fof(f248,definition,
( spl2_6
<=> x = not_subclass_element(sF1,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_6])],[avatar_definition]) ).
fof(f249,plain,
( x != not_subclass_element(sF1,sF0)
| spl2_6 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f250,plain,
( x = not_subclass_element(sF1,sF0)
| ~ spl2_6 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f252,definition,
( spl2_7
<=> x = not_subclass_element(sF0,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_7])],[avatar_definition]) ).
fof(f253,plain,
( x != not_subclass_element(sF0,sF1)
| spl2_7 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( x = not_subclass_element(sF0,sF1)
| ~ spl2_7 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f256,definition,
( spl2_8
<=> universal_class = not_subclass_element(sF0,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_8])],[avatar_definition]) ).
fof(f257,plain,
( universal_class != not_subclass_element(sF0,sF1)
| spl2_8 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( universal_class = not_subclass_element(sF0,sF1)
| ~ spl2_8 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,plain,
( spl2_6
| spl2_7
| spl2_8 ),
inference(avatar_split_clause,[],[f246,f256,f252,f248]) ).
fof(f260,plain,
( ~ member(x,sF0)
| subclass(sF1,sF0)
| ~ spl2_6 ),
inference(superposition,[],[f3,f250]) ).
fof(f261,plain,
( member(x,sF1)
| subclass(sF1,sF0)
| ~ spl2_6 ),
inference(superposition,[],[f2,f250]) ).
fof(f263,definition,
( spl2_9
<=> subclass(sF1,sF0) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f265,plain,
( subclass(sF1,sF0)
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f266,plain,
( spl2_9
| spl2_3
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f261,f248,f207,f263]) ).
fof(f267,plain,
( spl2_9
| ~ spl2_2
| ~ spl2_6 ),
inference(avatar_split_clause,[],[f260,f248,f202,f263]) ).
fof(f268,plain,
( ~ member(x,sF1)
| subclass(sF0,sF1)
| ~ spl2_7 ),
inference(superposition,[],[f3,f254]) ).
fof(f269,plain,
( member(x,sF0)
| subclass(sF0,sF1)
| ~ spl2_7 ),
inference(superposition,[],[f2,f254]) ).
fof(f271,definition,
( spl2_10
<=> subclass(sF0,sF1) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f272,plain,
( ~ subclass(sF0,sF1)
| spl2_10 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( subclass(sF0,sF1)
| ~ spl2_10 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
( spl2_10
| spl2_2
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f269,f252,f202,f271]) ).
fof(f275,plain,
( spl2_10
| ~ spl2_3
| ~ spl2_7 ),
inference(avatar_split_clause,[],[f268,f252,f207,f271]) ).
fof(f287,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f239,f3]) ).
fof(f294,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f287]) ).
fof(f310,plain,
! [X0,X1] :
( regular(unordered_pair(X0,X1)) = X1
| regular(unordered_pair(X0,X1)) = X0
| unordered_pair(X0,X1) = null_class ),
inference(resolution,[],[f68,f8]) ).
fof(f343,plain,
! [X0,X1] :
( X0 != X1
| regular(unordered_pair(X0,X1)) = X0
| unordered_pair(X0,X1) = null_class ),
inference(equality_factoring,[],[f310]) ).
fof(f349,plain,
! [X0] :
( regular(unordered_pair(X0,X0)) = X0
| unordered_pair(X0,X0) = null_class ),
inference(equality_resolution,[],[f343]) ).
fof(f360,plain,
( x = not_subclass_element(sF1,sF0)
| sF0 = sF1
| ~ spl2_10 ),
inference(resolution,[],[f273,f229]) ).
fof(f361,plain,
( ~ subclass(sF1,sF0)
| sF0 = sF1
| ~ spl2_10 ),
inference(resolution,[],[f273,f7]) ).
fof(f362,plain,
( ~ subclass(sF1,sF0)
| ~ spl2_10 ),
inference(forward_subsumption_resolution,[],[f361,f194]) ).
fof(f363,plain,
( sF0 = sF1
| spl2_6
| ~ spl2_10 ),
inference(forward_subsumption_resolution,[],[f360,f249]) ).
fof(f364,plain,
( ~ spl2_9
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f362,f271,f263]) ).
fof(f365,plain,
( $false
| spl2_6
| ~ spl2_10 ),
inference(forward_subsumption_resolution,[],[f363,f194]) ).
fof(f366,plain,
( spl2_6
| ~ spl2_10 ),
inference(avatar_contradiction_clause,[],[f365]) ).
fof(f382,plain,
! [X2,X3,X0,X1] :
( ~ subclass(intersection(X2,X1),X3)
| ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,X3) ),
inference(resolution,[],[f23,f1]) ).
fof(f383,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(f386,plain,
! [X0] :
( null_class = intersection(unordered_pair(X0,X0),X0)
| unordered_pair(X0,X0) = null_class
| unordered_pair(X0,X0) = null_class ),
inference(superposition,[],[f70,f349]) ).
fof(f393,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f294,f70]) ).
fof(f395,plain,
! [X0] :
( null_class = intersection(unordered_pair(X0,X0),X0)
| unordered_pair(X0,X0) = null_class ),
inference(duplicate_literal_removal,[],[f386]) ).
fof(f398,plain,
! [X0] :
( null_class = X0
| ~ subclass(X0,null_class)
| null_class = X0 ),
inference(resolution,[],[f393,f7]) ).
fof(f403,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f398]) ).
fof(f404,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f403,f294]) ).
fof(f425,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f143,f404]) ).
fof(f426,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f425]) ).
fof(f430,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f426,f68]) ).
fof(f436,plain,
! [X0] : ~ member(X0,null_class),
inference(superposition,[],[f426,f430]) ).
fof(f446,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,universal_class) ),
inference(resolution,[],[f382,f4]) ).
fof(f451,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,X1),X2)
| member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(resolution,[],[f446,f2]) ).
fof(f460,plain,
( ! [X0] :
( ~ member(x,X0)
| member(x,universal_class) )
| ~ spl2_2 ),
inference(resolution,[],[f446,f204]) ).
fof(f461,plain,
( ! [X0] : ~ member(x,X0)
| spl2_1
| ~ spl2_2 ),
inference(forward_subsumption_resolution,[],[f460,f200]) ).
fof(f465,plain,
( $false
| spl2_1
| ~ spl2_2 ),
inference(resolution,[],[f461,f204]) ).
fof(f466,plain,
( spl2_1
| ~ spl2_2 ),
inference(avatar_contradiction_clause,[],[f465]) ).
fof(f534,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1)
| subclass(X0,X1) ),
inference(resolution,[],[f451,f2]) ).
fof(f545,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),universal_class)
| subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f534]) ).
fof(f615,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,[],[f383,f235]) ).
fof(f623,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,[],[f615]) ).
fof(f853,plain,
( ! [X0] :
( ~ member(x,X0)
| member(x,universal_class) )
| ~ spl2_3 ),
inference(resolution,[],[f209,f446]) ).
fof(f855,plain,
( ! [X0] : ~ member(x,X0)
| spl2_1
| ~ spl2_3 ),
inference(forward_subsumption_resolution,[],[f853,f200]) ).
fof(f861,plain,
( $false
| spl2_1
| ~ spl2_3 ),
inference(resolution,[],[f855,f209]) ).
fof(f862,plain,
( spl2_1
| ~ spl2_3 ),
inference(avatar_contradiction_clause,[],[f861]) ).
fof(f877,plain,
( x = not_subclass_element(sF0,sF1)
| universal_class = not_subclass_element(sF0,sF1)
| sF0 = sF1
| ~ spl2_9 ),
inference(resolution,[],[f265,f244]) ).
fof(f879,plain,
( universal_class = not_subclass_element(sF0,sF1)
| sF0 = sF1
| spl2_7
| ~ spl2_9 ),
inference(forward_subsumption_resolution,[],[f877,f253]) ).
fof(f880,plain,
( sF0 = sF1
| spl2_7
| spl2_8
| ~ spl2_9 ),
inference(forward_subsumption_resolution,[],[f879,f257]) ).
fof(f881,plain,
( $false
| spl2_7
| spl2_8
| ~ spl2_9 ),
inference(forward_subsumption_resolution,[],[f880,f194]) ).
fof(f882,plain,
( spl2_7
| spl2_8
| ~ spl2_9 ),
inference(avatar_contradiction_clause,[],[f881]) ).
fof(f886,plain,
( member(universal_class,universal_class)
| subclass(sF0,sF1)
| ~ spl2_8 ),
inference(superposition,[],[f545,f258]) ).
fof(f895,plain,
( subclass(sF0,sF1)
| spl2_4
| ~ spl2_8 ),
inference(forward_subsumption_resolution,[],[f886,f216]) ).
fof(f899,plain,
( $false
| spl2_4
| ~ spl2_8
| spl2_10 ),
inference(forward_subsumption_resolution,[],[f895,f272]) ).
fof(f900,plain,
( spl2_4
| ~ spl2_8
| spl2_10 ),
inference(avatar_contradiction_clause,[],[f899]) ).
fof(f1204,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f623,f2]) ).
fof(f1222,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f1204]) ).
fof(f1224,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f1222,f7]) ).
fof(f1239,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f1224,f294]) ).
fof(f1240,plain,
! [X0] : intersection(X0,universal_class) = X0,
inference(resolution,[],[f1239,f4]) ).
fof(f1262,plain,
( null_class = unordered_pair(universal_class,universal_class)
| null_class = unordered_pair(universal_class,universal_class) ),
inference(superposition,[],[f395,f1240]) ).
fof(f1263,plain,
null_class = unordered_pair(universal_class,universal_class),
inference(duplicate_literal_removal,[],[f1262]) ).
fof(f1266,plain,
( member(universal_class,null_class)
| ~ member(universal_class,universal_class) ),
inference(superposition,[],[f9,f1263]) ).
fof(f1282,plain,
~ member(universal_class,universal_class),
inference(forward_subsumption_resolution,[],[f1266,f436]) ).
fof(f1285,plain,
( $false
| ~ spl2_4 ),
inference(forward_subsumption_resolution,[],[f1282,f215]) ).
fof(f1286,plain,
~ spl2_4,
inference(avatar_contradiction_clause,[],[f1285]) ).
cnf(s1,plain,
( ~ spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f205]) ).
cnf(s2,plain,
( ~ spl2_1
| spl2_3 ),
inference(sat_conversion,[],[f210]) ).
cnf(s4,plain,
( spl2_6
| spl2_7
| spl2_8 ),
inference(sat_conversion,[],[f259]) ).
cnf(s5,plain,
( spl2_3
| ~ spl2_6
| spl2_9 ),
inference(sat_conversion,[],[f266]) ).
cnf(s6,plain,
( ~ spl2_2
| ~ spl2_6
| spl2_9 ),
inference(sat_conversion,[],[f267]) ).
cnf(s7,plain,
( spl2_2
| ~ spl2_7
| spl2_10 ),
inference(sat_conversion,[],[f274]) ).
cnf(s8,plain,
( ~ spl2_3
| ~ spl2_7
| spl2_10 ),
inference(sat_conversion,[],[f275]) ).
cnf(s12,plain,
( ~ spl2_9
| ~ spl2_10 ),
inference(sat_conversion,[],[f364]) ).
cnf(s13,plain,
( spl2_6
| ~ spl2_10 ),
inference(sat_conversion,[],[f366]) ).
cnf(s16,plain,
( spl2_1
| ~ spl2_2 ),
inference(sat_conversion,[],[f466]) ).
cnf(s34,plain,
( spl2_1
| ~ spl2_3 ),
inference(sat_conversion,[],[f862]) ).
cnf(s38,plain,
( spl2_7
| spl2_8
| ~ spl2_9 ),
inference(sat_conversion,[],[f882]) ).
cnf(s40,plain,
( spl2_4
| ~ spl2_8
| spl2_10 ),
inference(sat_conversion,[],[f900]) ).
cnf(s50,plain,
~ spl2_4,
inference(sat_conversion,[],[f1286]) ).
cnf(s51,plain,
( ~ spl2_8
| spl2_10 ),
inference(rat,[],[s40,s50]) ).
cnf(s53,plain,
( spl2_6
| spl2_2 ),
inference(rat,[],[s4,s7,s51,s13]) ).
cnf(s54,plain,
spl2_1,
inference(rat,[],[s38,s7,s51,s12,s5,s53,s16,s34]) ).
cnf(s55,plain,
spl2_3,
inference(rat,[],[s2,s54]) ).
cnf(s56,plain,
spl2_2,
inference(rat,[],[s1,s54]) ).
cnf(s59,plain,
spl2_6,
inference(rat,[],[s4,s8,s51,s13,s55]) ).
cnf(s60,plain,
spl2_9,
inference(rat,[],[s6,s56,s59]) ).
cnf(s61,plain,
~ spl2_10,
inference(rat,[],[s12,s60]) ).
cnf(s62,plain,
~ spl2_8,
inference(rat,[],[s51,s61]) ).
cnf(s64,plain,
~ spl2_7,
inference(rat,[],[s8,s55,s61]) ).
cnf(s65,plain,
$false,
inference(rat,[],[s38,s60,s62,s64]) ).
fof(f1287,plain,
$false,
inference(avatar_sat_refutation,[],[s65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET508-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.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 28 02:02:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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
% 4.31/1.58 % (3960168)Input is clausal, will run a generic CNF schedule.
% 4.31/1.58 % (3960173)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=1034222762:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.31/1.58 % (3960178)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1031522982:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.31/1.58 % (3960174)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1600469074:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.31/1.58 % (3960176)lrs+10_1_sil=8000:sp=occurrence:random_seed=770556937:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.31/1.58 % (3960177)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2765382389:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.31/1.58 % (3960175)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2155058296:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.31/1.58 % (3960179)dis-21_1_sil=8000:lcm=predicate:random_seed=4249458951: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)
% 4.31/1.58 % (3960176)Refutation not found, incomplete strategy
% 4.31/1.58 % (3960176)------------------------------
% 4.31/1.58 % (3960176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960176)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960176)Termination reason: Refutation not found, incomplete strategy
% 4.31/1.58 % (3960176)Time elapsed: 0.002 s
% 4.31/1.58 % (3960176)Peak memory usage: 88 MB
% 4.31/1.58 % (3960176)Instructions burned: 1 (million)
% 4.31/1.58 % (3960177)Instruction limit reached!
% 4.31/1.58 % (3960177)------------------------------
% 4.31/1.58 % (3960177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960177)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960177)Termination reason: Instruction limit
% 4.31/1.58 % (3960177)Termination phase: Saturation
% 4.31/1.58 % (3960177)Time elapsed: 0.065 s
% 4.31/1.58 % (3960177)Peak memory usage: 88 MB
% 4.31/1.58 % (3960177)Instructions burned: 114 (million)
% 4.31/1.58 % (3960179)Instruction limit reached!
% 4.31/1.58 % (3960179)------------------------------
% 4.31/1.58 % (3960179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960179)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960179)Termination reason: Instruction limit
% 4.31/1.58 % (3960179)Termination phase: Saturation
% 4.31/1.58 % (3960179)Time elapsed: 0.071 s
% 4.31/1.58 % (3960179)Peak memory usage: 89 MB
% 4.31/1.58 % (3960179)Instructions burned: 117 (million)
% 4.31/1.58 % (3960178)Instruction limit reached!
% 4.31/1.58 % (3960178)------------------------------
% 4.31/1.58 % (3960178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960178)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960178)Termination reason: Instruction limit
% 4.31/1.58 % (3960178)Termination phase: Saturation
% 4.31/1.58 % (3960178)Time elapsed: 0.134 s
% 4.31/1.58 % (3960178)Peak memory usage: 90 MB
% 4.31/1.58 % (3960178)Instructions burned: 181 (million)
% 4.31/1.58 % (3960187)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=3538606659:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.31/1.58 % (3960188)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=12266488: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)
% 4.31/1.58 % (3960187)Refutation not found, incomplete strategy
% 4.31/1.58 % (3960187)------------------------------
% 4.31/1.58 % (3960187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960187)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960187)Termination reason: Refutation not found, incomplete strategy
% 4.31/1.58 % (3960187)Time elapsed: 0.003 s
% 4.31/1.58 % (3960187)Peak memory usage: 88 MB
% 4.31/1.58 % (3960187)Instructions burned: 3 (million)
% 4.31/1.58 % (3960176)------------------------------
% 4.31/1.58 % (3960176)------------------------------
% 4.31/1.58 % (3960189)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3100718918:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 4.31/1.58 % (3960189)Refutation not found, incomplete strategy
% 4.31/1.58 % (3960189)------------------------------
% 4.31/1.58 % (3960189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960189)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960189)Termination reason: Refutation not found, incomplete strategy
% 4.31/1.58 % (3960189)Time elapsed: 0.003 s
% 4.31/1.58 % (3960189)Peak memory usage: 88 MB
% 4.31/1.58 % (3960189)Instructions burned: 3 (million)
% 4.31/1.58 % (3960188)Instruction limit reached!
% 4.31/1.58 % (3960188)------------------------------
% 4.31/1.58 % (3960188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960188)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960188)Termination reason: Instruction limit
% 4.31/1.58 % (3960188)Termination phase: Saturation
% 4.31/1.58 % (3960188)Time elapsed: 0.104 s
% 4.31/1.58 % (3960188)Peak memory usage: 91 MB
% 4.31/1.58 % (3960188)Instructions burned: 190 (million)
% 4.31/1.58 % (3960173)First to succeed.
% 4.31/1.58 % (3960173)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3960168"
% 4.31/1.58 % (3960192)lrs+10_64_to=lpo:sil=8000:random_seed=420978887:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 4.31/1.58 % (3960187)------------------------------
% 4.31/1.58 % (3960187)------------------------------
% 4.31/1.58 % (3960192)Instruction limit reached!
% 4.31/1.58 % (3960192)------------------------------
% 4.31/1.58 % (3960192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.31/1.58 % (3960192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.31/1.58 % (3960192)CaDiCaL version: 2.1.3
% 4.31/1.58 % (3960192)Termination reason: Instruction limit
% 4.31/1.58 % (3960192)Termination phase: Saturation
% 4.31/1.58 % (3960192)Time elapsed: 0.081 s
% 4.31/1.58 % (3960192)Peak memory usage: 89 MB
% 4.31/1.58 % (3960192)Instructions burned: 126 (million)
% 4.31/1.58 % (3960194)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3309752153:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 4.31/1.58 % (3960189)------------------------------
% 4.31/1.58 % (3960189)------------------------------
% 4.31/1.58 % (3960173)Refutation found. Thanks to Tanya!
% 4.31/1.58 % SZS status Unsatisfiable for theBenchmark
% 4.31/1.58 % SZS output start Proof for theBenchmark
% See solution above
% 5.72/1.78 % (3960173)------------------------------
% 5.72/1.78 % (3960173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.72/1.78 % (3960173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.72/1.78 % (3960173)CaDiCaL version: 2.1.3
% 5.72/1.78 % (3960173)Termination reason: Refutation
% 5.72/1.78 % (3960173)Time elapsed: 0.430 s
% 5.72/1.78 % (3960173)Peak memory usage: 132 MB
% 5.72/1.78 % (3960173)Instructions burned: 1168 (million)
% 5.72/1.78 % (3960173)------------------------------
% 5.72/1.78 % (3960173)------------------------------
% 5.72/1.78 % (3960168)Success in time 0.739 s
% 5.72/1.78 % Vampire exiting
%------------------------------------------------------------------------------