%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM071-1 : 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 : n015.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:42 PM UTC 2026
% Result : Unsatisfiable 8.35s 2.23s
% Output : Refutation 10.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 32
% Syntax : Number of formulae : 128 ( 37 unt; 10 def)
% Number of atoms : 281 ( 52 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 294 ( 141 ~; 146 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 8 con; 0-3 aty)
% Number of variables : 121 ( 0 sgn 121 !; 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(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(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(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(f135,axiom,
! [X2,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| X2 = null_class
| member(least(X0,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering2) ).
fof(f136,plain,
! [X2,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| null_class = X2
| member(least(X0,X2),X2) ),
inference(reorient_equations,[],[f135]) ).
fof(f137,axiom,
! [X2,X3,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| ~ member(X3,X2)
| member(least(X0,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering3) ).
fof(f140,axiom,
! [X2,X3,X0,X1] :
( ~ well_ordering(X0,X1)
| ~ subclass(X2,X1)
| ~ member(X3,X2)
| ~ member(ordered_pair(X3,least(X0,X2)),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_ordering5) ).
fof(f176,negated_conjecture,
well_ordering(xr,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_is_irreflexive_1) ).
fof(f177,negated_conjecture,
member(ordered_pair(u,u),xr),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_is_irreflexive_2) ).
fof(f178,negated_conjecture,
member(u,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_well_ordering_is_irreflexive_3) ).
fof(f179,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(f203,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(f254,plain,
! [X2,X3,X0,X1] :
( ~ member(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(least(X0,X2),least(X0,X2)))),X0)
| ~ subclass(X2,X1)
| ~ member(X3,X2)
| ~ well_ordering(X0,X1) ),
inference(definition_unfolding,[],[f140,f179]) ).
fof(f269,plain,
member(unordered_pair(unordered_pair(u,u),unordered_pair(u,unordered_pair(u,u))),xr),
inference(definition_unfolding,[],[f177,f179]) ).
fof(f276,definition,
sF0 = unordered_pair(u,u),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f277,plain,
unordered_pair(u,u) = sF0,
inference(reorient_equations,[],[f276]) ).
fof(f278,definition,
sF1 = unordered_pair(u,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f279,plain,
unordered_pair(u,sF0) = sF1,
inference(reorient_equations,[],[f278]) ).
fof(f280,definition,
sF2 = unordered_pair(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f281,plain,
unordered_pair(sF0,sF1) = sF2,
inference(reorient_equations,[],[f280]) ).
fof(f282,plain,
member(sF2,xr),
inference(definition_folding,[],[f269,f281,f279,f277,f277]) ).
fof(f284,plain,
( member(u,sF0)
| ~ member(u,universal_class) ),
inference(superposition,[],[f9,f277]) ).
fof(f296,definition,
( spl3_3
<=> member(u,universal_class) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f298,plain,
( ~ member(u,universal_class)
| spl3_3 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f300,definition,
( spl3_4
<=> member(u,sF0) ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f302,plain,
( member(u,sF0)
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f303,plain,
( ~ spl3_3
| spl3_4 ),
inference(avatar_split_clause,[],[f284,f300,f296]) ).
fof(f324,plain,
! [X0] :
( ~ member(X0,sF0)
| u = X0
| u = X0 ),
inference(superposition,[],[f8,f277]) ).
fof(f326,plain,
! [X0] :
( ~ member(X0,sF0)
| u = X0 ),
inference(duplicate_literal_removal,[],[f324]) ).
fof(f328,plain,
! [X0] :
( ~ subclass(y,X0)
| member(u,X0) ),
inference(resolution,[],[f1,f178]) ).
fof(f373,definition,
( spl3_15
<=> null_class = sF0 ),
introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition]) ).
fof(f374,plain,
( null_class != sF0
| spl3_15 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f375,plain,
( null_class = sF0
| ~ spl3_15 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f396,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X1),X2)
| ~ subclass(X0,X2)
| subclass(X0,X1) ),
inference(resolution,[],[f2,f1]) ).
fof(f398,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X1)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f22]) ).
fof(f399,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f401,plain,
! [X0] :
( subclass(sF0,X0)
| u = not_subclass_element(sF0,X0) ),
inference(resolution,[],[f2,f326]) ).
fof(f405,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f399,f3]) ).
fof(f415,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f405]) ).
fof(f416,plain,
! [X0] :
( subclass(null_class,X0)
| null_class = X0 ),
inference(superposition,[],[f415,f70]) ).
fof(f417,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X1)
| subclass(intersection(X0,X1),X1) ),
inference(resolution,[],[f398,f3]) ).
fof(f427,plain,
! [X0,X1] : subclass(intersection(X0,X1),X1),
inference(duplicate_literal_removal,[],[f417]) ).
fof(f466,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(f470,plain,
member(u,universal_class),
inference(resolution,[],[f328,f4]) ).
fof(f471,plain,
( $false
| spl3_3 ),
inference(forward_subsumption_resolution,[],[f470,f298]) ).
fof(f472,plain,
spl3_3,
inference(avatar_contradiction_clause,[],[f471]) ).
fof(f473,plain,
( member(u,null_class)
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_demodulation,[],[f302,f375]) ).
fof(f483,plain,
! [X0] :
( member(least(xr,X0),X0)
| null_class = X0
| ~ subclass(X0,y) ),
inference(resolution,[],[f136,f176]) ).
fof(f490,plain,
( null_class = sF0
| ~ subclass(sF0,y)
| u = least(xr,sF0) ),
inference(resolution,[],[f483,f326]) ).
fof(f541,plain,
! [X2,X0,X1] :
( ~ member(unordered_pair(sF0,unordered_pair(u,unordered_pair(least(X0,X1),least(X0,X1)))),X0)
| ~ subclass(X1,X2)
| ~ member(u,X1)
| ~ well_ordering(X0,X2) ),
inference(superposition,[],[f254,f277]) ).
fof(f645,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0
| null_class = X0 ),
inference(resolution,[],[f7,f416]) ).
fof(f647,plain,
! [X0] :
( ~ subclass(X0,null_class)
| null_class = X0 ),
inference(duplicate_literal_removal,[],[f645]) ).
fof(f650,plain,
! [X0] : null_class = intersection(null_class,X0),
inference(resolution,[],[f647,f415]) ).
fof(f661,plain,
! [X0] : subclass(null_class,X0),
inference(superposition,[],[f427,f650]) ).
fof(f663,plain,
! [X0] :
( null_class != null_class
| ~ member(X0,domain_of(null_class)) ),
inference(superposition,[],[f203,f650]) ).
fof(f664,plain,
! [X0] : ~ member(X0,domain_of(null_class)),
inference(trivial_inequality_removal,[],[f663]) ).
fof(f669,plain,
null_class = domain_of(null_class),
inference(resolution,[],[f664,f68]) ).
fof(f676,definition,
( spl3_27
<=> null_class = domain_of(null_class) ),
introduced(definition,[new_symbols(definition,[spl3_27])],[avatar_definition]) ).
fof(f678,plain,
( null_class = domain_of(null_class)
| ~ spl3_27 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f680,plain,
spl3_27,
inference(avatar_split_clause,[],[f669,f676]) ).
fof(f681,plain,
( ! [X0] : ~ member(X0,null_class)
| ~ spl3_27 ),
inference(superposition,[],[f664,f678]) ).
fof(f742,plain,
! [X0,X1] :
( ~ member(X1,X0)
| ~ subclass(X0,y)
| member(least(xr,X0),X0) ),
inference(resolution,[],[f137,f176]) ).
fof(f1476,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,[],[f466,f396]) ).
fof(f1484,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,[],[f1476]) ).
fof(f1493,plain,
( ~ subclass(null_class,y)
| member(least(xr,null_class),null_class)
| ~ spl3_4
| ~ spl3_15 ),
inference(resolution,[],[f473,f742]) ).
fof(f1498,plain,
( member(least(xr,null_class),null_class)
| ~ spl3_4
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f1493,f661]) ).
fof(f1500,plain,
( $false
| ~ spl3_4
| ~ spl3_15
| ~ spl3_27 ),
inference(forward_subsumption_resolution,[],[f1498,f681]) ).
fof(f1501,plain,
( ~ spl3_4
| ~ spl3_15
| ~ spl3_27 ),
inference(avatar_contradiction_clause,[],[f1500]) ).
fof(f1503,plain,
( ~ subclass(sF0,y)
| u = least(xr,sF0)
| spl3_15 ),
inference(forward_subsumption_resolution,[],[f490,f374]) ).
fof(f1510,definition,
( spl3_44
<=> u = least(xr,sF0) ),
introduced(definition,[new_symbols(definition,[spl3_44])],[avatar_definition]) ).
fof(f1512,plain,
( u = least(xr,sF0)
| ~ spl3_44 ),
inference(avatar_component_clause,[],[f1510]) ).
fof(f1517,definition,
( spl3_46
<=> subclass(sF0,y) ),
introduced(definition,[new_symbols(definition,[spl3_46])],[avatar_definition]) ).
fof(f1518,plain,
( subclass(sF0,y)
| ~ spl3_46 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1519,plain,
( ~ subclass(sF0,y)
| spl3_46 ),
inference(avatar_component_clause,[],[f1517]) ).
fof(f1527,plain,
( spl3_44
| ~ spl3_46
| spl3_15 ),
inference(avatar_split_clause,[],[f1503,f373,f1517,f1510]) ).
fof(f2847,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f1484,f2]) ).
fof(f2867,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f2847]) ).
fof(f2871,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f2867,f7]) ).
fof(f2935,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f2871,f415]) ).
fof(f2944,plain,
! [X0] :
( u = not_subclass_element(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(resolution,[],[f2935,f401]) ).
fof(f3006,plain,
! [X0] :
( ~ member(u,X0)
| subclass(sF0,X0)
| sF0 = intersection(sF0,X0) ),
inference(superposition,[],[f3,f2944]) ).
fof(f3011,plain,
! [X0] :
( ~ member(u,X0)
| sF0 = intersection(sF0,X0) ),
inference(forward_subsumption_resolution,[],[f3006,f2935]) ).
fof(f3017,plain,
sF0 = intersection(sF0,y),
inference(resolution,[],[f3011,f178]) ).
fof(f3038,plain,
subclass(sF0,y),
inference(superposition,[],[f427,f3017]) ).
fof(f3043,plain,
( $false
| spl3_46 ),
inference(forward_subsumption_resolution,[],[f3038,f1519]) ).
fof(f3044,plain,
spl3_46,
inference(avatar_contradiction_clause,[],[f3043]) ).
fof(f3169,plain,
( ! [X0] :
( ~ member(unordered_pair(sF0,unordered_pair(u,unordered_pair(u,u))),xr)
| ~ subclass(sF0,X0)
| ~ member(u,sF0)
| ~ well_ordering(xr,X0) )
| ~ spl3_44 ),
inference(superposition,[],[f541,f1512]) ).
fof(f3172,plain,
( ! [X0] :
( ~ member(unordered_pair(sF0,unordered_pair(u,unordered_pair(u,u))),xr)
| ~ subclass(sF0,X0)
| ~ well_ordering(xr,X0) )
| ~ spl3_4
| ~ spl3_44 ),
inference(forward_subsumption_resolution,[],[f3169,f302]) ).
fof(f3174,definition,
( spl3_143
<=> ! [X1] :
( ~ subclass(sF0,X1)
| ~ well_ordering(xr,X1) ) ),
introduced(definition,[new_symbols(definition,[spl3_143])],[avatar_definition]) ).
fof(f3175,plain,
( ! [X1] :
( ~ well_ordering(xr,X1)
| ~ subclass(sF0,X1) )
| ~ spl3_143 ),
inference(avatar_component_clause,[],[f3174]) ).
fof(f3180,plain,
( ! [X0] :
( ~ member(unordered_pair(sF0,unordered_pair(u,sF0)),xr)
| ~ subclass(sF0,X0)
| ~ well_ordering(xr,X0) )
| ~ spl3_4
| ~ spl3_44 ),
inference(forward_demodulation,[],[f3172,f277]) ).
fof(f3181,plain,
( ! [X0] :
( ~ member(unordered_pair(sF0,sF1),xr)
| ~ subclass(sF0,X0)
| ~ well_ordering(xr,X0) )
| ~ spl3_4
| ~ spl3_44 ),
inference(forward_demodulation,[],[f3180,f279]) ).
fof(f3182,plain,
( ! [X0] :
( ~ member(sF2,xr)
| ~ subclass(sF0,X0)
| ~ well_ordering(xr,X0) )
| ~ spl3_4
| ~ spl3_44 ),
inference(forward_demodulation,[],[f3181,f281]) ).
fof(f3183,plain,
( ! [X0] :
( ~ subclass(sF0,X0)
| ~ well_ordering(xr,X0) )
| ~ spl3_4
| ~ spl3_44 ),
inference(forward_subsumption_resolution,[],[f3182,f282]) ).
fof(f3184,plain,
( spl3_143
| ~ spl3_4
| ~ spl3_44 ),
inference(avatar_split_clause,[],[f3183,f1510,f300,f3174]) ).
fof(f3185,plain,
( ~ subclass(sF0,y)
| ~ spl3_143 ),
inference(resolution,[],[f3175,f176]) ).
fof(f3186,plain,
( $false
| ~ spl3_46
| ~ spl3_143 ),
inference(forward_subsumption_resolution,[],[f3185,f1518]) ).
fof(f3187,plain,
( ~ spl3_46
| ~ spl3_143 ),
inference(avatar_contradiction_clause,[],[f3186]) ).
cnf(s2,plain,
( ~ spl3_3
| spl3_4 ),
inference(sat_conversion,[],[f303]) ).
cnf(s11,plain,
spl3_3,
inference(sat_conversion,[],[f472]) ).
cnf(s17,plain,
spl3_27,
inference(sat_conversion,[],[f680]) ).
cnf(s31,plain,
( ~ spl3_4
| ~ spl3_15
| ~ spl3_27 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s34,plain,
( spl3_15
| spl3_44
| ~ spl3_46 ),
inference(sat_conversion,[],[f1527]) ).
cnf(s148,plain,
spl3_46,
inference(sat_conversion,[],[f3044]) ).
cnf(s150,plain,
( ~ spl3_4
| ~ spl3_44
| spl3_143 ),
inference(sat_conversion,[],[f3184]) ).
cnf(s151,plain,
( ~ spl3_46
| ~ spl3_143 ),
inference(sat_conversion,[],[f3187]) ).
cnf(s152,plain,
~ spl3_143,
inference(rat,[],[s151,s148]) ).
cnf(s157,plain,
( spl3_15
| spl3_44 ),
inference(rat,[],[s34,s148]) ).
cnf(s179,plain,
spl3_4,
inference(rat,[],[s2,s11]) ).
cnf(s180,plain,
~ spl3_44,
inference(rat,[],[s150,s152,s179]) ).
cnf(s184,plain,
~ spl3_15,
inference(rat,[],[s31,s17,s179]) ).
cnf(s187,plain,
$false,
inference(rat,[],[s157,s180,s184]) ).
fof(f3188,plain,
$false,
inference(avatar_sat_refutation,[],[s187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM071-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n015.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 18:50:46 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 8.35/2.23 % (1942814)Input is clausal, will run a generic CNF schedule.
% 8.35/2.23 % (1942821)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1233623706:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.35/2.23 % (1942824)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2477698677:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.35/2.23 % (1942820)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3020368480:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.35/2.23 % (1942819)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=1880908233:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.35/2.23 % (1942822)lrs+10_1_sil=8000:sp=occurrence:random_seed=484605117:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.35/2.23 % (1942825)dis-21_1_sil=8000:lcm=predicate:random_seed=516736652: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)
% 8.35/2.23 % (1942823)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2500713973:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.35/2.23 % (1942822)Refutation not found, incomplete strategy
% 8.35/2.23 % (1942822)------------------------------
% 8.35/2.23 % (1942822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942822)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942822)Termination reason: Refutation not found, incomplete strategy
% 8.35/2.23 % (1942822)Time elapsed: 0.001 s
% 8.35/2.23 % (1942822)Peak memory usage: 86 MB
% 8.35/2.23 % (1942825)Instruction limit reached!
% 8.35/2.23 % (1942825)------------------------------
% 8.35/2.23 % (1942825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942825)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942825)Termination reason: Instruction limit
% 8.35/2.23 % (1942825)Termination phase: Saturation
% 8.35/2.23 % (1942825)Time elapsed: 0.066 s
% 8.35/2.23 % (1942825)Peak memory usage: 89 MB
% 8.35/2.23 % (1942825)Instructions burned: 118 (million)
% 8.35/2.23 % (1942823)Instruction limit reached!
% 8.35/2.23 % (1942823)------------------------------
% 8.35/2.23 % (1942823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942823)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942823)Termination reason: Instruction limit
% 8.35/2.23 % (1942823)Termination phase: Saturation
% 8.35/2.23 % (1942823)Time elapsed: 0.068 s
% 8.35/2.23 % (1942823)Peak memory usage: 89 MB
% 8.35/2.23 % (1942823)Instructions burned: 114 (million)
% 8.35/2.23 % (1942824)Instruction limit reached!
% 8.35/2.23 % (1942824)------------------------------
% 8.35/2.23 % (1942824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942824)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942824)Termination reason: Instruction limit
% 8.35/2.23 % (1942824)Termination phase: Saturation
% 8.35/2.23 % (1942824)Time elapsed: 0.132 s
% 8.35/2.23 % (1942824)Peak memory usage: 90 MB
% 8.35/2.23 % (1942824)Instructions burned: 181 (million)
% 8.35/2.23 % (1942833)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=4191655013:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 8.35/2.23 % (1942834)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1071461473: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)
% 8.35/2.23 % (1942822)------------------------------
% 8.35/2.23 % (1942822)------------------------------
% 8.35/2.23 % (1942835)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1626008896:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 8.35/2.23 % (1942835)Refutation not found, incomplete strategy
% 8.35/2.23 % (1942835)------------------------------
% 8.35/2.23 % (1942835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942835)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942835)Termination reason: Refutation not found, incomplete strategy
% 8.35/2.23 % (1942835)Time elapsed: 0.004 s
% 8.35/2.23 % (1942835)Peak memory usage: 88 MB
% 8.35/2.23 % (1942835)Instructions burned: 4 (million)
% 8.35/2.23 % (1942833)Instruction limit reached!
% 8.35/2.23 % (1942833)------------------------------
% 8.35/2.23 % (1942833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942833)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942833)Termination reason: Instruction limit
% 8.35/2.23 % (1942833)Termination phase: Saturation
% 8.35/2.23 % (1942833)Time elapsed: 0.076 s
% 8.35/2.23 % (1942833)Peak memory usage: 88 MB
% 8.35/2.23 % (1942833)Instructions burned: 144 (million)
% 8.35/2.23 % (1942834)Instruction limit reached!
% 8.35/2.23 % (1942834)------------------------------
% 8.35/2.23 % (1942834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942834)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942834)Termination reason: Instruction limit
% 8.35/2.23 % (1942834)Termination phase: Saturation
% 8.35/2.23 % (1942834)Time elapsed: 0.095 s
% 8.35/2.23 % (1942834)Peak memory usage: 90 MB
% 8.35/2.23 % (1942834)Instructions burned: 189 (million)
% 8.35/2.23 % (1942838)lrs+10_64_to=lpo:sil=8000:random_seed=4225321691:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 8.35/2.23 % (1942840)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1329881018:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 8.35/2.23 % (1942841)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2951990584:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 8.35/2.23 % (1942838)Instruction limit reached!
% 8.35/2.23 % (1942838)------------------------------
% 8.35/2.23 % (1942838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942838)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942838)Termination reason: Instruction limit
% 8.35/2.23 % (1942838)Termination phase: Saturation
% 8.35/2.23 % (1942838)Time elapsed: 0.080 s
% 8.35/2.23 % (1942838)Peak memory usage: 89 MB
% 8.35/2.23 % (1942838)Instructions burned: 126 (million)
% 8.35/2.23 % (1942835)------------------------------
% 8.35/2.23 % (1942835)------------------------------
% 8.35/2.23 % (1942840)Instruction limit reached!
% 8.35/2.23 % (1942840)------------------------------
% 8.35/2.23 % (1942840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942841)Instruction limit reached!
% 8.35/2.23 % (1942841)------------------------------
% 8.35/2.23 % (1942841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942840)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942840)Termination reason: Instruction limit
% 8.35/2.23 % (1942840)Termination phase: Saturation
% 8.35/2.23 % (1942840)Time elapsed: 0.135 s
% 8.35/2.23 % (1942840)Peak memory usage: 90 MB
% 8.35/2.23 % (1942840)Instructions burned: 216 (million)
% 8.35/2.23 % (1942841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942841)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942841)Termination reason: Instruction limit
% 8.35/2.23 % (1942841)Termination phase: Saturation
% 8.35/2.23 % (1942841)Time elapsed: 0.116 s
% 8.35/2.23 % (1942841)Peak memory usage: 91 MB
% 8.35/2.23 % (1942841)Instructions burned: 164 (million)
% 8.35/2.23 % (1942845)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=723381844:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 8.35/2.23 % (1942846)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=327349964:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 8.35/2.23 % (1942847)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=100696213:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 8.35/2.23 % (1942848)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3014034180:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 8.35/2.23 % (1942846)Instruction limit reached!
% 8.35/2.23 % (1942846)------------------------------
% 8.35/2.23 % (1942846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942846)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942846)Termination reason: Instruction limit
% 8.35/2.23 % (1942846)Termination phase: Saturation
% 8.35/2.23 % (1942846)Time elapsed: 0.065 s
% 8.35/2.23 % (1942846)Peak memory usage: 89 MB
% 8.35/2.23 % (1942846)Instructions burned: 107 (million)
% 8.35/2.23 % (1942847)Instruction limit reached!
% 8.35/2.23 % (1942847)------------------------------
% 8.35/2.23 % (1942847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942847)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942847)Termination reason: Instruction limit
% 8.35/2.23 % (1942847)Termination phase: Saturation
% 8.35/2.23 % (1942847)Time elapsed: 0.073 s
% 8.35/2.23 % (1942847)Peak memory usage: 89 MB
% 8.35/2.23 % (1942847)Instructions burned: 107 (million)
% 8.35/2.23 % (1942853)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3024805767:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 8.35/2.23 % (1942848)Instruction limit reached!
% 8.35/2.23 % (1942848)------------------------------
% 8.35/2.23 % (1942848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942848)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942848)Termination reason: Instruction limit
% 8.35/2.23 % (1942848)Termination phase: Saturation
% 8.35/2.23 % (1942848)Time elapsed: 0.161 s
% 8.35/2.23 % (1942848)Peak memory usage: 90 MB
% 8.35/2.23 % (1942848)Instructions burned: 243 (million)
% 8.35/2.23 % (1942854)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4021551903:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 8.35/2.23 % (1942819)First to succeed.
% 8.35/2.23 % (1942819)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1942814"
% 8.35/2.23 % (1942856)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2978510845:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 8.35/2.23 % (1942854)Instruction limit reached!
% 8.35/2.23 % (1942854)------------------------------
% 8.35/2.23 % (1942854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.35/2.23 % (1942854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.35/2.23 % (1942854)CaDiCaL version: 2.1.3
% 8.35/2.23 % (1942854)Termination reason: Instruction limit
% 8.35/2.23 % (1942854)Termination phase: Saturation
% 8.35/2.23 % (1942854)Time elapsed: 0.097 s
% 8.35/2.23 % (1942854)Peak memory usage: 89 MB
% 8.35/2.23 % (1942854)Instructions burned: 138 (million)
% 8.35/2.23 % (1942859)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2728332658:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 8.35/2.23 % (1942819)Refutation found. Thanks to Tanya!
% 8.35/2.23 % SZS status Unsatisfiable for theBenchmark
% 8.35/2.23 % SZS output start Proof for theBenchmark
% See solution above
% 10.26/2.42 % (1942819)------------------------------
% 10.26/2.42 % (1942819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.26/2.42 % (1942819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.26/2.42 % (1942819)CaDiCaL version: 2.1.3
% 10.26/2.42 % (1942819)Termination reason: Refutation
% 10.26/2.42 % (1942819)Time elapsed: 0.951 s
% 10.26/2.42 % (1942819)Peak memory usage: 134 MB
% 10.26/2.42 % (1942819)Instructions burned: 1435 (million)
% 10.26/2.42 % (1942819)------------------------------
% 10.26/2.42 % (1942819)------------------------------
% 10.26/2.42 % (1942814)Success in time 1.369 s
% 10.26/2.42 % Vampire exiting
%------------------------------------------------------------------------------