%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET021-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:39:37 PM UTC 2026
% Result : Unsatisfiable 6.85s 2.02s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 28
% Syntax : Number of formulae : 171 ( 41 unt; 13 def)
% Number of atoms : 393 ( 92 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 422 ( 200 ~; 213 |; 0 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 68 ( 0 sgn 68 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] :
( member(f1(X0,X1),X1)
| member(f1(X0,X1),X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality2) ).
fof(f4,axiom,
! [X0,X1] :
( ~ member(f1(X0,X1),X1)
| ~ member(f1(X0,X1),X0)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',extensionality3) ).
fof(f5,axiom,
! [X2,X0,X1] :
( ~ member(X0,non_ordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair1) ).
fof(f6,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair2) ).
fof(f7,axiom,
! [X2,X0,X1] :
( member(X0,non_ordered_pair(X1,X2))
| ~ little_set(X0)
| X0 != X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair3) ).
fof(f8,axiom,
! [X0,X1] : little_set(non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',non_ordered_pair4) ).
fof(f9,axiom,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton_set) ).
fof(f10,axiom,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(singleton_set(X0),non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pair) ).
fof(f25,axiom,
! [X0,X1] :
( ~ member(X0,second(X1))
| little_set(f7(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second2) ).
fof(f26,axiom,
! [X0,X1] :
( ~ member(X0,second(X1))
| X1 = ordered_pair(f6(X0,X1),f7(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second3) ).
fof(f27,plain,
! [X0,X1] :
( ~ member(X0,second(X1))
| ordered_pair(f6(X0,X1),f7(X0,X1)) = X1 ),
inference(reorient_equations,[],[f26]) ).
fof(f28,axiom,
! [X0,X1] :
( member(X0,f7(X0,X1))
| ~ member(X0,second(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second4) ).
fof(f29,axiom,
! [X2,X3,X0,X1] :
( member(X0,second(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3)
| ~ member(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second5) ).
fof(f30,plain,
! [X2,X3,X0,X1] :
( member(X0,second(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| ordered_pair(X2,X3) != X1
| ~ member(X0,X3) ),
inference(reorient_equations,[],[f29]) ).
fof(f162,axiom,
little_set(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_little_set) ).
fof(f163,axiom,
little_set(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_little_set) ).
fof(f164,negated_conjecture,
second(ordered_pair(a,b)) != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_second_is_second) ).
fof(f165,plain,
b != second(ordered_pair(a,b)),
inference(reorient_equations,[],[f164]) ).
fof(f167,plain,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1)),
inference(definition_unfolding,[],[f10,f9]) ).
fof(f173,plain,
! [X0,X1] :
( ~ member(X0,second(X1))
| non_ordered_pair(non_ordered_pair(f6(X0,X1),f6(X0,X1)),non_ordered_pair(f6(X0,X1),f7(X0,X1))) = X1 ),
inference(definition_unfolding,[],[f27,f167]) ).
fof(f174,plain,
! [X2,X3,X0,X1] :
( member(X0,second(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3)) != X1
| ~ member(X0,X3) ),
inference(definition_unfolding,[],[f30,f167]) ).
fof(f194,plain,
b != second(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),
inference(definition_unfolding,[],[f165,f167]) ).
fof(f195,plain,
! [X2,X1] :
( member(X1,non_ordered_pair(X1,X2))
| ~ little_set(X1) ),
inference(equality_resolution,[],[f6]) ).
fof(f196,plain,
! [X2,X1] :
( member(X2,non_ordered_pair(X1,X2))
| ~ little_set(X2) ),
inference(equality_resolution,[],[f7]) ).
fof(f199,plain,
! [X2,X3,X0] :
( member(X0,second(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3))))
| ~ little_set(X2)
| ~ little_set(X3)
| ~ member(X0,X3) ),
inference(equality_resolution,[],[f174]) ).
fof(f209,definition,
sF0 = non_ordered_pair(a,a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f210,plain,
non_ordered_pair(a,a) = sF0,
inference(reorient_equations,[],[f209]) ).
fof(f211,definition,
sF1 = non_ordered_pair(a,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f212,plain,
non_ordered_pair(a,b) = sF1,
inference(reorient_equations,[],[f211]) ).
fof(f213,definition,
sF2 = non_ordered_pair(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f214,plain,
non_ordered_pair(sF0,sF1) = sF2,
inference(reorient_equations,[],[f213]) ).
fof(f215,definition,
sF3 = second(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f216,plain,
second(sF2) = sF3,
inference(reorient_equations,[],[f215]) ).
fof(f217,plain,
b != sF3,
inference(definition_folding,[],[f194,f216,f214,f212,f210]) ).
fof(f218,plain,
( member(a,sF0)
| ~ little_set(a) ),
inference(superposition,[],[f195,f210]) ).
fof(f219,plain,
( member(a,sF1)
| ~ little_set(a) ),
inference(superposition,[],[f195,f212]) ).
fof(f230,plain,
member(a,sF1),
inference(forward_subsumption_resolution,[],[f219,f162]) ).
fof(f231,plain,
member(a,sF0),
inference(forward_subsumption_resolution,[],[f218,f162]) ).
fof(f233,plain,
( member(b,sF1)
| ~ little_set(b) ),
inference(superposition,[],[f196,f212]) ).
fof(f234,plain,
( member(sF1,sF2)
| ~ little_set(sF1) ),
inference(superposition,[],[f196,f214]) ).
fof(f236,definition,
( spl4_3
<=> little_set(sF1) ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f238,plain,
( ~ little_set(sF1)
| spl4_3 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f240,definition,
( spl4_4
<=> member(sF1,sF2) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f242,plain,
( member(sF1,sF2)
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f243,plain,
( ~ spl4_3
| spl4_4 ),
inference(avatar_split_clause,[],[f234,f240,f236]) ).
fof(f244,plain,
member(b,sF1),
inference(forward_subsumption_resolution,[],[f233,f163]) ).
fof(f247,plain,
! [X0] :
( member(X0,second(non_ordered_pair(non_ordered_pair(a,a),sF1)))
| ~ little_set(a)
| ~ little_set(b)
| ~ member(X0,b) ),
inference(superposition,[],[f199,f212]) ).
fof(f250,plain,
! [X0] :
( member(X0,second(non_ordered_pair(non_ordered_pair(a,a),sF1)))
| ~ little_set(b)
| ~ member(X0,b) ),
inference(forward_subsumption_resolution,[],[f247,f162]) ).
fof(f253,plain,
! [X0] :
( member(X0,second(non_ordered_pair(non_ordered_pair(a,a),sF1)))
| ~ member(X0,b) ),
inference(forward_subsumption_resolution,[],[f250,f163]) ).
fof(f254,plain,
! [X0] :
( member(X0,second(non_ordered_pair(sF0,sF1)))
| ~ member(X0,b) ),
inference(forward_demodulation,[],[f253,f210]) ).
fof(f255,plain,
! [X0] :
( member(X0,second(sF2))
| ~ member(X0,b) ),
inference(forward_demodulation,[],[f254,f214]) ).
fof(f256,plain,
! [X0] :
( ~ member(X0,b)
| member(X0,sF3) ),
inference(forward_demodulation,[],[f255,f216]) ).
fof(f258,plain,
! [X0] :
( ~ member(X0,sF3)
| sF2 = non_ordered_pair(non_ordered_pair(f6(X0,sF2),f6(X0,sF2)),non_ordered_pair(f6(X0,sF2),f7(X0,sF2))) ),
inference(superposition,[],[f173,f216]) ).
fof(f260,plain,
little_set(sF1),
inference(superposition,[],[f8,f212]) ).
fof(f262,plain,
( $false
| spl4_3 ),
inference(forward_subsumption_resolution,[],[f260,f238]) ).
fof(f263,plain,
spl4_3,
inference(avatar_contradiction_clause,[],[f262]) ).
fof(f271,plain,
! [X0] :
( ~ member(X0,sF1)
| a = X0
| b = X0 ),
inference(superposition,[],[f5,f212]) ).
fof(f272,plain,
! [X0] :
( ~ member(X0,sF2)
| sF0 = X0
| sF1 = X0 ),
inference(superposition,[],[f5,f214]) ).
fof(f285,plain,
! [X0] :
( little_set(f7(X0,sF2))
| ~ member(X0,sF3) ),
inference(superposition,[],[f25,f216]) ).
fof(f319,plain,
! [X0] :
( member(f1(b,X0),sF3)
| member(f1(b,X0),X0)
| b = X0 ),
inference(resolution,[],[f3,f256]) ).
fof(f334,plain,
( member(f1(b,sF3),sF3)
| b = sF3 ),
inference(factoring,[],[f319]) ).
fof(f336,plain,
member(f1(b,sF3),sF3),
inference(forward_subsumption_resolution,[],[f334,f217]) ).
fof(f337,plain,
( ~ member(f1(b,sF3),b)
| b = sF3 ),
inference(resolution,[],[f336,f4]) ).
fof(f338,plain,
sF2 = non_ordered_pair(non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2)),non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2))),
inference(resolution,[],[f336,f258]) ).
fof(f340,plain,
~ member(f1(b,sF3),b),
inference(forward_subsumption_resolution,[],[f337,f217]) ).
fof(f356,plain,
( member(non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2)),sF2)
| ~ little_set(non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2))) ),
inference(superposition,[],[f196,f338]) ).
fof(f357,plain,
( member(non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2)),sF2)
| ~ little_set(non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2))) ),
inference(superposition,[],[f195,f338]) ).
fof(f358,plain,
member(non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2)),sF2),
inference(forward_subsumption_resolution,[],[f357,f8]) ).
fof(f359,plain,
member(non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2)),sF2),
inference(forward_subsumption_resolution,[],[f356,f8]) ).
fof(f364,definition,
( spl4_5
<=> little_set(f7(f1(b,sF3),sF2)) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f365,plain,
( little_set(f7(f1(b,sF3),sF2))
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f366,plain,
( ~ little_set(f7(f1(b,sF3),sF2))
| spl4_5 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f375,plain,
( sF0 = non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2))
| sF1 = non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2)) ),
inference(resolution,[],[f358,f272]) ).
fof(f378,definition,
( spl4_8
<=> sF1 = non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2)) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f379,plain,
( sF1 != non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2))
| spl4_8 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f380,plain,
( sF1 = non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2))
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f382,definition,
( spl4_9
<=> sF0 = non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2)) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f383,plain,
( sF0 != non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2))
| spl4_9 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f384,plain,
( sF0 = non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2))
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f385,plain,
( spl4_8
| spl4_9 ),
inference(avatar_split_clause,[],[f375,f382,f378]) ).
fof(f386,plain,
( sF0 = non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2))
| sF1 = non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2)) ),
inference(resolution,[],[f359,f272]) ).
fof(f389,definition,
( spl4_10
<=> sF1 = non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2)) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f390,plain,
( sF1 != non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2))
| spl4_10 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f391,plain,
( sF1 = non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2))
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f393,definition,
( spl4_11
<=> sF0 = non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2)) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f395,plain,
( sF0 = non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2))
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,plain,
( spl4_10
| spl4_11 ),
inference(avatar_split_clause,[],[f386,f393,f389]) ).
fof(f399,plain,
( ! [X0] :
( ~ member(X0,sF1)
| f6(f1(b,sF3),sF2) = X0
| f6(f1(b,sF3),sF2) = X0 )
| ~ spl4_8 ),
inference(superposition,[],[f5,f380]) ).
fof(f406,plain,
( ! [X0] :
( ~ member(X0,sF1)
| f6(f1(b,sF3),sF2) = X0 )
| ~ spl4_8 ),
inference(duplicate_literal_removal,[],[f399]) ).
fof(f499,plain,
( member(f7(f1(b,sF3),sF2),sF1)
| ~ little_set(f7(f1(b,sF3),sF2))
| ~ spl4_10 ),
inference(superposition,[],[f196,f391]) ).
fof(f514,plain,
( ~ member(f1(b,sF3),sF3)
| spl4_5 ),
inference(resolution,[],[f366,f285]) ).
fof(f515,plain,
( $false
| spl4_5 ),
inference(forward_subsumption_resolution,[],[f514,f336]) ).
fof(f516,plain,
spl4_5,
inference(avatar_contradiction_clause,[],[f515]) ).
fof(f517,plain,
( member(f7(f1(b,sF3),sF2),sF1)
| ~ spl4_5
| ~ spl4_10 ),
inference(forward_subsumption_resolution,[],[f499,f365]) ).
fof(f518,plain,
( b = f6(f1(b,sF3),sF2)
| ~ spl4_8 ),
inference(resolution,[],[f406,f244]) ).
fof(f519,plain,
( a = f6(f1(b,sF3),sF2)
| ~ spl4_8 ),
inference(resolution,[],[f406,f230]) ).
fof(f522,plain,
( a = b
| ~ spl4_8 ),
inference(forward_demodulation,[],[f518,f519]) ).
fof(f524,plain,
( non_ordered_pair(a,a) = sF1
| ~ spl4_8 ),
inference(superposition,[],[f212,f522]) ).
fof(f533,plain,
( ~ member(f1(a,sF3),a)
| ~ spl4_8 ),
inference(superposition,[],[f340,f522]) ).
fof(f539,plain,
( sF1 = non_ordered_pair(f6(f1(a,sF3),sF2),f6(f1(a,sF3),sF2))
| ~ spl4_8 ),
inference(superposition,[],[f380,f522]) ).
fof(f552,plain,
( sF0 = sF1
| ~ spl4_8 ),
inference(forward_demodulation,[],[f524,f210]) ).
fof(f725,definition,
( spl4_28
<=> b = f7(f1(b,sF3),sF2) ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f727,plain,
( b = f7(f1(b,sF3),sF2)
| ~ spl4_28 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f739,plain,
( sF2 = non_ordered_pair(sF0,non_ordered_pair(f6(f1(b,sF3),sF2),f7(f1(b,sF3),sF2)))
| ~ spl4_9 ),
inference(superposition,[],[f338,f384]) ).
fof(f740,plain,
( ! [X0] :
( ~ member(X0,sF0)
| f6(f1(b,sF3),sF2) = X0
| f6(f1(b,sF3),sF2) = X0 )
| ~ spl4_9 ),
inference(superposition,[],[f5,f384]) ).
fof(f747,plain,
( ! [X0] :
( ~ member(X0,sF0)
| f6(f1(b,sF3),sF2) = X0 )
| ~ spl4_9 ),
inference(duplicate_literal_removal,[],[f740]) ).
fof(f760,plain,
( a = f6(f1(b,sF3),sF2)
| ~ spl4_9 ),
inference(resolution,[],[f747,f231]) ).
fof(f848,plain,
( a = f7(f1(b,sF3),sF2)
| b = f7(f1(b,sF3),sF2)
| ~ spl4_5
| ~ spl4_10 ),
inference(resolution,[],[f517,f271]) ).
fof(f851,definition,
( spl4_34
<=> a = f7(f1(b,sF3),sF2) ),
introduced(definition,[new_symbols(definition,[spl4_34])],[avatar_definition]) ).
fof(f853,plain,
( a = f7(f1(b,sF3),sF2)
| ~ spl4_34 ),
inference(avatar_component_clause,[],[f851]) ).
fof(f854,plain,
( spl4_28
| spl4_34
| ~ spl4_5
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f848,f389,f364,f851,f725]) ).
fof(f855,plain,
( sF2 = non_ordered_pair(non_ordered_pair(f6(f1(b,sF3),sF2),f6(f1(b,sF3),sF2)),non_ordered_pair(f6(f1(b,sF3),sF2),a))
| ~ spl4_34 ),
inference(superposition,[],[f338,f853]) ).
fof(f862,plain,
( member(f1(b,sF3),a)
| ~ member(f1(b,sF3),second(sF2))
| ~ spl4_34 ),
inference(superposition,[],[f28,f853]) ).
fof(f863,plain,
( ~ member(f1(b,sF3),sF3)
| member(f1(b,sF3),a)
| ~ spl4_34 ),
inference(forward_demodulation,[],[f862,f216]) ).
fof(f866,plain,
( sF2 = non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,a))
| ~ spl4_9
| ~ spl4_34 ),
inference(forward_demodulation,[],[f855,f760]) ).
fof(f867,plain,
( member(f1(b,sF3),a)
| ~ spl4_34 ),
inference(forward_subsumption_resolution,[],[f863,f336]) ).
fof(f870,plain,
( sF2 = non_ordered_pair(sF0,sF0)
| ~ spl4_9
| ~ spl4_34 ),
inference(forward_demodulation,[],[f866,f210]) ).
fof(f880,plain,
( ! [X0] :
( ~ member(X0,sF2)
| sF0 = X0
| sF0 = X0 )
| ~ spl4_9
| ~ spl4_34 ),
inference(superposition,[],[f5,f870]) ).
fof(f887,plain,
( ! [X0] :
( ~ member(X0,sF2)
| sF0 = X0 )
| ~ spl4_9
| ~ spl4_34 ),
inference(duplicate_literal_removal,[],[f880]) ).
fof(f891,plain,
( sF0 = sF1
| ~ spl4_4
| ~ spl4_9
| ~ spl4_34 ),
inference(resolution,[],[f887,f242]) ).
fof(f925,plain,
( non_ordered_pair(a,a) != sF1
| spl4_8
| ~ spl4_9 ),
inference(superposition,[],[f379,f760]) ).
fof(f926,plain,
( sF0 != sF1
| spl4_8
| ~ spl4_9 ),
inference(superposition,[],[f379,f384]) ).
fof(f941,plain,
( non_ordered_pair(a,a) != sF0
| ~ spl4_4
| spl4_8
| ~ spl4_9
| ~ spl4_34 ),
inference(forward_demodulation,[],[f925,f891]) ).
fof(f948,plain,
( $false
| ~ spl4_4
| spl4_8
| ~ spl4_9
| ~ spl4_34 ),
inference(forward_subsumption_resolution,[],[f941,f210]) ).
fof(f949,plain,
( ~ spl4_4
| spl4_8
| ~ spl4_9
| ~ spl4_34 ),
inference(avatar_contradiction_clause,[],[f948]) ).
fof(f955,plain,
( sF0 = non_ordered_pair(a,f7(f1(b,sF3),sF2))
| ~ spl4_9
| ~ spl4_11 ),
inference(forward_demodulation,[],[f395,f760]) ).
fof(f956,plain,
( sF2 = non_ordered_pair(sF0,non_ordered_pair(a,f7(f1(b,sF3),sF2)))
| ~ spl4_9 ),
inference(forward_demodulation,[],[f739,f760]) ).
fof(f960,plain,
( sF2 = non_ordered_pair(sF0,sF0)
| ~ spl4_9
| ~ spl4_11 ),
inference(forward_demodulation,[],[f956,f955]) ).
fof(f1024,plain,
( ! [X0] :
( ~ member(X0,sF2)
| sF0 = X0
| sF0 = X0 )
| ~ spl4_9
| ~ spl4_11 ),
inference(superposition,[],[f5,f960]) ).
fof(f1031,plain,
( ! [X0] :
( ~ member(X0,sF2)
| sF0 = X0 )
| ~ spl4_9
| ~ spl4_11 ),
inference(duplicate_literal_removal,[],[f1024]) ).
fof(f1035,plain,
( sF0 = sF1
| ~ spl4_4
| ~ spl4_9
| ~ spl4_11 ),
inference(resolution,[],[f1031,f242]) ).
fof(f1044,plain,
( $false
| ~ spl4_4
| spl4_8
| ~ spl4_9
| ~ spl4_11 ),
inference(forward_subsumption_resolution,[],[f1035,f926]) ).
fof(f1045,plain,
( ~ spl4_4
| spl4_8
| ~ spl4_9
| ~ spl4_11 ),
inference(avatar_contradiction_clause,[],[f1044]) ).
fof(f1064,plain,
( member(f1(b,sF3),b)
| ~ member(f1(b,sF3),second(sF2))
| ~ spl4_28 ),
inference(superposition,[],[f28,f727]) ).
fof(f1065,plain,
( ~ member(f1(b,sF3),second(sF2))
| ~ spl4_28 ),
inference(forward_subsumption_resolution,[],[f1064,f340]) ).
fof(f1068,plain,
( ~ member(f1(b,sF3),sF3)
| ~ spl4_28 ),
inference(forward_demodulation,[],[f1065,f216]) ).
fof(f1071,plain,
( $false
| ~ spl4_28 ),
inference(forward_subsumption_resolution,[],[f1068,f336]) ).
fof(f1072,plain,
~ spl4_28,
inference(avatar_contradiction_clause,[],[f1071]) ).
fof(f1092,plain,
( sF1 != non_ordered_pair(a,f7(f1(b,sF3),sF2))
| ~ spl4_9
| spl4_10 ),
inference(forward_demodulation,[],[f390,f760]) ).
fof(f1102,plain,
( sF0 != sF1
| ~ spl4_9
| spl4_10
| ~ spl4_11 ),
inference(forward_demodulation,[],[f1092,f955]) ).
fof(f1106,plain,
( $false
| ~ spl4_8
| ~ spl4_9
| spl4_10
| ~ spl4_11 ),
inference(forward_subsumption_resolution,[],[f1102,f552]) ).
fof(f1107,plain,
( ~ spl4_8
| ~ spl4_9
| spl4_10
| ~ spl4_11 ),
inference(avatar_contradiction_clause,[],[f1106]) ).
fof(f1213,plain,
( member(f1(a,sF3),a)
| ~ spl4_8
| ~ spl4_34 ),
inference(superposition,[],[f867,f522]) ).
fof(f1214,plain,
( $false
| ~ spl4_8
| ~ spl4_34 ),
inference(forward_subsumption_resolution,[],[f1213,f533]) ).
fof(f1215,plain,
( ~ spl4_8
| ~ spl4_34 ),
inference(avatar_contradiction_clause,[],[f1214]) ).
fof(f1216,plain,
( sF0 != non_ordered_pair(f6(f1(a,sF3),sF2),f6(f1(a,sF3),sF2))
| ~ spl4_8
| spl4_9 ),
inference(forward_demodulation,[],[f383,f522]) ).
fof(f1232,plain,
( sF0 != sF1
| ~ spl4_8
| spl4_9 ),
inference(forward_demodulation,[],[f1216,f539]) ).
fof(f1244,plain,
( $false
| ~ spl4_8
| spl4_9 ),
inference(forward_subsumption_resolution,[],[f1232,f552]) ).
fof(f1245,plain,
( ~ spl4_8
| spl4_9 ),
inference(avatar_contradiction_clause,[],[f1244]) ).
cnf(s2,plain,
( ~ spl4_3
| spl4_4 ),
inference(sat_conversion,[],[f243]) ).
cnf(s3,plain,
spl4_3,
inference(sat_conversion,[],[f263]) ).
cnf(s6,plain,
( spl4_8
| spl4_9 ),
inference(sat_conversion,[],[f385]) ).
cnf(s7,plain,
( spl4_10
| spl4_11 ),
inference(sat_conversion,[],[f396]) ).
cnf(s20,plain,
spl4_5,
inference(sat_conversion,[],[f516]) ).
cnf(s34,plain,
( ~ spl4_5
| ~ spl4_10
| spl4_28
| spl4_34 ),
inference(sat_conversion,[],[f854]) ).
cnf(s39,plain,
( ~ spl4_4
| spl4_8
| ~ spl4_9
| ~ spl4_34 ),
inference(sat_conversion,[],[f949]) ).
cnf(s44,plain,
( ~ spl4_4
| spl4_8
| ~ spl4_9
| ~ spl4_11 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s46,plain,
~ spl4_28,
inference(sat_conversion,[],[f1072]) ).
cnf(s49,plain,
( ~ spl4_8
| ~ spl4_9
| spl4_10
| ~ spl4_11 ),
inference(sat_conversion,[],[f1107]) ).
cnf(s51,plain,
( ~ spl4_8
| ~ spl4_34 ),
inference(sat_conversion,[],[f1215]) ).
cnf(s53,plain,
( ~ spl4_8
| spl4_9 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s55,plain,
( ~ spl4_5
| ~ spl4_10
| spl4_34 ),
inference(rat,[],[s34,s46]) ).
cnf(s60,plain,
spl4_4,
inference(rat,[],[s2,s3]) ).
cnf(s66,plain,
( ~ spl4_9
| spl4_8 ),
inference(rat,[],[s55,s7,s39,s44,s60,s20]) ).
cnf(s67,plain,
spl4_8,
inference(rat,[],[s66,s6]) ).
cnf(s68,plain,
spl4_9,
inference(rat,[],[s53,s67]) ).
cnf(s69,plain,
~ spl4_34,
inference(rat,[],[s51,s67]) ).
cnf(s76,plain,
~ spl4_10,
inference(rat,[],[s55,s20,s69]) ).
cnf(s77,plain,
spl4_11,
inference(rat,[],[s7,s76]) ).
cnf(s78,plain,
$false,
inference(rat,[],[s49,s68,s67,s76,s77]) ).
fof(f1255,plain,
$false,
inference(avatar_sat_refutation,[],[s78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET021-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n018.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 00:11:39 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 6.85/2.02 % (2872398)Input is clausal, will run a generic CNF schedule.
% 6.85/2.02 % (2872407)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2301519673:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.85/2.02 % (2872407)Refutation not found, incomplete strategy
% 6.85/2.02 % (2872407)------------------------------
% 6.85/2.02 % (2872407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872407)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872407)Termination reason: Refutation not found, incomplete strategy
% 6.85/2.02 % (2872407)Time elapsed: 0.001 s
% 6.85/2.02 % (2872407)Peak memory usage: 88 MB
% 6.85/2.02 % (2872407)Instructions burned: 1 (million)
% 6.85/2.02 % (2872405)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1150290689:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.85/2.02 % (2872404)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1659377463:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.85/2.02 % (2872406)lrs+10_1_sil=8000:sp=occurrence:random_seed=3736064525:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.85/2.02 % (2872403)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=739995669:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.85/2.02 % (2872406)Refutation not found, incomplete strategy
% 6.85/2.02 % (2872406)------------------------------
% 6.85/2.02 % (2872406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872406)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872406)Termination reason: Refutation not found, incomplete strategy
% 6.85/2.02 % (2872406)Time elapsed: 0.001 s
% 6.85/2.02 % (2872406)Peak memory usage: 87 MB
% 6.85/2.02 % (2872409)dis-21_1_sil=8000:lcm=predicate:random_seed=4044253262: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)
% 6.85/2.02 % (2872408)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2041794191:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.85/2.02 % (2872409)Instruction limit reached!
% 6.85/2.02 % (2872409)------------------------------
% 6.85/2.02 % (2872409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872409)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872409)Termination reason: Instruction limit
% 6.85/2.02 % (2872409)Termination phase: Saturation
% 6.85/2.02 % (2872409)Time elapsed: 0.073 s
% 6.85/2.02 % (2872409)Peak memory usage: 89 MB
% 6.85/2.02 % (2872409)Instructions burned: 118 (million)
% 6.85/2.02 % (2872407)------------------------------
% 6.85/2.02 % (2872407)------------------------------
% 6.85/2.02 % (2872408)Instruction limit reached!
% 6.85/2.02 % (2872408)------------------------------
% 6.85/2.02 % (2872408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872408)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872408)Termination reason: Instruction limit
% 6.85/2.02 % (2872408)Termination phase: Saturation
% 6.85/2.02 % (2872408)Time elapsed: 0.120 s
% 6.85/2.02 % (2872408)Peak memory usage: 90 MB
% 6.85/2.02 % (2872408)Instructions burned: 181 (million)
% 6.85/2.02 % (2872418)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=122637112: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)
% 6.85/2.02 % (2872417)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=4220487430:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.85/2.02 % (2872417)Refutation not found, incomplete strategy
% 6.85/2.02 % (2872417)------------------------------
% 6.85/2.02 % (2872417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872417)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872417)Termination reason: Refutation not found, incomplete strategy
% 6.85/2.02 % (2872417)Time elapsed: 0.001 s
% 6.85/2.02 % (2872417)Peak memory usage: 88 MB
% 6.85/2.02 % (2872406)------------------------------
% 6.85/2.02 % (2872406)------------------------------
% 6.85/2.02 % (2872418)Instruction limit reached!
% 6.85/2.02 % (2872418)------------------------------
% 6.85/2.02 % (2872418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872418)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872418)Termination reason: Instruction limit
% 6.85/2.02 % (2872418)Termination phase: Saturation
% 6.85/2.02 % (2872418)Time elapsed: 0.057 s
% 6.85/2.02 % (2872418)Peak memory usage: 91 MB
% 6.85/2.02 % (2872418)Instructions burned: 192 (million)
% 6.85/2.02 % (2872419)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4206209904:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 6.85/2.02 % (2872419)Refutation not found, incomplete strategy
% 6.85/2.02 % (2872419)------------------------------
% 6.85/2.02 % (2872419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872419)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872419)Termination reason: Refutation not found, incomplete strategy
% 6.85/2.02 % (2872419)Time elapsed: 0.003 s
% 6.85/2.02 % (2872419)Peak memory usage: 88 MB
% 6.85/2.02 % (2872419)Instructions burned: 3 (million)
% 6.85/2.02 % (2872422)lrs+10_64_to=lpo:sil=8000:random_seed=4279437828:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.85/2.02 % (2872423)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3830317809:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.85/2.02 % (2872423)Instruction limit reached!
% 6.85/2.02 % (2872423)------------------------------
% 6.85/2.02 % (2872423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872423)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872423)Termination reason: Instruction limit
% 6.85/2.02 % (2872423)Termination phase: Saturation
% 6.85/2.02 % (2872423)Time elapsed: 0.064 s
% 6.85/2.02 % (2872423)Peak memory usage: 89 MB
% 6.85/2.02 % (2872423)Instructions burned: 196 (million)
% 6.85/2.02 % (2872417)------------------------------
% 6.85/2.02 % (2872417)------------------------------
% 6.85/2.02 % (2872422)Instruction limit reached!
% 6.85/2.02 % (2872422)------------------------------
% 6.85/2.02 % (2872422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872422)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872422)Termination reason: Instruction limit
% 6.85/2.02 % (2872422)Termination phase: Saturation
% 6.85/2.02 % (2872422)Time elapsed: 0.074 s
% 6.85/2.02 % (2872422)Peak memory usage: 90 MB
% 6.85/2.02 % (2872422)Instructions burned: 126 (million)
% 6.85/2.02 % (2872419)------------------------------
% 6.85/2.02 % (2872419)------------------------------
% 6.85/2.02 % (2872427)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4039926928:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 6.85/2.02 % (2872429)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=2503618972:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 6.85/2.02 % (2872428)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=933002328:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 6.85/2.02 % (2872429)Refutation not found, incomplete strategy
% 6.85/2.02 % (2872429)------------------------------
% 6.85/2.02 % (2872429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872429)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872429)Termination reason: Refutation not found, incomplete strategy
% 6.85/2.02 % (2872429)Time elapsed: 0.002 s
% 6.85/2.02 % (2872429)Peak memory usage: 88 MB
% 6.85/2.02 % (2872429)Instructions burned: 1 (million)
% 6.85/2.02 % (2872427)Instruction limit reached!
% 6.85/2.02 % (2872427)------------------------------
% 6.85/2.02 % (2872427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872427)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872427)Termination reason: Instruction limit
% 6.85/2.02 % (2872427)Termination phase: Saturation
% 6.85/2.02 % (2872427)Time elapsed: 0.055 s
% 6.85/2.02 % (2872427)Peak memory usage: 91 MB
% 6.85/2.02 % (2872427)Instructions burned: 158 (million)
% 6.85/2.02 % (2872430)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2932825526:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 6.85/2.02 % (2872403)First to succeed.
% 6.85/2.02 % (2872403)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2872398"
% 6.85/2.02 % (2872434)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3121727066:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 6.85/2.02 % (2872430)Instruction limit reached!
% 6.85/2.02 % (2872430)------------------------------
% 6.85/2.02 % (2872430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872430)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872430)Termination reason: Instruction limit
% 6.85/2.02 % (2872430)Termination phase: Saturation
% 6.85/2.02 % (2872430)Time elapsed: 0.076 s
% 6.85/2.02 % (2872430)Peak memory usage: 89 MB
% 6.85/2.02 % (2872430)Instructions burned: 107 (million)
% 6.85/2.02 % (2872434)Instruction limit reached!
% 6.85/2.02 % (2872434)------------------------------
% 6.85/2.02 % (2872434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872434)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872434)Termination reason: Instruction limit
% 6.85/2.02 % (2872434)Termination phase: Saturation
% 6.85/2.02 % (2872434)Time elapsed: 0.083 s
% 6.85/2.02 % (2872434)Peak memory usage: 90 MB
% 6.85/2.02 % (2872434)Instructions burned: 243 (million)
% 6.85/2.02 % (2872429)------------------------------
% 6.85/2.02 % (2872429)------------------------------
% 6.85/2.02 % (2872437)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3283377547:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 6.85/2.02 % (2872438)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4096121444:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 6.85/2.02 % (2872438)Refutation not found, incomplete strategy
% 6.85/2.02 % (2872438)------------------------------
% 6.85/2.02 % (2872438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.85/2.02 % (2872438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.85/2.02 % (2872438)CaDiCaL version: 2.1.3
% 6.85/2.02 % (2872438)Termination reason: Refutation not found, incomplete strategy
% 6.85/2.02 % (2872438)Time elapsed: 0.001 s
% 6.85/2.02 % (2872438)Peak memory usage: 88 MB
% 6.85/2.02 % (2872403)Refutation found. Thanks to Tanya!
% 6.85/2.02 % SZS status Unsatisfiable for theBenchmark
% 6.85/2.02 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/2.20 % (2872403)------------------------------
% 0.17/2.20 % (2872403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/2.20 % (2872403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/2.20 % (2872403)CaDiCaL version: 2.1.3
% 0.17/2.20 % (2872403)Termination reason: Refutation
% 0.17/2.20 % (2872403)Time elapsed: 0.735 s
% 0.17/2.20 % (2872403)Peak memory usage: 130 MB
% 0.17/2.20 % (2872403)Instructions burned: 1086 (million)
% 0.17/2.20 % (2872403)------------------------------
% 0.17/2.20 % (2872403)------------------------------
% 0.17/2.20 % (2872398)Success in time 1.154 s
% 0.17/2.20 % Vampire exiting
%------------------------------------------------------------------------------