%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM145-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:11:49 PM UTC 2026
% Result : Unsatisfiable 10.00s 3.04s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 30
% Syntax : Number of formulae : 146 ( 28 unt; 12 def)
% Number of atoms : 314 ( 56 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 281 ( 113 ~; 161 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-2 aty)
% Number of variables : 126 ( 0 sgn 126 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( ~ member(X2,X0)
| ~ subclass(X0,X1)
| member(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_members) ).
fof(f2,axiom,
! [X0,X1] :
( member(not_subclass_element(X0,X1),X0)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members1) ).
fof(f3,axiom,
! [X0,X1] :
( ~ member(not_subclass_element(X0,X1),X1)
| subclass(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_subclass_members2) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f7,axiom,
! [X0,X1] :
( ~ subclass(X1,X0)
| ~ subclass(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subclass_implies_equal) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f9,axiom,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unordered_pair2) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection1) ).
fof(f22,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection2) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,complement(X1))
| ~ member(X0,universal_class)
| member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement2) ).
fof(f26,axiom,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union) ).
fof(f44,axiom,
! [X0] : union(X0,singleton(X0)) = successor(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',successor) ).
fof(f67,axiom,
! [X0] :
( X0 = null_class
| member(regular(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',regularity1) ).
fof(f68,plain,
! [X0] :
( member(regular(X0),X0)
| null_class = X0 ),
inference(reorient_equations,[],[f67]) ).
fof(f176,negated_conjecture,
member(successor(x),universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_1) ).
fof(f177,negated_conjecture,
~ member(x,successor(x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_corollary_2) ).
fof(f183,plain,
! [X0] : successor(X0) = complement(intersection(complement(X0),complement(unordered_pair(X0,X0)))),
inference(definition_unfolding,[],[f44,f26,f12]) ).
fof(f268,plain,
member(complement(intersection(complement(x),complement(unordered_pair(x,x)))),universal_class),
inference(definition_unfolding,[],[f176,f183]) ).
fof(f269,plain,
~ member(x,complement(intersection(complement(x),complement(unordered_pair(x,x))))),
inference(definition_unfolding,[],[f177,f183]) ).
fof(f276,definition,
sF0 = complement(x),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f277,plain,
complement(x) = sF0,
inference(reorient_equations,[],[f276]) ).
fof(f278,definition,
sF1 = unordered_pair(x,x),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f279,plain,
unordered_pair(x,x) = sF1,
inference(reorient_equations,[],[f278]) ).
fof(f280,definition,
sF2 = complement(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f281,plain,
complement(sF1) = sF2,
inference(reorient_equations,[],[f280]) ).
fof(f282,definition,
sF3 = intersection(sF0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f283,plain,
intersection(sF0,sF2) = sF3,
inference(reorient_equations,[],[f282]) ).
fof(f284,definition,
sF4 = complement(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f285,plain,
complement(sF3) = sF4,
inference(reorient_equations,[],[f284]) ).
fof(f286,plain,
member(sF4,universal_class),
inference(definition_folding,[],[f268,f285,f283,f281,f279,f277]) ).
fof(f287,plain,
~ member(x,sF4),
inference(definition_folding,[],[f269,f285,f283,f281,f279,f277]) ).
fof(f288,plain,
! [X0] :
( ~ member(X0,sF0)
| ~ member(X0,x) ),
inference(superposition,[],[f24,f277]) ).
fof(f289,plain,
! [X0] :
( ~ member(X0,sF3)
| member(X0,sF0) ),
inference(superposition,[],[f21,f283]) ).
fof(f291,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF0)
| member(X0,x) ),
inference(superposition,[],[f25,f277]) ).
fof(f292,plain,
( member(x,sF1)
| ~ member(x,universal_class) ),
inference(superposition,[],[f9,f279]) ).
fof(f294,definition,
( spl5_1
<=> member(x,universal_class) ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f295,plain,
( member(x,universal_class)
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f296,plain,
( ~ member(x,universal_class)
| spl5_1 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f298,definition,
( spl5_2
<=> member(x,sF1) ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
fof(f300,plain,
( member(x,sF1)
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f301,plain,
( ~ spl5_1
| spl5_2 ),
inference(avatar_split_clause,[],[f292,f298,f294]) ).
fof(f302,plain,
! [X0] :
( ~ member(X0,sF3)
| member(X0,sF2) ),
inference(superposition,[],[f22,f283]) ).
fof(f313,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF4)
| member(X0,sF3) ),
inference(superposition,[],[f25,f285]) ).
fof(f314,plain,
! [X0] :
( ~ member(X0,sF4)
| ~ member(X0,sF3) ),
inference(superposition,[],[f24,f285]) ).
fof(f325,plain,
! [X0] :
( ~ member(X0,universal_class)
| member(X0,sF2)
| member(X0,sF1) ),
inference(superposition,[],[f25,f281]) ).
fof(f326,plain,
! [X0] :
( ~ member(X0,sF2)
| ~ member(X0,sF1) ),
inference(superposition,[],[f24,f281]) ).
fof(f350,plain,
! [X2,X3,X0,X1] :
( ~ subclass(intersection(X2,X1),X3)
| ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,X3) ),
inference(resolution,[],[f23,f1]) ).
fof(f352,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| ~ member(X0,X1)
| member(X0,universal_class) ),
inference(resolution,[],[f350,f4]) ).
fof(f364,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0
| x = X0 ),
inference(superposition,[],[f8,f279]) ).
fof(f365,plain,
! [X0] :
( ~ member(X0,sF1)
| x = X0 ),
inference(duplicate_literal_removal,[],[f364]) ).
fof(f394,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(f395,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X1)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f22]) ).
fof(f396,plain,
! [X0,X1] :
( member(regular(intersection(X0,X1)),X0)
| intersection(X0,X1) = null_class ),
inference(resolution,[],[f68,f21]) ).
fof(f400,plain,
( null_class = sF1
| x = regular(sF1) ),
inference(resolution,[],[f68,f365]) ).
fof(f448,definition,
( spl5_18
<=> x = regular(sF1) ),
introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition]) ).
fof(f450,plain,
( x = regular(sF1)
| ~ spl5_18 ),
inference(avatar_component_clause,[],[f448]) ).
fof(f452,definition,
( spl5_19
<=> null_class = sF1 ),
introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition]) ).
fof(f453,plain,
( null_class != sF1
| spl5_19 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f454,plain,
( null_class = sF1
| ~ spl5_19 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,plain,
( spl5_18
| spl5_19 ),
inference(avatar_split_clause,[],[f400,f452,f448]) ).
fof(f502,plain,
! [X0,X1] :
( X0 != X1
| regular(unordered_pair(X0,X1)) = X0
| unordered_pair(X0,X1) = null_class ),
inference(equality_factoring,[],[f394]) ).
fof(f510,plain,
( member(x,sF1)
| null_class = sF1
| ~ spl5_18 ),
inference(superposition,[],[f68,f450]) ).
fof(f517,plain,
( spl5_19
| spl5_2
| ~ spl5_18 ),
inference(avatar_split_clause,[],[f510,f448,f298,f452]) ).
fof(f525,plain,
! [X0] :
( regular(unordered_pair(X0,X0)) = X0
| unordered_pair(X0,X0) = null_class ),
inference(equality_resolution,[],[f502]) ).
fof(f527,plain,
! [X0] :
( member(X0,unordered_pair(X0,X0))
| unordered_pair(X0,X0) = null_class
| unordered_pair(X0,X0) = null_class ),
inference(superposition,[],[f68,f525]) ).
fof(f530,plain,
! [X0] :
( member(X0,unordered_pair(X0,X0))
| unordered_pair(X0,X0) = null_class ),
inference(duplicate_literal_removal,[],[f527]) ).
fof(f576,plain,
! [X0,X1] :
( ~ member(regular(intersection(X0,complement(X1))),X1)
| null_class = intersection(X0,complement(X1)) ),
inference(resolution,[],[f395,f24]) ).
fof(f644,plain,
! [X0] :
( null_class = intersection(X0,complement(X0))
| null_class = intersection(X0,complement(X0)) ),
inference(resolution,[],[f576,f396]) ).
fof(f651,plain,
! [X0] : null_class = intersection(X0,complement(X0)),
inference(duplicate_literal_removal,[],[f644]) ).
fof(f662,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1) ),
inference(superposition,[],[f21,f651]) ).
fof(f698,plain,
! [X2,X0,X1] :
( member(not_subclass_element(X0,X1),X2)
| ~ subclass(X0,X2)
| subclass(X0,X1) ),
inference(resolution,[],[f2,f1]) ).
fof(f704,plain,
! [X2,X0,X1] :
( member(not_subclass_element(intersection(X0,X1),X2),X0)
| subclass(intersection(X0,X1),X2) ),
inference(resolution,[],[f2,f21]) ).
fof(f713,plain,
! [X0] :
( ~ member(not_subclass_element(sF4,X0),sF3)
| subclass(sF4,X0) ),
inference(resolution,[],[f2,f314]) ).
fof(f835,plain,
! [X0,X1] :
( subclass(intersection(X0,X1),X0)
| subclass(intersection(X0,X1),X0) ),
inference(resolution,[],[f3,f704]) ).
fof(f837,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X1,X2)),X2)
| subclass(X0,intersection(X1,X2))
| ~ member(not_subclass_element(X0,intersection(X1,X2)),X1) ),
inference(resolution,[],[f3,f23]) ).
fof(f841,plain,
! [X0,X1] : subclass(intersection(X0,X1),X0),
inference(duplicate_literal_removal,[],[f835]) ).
fof(f914,plain,
! [X2,X0,X1] :
( ~ subclass(X0,X1)
| subclass(X0,intersection(X2,X1))
| subclass(X0,intersection(X2,X1))
| ~ member(not_subclass_element(X0,intersection(X2,X1)),X2) ),
inference(resolution,[],[f698,f837]) ).
fof(f918,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF1) ),
inference(resolution,[],[f698,f325]) ).
fof(f919,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF4)
| member(not_subclass_element(X0,X1),sF3) ),
inference(resolution,[],[f698,f313]) ).
fof(f920,plain,
! [X0,X1] :
( ~ subclass(X0,universal_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF0)
| member(not_subclass_element(X0,X1),x) ),
inference(resolution,[],[f698,f291]) ).
fof(f934,plain,
! [X2,X0,X1] :
( ~ member(not_subclass_element(X0,intersection(X2,X1)),X2)
| subclass(X0,intersection(X2,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f914]) ).
fof(f942,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),x)
| member(not_subclass_element(X0,X1),sF0)
| subclass(X0,X1) ),
inference(forward_subsumption_resolution,[],[f920,f4]) ).
fof(f943,plain,
! [X0,X1] :
( member(not_subclass_element(X0,X1),sF4)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF3) ),
inference(forward_subsumption_resolution,[],[f919,f4]) ).
fof(f944,plain,
! [X0,X1] :
( subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF2)
| member(not_subclass_element(X0,X1),sF1) ),
inference(forward_subsumption_resolution,[],[f918,f4]) ).
fof(f947,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),null_class)
| subclass(X0,X1)
| member(not_subclass_element(X0,X1),sF2) )
| ~ spl5_19 ),
inference(forward_demodulation,[],[f944,f454]) ).
fof(f949,plain,
( ! [X0,X1] :
( member(not_subclass_element(X0,X1),sF2)
| subclass(X0,X1) )
| ~ spl5_19 ),
inference(forward_subsumption_resolution,[],[f947,f662]) ).
fof(f950,plain,
( ! [X0] :
( subclass(X0,sF2)
| subclass(X0,sF2) )
| ~ spl5_19 ),
inference(resolution,[],[f949,f3]) ).
fof(f959,plain,
( ! [X0] : subclass(X0,sF2)
| ~ spl5_19 ),
inference(duplicate_literal_removal,[],[f950]) ).
fof(f963,plain,
! [X0] :
( member(not_subclass_element(X0,x),sF0)
| subclass(X0,x)
| subclass(X0,x) ),
inference(resolution,[],[f942,f3]) ).
fof(f970,plain,
! [X0] :
( member(not_subclass_element(X0,x),sF0)
| subclass(X0,x) ),
inference(duplicate_literal_removal,[],[f963]) ).
fof(f1377,plain,
! [X0] :
( subclass(X0,sF4)
| member(not_subclass_element(X0,sF4),sF3)
| subclass(X0,sF4) ),
inference(resolution,[],[f943,f3]) ).
fof(f1387,plain,
! [X0] :
( member(not_subclass_element(X0,sF4),sF3)
| subclass(X0,sF4) ),
inference(duplicate_literal_removal,[],[f1377]) ).
fof(f1391,plain,
! [X0] :
( member(not_subclass_element(X0,sF4),sF0)
| subclass(X0,sF4) ),
inference(resolution,[],[f1387,f289]) ).
fof(f1398,plain,
! [X0] :
( ~ member(not_subclass_element(X0,sF4),x)
| subclass(X0,sF4) ),
inference(resolution,[],[f1391,f288]) ).
fof(f1403,plain,
( subclass(x,sF4)
| subclass(x,sF4) ),
inference(resolution,[],[f1398,f2]) ).
fof(f1410,plain,
subclass(x,sF4),
inference(duplicate_literal_removal,[],[f1403]) ).
fof(f1413,plain,
( ~ subclass(sF4,x)
| x = sF4 ),
inference(resolution,[],[f1410,f7]) ).
fof(f1415,definition,
( spl5_39
<=> x = sF4 ),
introduced(definition,[new_symbols(definition,[spl5_39])],[avatar_definition]) ).
fof(f1417,plain,
( x = sF4
| ~ spl5_39 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1419,definition,
( spl5_40
<=> subclass(sF4,x) ),
introduced(definition,[new_symbols(definition,[spl5_40])],[avatar_definition]) ).
fof(f1421,plain,
( ~ subclass(sF4,x)
| spl5_40 ),
inference(avatar_component_clause,[],[f1419]) ).
fof(f1422,plain,
( spl5_39
| ~ spl5_40 ),
inference(avatar_split_clause,[],[f1413,f1419,f1415]) ).
fof(f2653,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1)
| subclass(X0,intersection(X0,X1)) ),
inference(resolution,[],[f934,f2]) ).
fof(f2684,plain,
! [X0,X1] :
( subclass(X0,intersection(X0,X1))
| ~ subclass(X0,X1) ),
inference(duplicate_literal_removal,[],[f2653]) ).
fof(f2692,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| ~ subclass(intersection(X0,X1),X0)
| intersection(X0,X1) = X0 ),
inference(resolution,[],[f2684,f7]) ).
fof(f2727,plain,
! [X0,X1] :
( ~ subclass(X0,X1)
| intersection(X0,X1) = X0 ),
inference(forward_subsumption_resolution,[],[f2692,f841]) ).
fof(f2740,plain,
( ! [X0] : intersection(X0,sF2) = X0
| ~ spl5_19 ),
inference(resolution,[],[f2727,f959]) ).
fof(f2901,plain,
( sF0 = sF3
| ~ spl5_19 ),
inference(superposition,[],[f283,f2740]) ).
fof(f2911,plain,
( ! [X0] :
( ~ member(not_subclass_element(sF4,X0),sF0)
| subclass(sF4,X0) )
| ~ spl5_19 ),
inference(superposition,[],[f713,f2901]) ).
fof(f3008,plain,
( subclass(sF4,x)
| subclass(sF4,x)
| ~ spl5_19 ),
inference(resolution,[],[f2911,f970]) ).
fof(f3019,plain,
( subclass(sF4,x)
| ~ spl5_19 ),
inference(duplicate_literal_removal,[],[f3008]) ).
fof(f3021,plain,
( $false
| ~ spl5_19
| spl5_40 ),
inference(forward_subsumption_resolution,[],[f3019,f1421]) ).
fof(f3022,plain,
( ~ spl5_19
| spl5_40 ),
inference(avatar_contradiction_clause,[],[f3021]) ).
fof(f3025,plain,
( member(x,universal_class)
| ~ spl5_39 ),
inference(superposition,[],[f286,f1417]) ).
fof(f3062,plain,
( $false
| spl5_1
| ~ spl5_39 ),
inference(forward_subsumption_resolution,[],[f3025,f296]) ).
fof(f3063,plain,
( spl5_1
| ~ spl5_39 ),
inference(avatar_contradiction_clause,[],[f3062]) ).
fof(f3177,plain,
( ! [X0] :
( ~ member(x,X0)
| member(x,universal_class) )
| ~ spl5_2 ),
inference(resolution,[],[f300,f352]) ).
fof(f3180,definition,
( spl5_53
<=> ! [X0] : ~ member(x,X0) ),
introduced(definition,[new_symbols(definition,[spl5_53])],[avatar_definition]) ).
fof(f3181,plain,
( ! [X0] : ~ member(x,X0)
| ~ spl5_53 ),
inference(avatar_component_clause,[],[f3180]) ).
fof(f3182,plain,
( spl5_1
| spl5_53
| ~ spl5_2 ),
inference(avatar_split_clause,[],[f3177,f298,f3180,f294]) ).
fof(f3223,plain,
( null_class = unordered_pair(x,x)
| ~ spl5_53 ),
inference(resolution,[],[f3181,f530]) ).
fof(f3229,plain,
( null_class = sF1
| ~ spl5_53 ),
inference(forward_demodulation,[],[f3223,f279]) ).
fof(f3230,plain,
( $false
| spl5_19
| ~ spl5_53 ),
inference(forward_subsumption_resolution,[],[f3229,f453]) ).
fof(f3231,plain,
( spl5_19
| ~ spl5_53 ),
inference(avatar_contradiction_clause,[],[f3230]) ).
fof(f3234,plain,
( member(x,sF4)
| member(x,sF3)
| ~ spl5_1 ),
inference(resolution,[],[f295,f313]) ).
fof(f3247,plain,
( member(x,sF3)
| ~ spl5_1 ),
inference(forward_subsumption_resolution,[],[f3234,f287]) ).
fof(f3252,plain,
( member(x,sF2)
| ~ spl5_1 ),
inference(resolution,[],[f3247,f302]) ).
fof(f3258,plain,
( ~ member(x,sF1)
| ~ spl5_1 ),
inference(resolution,[],[f3252,f326]) ).
fof(f3261,plain,
( $false
| ~ spl5_1
| ~ spl5_2 ),
inference(forward_subsumption_resolution,[],[f3258,f300]) ).
fof(f3262,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(avatar_contradiction_clause,[],[f3261]) ).
cnf(s1,plain,
( ~ spl5_1
| spl5_2 ),
inference(sat_conversion,[],[f301]) ).
cnf(s15,plain,
( spl5_18
| spl5_19 ),
inference(sat_conversion,[],[f455]) ).
cnf(s21,plain,
( spl5_2
| ~ spl5_18
| spl5_19 ),
inference(sat_conversion,[],[f517]) ).
cnf(s32,plain,
( spl5_39
| ~ spl5_40 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s43,plain,
( ~ spl5_19
| spl5_40 ),
inference(sat_conversion,[],[f3022]) ).
cnf(s45,plain,
( spl5_1
| ~ spl5_39 ),
inference(sat_conversion,[],[f3063]) ).
cnf(s53,plain,
( spl5_1
| ~ spl5_2
| spl5_53 ),
inference(sat_conversion,[],[f3182]) ).
cnf(s55,plain,
( spl5_19
| ~ spl5_53 ),
inference(sat_conversion,[],[f3231]) ).
cnf(s59,plain,
( ~ spl5_1
| ~ spl5_2 ),
inference(sat_conversion,[],[f3262]) ).
cnf(s60,plain,
spl5_1,
inference(rat,[],[s21,s53,s15,s55,s43,s32,s45]) ).
cnf(s61,plain,
~ spl5_2,
inference(rat,[],[s59,s60]) ).
cnf(s64,plain,
$false,
inference(rat,[],[s1,s61,s60]) ).
fof(f3263,plain,
$false,
inference(avatar_sat_refutation,[],[s64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM145-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 19:02:56 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.49/2.84 % (3145873)Input is clausal, will run a generic CNF schedule.
% 13.49/2.84 % (3145947)dis-21_1_sil=8000:lcm=predicate:random_seed=358305063: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)
% 13.49/2.84 % (3145940)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=3965147269:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.49/2.84 % (3145947)Instruction limit reached!
% 13.49/2.84 % (3145947)------------------------------
% 13.49/2.84 % (3145947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.49/2.84 % (3145947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.49/2.84 % (3145947)CaDiCaL version: 2.1.3
% 13.49/2.84 % (3145947)Termination reason: Instruction limit
% 13.49/2.84 % (3145947)Termination phase: Saturation
% 13.49/2.84 % (3145947)Time elapsed: 0.053 s
% 13.49/2.84 % (3145947)Peak memory usage: 89 MB
% 13.49/2.84 % (3145947)Instructions burned: 117 (million)
% 13.49/2.84 % (3145941)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1058727532:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.49/2.84 % (3145942)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2840478445:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.49/2.84 % (3145945)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3404745587:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.49/2.84 % (3145944)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4282683371:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.49/2.84 % (3145943)lrs+10_1_sil=8000:sp=occurrence:random_seed=335237044:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.49/2.84 % (3145943)Instruction limit reached!
% 13.49/2.84 % (3145943)------------------------------
% 13.49/2.84 % (3145943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.49/2.84 % (3145943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.49/2.84 % (3145943)CaDiCaL version: 2.1.3
% 13.49/2.84 % (3145943)Termination reason: Instruction limit
% 13.49/2.84 % (3145943)Termination phase: Saturation
% 13.49/2.84 % (3145943)Time elapsed: 0.122 s
% 13.49/2.84 % (3145943)Peak memory usage: 89 MB
% 13.49/2.84 % (3145943)Instructions burned: 107 (million)
% 13.49/2.84 % (3145944)Instruction limit reached!
% 13.49/2.84 % (3145944)------------------------------
% 13.49/2.84 % (3145944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.49/2.84 % (3145944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.49/2.84 % (3145944)CaDiCaL version: 2.1.3
% 13.49/2.84 % (3145944)Termination reason: Instruction limit
% 13.49/2.84 % (3145944)Termination phase: Saturation
% 13.49/2.84 % (3145944)Time elapsed: 0.125 s
% 13.49/2.84 % (3145944)Peak memory usage: 89 MB
% 13.49/2.84 % (3145944)Instructions burned: 115 (million)
% 13.49/2.84 % (3145945)Instruction limit reached!
% 13.49/2.84 % (3145945)------------------------------
% 13.49/2.84 % (3145945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.49/2.84 % (3145945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.49/2.84 % (3145945)CaDiCaL version: 2.1.3
% 13.49/2.84 % (3145945)Termination reason: Instruction limit
% 13.49/2.84 % (3145945)Termination phase: Saturation
% 13.49/2.84 % (3145945)Time elapsed: 0.165 s
% 13.49/2.84 % (3145945)Peak memory usage: 90 MB
% 13.49/2.84 % (3145945)Instructions burned: 180 (million)
% 13.49/2.84 % (3145959)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=4206626667:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 13.49/2.84 % (3145959)Instruction limit reached!
% 13.49/2.84 % (3145959)------------------------------
% 13.49/2.84 % (3145959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.49/2.84 % (3145959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.49/2.84 % (3145959)CaDiCaL version: 2.1.3
% 13.49/2.84 % (3145959)Termination reason: Instruction limit
% 13.49/2.84 % (3145959)Termination phase: Saturation
% 13.49/2.84 % (3145959)Time elapsed: 0.055 s
% 13.49/2.84 % (3145959)Peak memory usage: 87 MB
% 13.49/2.84 % (3145959)Instructions burned: 145 (million)
% 13.49/2.84 % (3145970)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=50972445:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 10.00/3.04 % (3145969)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3830242133:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 10.00/3.04 % (3145972)lrs+10_64_to=lpo:sil=8000:random_seed=357848118:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 10.00/3.04 % (3145973)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3364194329:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 10.00/3.04 % (3145973)Instruction limit reached!
% 10.00/3.04 % (3145973)------------------------------
% 10.00/3.04 % (3145973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145973)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145973)Termination reason: Instruction limit
% 10.00/3.04 % (3145973)Termination phase: Saturation
% 10.00/3.04 % (3145973)Time elapsed: 0.087 s
% 10.00/3.04 % (3145973)Peak memory usage: 90 MB
% 10.00/3.04 % (3145973)Instructions burned: 196 (million)
% 10.00/3.04 % (3145972)Instruction limit reached!
% 10.00/3.04 % (3145972)------------------------------
% 10.00/3.04 % (3145972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145972)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145972)Termination reason: Instruction limit
% 10.00/3.04 % (3145972)Termination phase: Saturation
% 10.00/3.04 % (3145972)Time elapsed: 0.132 s
% 10.00/3.04 % (3145972)Peak memory usage: 89 MB
% 10.00/3.04 % (3145972)Instructions burned: 127 (million)
% 10.00/3.04 % (3145969)Instruction limit reached!
% 10.00/3.04 % (3145969)------------------------------
% 10.00/3.04 % (3145969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145969)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145969)Termination reason: Instruction limit
% 10.00/3.04 % (3145969)Termination phase: Saturation
% 10.00/3.04 % (3145969)Time elapsed: 0.159 s
% 10.00/3.04 % (3145969)Peak memory usage: 90 MB
% 10.00/3.04 % (3145969)Instructions burned: 191 (million)
% 10.00/3.04 % (3145970)Instruction limit reached!
% 10.00/3.04 % (3145970)------------------------------
% 10.00/3.04 % (3145970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145970)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145970)Termination reason: Instruction limit
% 10.00/3.04 % (3145970)Termination phase: Saturation
% 10.00/3.04 % (3145970)Time elapsed: 0.229 s
% 10.00/3.04 % (3145970)Peak memory usage: 90 MB
% 10.00/3.04 % (3145970)Instructions burned: 219 (million)
% 10.00/3.04 % (3145978)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=104926932:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 10.00/3.04 % (3145980)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1409901691:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 10.00/3.04 % (3145981)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=3536776:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 10.00/3.04 % (3145978)Instruction limit reached!
% 10.00/3.04 % (3145978)------------------------------
% 10.00/3.04 % (3145978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145978)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145978)Termination reason: Instruction limit
% 10.00/3.04 % (3145978)Termination phase: Saturation
% 10.00/3.04 % (3145978)Time elapsed: 0.096 s
% 10.00/3.04 % (3145978)Peak memory usage: 91 MB
% 10.00/3.04 % (3145978)Instructions burned: 158 (million)
% 10.00/3.04 % (3145985)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1511021865:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 10.00/3.04 % (3145981)Instruction limit reached!
% 10.00/3.04 % (3145981)------------------------------
% 10.00/3.04 % (3145981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145981)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145981)Termination reason: Instruction limit
% 10.00/3.04 % (3145981)Termination phase: Saturation
% 10.00/3.04 % (3145981)Time elapsed: 0.108 s
% 10.00/3.04 % (3145981)Peak memory usage: 90 MB
% 10.00/3.04 % (3145981)Instructions burned: 106 (million)
% 10.00/3.04 % (3145992)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=330550205:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 10.00/3.04 % (3145985)Instruction limit reached!
% 10.00/3.04 % (3145985)------------------------------
% 10.00/3.04 % (3145985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145985)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145985)Termination reason: Instruction limit
% 10.00/3.04 % (3145985)Termination phase: Saturation
% 10.00/3.04 % (3145985)Time elapsed: 0.114 s
% 10.00/3.04 % (3145985)Peak memory usage: 89 MB
% 10.00/3.04 % (3145985)Instructions burned: 107 (million)
% 10.00/3.04 % (3145992)Instruction limit reached!
% 10.00/3.04 % (3145992)------------------------------
% 10.00/3.04 % (3145992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145992)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145992)Termination reason: Instruction limit
% 10.00/3.04 % (3145992)Termination phase: Saturation
% 10.00/3.04 % (3145992)Time elapsed: 0.149 s
% 10.00/3.04 % (3145992)Peak memory usage: 90 MB
% 10.00/3.04 % (3145992)Instructions burned: 242 (million)
% 10.00/3.04 % (3145995)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1379634339:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 10.00/3.04 % (3145997)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1171847457:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 10.00/3.04 % (3145998)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=935174798:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 10.00/3.04 % (3145997)Instruction limit reached!
% 10.00/3.04 % (3145997)------------------------------
% 10.00/3.04 % (3145997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145997)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145997)Termination reason: Instruction limit
% 10.00/3.04 % (3145997)Termination phase: Saturation
% 10.00/3.04 % (3145997)Time elapsed: 0.087 s
% 10.00/3.04 % (3145997)Peak memory usage: 88 MB
% 10.00/3.04 % (3145997)Instructions burned: 135 (million)
% 10.00/3.04 % (3145940)First to succeed.
% 10.00/3.04 % (3145940)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3145873"
% 10.00/3.04 % (3145998)Instruction limit reached!
% 10.00/3.04 % (3145998)------------------------------
% 10.00/3.04 % (3145998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3145998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3145998)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3145998)Termination reason: Instruction limit
% 10.00/3.04 % (3145998)Termination phase: Saturation
% 10.00/3.04 % (3145998)Time elapsed: 0.270 s
% 10.00/3.04 % (3145998)Peak memory usage: 97 MB
% 10.00/3.04 % (3145998)Instructions burned: 500 (million)
% 10.00/3.04 % (3146008)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1314137580:i=191:fgj=on:bd=all_2984 on theBenchmark for (2984ds/191Mi)
% 10.00/3.04 % (3146009)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=448928873:i=264:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/264Mi)
% 10.00/3.04 % (3146008)Instruction limit reached!
% 10.00/3.04 % (3146008)------------------------------
% 10.00/3.04 % (3146008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3146008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3146008)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3146008)Termination reason: Instruction limit
% 10.00/3.04 % (3146008)Termination phase: Saturation
% 10.00/3.04 % (3146008)Time elapsed: 0.205 s
% 10.00/3.04 % (3146008)Peak memory usage: 90 MB
% 10.00/3.04 % (3146008)Instructions burned: 191 (million)
% 10.00/3.04 % (3146009)Instruction limit reached!
% 10.00/3.04 % (3146009)------------------------------
% 10.00/3.04 % (3146009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.00/3.04 % (3146009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.00/3.04 % (3146009)CaDiCaL version: 2.1.3
% 10.00/3.04 % (3146009)Termination reason: Instruction limit
% 10.00/3.04 % (3146009)Termination phase: Saturation
% 10.00/3.04 % (3146009)Time elapsed: 0.142 s
% 10.00/3.04 % (3146009)Peak memory usage: 91 MB
% 10.00/3.04 % (3146009)Instructions burned: 264 (million)
% 10.00/3.04 % (3145940)Refutation found. Thanks to Tanya!
% 10.00/3.04 % SZS status Unsatisfiable for theBenchmark
% 10.00/3.04 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/3.32 % (3145940)------------------------------
% 0.17/3.32 % (3145940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/3.32 % (3145940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/3.32 % (3145940)CaDiCaL version: 2.1.3
% 0.17/3.32 % (3145940)Termination reason: Refutation
% 0.17/3.32 % (3145940)Time elapsed: 1.505 s
% 0.17/3.32 % (3145940)Peak memory usage: 134 MB
% 0.17/3.32 % (3145940)Instructions burned: 1459 (million)
% 0.17/3.32 % (3145940)------------------------------
% 0.17/3.32 % (3145940)------------------------------
% 0.17/3.32 % (3145873)Success in time 2.17 s
% 0.17/3.32 % Vampire exiting
%------------------------------------------------------------------------------