%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV640+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:58:29 PM UTC 2026
% Result : Theorem 7.41s 3.33s
% Output : Refutation 16.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 71 ( 17 unt; 2 def)
% Number of atoms : 199 ( 61 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 216 ( 88 ~; 82 |; 33 &)
% ( 4 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-2 aty)
% Number of variables : 88 ( 0 sgn 74 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f276,axiom,
! [X0] :
( cLists_2eNatList_2enatprod___24t(X0)
=> ? [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
& ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& X0 = cLists_2eNatList_2epair___24a2(X1,X2)
& cLists_2eNatList_2efst___24a1(X0) = X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_Lists.NatList.fst') ).
fof(f280,axiom,
! [X0] :
( cLists_2eNatList_2enatprod___24t(X0)
=> ? [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
& ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& X0 = cLists_2eNatList_2epair___24a2(X1,X2)
& cLists_2eNatList_2esnd___24a1(X0) = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_def_Lists.NatList.snd') ).
fof(f448,axiom,
! [X0,X1,X2,X3] :
( cLists_2eNatList_2epair___24a2(X0,X2) = cLists_2eNatList_2epair___24a2(X1,X3)
=> ( X2 = X3
& X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_inj_Lists.NatList.pair') ).
fof(f592,axiom,
! [X0] :
( c_24__type__128___24t(X0)
<=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
=> ! [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
=> cLists_2eNatList_2enatprod___24t(happ(happ(X0,X1),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_type_128') ).
fof(f1555,axiom,
c_24__type__128___24t(cLists_2eNatList_2epair),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_Lists.NatList.pair') ).
fof(f1958,axiom,
! [X0] : happ(cLists_2eNatList_2esnd,X0) = cLists_2eNatList_2esnd___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Lists.NatList.snd_$a1') ).
fof(f2029,axiom,
! [X0] : happ(cLists_2eNatList_2efst,X0) = cLists_2eNatList_2efst___24a1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Lists.NatList.fst_$a1') ).
fof(f2129,axiom,
! [X0,X1] : happ(happ(cLists_2eNatList_2epair,X0),X1) = cLists_2eNatList_2epair___24a2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_Lists.NatList.pair_$a2') ).
fof(f2767,conjecture,
! [X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X0)
=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
=> cLists_2eNatList_2epair___24a2(X0,X1) = cLists_2eNatList_2epair___24a2(cLists_2eNatList_2efst___24a1(cLists_2eNatList_2epair___24a2(X0,X1)),cLists_2eNatList_2esnd___24a1(cLists_2eNatList_2epair___24a2(X0,X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof(f2768,negated_conjecture,
~ ! [X0] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X0)
=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
=> cLists_2eNatList_2epair___24a2(X0,X1) = cLists_2eNatList_2epair___24a2(cLists_2eNatList_2efst___24a1(cLists_2eNatList_2epair___24a2(X0,X1)),cLists_2eNatList_2esnd___24a1(cLists_2eNatList_2epair___24a2(X0,X1))) ) ),
inference(negated_conjecture,[status(cth)],[f2767]) ).
fof(f2769,plain,
? [X0] :
( ? [X1] :
( cLists_2eNatList_2epair___24a2(X0,X1) != cLists_2eNatList_2epair___24a2(cLists_2eNatList_2efst___24a1(cLists_2eNatList_2epair___24a2(X0,X1)),cLists_2eNatList_2esnd___24a1(cLists_2eNatList_2epair___24a2(X0,X1)))
& cCoq_2eInit_2eDatatypes_2enat___24t(X1) )
& cCoq_2eInit_2eDatatypes_2enat___24t(X0) ),
inference(ennf_transformation,[],[f2768]) ).
fof(f2801,plain,
! [X0,X1,X2,X3] :
( ( X2 = X3
& X0 = X1 )
| cLists_2eNatList_2epair___24a2(X0,X2) != cLists_2eNatList_2epair___24a2(X1,X3) ),
inference(ennf_transformation,[],[f448]) ).
fof(f2804,plain,
! [X0] :
( ? [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
& ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& X0 = cLists_2eNatList_2epair___24a2(X1,X2)
& cLists_2eNatList_2esnd___24a1(X0) = X2 ) )
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(ennf_transformation,[],[f280]) ).
fof(f2808,plain,
! [X0] :
( ? [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
& ? [X2] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2)
& X0 = cLists_2eNatList_2epair___24a2(X1,X2)
& cLists_2eNatList_2efst___24a1(X0) = X1 ) )
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(ennf_transformation,[],[f276]) ).
fof(f2813,plain,
! [X0] :
( c_24__type__128___24t(X0)
<=> ! [X1] :
( ! [X2] :
( cLists_2eNatList_2enatprod___24t(happ(happ(X0,X1),X2))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) ),
inference(ennf_transformation,[],[f592]) ).
fof(f2818,plain,
( cLists_2eNatList_2epair___24a2(sK0,sK1) != cLists_2eNatList_2epair___24a2(cLists_2eNatList_2efst___24a1(cLists_2eNatList_2epair___24a2(sK0,sK1)),cLists_2eNatList_2esnd___24a1(cLists_2eNatList_2epair___24a2(sK0,sK1)))
& cCoq_2eInit_2eDatatypes_2enat___24t(sK1)
& cCoq_2eInit_2eDatatypes_2enat___24t(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f2769]) ).
fof(f2828,plain,
! [X0] :
( ( cCoq_2eInit_2eDatatypes_2enat___24t(sK12(X0))
& cCoq_2eInit_2eDatatypes_2enat___24t(sK13(X0))
& cLists_2eNatList_2epair___24a2(sK12(X0),sK13(X0)) = X0
& cLists_2eNatList_2esnd___24a1(X0) = sK13(X0) )
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X1,sK12(X0)),skolemize(X2,sK13(X0))],[f2804]) ).
fof(f2831,plain,
! [X0] :
( ( cCoq_2eInit_2eDatatypes_2enat___24t(sK18(X0))
& cCoq_2eInit_2eDatatypes_2enat___24t(sK19(X0))
& cLists_2eNatList_2epair___24a2(sK18(X0),sK19(X0)) = X0
& cLists_2eNatList_2efst___24a1(X0) = sK18(X0) )
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19]),skolemize(X1,sK18(X0)),skolemize(X2,sK19(X0))],[f2808]) ).
fof(f2845,plain,
! [X0] :
( ( c_24__type__128___24t(X0)
| ? [X1] :
( ? [X2] :
( ~ cLists_2eNatList_2enatprod___24t(happ(happ(X0,X1),X2))
& cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
& cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) )
& ( ! [X1] :
( ! [X2] :
( cLists_2eNatList_2enatprod___24t(happ(happ(X0,X1),X2))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1) )
| ~ c_24__type__128___24t(X0) ) ),
inference(nnf_transformation,[],[f2813]) ).
fof(f2846,plain,
! [X0] :
( ( c_24__type__128___24t(X0)
| ? [X1] :
( ? [X2] :
( ~ cLists_2eNatList_2enatprod___24t(happ(happ(X0,X1),X2))
& cCoq_2eInit_2eDatatypes_2enat___24t(X2) )
& cCoq_2eInit_2eDatatypes_2enat___24t(X1) ) )
& ( ! [X3] :
( ! [X4] :
( cLists_2eNatList_2enatprod___24t(happ(happ(X0,X3),X4))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X4) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3) )
| ~ c_24__type__128___24t(X0) ) ),
inference(rectify,[],[f2845]) ).
fof(f2847,plain,
! [X0] :
( ( c_24__type__128___24t(X0)
| ( ~ cLists_2eNatList_2enatprod___24t(happ(happ(X0,sK26(X0)),sK27(X0)))
& cCoq_2eInit_2eDatatypes_2enat___24t(sK27(X0))
& cCoq_2eInit_2eDatatypes_2enat___24t(sK26(X0)) ) )
& ( ! [X3] :
( ! [X4] :
( cLists_2eNatList_2enatprod___24t(happ(happ(X0,X3),X4))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X4) )
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3) )
| ~ c_24__type__128___24t(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26,sK27]),skolemize(X1,sK26(X0)),skolemize(X2,sK27(X0))],[f2846]) ).
fof(f2862,plain,
cCoq_2eInit_2eDatatypes_2enat___24t(sK0),
inference(cnf_transformation,[],[f2818]) ).
fof(f2863,plain,
cCoq_2eInit_2eDatatypes_2enat___24t(sK1),
inference(cnf_transformation,[],[f2818]) ).
fof(f2864,plain,
cLists_2eNatList_2epair___24a2(sK0,sK1) != cLists_2eNatList_2epair___24a2(cLists_2eNatList_2efst___24a1(cLists_2eNatList_2epair___24a2(sK0,sK1)),cLists_2eNatList_2esnd___24a1(cLists_2eNatList_2epair___24a2(sK0,sK1))),
inference(cnf_transformation,[],[f2818]) ).
fof(f2881,plain,
! [X0,X1] : happ(happ(cLists_2eNatList_2epair,X0),X1) = cLists_2eNatList_2epair___24a2(X0,X1),
inference(cnf_transformation,[],[f2129]) ).
fof(f2893,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| cLists_2eNatList_2epair___24a2(X0,X2) != cLists_2eNatList_2epair___24a2(X1,X3) ),
inference(cnf_transformation,[],[f2801]) ).
fof(f2902,plain,
! [X0] :
( cLists_2eNatList_2esnd___24a1(X0) = sK13(X0)
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(cnf_transformation,[],[f2828]) ).
fof(f2903,plain,
! [X0] :
( cLists_2eNatList_2epair___24a2(sK12(X0),sK13(X0)) = X0
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(cnf_transformation,[],[f2828]) ).
fof(f2914,plain,
! [X0] :
( cLists_2eNatList_2efst___24a1(X0) = sK18(X0)
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(cnf_transformation,[],[f2831]) ).
fof(f2915,plain,
! [X0] :
( cLists_2eNatList_2epair___24a2(sK18(X0),sK19(X0)) = X0
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(cnf_transformation,[],[f2831]) ).
fof(f2918,plain,
! [X0] : cLists_2eNatList_2efst___24a1(X0) = happ(cLists_2eNatList_2efst,X0),
inference(cnf_transformation,[],[f2029]) ).
fof(f2919,plain,
! [X0] : cLists_2eNatList_2esnd___24a1(X0) = happ(cLists_2eNatList_2esnd,X0),
inference(cnf_transformation,[],[f1958]) ).
fof(f2920,plain,
c_24__type__128___24t(cLists_2eNatList_2epair),
inference(cnf_transformation,[],[f1555]) ).
fof(f2937,plain,
! [X3,X0,X4] :
( cLists_2eNatList_2enatprod___24t(happ(happ(X0,X3),X4))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X4)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3)
| ~ c_24__type__128___24t(X0) ),
inference(cnf_transformation,[],[f2847]) ).
fof(f2980,plain,
happ(happ(cLists_2eNatList_2epair,sK0),sK1) != happ(happ(cLists_2eNatList_2epair,happ(cLists_2eNatList_2efst,happ(happ(cLists_2eNatList_2epair,sK0),sK1))),happ(cLists_2eNatList_2esnd,happ(happ(cLists_2eNatList_2epair,sK0),sK1))),
inference(definition_unfolding,[],[f2864,f2881,f2881,f2918,f2881,f2919,f2881]) ).
fof(f2985,plain,
! [X2,X3,X0,X1] :
( happ(happ(cLists_2eNatList_2epair,X0),X2) != happ(happ(cLists_2eNatList_2epair,X1),X3)
| X2 = X3 ),
inference(definition_unfolding,[],[f2893,f2881,f2881]) ).
fof(f2991,plain,
! [X0] :
( happ(happ(cLists_2eNatList_2epair,sK12(X0)),sK13(X0)) = X0
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(definition_unfolding,[],[f2903,f2881]) ).
fof(f2992,plain,
! [X0] :
( happ(cLists_2eNatList_2esnd,X0) = sK13(X0)
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(definition_unfolding,[],[f2902,f2919]) ).
fof(f2997,plain,
! [X0] :
( happ(happ(cLists_2eNatList_2epair,sK18(X0)),sK19(X0)) = X0
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(definition_unfolding,[],[f2915,f2881]) ).
fof(f2998,plain,
! [X0] :
( happ(cLists_2eNatList_2efst,X0) = sK18(X0)
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(definition_unfolding,[],[f2914,f2918]) ).
fof(f3036,plain,
( happ(happ(cLists_2eNatList_2epair,sK0),sK1) != happ(happ(cLists_2eNatList_2epair,happ(cLists_2eNatList_2efst,happ(happ(cLists_2eNatList_2epair,sK0),sK1))),sK13(happ(happ(cLists_2eNatList_2epair,sK0),sK1)))
| ~ cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1)) ),
inference(superposition,[],[f2980,f2992]) ).
fof(f3039,definition,
( spl30_1
<=> cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1)) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f3040,plain,
( cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1))
| ~ spl30_1 ),
inference(avatar_component_clause,[],[f3039]) ).
fof(f3041,plain,
( ~ cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1))
| spl30_1 ),
inference(avatar_component_clause,[],[f3039]) ).
fof(f3043,definition,
( spl30_2
<=> happ(happ(cLists_2eNatList_2epair,sK0),sK1) = happ(happ(cLists_2eNatList_2epair,happ(cLists_2eNatList_2efst,happ(happ(cLists_2eNatList_2epair,sK0),sK1))),sK13(happ(happ(cLists_2eNatList_2epair,sK0),sK1))) ),
introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition]) ).
fof(f3045,plain,
( happ(happ(cLists_2eNatList_2epair,sK0),sK1) != happ(happ(cLists_2eNatList_2epair,happ(cLists_2eNatList_2efst,happ(happ(cLists_2eNatList_2epair,sK0),sK1))),sK13(happ(happ(cLists_2eNatList_2epair,sK0),sK1)))
| spl30_2 ),
inference(avatar_component_clause,[],[f3043]) ).
fof(f3046,plain,
( ~ spl30_1
| ~ spl30_2 ),
inference(avatar_split_clause,[],[f3036,f3043,f3039]) ).
fof(f3055,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK1)
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK0)
| ~ c_24__type__128___24t(cLists_2eNatList_2epair)
| spl30_1 ),
inference(resolution,[],[f3041,f2937]) ).
fof(f3056,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(sK0)
| ~ c_24__type__128___24t(cLists_2eNatList_2epair)
| spl30_1 ),
inference(forward_subsumption_resolution,[],[f3055,f2863]) ).
fof(f3057,plain,
( ~ c_24__type__128___24t(cLists_2eNatList_2epair)
| spl30_1 ),
inference(forward_subsumption_resolution,[],[f3056,f2862]) ).
fof(f3058,plain,
( $false
| spl30_1 ),
inference(forward_subsumption_resolution,[],[f3057,f2920]) ).
fof(f3059,plain,
spl30_1,
inference(avatar_contradiction_clause,[],[f3058]) ).
fof(f3073,plain,
( happ(happ(cLists_2eNatList_2epair,sK0),sK1) != happ(happ(cLists_2eNatList_2epair,sK18(happ(happ(cLists_2eNatList_2epair,sK0),sK1))),sK13(happ(happ(cLists_2eNatList_2epair,sK0),sK1)))
| ~ cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1))
| spl30_2 ),
inference(superposition,[],[f3045,f2998]) ).
fof(f3077,plain,
( happ(happ(cLists_2eNatList_2epair,sK0),sK1) != happ(happ(cLists_2eNatList_2epair,sK18(happ(happ(cLists_2eNatList_2epair,sK0),sK1))),sK13(happ(happ(cLists_2eNatList_2epair,sK0),sK1)))
| ~ spl30_1
| spl30_2 ),
inference(forward_subsumption_resolution,[],[f3073,f3040]) ).
fof(f3115,plain,
! [X2,X0,X1] :
( happ(happ(cLists_2eNatList_2epair,X1),X2) != X0
| sK19(X0) = X2
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(superposition,[],[f2985,f2997]) ).
fof(f3164,plain,
! [X0,X1] :
( sK19(X0) = sK19(X1)
| X0 != X1
| ~ cLists_2eNatList_2enatprod___24t(X1)
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(superposition,[],[f3115,f2997]) ).
fof(f3218,plain,
! [X0,X1] :
( sK13(X0) = sK19(X1)
| X0 != X1
| ~ cLists_2eNatList_2enatprod___24t(X1)
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(superposition,[],[f3115,f2991]) ).
fof(f4053,plain,
! [X0,X1] :
( happ(happ(cLists_2eNatList_2epair,sK18(X1)),sK19(X0)) = X1
| ~ cLists_2eNatList_2enatprod___24t(X1)
| X0 != X1
| ~ cLists_2eNatList_2enatprod___24t(X1)
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(superposition,[],[f2997,f3164]) ).
fof(f4064,plain,
! [X0,X1] :
( happ(happ(cLists_2eNatList_2epair,sK18(X1)),sK19(X0)) = X1
| ~ cLists_2eNatList_2enatprod___24t(X1)
| X0 != X1
| ~ cLists_2eNatList_2enatprod___24t(X0) ),
inference(duplicate_literal_removal,[],[f4053]) ).
fof(f4093,plain,
( ! [X0] :
( happ(happ(cLists_2eNatList_2epair,sK0),sK1) != happ(happ(cLists_2eNatList_2epair,sK18(happ(happ(cLists_2eNatList_2epair,sK0),sK1))),sK19(X0))
| happ(happ(cLists_2eNatList_2epair,sK0),sK1) != X0
| ~ cLists_2eNatList_2enatprod___24t(X0)
| ~ cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1)) )
| ~ spl30_1
| spl30_2 ),
inference(superposition,[],[f3077,f3218]) ).
fof(f4129,plain,
( ! [X0] :
( happ(happ(cLists_2eNatList_2epair,sK0),sK1) != X0
| ~ cLists_2eNatList_2enatprod___24t(X0)
| ~ cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1)) )
| ~ spl30_1
| spl30_2 ),
inference(forward_subsumption_resolution,[],[f4093,f4064]) ).
fof(f4130,plain,
( ! [X0] :
( happ(happ(cLists_2eNatList_2epair,sK0),sK1) != X0
| ~ cLists_2eNatList_2enatprod___24t(X0) )
| ~ spl30_1
| spl30_2 ),
inference(forward_subsumption_resolution,[],[f4129,f3040]) ).
fof(f4131,plain,
( ~ cLists_2eNatList_2enatprod___24t(happ(happ(cLists_2eNatList_2epair,sK0),sK1))
| ~ spl30_1
| spl30_2 ),
inference(equality_resolution,[],[f4130]) ).
fof(f4132,plain,
( $false
| ~ spl30_1
| spl30_2 ),
inference(forward_subsumption_resolution,[],[f4131,f3040]) ).
fof(f4133,plain,
( ~ spl30_1
| spl30_2 ),
inference(avatar_contradiction_clause,[],[f4132]) ).
cnf(s1,plain,
( ~ spl30_1
| ~ spl30_2 ),
inference(sat_conversion,[],[f3046]) ).
cnf(s3,plain,
spl30_1,
inference(sat_conversion,[],[f3059]) ).
cnf(s33,plain,
( ~ spl30_1
| spl30_2 ),
inference(sat_conversion,[],[f4133]) ).
cnf(s34,plain,
spl30_2,
inference(rat,[],[s33,s3]) ).
cnf(s35,plain,
$false,
inference(rat,[],[s1,s34,s3]) ).
fof(f4134,plain,
$false,
inference(avatar_sat_refutation,[],[s35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV640+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n015.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % 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 06:50:32 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.90/3.15 % (2434281)Detected formulas, will run a generic FOF schedule.
% 14.90/3.15 % (2434287)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1805696245:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 14.90/3.15 % (2434288)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1698443913:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 14.90/3.15 % (2434292)dis-21_1_sil=8000:lcm=predicate:random_seed=2295954605:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 14.90/3.15 % (2434291)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2517962769:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 14.90/3.15 % (2434286)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=2104031542:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 14.90/3.15 % (2434290)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2821361764:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 14.90/3.15 % (2434289)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3959299194:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 14.90/3.15 % (2434290)Refutation not found, incomplete strategy
% 14.90/3.15 % (2434290)------------------------------
% 14.90/3.15 % (2434290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.15 % (2434290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.15 % (2434290)CaDiCaL version: 2.1.3
% 14.90/3.15 % (2434290)Termination reason: Refutation not found, incomplete strategy
% 14.90/3.15 % (2434290)Time elapsed: 0.016 s
% 14.90/3.15 % (2434290)Peak memory usage: 91 MB
% 14.90/3.15 % (2434290)Instructions burned: 35 (million)
% 14.90/3.15 % (2434289)Refutation not found, incomplete strategy
% 14.90/3.15 % (2434289)------------------------------
% 14.90/3.15 % (2434289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.15 % (2434289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.15 % (2434289)CaDiCaL version: 2.1.3
% 14.90/3.15 % (2434289)Termination reason: Refutation not found, incomplete strategy
% 14.90/3.15 % (2434289)Time elapsed: 0.016 s
% 14.90/3.15 % (2434289)Peak memory usage: 92 MB
% 14.90/3.15 % (2434289)Instructions burned: 36 (million)
% 14.90/3.15 % (2434291)Instruction limit reached!
% 14.90/3.15 % (2434291)------------------------------
% 14.90/3.15 % (2434291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.15 % (2434291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.15 % (2434291)CaDiCaL version: 2.1.3
% 14.90/3.15 % (2434291)Termination reason: Instruction limit
% 14.90/3.15 % (2434291)Termination phase: Naming
% 14.90/3.15 % (2434291)Time elapsed: 0.057 s
% 14.90/3.15 % (2434291)Peak memory usage: 90 MB
% 14.90/3.15 % (2434291)Instructions burned: 140 (million)
% 14.90/3.15 % (2434292)Instruction limit reached!
% 14.90/3.15 % (2434292)------------------------------
% 14.90/3.15 % (2434292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.15 % (2434292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.15 % (2434292)CaDiCaL version: 2.1.3
% 14.90/3.15 % (2434292)Termination reason: Instruction limit
% 14.90/3.15 % (2434292)Termination phase: Preprocessing 3
% 14.90/3.15 % (2434292)Time elapsed: 0.064 s
% 14.90/3.15 % (2434292)Peak memory usage: 92 MB
% 14.90/3.15 % (2434292)Instructions burned: 130 (million)
% 14.90/3.15 % (2434301)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2076881375:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 14.90/3.15 % (2434300)lrs+10_1_sil=8000:sp=occurrence:random_seed=72667308:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 14.90/3.15 % (2434300)Refutation not found, incomplete strategy
% 14.90/3.15 % (2434300)------------------------------
% 14.90/3.15 % (2434300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.90/3.15 % (2434300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.90/3.15 % (2434300)CaDiCaL version: 2.1.3
% 14.90/3.15 % (2434300)Termination reason: Refutation not found, incomplete strategy
% 7.41/3.33 % (2434300)Time elapsed: 0.017 s
% 7.41/3.33 % (2434300)Peak memory usage: 92 MB
% 7.41/3.33 % (2434300)Instructions burned: 35 (million)
% 7.41/3.33 % (2434289)------------------------------
% 7.41/3.33 % (2434289)------------------------------
% 7.41/3.33 % (2434290)------------------------------
% 7.41/3.33 % (2434290)------------------------------
% 7.41/3.33 % (2434301)Instruction limit reached!
% 7.41/3.33 % (2434301)------------------------------
% 7.41/3.33 % (2434301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434301)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434301)Termination reason: Instruction limit
% 7.41/3.33 % (2434301)Termination phase: Saturation
% 7.41/3.33 % (2434301)Time elapsed: 0.069 s
% 7.41/3.33 % (2434301)Peak memory usage: 92 MB
% 7.41/3.33 % (2434301)Instructions burned: 157 (million)
% 7.41/3.33 % (2434304)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1746359667:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 7.41/3.33 % (2434305)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3853518306:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 7.41/3.33 % (2434304)Refutation not found, incomplete strategy
% 7.41/3.33 % (2434304)------------------------------
% 7.41/3.33 % (2434304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434304)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434304)Termination reason: Refutation not found, incomplete strategy
% 7.41/3.33 % (2434304)Time elapsed: 0.016 s
% 7.41/3.33 % (2434304)Peak memory usage: 92 MB
% 7.41/3.33 % (2434304)Instructions burned: 34 (million)
% 7.41/3.33 % (2434306)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4136785852:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 7.41/3.33 % (2434300)------------------------------
% 7.41/3.33 % (2434300)------------------------------
% 7.41/3.33 % (2434306)Refutation not found, incomplete strategy
% 7.41/3.33 % (2434306)------------------------------
% 7.41/3.33 % (2434306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434306)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434306)Termination reason: Refutation not found, incomplete strategy
% 7.41/3.33 % (2434306)Time elapsed: 0.024 s
% 7.41/3.33 % (2434306)Peak memory usage: 92 MB
% 7.41/3.33 % (2434306)Instructions burned: 56 (million)
% 7.41/3.33 % (2434305)Instruction limit reached!
% 7.41/3.33 % (2434305)------------------------------
% 7.41/3.33 % (2434305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434305)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434305)Termination reason: Instruction limit
% 7.41/3.33 % (2434305)Termination phase: Property scanning
% 7.41/3.33 % (2434305)Time elapsed: 0.112 s
% 7.41/3.33 % (2434305)Peak memory usage: 94 MB
% 7.41/3.33 % (2434305)Instructions burned: 248 (million)
% 7.41/3.33 % (2434310)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2917008615:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 7.41/3.33 % (2434304)------------------------------
% 7.41/3.33 % (2434304)------------------------------
% 7.41/3.33 % (2434311)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=59842127:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 7.41/3.33 % (2434306)------------------------------
% 7.41/3.33 % (2434306)------------------------------
% 7.41/3.33 % (2434311)Instruction limit reached!
% 7.41/3.33 % (2434311)------------------------------
% 7.41/3.33 % (2434311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434311)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434311)Termination reason: Instruction limit
% 7.41/3.33 % (2434311)Termination phase: Preprocessing 3
% 7.41/3.33 % (2434311)Time elapsed: 0.056 s
% 7.41/3.33 % (2434311)Peak memory usage: 91 MB
% 7.41/3.33 % (2434311)Instructions burned: 114 (million)
% 7.41/3.33 % (2434313)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=246642062:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 7.41/3.33 % (2434315)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=50669343:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 7.41/3.33 % (2434313)Instruction limit reached!
% 7.41/3.33 % (2434313)------------------------------
% 7.41/3.33 % (2434313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434313)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434313)Termination reason: Instruction limit
% 7.41/3.33 % (2434313)Termination phase: Clausification
% 7.41/3.33 % (2434313)Time elapsed: 0.073 s
% 7.41/3.33 % (2434313)Peak memory usage: 94 MB
% 7.41/3.33 % (2434313)Instructions burned: 127 (million)
% 7.41/3.33 % (2434316)lrs+10_1_sil=8000:sp=occurrence:random_seed=1515534465:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 7.41/3.33 % (2434315)Instruction limit reached!
% 7.41/3.33 % (2434315)------------------------------
% 7.41/3.33 % (2434315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434315)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434315)Termination reason: Instruction limit
% 7.41/3.33 % (2434315)Termination phase: Property scanning
% 7.41/3.33 % (2434315)Time elapsed: 0.043 s
% 7.41/3.33 % (2434315)Peak memory usage: 88 MB
% 7.41/3.33 % (2434315)Instructions burned: 117 (million)
% 7.41/3.33 % (2434319)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2655251302:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 7.41/3.33 % (2434321)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2761925556:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 7.41/3.33 % (2434319)Instruction limit reached!
% 7.41/3.33 % (2434319)------------------------------
% 7.41/3.33 % (2434319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434319)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434319)Termination reason: Instruction limit
% 7.41/3.33 % (2434319)Termination phase: Saturation
% 7.41/3.33 % (2434319)Time elapsed: 0.189 s
% 7.41/3.33 % (2434319)Peak memory usage: 98 MB
% 7.41/3.33 % (2434319)Instructions burned: 438 (million)
% 7.41/3.33 % (2434316)Instruction limit reached!
% 7.41/3.33 % (2434316)------------------------------
% 7.41/3.33 % (2434316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434316)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434316)Termination reason: Instruction limit
% 7.41/3.33 % (2434316)Termination phase: Saturation
% 7.41/3.33 % (2434316)Time elapsed: 0.467 s
% 7.41/3.33 % (2434316)Peak memory usage: 102 MB
% 7.41/3.33 % (2434316)Instructions burned: 907 (million)
% 7.41/3.33 % (2434324)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2475141336:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 7.41/3.33 % (2434324)Instruction limit reached!
% 7.41/3.33 % (2434324)------------------------------
% 7.41/3.33 % (2434324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434324)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434324)Termination reason: Instruction limit
% 7.41/3.33 % (2434324)Termination phase: NewCNF
% 7.41/3.33 % (2434324)Time elapsed: 0.072 s
% 7.41/3.33 % (2434324)Peak memory usage: 93 MB
% 7.41/3.33 % (2434324)Instructions burned: 135 (million)
% 7.41/3.33 % (2434325)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1530835404:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 7.41/3.33 % (2434327)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=577192719:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 7.41/3.33 % (2434321)First to succeed.
% 7.41/3.33 % (2434321)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2434281"
% 7.41/3.33 % (2434325)Instruction limit reached!
% 7.41/3.33 % (2434325)------------------------------
% 7.41/3.33 % (2434325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.41/3.33 % (2434325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.41/3.33 % (2434325)CaDiCaL version: 2.1.3
% 7.41/3.33 % (2434325)Termination reason: Instruction limit
% 7.41/3.33 % (2434325)Termination phase: Saturation
% 7.41/3.33 % (2434325)Time elapsed: 0.271 s
% 7.41/3.33 % (2434325)Peak memory usage: 96 MB
% 7.41/3.33 % (2434325)Instructions burned: 593 (million)
% 7.41/3.33 % (2434321)Refutation found. Thanks to Tanya!
% 7.41/3.33 % SZS status Theorem for theBenchmark
% 7.41/3.33 % SZS output start Proof for theBenchmark
% See solution above
% 16.37/3.52 % (2434321)------------------------------
% 16.37/3.52 % (2434321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.37/3.52 % (2434321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.37/3.52 % (2434321)CaDiCaL version: 2.1.3
% 16.37/3.52 % (2434321)Termination reason: Refutation
% 16.37/3.52 % (2434321)Time elapsed: 0.719 s
% 16.37/3.52 % (2434321)Peak memory usage: 138 MB
% 16.37/3.52 % (2434321)Instructions burned: 1225 (million)
% 16.37/3.52 % (2434321)------------------------------
% 16.37/3.52 % (2434321)------------------------------
% 16.37/3.52 % (2434281)Success in time 2.459 s
% 16.37/3.52 % Vampire exiting
%------------------------------------------------------------------------------