%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET020-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 : n017.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 4.97s 1.62s
% Output : Refutation 5.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 27
% Syntax : Number of formulae : 135 ( 30 unt; 11 def)
% Number of atoms : 400 ( 85 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 513 ( 248 ~; 258 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 153 ( 0 sgn 153 !; 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(f17,axiom,
! [X0,X1] :
( little_set(f4(X0,X1))
| ~ member(X0,first(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first1) ).
fof(f18,axiom,
! [X0,X1] :
( little_set(f5(X0,X1))
| ~ member(X0,first(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first2) ).
fof(f19,axiom,
! [X0,X1] :
( ~ member(X0,first(X1))
| X1 = ordered_pair(f4(X0,X1),f5(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first3) ).
fof(f20,plain,
! [X0,X1] :
( ~ member(X0,first(X1))
| ordered_pair(f4(X0,X1),f5(X0,X1)) = X1 ),
inference(reorient_equations,[],[f19]) ).
fof(f21,axiom,
! [X0,X1] :
( member(X0,f4(X0,X1))
| ~ member(X0,first(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first4) ).
fof(f22,axiom,
! [X2,X3,X0,X1] :
( member(X0,first(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3)
| ~ member(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first5) ).
fof(f23,plain,
! [X2,X3,X0,X1] :
( member(X0,first(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| ordered_pair(X2,X3) != X1
| ~ member(X0,X2) ),
inference(reorient_equations,[],[f22]) ).
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,
first(ordered_pair(a,b)) != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_first_is_first) ).
fof(f165,plain,
a != first(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(f171,plain,
! [X0,X1] :
( non_ordered_pair(non_ordered_pair(f4(X0,X1),f4(X0,X1)),non_ordered_pair(f4(X0,X1),f5(X0,X1))) = X1
| ~ member(X0,first(X1)) ),
inference(definition_unfolding,[],[f20,f167]) ).
fof(f172,plain,
! [X2,X3,X0,X1] :
( member(X0,first(X1))
| ~ little_set(X2)
| ~ little_set(X3)
| non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3)) != X1
| ~ member(X0,X2) ),
inference(definition_unfolding,[],[f23,f167]) ).
fof(f194,plain,
a != first(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(f198,plain,
! [X2,X3,X0] :
( member(X0,first(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3))))
| ~ little_set(X2)
| ~ little_set(X3)
| ~ member(X0,X2) ),
inference(equality_resolution,[],[f172]) ).
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 = first(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f216,plain,
first(sF2) = sF3,
inference(reorient_equations,[],[f215]) ).
fof(f217,plain,
a != sF3,
inference(definition_folding,[],[f194,f216,f214,f212,f210]) ).
fof(f220,plain,
( member(a,sF0)
| ~ little_set(a) ),
inference(superposition,[],[f195,f210]) ).
fof(f221,plain,
( member(a,sF1)
| ~ little_set(a) ),
inference(superposition,[],[f195,f212]) ).
fof(f222,plain,
member(a,sF1),
inference(forward_subsumption_resolution,[],[f221,f162]) ).
fof(f223,plain,
member(a,sF0),
inference(forward_subsumption_resolution,[],[f220,f162]) ).
fof(f225,plain,
( member(b,sF1)
| ~ little_set(b) ),
inference(superposition,[],[f196,f212]) ).
fof(f226,plain,
member(b,sF1),
inference(forward_subsumption_resolution,[],[f225,f163]) ).
fof(f233,plain,
! [X0,X1] :
( member(non_ordered_pair(f4(X1,X0),f4(X1,X0)),X0)
| ~ little_set(non_ordered_pair(f4(X1,X0),f4(X1,X0)))
| ~ member(X1,first(X0)) ),
inference(superposition,[],[f195,f171]) ).
fof(f235,plain,
! [X0,X1] :
( member(non_ordered_pair(f4(X1,X0),f4(X1,X0)),X0)
| ~ member(X1,first(X0)) ),
inference(forward_subsumption_resolution,[],[f233,f8]) ).
fof(f239,plain,
! [X0] :
( member(X0,first(non_ordered_pair(non_ordered_pair(a,a),sF1)))
| ~ little_set(a)
| ~ little_set(b)
| ~ member(X0,a) ),
inference(superposition,[],[f198,f212]) ).
fof(f242,plain,
! [X2,X0,X1] :
( member(X1,first(X0))
| ~ little_set(f4(X2,X0))
| ~ little_set(f5(X2,X0))
| ~ member(X1,f4(X2,X0))
| ~ member(X2,first(X0)) ),
inference(superposition,[],[f198,f171]) ).
fof(f244,plain,
! [X2,X0,X1] :
( member(X1,first(X0))
| ~ little_set(f5(X2,X0))
| ~ member(X1,f4(X2,X0))
| ~ member(X2,first(X0)) ),
inference(forward_subsumption_resolution,[],[f242,f17]) ).
fof(f247,plain,
! [X0] :
( member(X0,first(non_ordered_pair(non_ordered_pair(a,a),sF1)))
| ~ little_set(b)
| ~ member(X0,a) ),
inference(forward_subsumption_resolution,[],[f239,f162]) ).
fof(f250,plain,
! [X2,X0,X1] :
( ~ member(X1,f4(X2,X0))
| member(X1,first(X0))
| ~ member(X2,first(X0)) ),
inference(forward_subsumption_resolution,[],[f244,f18]) ).
fof(f253,plain,
! [X0] :
( member(X0,first(non_ordered_pair(non_ordered_pair(a,a),sF1)))
| ~ member(X0,a) ),
inference(forward_subsumption_resolution,[],[f247,f163]) ).
fof(f254,plain,
! [X0] :
( member(X0,first(non_ordered_pair(sF0,sF1)))
| ~ member(X0,a) ),
inference(forward_demodulation,[],[f253,f210]) ).
fof(f255,plain,
! [X0] :
( member(X0,first(sF2))
| ~ member(X0,a) ),
inference(forward_demodulation,[],[f254,f214]) ).
fof(f256,plain,
! [X0] :
( member(X0,sF3)
| ~ member(X0,a) ),
inference(forward_demodulation,[],[f255,f216]) ).
fof(f269,plain,
! [X0] :
( ~ member(X0,sF2)
| sF0 = X0
| sF1 = X0 ),
inference(superposition,[],[f5,f214]) ).
fof(f319,plain,
! [X0] :
( ~ member(f1(X0,sF3),a)
| sF3 = X0
| ~ member(f1(X0,sF3),X0) ),
inference(resolution,[],[f4,f256]) ).
fof(f337,plain,
! [X0] :
( sF0 = non_ordered_pair(f4(X0,sF2),f4(X0,sF2))
| sF1 = non_ordered_pair(f4(X0,sF2),f4(X0,sF2))
| ~ member(X0,first(sF2)) ),
inference(resolution,[],[f269,f235]) ).
fof(f340,plain,
! [X0] :
( sF1 = non_ordered_pair(f4(X0,sF2),f4(X0,sF2))
| sF0 = non_ordered_pair(f4(X0,sF2),f4(X0,sF2))
| ~ member(X0,sF3) ),
inference(forward_demodulation,[],[f337,f216]) ).
fof(f368,plain,
! [X0,X1] :
( ~ member(X0,sF1)
| f4(X1,sF2) = X0
| f4(X1,sF2) = X0
| sF0 = non_ordered_pair(f4(X1,sF2),f4(X1,sF2))
| ~ member(X1,sF3) ),
inference(superposition,[],[f5,f340]) ).
fof(f377,plain,
! [X0,X1] :
( sF0 = non_ordered_pair(f4(X1,sF2),f4(X1,sF2))
| f4(X1,sF2) = X0
| ~ member(X0,sF1)
| ~ member(X1,sF3) ),
inference(duplicate_literal_removal,[],[f368]) ).
fof(f383,definition,
( spl4_2
<=> sF0 = sF1 ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f384,plain,
( sF0 = sF1
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f385,plain,
( sF0 != sF1
| spl4_2 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f445,definition,
( spl4_7
<=> ! [X0] : ~ member(X0,sF3) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f446,plain,
( ! [X0] : ~ member(X0,sF3)
| ~ spl4_7 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f476,plain,
! [X2,X0,X1] :
( ~ member(X0,sF0)
| f4(X1,sF2) = X0
| f4(X1,sF2) = X0
| f4(X1,sF2) = X2
| ~ member(X2,sF1)
| ~ member(X1,sF3) ),
inference(superposition,[],[f5,f377]) ).
fof(f485,plain,
! [X2,X0,X1] :
( f4(X1,sF2) = X2
| f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X2,sF1)
| ~ member(X1,sF3) ),
inference(duplicate_literal_removal,[],[f476]) ).
fof(f501,plain,
! [X0,X1] :
( f4(X1,sF2) != f4(X1,sF2)
| f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X0,sF1)
| ~ member(X1,sF3) ),
inference(equality_factoring,[],[f485]) ).
fof(f502,plain,
! [X0,X1] :
( f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X0,sF1)
| ~ member(X1,sF3) ),
inference(trivial_inequality_removal,[],[f501]) ).
fof(f521,definition,
( spl4_8
<=> ! [X2,X1] :
( ~ member(X1,sF3)
| ~ member(X2,sF0)
| f4(X1,sF2) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f522,plain,
( ! [X2,X1] :
( f4(X1,sF2) = X2
| ~ member(X2,sF0)
| ~ member(X1,sF3) )
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f611,plain,
( ! [X0] :
( member(f1(X0,sF3),X0)
| sF3 = X0 )
| ~ spl4_7 ),
inference(resolution,[],[f446,f3]) ).
fof(f616,plain,
( a = sF3
| a = sF3
| ~ member(f1(a,sF3),a)
| ~ spl4_7 ),
inference(resolution,[],[f611,f319]) ).
fof(f626,plain,
( a = sF3
| ~ member(f1(a,sF3),a)
| ~ spl4_7 ),
inference(duplicate_literal_removal,[],[f616]) ).
fof(f663,plain,
( a = sF3
| ~ spl4_7 ),
inference(forward_subsumption_resolution,[],[f626,f611]) ).
fof(f664,plain,
( $false
| ~ spl4_7 ),
inference(forward_subsumption_resolution,[],[f663,f217]) ).
fof(f665,plain,
~ spl4_7,
inference(avatar_contradiction_clause,[],[f664]) ).
fof(f669,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| ~ member(X2,sF0)
| ~ member(X2,sF1)
| ~ member(X1,sF3)
| f4(X1,sF2) = X3
| ~ member(X3,sF0)
| ~ member(X0,sF1)
| ~ member(X1,sF3) ),
inference(superposition,[],[f502,f485]) ).
fof(f685,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| ~ member(X2,sF0)
| ~ member(X2,sF1)
| ~ member(X1,sF3)
| f4(X1,sF2) = X3
| ~ member(X3,sF0)
| ~ member(X0,sF1) ),
inference(duplicate_literal_removal,[],[f669]) ).
fof(f696,definition,
( spl4_30
<=> ! [X2,X0] :
( X0 = X2
| ~ member(X0,sF1)
| ~ member(X2,sF1)
| ~ member(X2,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl4_30])],[avatar_definition]) ).
fof(f697,plain,
( ! [X2,X0] :
( ~ member(X2,sF1)
| ~ member(X0,sF1)
| X0 = X2
| ~ member(X2,sF0) )
| ~ spl4_30 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f698,plain,
( spl4_8
| spl4_30 ),
inference(avatar_split_clause,[],[f685,f696,f521]) ).
fof(f922,plain,
( ! [X0] :
( ~ member(X0,sF1)
| a = X0
| ~ member(a,sF0) )
| ~ spl4_30 ),
inference(resolution,[],[f697,f222]) ).
fof(f923,plain,
( ! [X0] :
( ~ member(X0,sF1)
| a = X0 )
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f922,f223]) ).
fof(f1040,plain,
( a = b
| ~ spl4_30 ),
inference(resolution,[],[f226,f923]) ).
fof(f1053,plain,
( sF0 = non_ordered_pair(b,b)
| ~ spl4_30 ),
inference(backward_demodulation,[],[f210,f1040]) ).
fof(f1054,plain,
( sF1 = non_ordered_pair(b,b)
| ~ spl4_30 ),
inference(backward_demodulation,[],[f212,f1040]) ).
fof(f1097,plain,
( sF0 = sF1
| ~ spl4_30 ),
inference(backward_demodulation,[],[f1054,f1053]) ).
fof(f1100,plain,
( $false
| spl4_2
| ~ spl4_30 ),
inference(forward_subsumption_resolution,[],[f1097,f385]) ).
fof(f1101,plain,
( spl4_2
| ~ spl4_30 ),
inference(avatar_contradiction_clause,[],[f1100]) ).
fof(f1373,plain,
( ! [X0,X1] :
( ~ member(X0,sF0)
| f4(X1,sF2) = X0
| ~ member(X0,sF0)
| ~ member(X1,sF3) )
| ~ spl4_2 ),
inference(backward_demodulation,[],[f502,f384]) ).
fof(f1434,plain,
( ! [X0,X1] :
( ~ member(X0,sF0)
| f4(X1,sF2) = X0
| ~ member(X1,sF3) )
| ~ spl4_2 ),
inference(duplicate_literal_removal,[],[f1373]) ).
fof(f1458,plain,
( spl4_8
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f1434,f383,f521]) ).
fof(f1481,definition,
( spl4_60
<=> ! [X1] : ~ member(X1,sF0) ),
introduced(definition,[new_symbols(definition,[spl4_60])],[avatar_definition]) ).
fof(f1482,plain,
( ! [X1] : ~ member(X1,sF0)
| ~ spl4_60 ),
inference(avatar_component_clause,[],[f1481]) ).
fof(f1560,plain,
( ! [X0,X1] :
( member(X1,X0)
| ~ member(X1,first(sF2))
| ~ member(X0,sF0)
| ~ member(X1,sF3) )
| ~ spl4_8 ),
inference(superposition,[],[f21,f522]) ).
fof(f1573,plain,
( ! [X0,X1] :
( ~ member(X1,sF3)
| member(X1,X0)
| ~ member(X0,sF0)
| ~ member(X1,sF3) )
| ~ spl4_8 ),
inference(forward_demodulation,[],[f1560,f216]) ).
fof(f1574,plain,
( ! [X0,X1] :
( member(X1,X0)
| ~ member(X1,sF3)
| ~ member(X0,sF0) )
| ~ spl4_8 ),
inference(duplicate_literal_removal,[],[f1573]) ).
fof(f2047,plain,
( ! [X2,X0,X1] :
( ~ member(X1,X0)
| member(X1,first(sF2))
| ~ member(X2,first(sF2))
| ~ member(X0,sF0)
| ~ member(X2,sF3) )
| ~ spl4_8 ),
inference(superposition,[],[f250,f522]) ).
fof(f2049,plain,
( ! [X2,X0,X1] :
( member(X1,sF3)
| ~ member(X1,X0)
| ~ member(X2,first(sF2))
| ~ member(X0,sF0)
| ~ member(X2,sF3) )
| ~ spl4_8 ),
inference(forward_demodulation,[],[f2047,f216]) ).
fof(f2050,plain,
( ! [X2,X0,X1] :
( ~ member(X2,sF3)
| member(X1,sF3)
| ~ member(X1,X0)
| ~ member(X0,sF0)
| ~ member(X2,sF3) )
| ~ spl4_8 ),
inference(forward_demodulation,[],[f2049,f216]) ).
fof(f2051,plain,
( ! [X2,X0,X1] :
( ~ member(X2,sF3)
| member(X1,sF3)
| ~ member(X1,X0)
| ~ member(X0,sF0) )
| ~ spl4_8 ),
inference(duplicate_literal_removal,[],[f2050]) ).
fof(f2053,definition,
( spl4_67
<=> ! [X0,X1] :
( member(X1,sF3)
| ~ member(X0,sF0)
| ~ member(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_67])],[avatar_definition]) ).
fof(f2054,plain,
( ! [X0,X1] :
( member(X1,sF3)
| ~ member(X0,sF0)
| ~ member(X1,X0) )
| ~ spl4_67 ),
inference(avatar_component_clause,[],[f2053]) ).
fof(f2055,plain,
( spl4_67
| spl4_7
| ~ spl4_8 ),
inference(avatar_split_clause,[],[f2051,f521,f445,f2053]) ).
fof(f2059,plain,
( ! [X0,X1] :
( ~ member(f1(X1,sF3),X1)
| ~ member(f1(X1,sF3),X0)
| ~ member(X0,sF0)
| sF3 = X1 )
| ~ spl4_67 ),
inference(resolution,[],[f2054,f4]) ).
fof(f2062,plain,
( ! [X0,X1] :
( ~ member(f1(X0,sF3),X1)
| ~ member(X1,sF0)
| sF3 = X0
| ~ member(f1(X0,sF3),sF3)
| ~ member(X0,sF0) )
| ~ spl4_8
| ~ spl4_67 ),
inference(resolution,[],[f2059,f1574]) ).
fof(f2070,plain,
( ! [X0,X1] :
( ~ member(f1(X0,sF3),X1)
| ~ member(X1,sF0)
| sF3 = X0
| ~ member(X0,sF0) )
| ~ spl4_8
| ~ spl4_67 ),
inference(forward_subsumption_resolution,[],[f2062,f2054]) ).
fof(f2072,plain,
( ! [X0,X1] :
( ~ member(X0,sF0)
| sF3 = X1
| ~ member(X1,sF0)
| ~ member(f1(X1,sF3),sF3)
| ~ member(X0,sF0) )
| ~ spl4_8
| ~ spl4_67 ),
inference(resolution,[],[f2070,f1574]) ).
fof(f2082,plain,
( ! [X0,X1] :
( ~ member(X0,sF0)
| sF3 = X1
| ~ member(X1,sF0)
| ~ member(f1(X1,sF3),sF3) )
| ~ spl4_8
| ~ spl4_67 ),
inference(duplicate_literal_removal,[],[f2072]) ).
fof(f2094,definition,
( spl4_70
<=> ! [X1] :
( sF3 = X1
| ~ member(f1(X1,sF3),sF3)
| ~ member(X1,sF0) ) ),
introduced(definition,[new_symbols(definition,[spl4_70])],[avatar_definition]) ).
fof(f2095,plain,
( ! [X1] :
( ~ member(f1(X1,sF3),sF3)
| sF3 = X1
| ~ member(X1,sF0) )
| ~ spl4_70 ),
inference(avatar_component_clause,[],[f2094]) ).
fof(f2100,plain,
( spl4_70
| spl4_60
| ~ spl4_8
| ~ spl4_67 ),
inference(avatar_split_clause,[],[f2082,f2053,f521,f1481,f2094]) ).
fof(f2107,plain,
( $false
| ~ spl4_60 ),
inference(resolution,[],[f1482,f223]) ).
fof(f2108,plain,
~ spl4_60,
inference(avatar_contradiction_clause,[],[f2107]) ).
fof(f2109,plain,
( ! [X0] :
( sF3 = X0
| ~ member(X0,sF0)
| member(f1(X0,sF3),X0)
| sF3 = X0 )
| ~ spl4_70 ),
inference(resolution,[],[f2095,f3]) ).
fof(f2114,plain,
( ! [X0] :
( member(f1(X0,sF3),X0)
| ~ member(X0,sF0)
| sF3 = X0 )
| ~ spl4_70 ),
inference(duplicate_literal_removal,[],[f2109]) ).
fof(f2118,plain,
( ! [X0] :
( ~ member(X0,sF0)
| sF3 = X0
| ~ member(X0,sF0)
| sF3 = X0
| ~ member(X0,sF0) )
| ~ spl4_8
| ~ spl4_67
| ~ spl4_70 ),
inference(resolution,[],[f2114,f2070]) ).
fof(f2146,plain,
( ! [X0] :
( ~ member(X0,sF0)
| sF3 = X0 )
| ~ spl4_8
| ~ spl4_67
| ~ spl4_70 ),
inference(duplicate_literal_removal,[],[f2118]) ).
fof(f2160,plain,
( a = sF3
| ~ spl4_8
| ~ spl4_67
| ~ spl4_70 ),
inference(resolution,[],[f2146,f223]) ).
fof(f2161,plain,
( $false
| ~ spl4_8
| ~ spl4_67
| ~ spl4_70 ),
inference(forward_subsumption_resolution,[],[f2160,f217]) ).
fof(f2162,plain,
( ~ spl4_8
| ~ spl4_67
| ~ spl4_70 ),
inference(avatar_contradiction_clause,[],[f2161]) ).
cnf(s21,plain,
~ spl4_7,
inference(sat_conversion,[],[f665]) ).
cnf(s22,plain,
( spl4_8
| spl4_30 ),
inference(sat_conversion,[],[f698]) ).
cnf(s40,plain,
( spl4_2
| ~ spl4_30 ),
inference(sat_conversion,[],[f1101]) ).
cnf(s48,plain,
( ~ spl4_2
| spl4_8 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s60,plain,
( spl4_7
| ~ spl4_8
| spl4_67 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s63,plain,
( ~ spl4_8
| spl4_60
| ~ spl4_67
| spl4_70 ),
inference(sat_conversion,[],[f2100]) ).
cnf(s64,plain,
~ spl4_60,
inference(sat_conversion,[],[f2108]) ).
cnf(s66,plain,
( ~ spl4_8
| ~ spl4_67
| ~ spl4_70 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s67,plain,
( ~ spl4_8
| ~ spl4_67
| spl4_70 ),
inference(rat,[],[s63,s64]) ).
cnf(s81,plain,
( ~ spl4_67
| ~ spl4_8 ),
inference(rat,[],[s67,s66]) ).
cnf(s82,plain,
~ spl4_8,
inference(rat,[],[s81,s60,s21]) ).
cnf(s83,plain,
~ spl4_2,
inference(rat,[],[s48,s82]) ).
cnf(s84,plain,
spl4_30,
inference(rat,[],[s22,s82]) ).
cnf(s91,plain,
$false,
inference(rat,[],[s40,s84,s83]) ).
fof(f2163,plain,
$false,
inference(avatar_sat_refutation,[],[s91]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET020-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.11/0.38 % Computer : n017.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.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Mon Sep 28 00:05:05 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 4.97/1.62 % (3097948)Input is clausal, will run a generic CNF schedule.
% 4.97/1.62 % (3097955)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=192268720:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.97/1.62 % (3097953)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=3044838519:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.97/1.62 % (3097957)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4117212406:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.97/1.62 % (3097956)lrs+10_1_sil=8000:sp=occurrence:random_seed=3597145568:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.97/1.62 % (3097954)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3225908412:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.97/1.62 % (3097958)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1004481566:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.97/1.62 % (3097959)dis-21_1_sil=8000:lcm=predicate:random_seed=3828813524:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 4.97/1.62 % (3097956)Refutation not found, incomplete strategy
% 4.97/1.62 % (3097956)------------------------------
% 4.97/1.62 % (3097956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097956)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097957)Refutation not found, incomplete strategy
% 4.97/1.62 % (3097957)------------------------------
% 4.97/1.62 % (3097957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097956)Termination reason: Refutation not found, incomplete strategy
% 4.97/1.62 % (3097956)Time elapsed: 0.001 s
% 4.97/1.62 % (3097956)Peak memory usage: 87 MB
% 4.97/1.62 % (3097957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097957)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097957)Termination reason: Refutation not found, incomplete strategy
% 4.97/1.62 % (3097957)Time elapsed: 0.002 s
% 4.97/1.62 % (3097957)Peak memory usage: 87 MB
% 4.97/1.62 % (3097957)Instructions burned: 1 (million)
% 4.97/1.62 % (3097959)Instruction limit reached!
% 4.97/1.62 % (3097959)------------------------------
% 4.97/1.62 % (3097959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097959)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097959)Termination reason: Instruction limit
% 4.97/1.62 % (3097959)Termination phase: Saturation
% 4.97/1.62 % (3097959)Time elapsed: 0.073 s
% 4.97/1.62 % (3097959)Peak memory usage: 89 MB
% 4.97/1.62 % (3097959)Instructions burned: 118 (million)
% 4.97/1.62 % (3097958)Instruction limit reached!
% 4.97/1.62 % (3097958)------------------------------
% 4.97/1.62 % (3097958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097958)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097958)Termination reason: Instruction limit
% 4.97/1.62 % (3097958)Termination phase: Saturation
% 4.97/1.62 % (3097958)Time elapsed: 0.120 s
% 4.97/1.62 % (3097958)Peak memory usage: 90 MB
% 4.97/1.62 % (3097958)Instructions burned: 181 (million)
% 4.97/1.62 % (3097967)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=2389671562:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.97/1.62 % (3097967)Refutation not found, incomplete strategy
% 4.97/1.62 % (3097967)------------------------------
% 4.97/1.62 % (3097967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097967)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097967)Termination reason: Refutation not found, incomplete strategy
% 4.97/1.62 % (3097967)Time elapsed: 0.002 s
% 4.97/1.62 % (3097967)Peak memory usage: 88 MB
% 4.97/1.62 % (3097956)------------------------------
% 4.97/1.62 % (3097956)------------------------------
% 4.97/1.62 % (3097957)------------------------------
% 4.97/1.62 % (3097957)------------------------------
% 4.97/1.62 % (3097968)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=365987551:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 4.97/1.62 % (3097968)Instruction limit reached!
% 4.97/1.62 % (3097968)------------------------------
% 4.97/1.62 % (3097968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097968)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097968)Termination reason: Instruction limit
% 4.97/1.62 % (3097968)Termination phase: Saturation
% 4.97/1.62 % (3097968)Time elapsed: 0.103 s
% 4.97/1.62 % (3097968)Peak memory usage: 91 MB
% 4.97/1.62 % (3097968)Instructions burned: 189 (million)
% 4.97/1.62 % (3097955)First to succeed.
% 4.97/1.62 % (3097971)lrs+10_64_to=lpo:sil=8000:random_seed=2418655776:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 4.97/1.62 % (3097970)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1278830174:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 4.97/1.62 % (3097955)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3097948"
% 4.97/1.62 % (3097970)Refutation not found, incomplete strategy
% 4.97/1.62 % (3097970)------------------------------
% 4.97/1.62 % (3097970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097970)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097970)Termination reason: Refutation not found, incomplete strategy
% 4.97/1.62 % (3097970)Time elapsed: 0.003 s
% 4.97/1.62 % (3097970)Peak memory usage: 87 MB
% 4.97/1.62 % (3097970)Instructions burned: 3 (million)
% 4.97/1.62 % (3097967)------------------------------
% 4.97/1.62 % (3097967)------------------------------
% 4.97/1.62 % (3097971)Instruction limit reached!
% 4.97/1.62 % (3097971)------------------------------
% 4.97/1.62 % (3097971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.97/1.62 % (3097971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.97/1.62 % (3097971)CaDiCaL version: 2.1.3
% 4.97/1.62 % (3097971)Termination reason: Instruction limit
% 4.97/1.62 % (3097971)Termination phase: Saturation
% 4.97/1.62 % (3097971)Time elapsed: 0.076 s
% 4.97/1.62 % (3097971)Peak memory usage: 90 MB
% 4.97/1.62 % (3097971)Instructions burned: 126 (million)
% 4.97/1.62 % (3097973)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3933634600:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 4.97/1.62 % (3097955)Refutation found. Thanks to Tanya!
% 4.97/1.62 % SZS status Unsatisfiable for theBenchmark
% 4.97/1.62 % SZS output start Proof for theBenchmark
% See solution above
% 5.93/1.82 % (3097955)------------------------------
% 5.93/1.82 % (3097955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.93/1.82 % (3097955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.93/1.82 % (3097955)CaDiCaL version: 2.1.3
% 5.93/1.82 % (3097955)Termination reason: Refutation
% 5.93/1.82 % (3097955)Time elapsed: 0.459 s
% 5.93/1.82 % (3097955)Peak memory usage: 132 MB
% 5.93/1.82 % (3097955)Instructions burned: 1222 (million)
% 5.93/1.82 % (3097955)------------------------------
% 5.93/1.82 % (3097955)------------------------------
% 5.93/1.82 % (3097948)Success in time 0.752 s
% 5.93/1.82 % Vampire exiting
%------------------------------------------------------------------------------