%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP006+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 11:33:59 AM UTC 2026
% Result : Theorem 8.13s 1.75s
% Output : Refutation 8.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 8
% Syntax : Number of formulae : 71 ( 16 unt; 5 def)
% Number of atoms : 362 ( 6 equ)
% Maximal formula atoms : 38 ( 5 avg)
% Number of connectives : 494 ( 203 ~; 185 |; 41 &)
% ( 23 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 165 ( 0 sgn 143 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001+2.ax',ap_tp) ).
fof(f40,axiom,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X0,X1))
=> ! [X3] :
( mem(X3,arr(X1,bool))
=> ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X0,X1),X2),X3))
<=> ! [X4] :
( mem(X4,X1)
=> ( p(ap(X3,X4))
=> ? [X5] :
( mem(X5,X0)
& p(ap(X3,ap(X2,X5))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X0,X1),X2),X3))
<=> ! [X6] :
( mem(X6,X1)
=> ( ~ p(ap(X3,X6))
=> ? [X7] :
( mem(X7,X0)
& ~ p(ap(X3,ap(X2,X7))) ) ) ) )
& ! [X8] :
( mem(X8,arr(X0,X1))
=> ! [X9] :
( mem(X9,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X8),X9))
<=> ! [X10] :
( mem(X10,X0)
=> p(ap(X9,ap(X8,X10))) ) ) ) )
& ! [X11] :
( mem(X11,arr(X0,X1))
=> ! [X12] :
( mem(X12,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
<=> ! [X13] :
( mem(X13,X0)
=> ~ p(ap(X12,ap(X11,X13))) ) ) ) )
& ! [X14] :
( mem(X14,arr(X0,X1))
=> ! [X15] :
( mem(X15,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X0,X1),X14),X15))
<=> ! [X16] :
( mem(X16,X1)
=> ( p(ap(X15,X16))
=> ? [X17] :
( mem(X17,X0)
& X16 = ap(X14,X17) ) ) ) ) ) )
& ! [X18] :
( mem(X18,arr(X0,X1))
=> ! [X19] :
( mem(X19,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X0,X1),X18),X19))
<=> ! [X20] :
( mem(X20,X1)
=> ( ~ p(ap(X19,X20))
=> ? [X21] :
( mem(X21,X0)
& X20 = ap(X18,X21) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__REWRITES) ).
fof(f52,conjecture,
! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X1,X0))
=> ! [X3] :
( mem(X3,arr(X0,bool))
=> ! [X4] :
( mem(X4,arr(X0,bool))
=> ( ! [X5] :
( mem(X5,X0)
=> ( p(ap(X4,X5))
=> p(ap(X3,X5)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X3))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X4)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
fof(f53,negated_conjecture,
~ ! [X0] :
( ne(X0)
=> ! [X1] :
( ne(X1)
=> ! [X2] :
( mem(X2,arr(X1,X0))
=> ! [X3] :
( mem(X3,arr(X0,bool))
=> ! [X4] :
( mem(X4,arr(X0,bool))
=> ( ! [X5] :
( mem(X5,X0)
=> ( p(ap(X4,X5))
=> p(ap(X3,X5)) ) )
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X3))
=> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X4)) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ! [X3] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f86,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X0,X1),X2),X3))
<=> ! [X4] :
( ? [X5] :
( mem(X5,X0)
& p(ap(X3,ap(X2,X5))) )
| ~ p(ap(X3,X4))
| ~ mem(X4,X1) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X0,X1),X2),X3))
<=> ! [X6] :
( ? [X7] :
( mem(X7,X0)
& ~ p(ap(X3,ap(X2,X7))) )
| p(ap(X3,X6))
| ~ mem(X6,X1) ) )
& ! [X8] :
( ! [X9] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X8),X9))
<=> ! [X10] :
( p(ap(X9,ap(X8,X10)))
| ~ mem(X10,X0) ) )
| ~ mem(X9,arr(X1,bool)) )
| ~ mem(X8,arr(X0,X1)) )
& ! [X11] :
( ! [X12] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
<=> ! [X13] :
( ~ p(ap(X12,ap(X11,X13)))
| ~ mem(X13,X0) ) )
| ~ mem(X12,arr(X1,bool)) )
| ~ mem(X11,arr(X0,X1)) )
& ! [X14] :
( ! [X15] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X0,X1),X14),X15))
<=> ! [X16] :
( ? [X17] :
( mem(X17,X0)
& X16 = ap(X14,X17) )
| ~ p(ap(X15,X16))
| ~ mem(X16,X1) ) )
| ~ mem(X15,arr(X1,bool)) )
| ~ mem(X14,arr(X0,X1)) )
& ! [X18] :
( ! [X19] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X0,X1),X18),X19))
<=> ! [X20] :
( ? [X21] :
( mem(X21,X0)
& X20 = ap(X18,X21) )
| p(ap(X19,X20))
| ~ mem(X20,X1) ) )
| ~ mem(X19,arr(X1,bool)) )
| ~ mem(X18,arr(X0,X1)) ) )
| ~ mem(X3,arr(X1,bool)) )
| ~ mem(X2,arr(X0,X1)) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f87,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X0,X1),X2),X3))
<=> ! [X4] :
( ? [X5] :
( mem(X5,X0)
& p(ap(X3,ap(X2,X5))) )
| ~ p(ap(X3,X4))
| ~ mem(X4,X1) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X0,X1),X2),X3))
<=> ! [X6] :
( ? [X7] :
( mem(X7,X0)
& ~ p(ap(X3,ap(X2,X7))) )
| p(ap(X3,X6))
| ~ mem(X6,X1) ) )
& ! [X8] :
( ! [X9] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X8),X9))
<=> ! [X10] :
( p(ap(X9,ap(X8,X10)))
| ~ mem(X10,X0) ) )
| ~ mem(X9,arr(X1,bool)) )
| ~ mem(X8,arr(X0,X1)) )
& ! [X11] :
( ! [X12] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
<=> ! [X13] :
( ~ p(ap(X12,ap(X11,X13)))
| ~ mem(X13,X0) ) )
| ~ mem(X12,arr(X1,bool)) )
| ~ mem(X11,arr(X0,X1)) )
& ! [X14] :
( ! [X15] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X0,X1),X14),X15))
<=> ! [X16] :
( ? [X17] :
( mem(X17,X0)
& X16 = ap(X14,X17) )
| ~ p(ap(X15,X16))
| ~ mem(X16,X1) ) )
| ~ mem(X15,arr(X1,bool)) )
| ~ mem(X14,arr(X0,X1)) )
& ! [X18] :
( ! [X19] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X0,X1),X18),X19))
<=> ! [X20] :
( ? [X21] :
( mem(X21,X0)
& X20 = ap(X18,X21) )
| p(ap(X19,X20))
| ~ mem(X20,X1) ) )
| ~ mem(X19,arr(X1,bool)) )
| ~ mem(X18,arr(X0,X1)) ) )
| ~ mem(X3,arr(X1,bool)) )
| ~ mem(X2,arr(X0,X1)) )
| ~ ne(X1) )
| ~ ne(X0) ),
inference(flattening,[],[f86]) ).
fof(f105,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X4))
& p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X3))
& ! [X5] :
( p(ap(X3,X5))
| ~ p(ap(X4,X5))
| ~ mem(X5,X0) )
& mem(X4,arr(X0,bool)) )
& mem(X3,arr(X0,bool)) )
& mem(X2,arr(X1,X0)) )
& ne(X1) )
& ne(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f106,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X4))
& p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X1,X0),X2),X3))
& ! [X5] :
( p(ap(X3,X5))
| ~ p(ap(X4,X5))
| ~ mem(X5,X0) )
& mem(X4,arr(X0,bool)) )
& mem(X3,arr(X0,bool)) )
& mem(X2,arr(X1,X0)) )
& ne(X1) )
& ne(X0) ),
inference(flattening,[],[f105]) ).
fof(f110,plain,
! [X2,X3,X0,X1] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0)
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f55]) ).
fof(f178,plain,
! [X2,X3,X0,X11,X1,X12,X13] :
( ~ p(ap(X12,ap(X11,X13)))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X2,arr(X0,X1))
| ~ mem(X13,X0)
| ~ mem(X12,arr(X1,bool))
| ~ mem(X11,arr(X0,X1))
| ~ ne(X1)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f179,plain,
! [X2,X3,X0,X11,X1,X12] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
| ~ ne(X1)
| ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X11,arr(X0,X1))
| ~ mem(X12,arr(X1,bool))
| mem(sK11(X0,X11,X12),X0)
| ~ ne(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f180,plain,
! [X2,X3,X0,X11,X1,X12] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
| ~ ne(X1)
| ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X11,arr(X0,X1))
| ~ mem(X12,arr(X1,bool))
| p(ap(X12,ap(X11,sK11(X0,X11,X12))))
| ~ ne(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f258,plain,
! [X5] :
( p(ap(sK25,X5))
| ~ p(ap(sK26,X5))
| ~ mem(X5,sK22) ),
inference(cnf_transformation,[],[f106]) ).
fof(f259,plain,
mem(sK26,arr(sK22,bool)),
inference(cnf_transformation,[],[f106]) ).
fof(f260,plain,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK23,sK22),sK24),sK25)),
inference(cnf_transformation,[],[f106]) ).
fof(f261,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK23,sK22),sK24),sK26)),
inference(cnf_transformation,[],[f106]) ).
fof(f262,plain,
mem(sK25,arr(sK22,bool)),
inference(cnf_transformation,[],[f106]) ).
fof(f263,plain,
mem(sK24,arr(sK23,sK22)),
inference(cnf_transformation,[],[f106]) ).
fof(f264,plain,
ne(sK23),
inference(cnf_transformation,[],[f106]) ).
fof(f265,plain,
ne(sK22),
inference(cnf_transformation,[],[f106]) ).
fof(f1074,plain,
! [X0,X1] :
( ~ ne(sK22)
| ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(sK24,arr(sK23,sK22))
| ~ mem(sK26,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23)
| ~ ne(sK23) ),
inference(resolution,[],[f179,f261]) ).
fof(f1075,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(sK24,arr(sK23,sK22))
| ~ mem(sK26,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23)
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1074,f265]) ).
fof(f1076,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(sK26,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23)
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1075,f263]) ).
fof(f1077,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23)
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1076,f259]) ).
fof(f1078,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23) ),
inference(forward_subsumption_resolution,[],[f1077,f264]) ).
fof(f1080,definition,
( spl27_7
<=> mem(sK11(sK23,sK24,sK26),sK23) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
fof(f1082,plain,
( mem(sK11(sK23,sK24,sK26),sK23)
| ~ spl27_7 ),
inference(avatar_component_clause,[],[f1080]) ).
fof(f1084,definition,
( spl27_8
<=> ! [X1] : ~ mem(X1,arr(sK22,bool)) ),
introduced(definition,[new_symbols(definition,[spl27_8])],[avatar_definition]) ).
fof(f1085,plain,
( ! [X1] : ~ mem(X1,arr(sK22,bool))
| ~ spl27_8 ),
inference(avatar_component_clause,[],[f1084]) ).
fof(f1087,definition,
( spl27_9
<=> ! [X0] : ~ mem(X0,arr(sK23,sK22)) ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
fof(f1088,plain,
( ! [X0] : ~ mem(X0,arr(sK23,sK22))
| ~ spl27_9 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1089,plain,
( spl27_7
| spl27_8
| spl27_9 ),
inference(avatar_split_clause,[],[f1078,f1087,f1084,f1080]) ).
fof(f1212,plain,
! [X2,X0,X1] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(X2,arr(sK23,sK22))
| ~ mem(X0,sK23)
| ~ mem(sK25,arr(sK22,bool))
| ~ mem(sK24,arr(sK23,sK22))
| ~ ne(sK22)
| ~ ne(sK23) ),
inference(resolution,[],[f178,f260]) ).
fof(f1317,plain,
! [X2,X0,X1] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(X2,arr(sK23,sK22))
| ~ mem(X0,sK23)
| ~ mem(sK24,arr(sK23,sK22))
| ~ ne(sK22)
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1212,f262]) ).
fof(f1318,plain,
! [X2,X0,X1] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(X2,arr(sK23,sK22))
| ~ mem(X0,sK23)
| ~ ne(sK22)
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1317,f263]) ).
fof(f1319,plain,
! [X2,X0,X1] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(X2,arr(sK23,sK22))
| ~ mem(X0,sK23)
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1318,f265]) ).
fof(f1320,plain,
! [X2,X0,X1] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(X2,arr(sK23,sK22))
| ~ mem(X0,sK23) ),
inference(forward_subsumption_resolution,[],[f1319,f264]) ).
fof(f1322,definition,
( spl27_10
<=> ! [X0] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X0,sK23) ) ),
introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition]) ).
fof(f1323,plain,
( ! [X0] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X0,sK23) )
| ~ spl27_10 ),
inference(avatar_component_clause,[],[f1322]) ).
fof(f1324,plain,
( spl27_9
| spl27_8
| spl27_10 ),
inference(avatar_split_clause,[],[f1320,f1322,f1084,f1087]) ).
fof(f1326,plain,
! [X0,X1] :
( ~ ne(sK22)
| ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(sK24,arr(sK23,sK22))
| ~ mem(sK26,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ ne(sK23) ),
inference(resolution,[],[f180,f261]) ).
fof(f1329,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(sK24,arr(sK23,sK22))
| ~ mem(sK26,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1326,f265]) ).
fof(f1330,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(sK26,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1329,f263]) ).
fof(f1331,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ ne(sK23) ),
inference(forward_subsumption_resolution,[],[f1330,f259]) ).
fof(f1332,plain,
! [X0,X1] :
( ~ mem(X0,arr(sK23,sK22))
| ~ mem(X1,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26)))) ),
inference(forward_subsumption_resolution,[],[f1331,f264]) ).
fof(f1333,plain,
( $false
| ~ spl27_8 ),
inference(resolution,[],[f1085,f259]) ).
fof(f1344,plain,
~ spl27_8,
inference(avatar_contradiction_clause,[],[f1333]) ).
fof(f1346,plain,
( $false
| ~ spl27_9 ),
inference(resolution,[],[f1088,f263]) ).
fof(f1355,plain,
~ spl27_9,
inference(avatar_contradiction_clause,[],[f1346]) ).
fof(f1357,plain,
( ! [X0] :
( ~ p(ap(sK26,ap(sK24,X0)))
| ~ mem(X0,sK23)
| ~ mem(ap(sK24,X0),sK22) )
| ~ spl27_10 ),
inference(resolution,[],[f1323,f258]) ).
fof(f1646,definition,
( spl27_11
<=> p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26)))) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
fof(f1648,plain,
( p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f1646]) ).
fof(f1649,plain,
( spl27_11
| spl27_8
| spl27_9 ),
inference(avatar_split_clause,[],[f1332,f1087,f1084,f1646]) ).
fof(f2352,plain,
( ~ mem(sK11(sK23,sK24,sK26),sK23)
| ~ mem(ap(sK24,sK11(sK23,sK24,sK26)),sK22)
| ~ spl27_10
| ~ spl27_11 ),
inference(resolution,[],[f1357,f1648]) ).
fof(f2394,plain,
( ~ mem(ap(sK24,sK11(sK23,sK24,sK26)),sK22)
| ~ spl27_7
| ~ spl27_10
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f2352,f1082]) ).
fof(f2408,plain,
( ! [X0] :
( ~ mem(sK11(sK23,sK24,sK26),X0)
| ~ mem(sK24,arr(X0,sK22)) )
| ~ spl27_7
| ~ spl27_10
| ~ spl27_11 ),
inference(resolution,[],[f2394,f110]) ).
fof(f2418,plain,
( ~ mem(sK24,arr(sK23,sK22))
| ~ spl27_7
| ~ spl27_10
| ~ spl27_11 ),
inference(resolution,[],[f2408,f1082]) ).
fof(f2419,plain,
( $false
| ~ spl27_7
| ~ spl27_10
| ~ spl27_11 ),
inference(forward_subsumption_resolution,[],[f2418,f263]) ).
fof(f2420,plain,
( ~ spl27_7
| ~ spl27_10
| ~ spl27_11 ),
inference(avatar_contradiction_clause,[],[f2419]) ).
cnf(s4,plain,
( spl27_7
| spl27_8
| spl27_9 ),
inference(sat_conversion,[],[f1089]) ).
cnf(s5,plain,
( spl27_8
| spl27_9
| spl27_10 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s7,plain,
~ spl27_8,
inference(sat_conversion,[],[f1344]) ).
cnf(s8,plain,
~ spl27_9,
inference(sat_conversion,[],[f1355]) ).
cnf(s9,plain,
( spl27_8
| spl27_9
| spl27_11 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s11,plain,
( ~ spl27_7
| ~ spl27_10
| ~ spl27_11 ),
inference(sat_conversion,[],[f2420]) ).
cnf(s12,plain,
spl27_11,
inference(rat,[],[s9,s8,s7]) ).
cnf(s13,plain,
spl27_10,
inference(rat,[],[s5,s8,s7]) ).
cnf(s14,plain,
~ spl27_7,
inference(rat,[],[s11,s12,s13]) ).
cnf(s15,plain,
$false,
inference(rat,[],[s4,s8,s7,s14]) ).
fof(f2421,plain,
$false,
inference(avatar_sat_refutation,[],[s15]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n011.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 : Sun Sep 27 11:52:45 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.13/1.75 % (2261874)Will run a generic schedule for satisfiability detection.
% 8.13/1.75 % (2261881)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3471898261:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.13/1.75 % (2261880)% WARNING: option uhcvi not known.
% 8.13/1.75 % (2261880)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=780639037:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.13/1.75 % (2261879)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3947900920_2999 on theBenchmark for (2999ds/0Mi)
% 8.13/1.75 % (2261884)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=68086441:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.13/1.75 % (2261882)dis+10_1_sil=32000:sp=arity:random_seed=1821352509:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.13/1.75 % (2261883)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2362403432:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.13/1.75 % (2261885)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3657312449:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.13/1.75 % TRYING [1]
% 8.13/1.75 % TRYING [2]
% 8.13/1.75 % TRYING [3]
% 8.13/1.75 % (2261882)Instruction limit reached!
% 8.13/1.75 % (2261882)------------------------------
% 8.13/1.75 % (2261882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261882)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261882)Termination reason: Instruction limit
% 8.13/1.75 % (2261882)Termination phase: Saturation
% 8.13/1.75 % (2261882)Time elapsed: 0.068 s
% 8.13/1.75 % (2261882)Peak memory usage: 13 MB
% 8.13/1.75 % (2261882)Instructions burned: 104 (million)
% 8.13/1.75 % (2261883)Instruction limit reached!
% 8.13/1.75 % (2261883)------------------------------
% 8.13/1.75 % (2261883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261883)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261883)Termination reason: Instruction limit
% 8.13/1.75 % (2261883)Termination phase: Saturation
% 8.13/1.75 % (2261883)Time elapsed: 0.070 s
% 8.13/1.75 % (2261883)Peak memory usage: 13 MB
% 8.13/1.75 % (2261883)Instructions burned: 117 (million)
% 8.13/1.75 % (2261884)Instruction limit reached!
% 8.13/1.75 % (2261884)------------------------------
% 8.13/1.75 % (2261884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261884)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261884)Termination reason: Instruction limit
% 8.13/1.75 % (2261884)Termination phase: Saturation
% 8.13/1.75 % (2261884)Time elapsed: 0.070 s
% 8.13/1.75 % (2261884)Peak memory usage: 14 MB
% 8.13/1.75 % (2261884)Instructions burned: 133 (million)
% 8.13/1.75 % TRYING [4]
% 8.13/1.75 % (2261893)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=501981287:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.13/1.75 % (2261895)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1018336021:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.13/1.75 % (2261894)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3701284638:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.13/1.75 % (2261885)Instruction limit reached!
% 8.13/1.75 % (2261885)------------------------------
% 8.13/1.75 % (2261885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261885)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261885)Termination reason: Instruction limit
% 8.13/1.75 % (2261885)Termination phase: Saturation
% 8.13/1.75 % (2261885)Time elapsed: 0.097 s
% 8.13/1.75 % (2261885)Peak memory usage: 14 MB
% 8.13/1.75 % (2261885)Instructions burned: 160 (million)
% 8.13/1.75 % TRYING [1]
% 8.13/1.75 % TRYING [2]
% 8.13/1.75 % TRYING [3]
% 8.13/1.75 % (2261899)ott-21_1_sil=16000:fs=off:random_seed=2486967486:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.13/1.75 % TRYING [4]
% 8.13/1.75 % (2261894)Instruction limit reached!
% 8.13/1.75 % (2261894)------------------------------
% 8.13/1.75 % (2261894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261894)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261894)Termination reason: Instruction limit
% 8.13/1.75 % (2261894)Termination phase: Saturation
% 8.13/1.75 % (2261894)Time elapsed: 0.073 s
% 8.13/1.75 % (2261894)Peak memory usage: 14 MB
% 8.13/1.75 % (2261894)Instructions burned: 131 (million)
% 8.13/1.75 % (2261901)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2362665158:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.13/1.75 % TRYING [5]
% 8.13/1.75 % (2261899)Instruction limit reached!
% 8.13/1.75 % (2261899)------------------------------
% 8.13/1.75 % (2261899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261899)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261899)Termination reason: Instruction limit
% 8.13/1.75 % (2261899)Termination phase: Saturation
% 8.13/1.75 % (2261899)Time elapsed: 0.097 s
% 8.13/1.75 % (2261899)Peak memory usage: 13 MB
% 8.13/1.75 % (2261899)Instructions burned: 180 (million)
% 8.13/1.75 % (2261903)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1208218811:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.13/1.75 % TRYING [1]
% 8.13/1.75 % TRYING [2]
% 8.13/1.75 % TRYING [3]
% 8.13/1.75 % TRYING [4]
% 8.13/1.75 % (2261893)Instruction limit reached!
% 8.13/1.75 % (2261893)------------------------------
% 8.13/1.75 % (2261893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261893)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261893)Termination reason: Instruction limit
% 8.13/1.75 % (2261893)Termination phase: Finite model building SAT solving
% 8.13/1.75 % (2261893)Time elapsed: 0.352 s
% 8.13/1.75 % (2261893)Peak memory usage: 34 MB
% 8.13/1.75 % (2261893)Instructions burned: 714 (million)
% 8.13/1.75 % (2261905)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2171922915:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 8.13/1.75 % (2261901)Instruction limit reached!
% 8.13/1.75 % (2261901)------------------------------
% 8.13/1.75 % (2261901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261901)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261901)Termination reason: Instruction limit
% 8.13/1.75 % (2261901)Termination phase: Saturation
% 8.13/1.75 % (2261901)Time elapsed: 0.315 s
% 8.13/1.75 % (2261901)Peak memory usage: 14 MB
% 8.13/1.75 % (2261901)Instructions burned: 477 (million)
% 8.13/1.75 % (2261895)Instruction limit reached!
% 8.13/1.75 % (2261895)------------------------------
% 8.13/1.75 % (2261895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261895)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261895)Termination reason: Instruction limit
% 8.13/1.75 % (2261895)Termination phase: Saturation
% 8.13/1.75 % (2261895)Time elapsed: 0.417 s
% 8.13/1.75 % (2261895)Peak memory usage: 18 MB
% 8.13/1.75 % (2261895)Instructions burned: 685 (million)
% 8.13/1.75 % (2261907)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3976784634:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 8.13/1.75 % (2261908)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=526390354:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 8.13/1.75 % TRYING [6]
% 8.13/1.75 % (2261903)Instruction limit reached!
% 8.13/1.75 % (2261903)------------------------------
% 8.13/1.75 % (2261903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261903)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261903)Termination reason: Instruction limit
% 8.13/1.75 % (2261903)Termination phase: Finite model building SAT solving
% 8.13/1.75 % (2261903)Time elapsed: 0.354 s
% 8.13/1.75 % (2261903)Peak memory usage: 29 MB
% 8.13/1.75 % (2261903)Instructions burned: 865 (million)
% 8.13/1.75 % (2261911)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=170880599:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 8.13/1.75 % (2261908)Instruction limit reached!
% 8.13/1.75 % (2261908)------------------------------
% 8.13/1.75 % (2261908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261908)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261908)Termination reason: Instruction limit
% 8.13/1.75 % (2261908)Termination phase: Saturation
% 8.13/1.75 % (2261908)Time elapsed: 0.339 s
% 8.13/1.75 % (2261908)Peak memory usage: 18 MB
% 8.13/1.75 % (2261908)Instructions burned: 692 (million)
% 8.13/1.75 % (2261913)fmb+10_1_sil=64000:random_seed=3550617540:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 8.13/1.75 % TRYING [1]
% 8.13/1.75 % TRYING [2]
% 8.13/1.75 % (2261907)Instruction limit reached!
% 8.13/1.75 % (2261907)------------------------------
% 8.13/1.75 % (2261907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261907)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261907)Termination reason: Instruction limit
% 8.13/1.75 % (2261907)Termination phase: Finite model building constraint generation
% 8.13/1.75 % (2261907)Time elapsed: 0.405 s
% 8.13/1.75 % (2261907)Peak memory usage: 102 MB
% 8.13/1.75 % (2261907)Instructions burned: 890 (million)
% 8.13/1.75 % TRYING [3]
% 8.13/1.75 % (2261915)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3095041803:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 8.13/1.75 % TRYING [20]
% 8.13/1.75 % TRYING [4]
% 8.13/1.75 % (2261911)Instruction limit reached!
% 8.13/1.75 % (2261911)------------------------------
% 8.13/1.75 % (2261911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261911)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261911)Termination reason: Instruction limit
% 8.13/1.75 % (2261911)Termination phase: Saturation
% 8.13/1.75 % (2261911)Time elapsed: 0.468 s
% 8.13/1.75 % (2261911)Peak memory usage: 19 MB
% 8.13/1.75 % (2261911)Instructions burned: 880 (million)
% 8.13/1.75 % (2261917)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4184244359:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 8.13/1.75 % (2261905)Instruction limit reached!
% 8.13/1.75 % (2261905)------------------------------
% 8.13/1.75 % (2261905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261905)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261905)Termination reason: Instruction limit
% 8.13/1.75 % (2261905)Termination phase: Saturation
% 8.13/1.75 % (2261905)Time elapsed: 0.662 s
% 8.13/1.75 % (2261905)Peak memory usage: 22 MB
% 8.13/1.75 % (2261905)Instructions burned: 1180 (million)
% 8.13/1.75 % TRYING [8]
% 8.13/1.75 % (2261919)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4020148774:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 8.13/1.75 % (2261919) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2261874-2261919"...
% 8.13/1.75 % (2261919)...printing done.
% 8.13/1.75 % (2261919)Refutation found. Thanks to Tanya!
% 8.13/1.75 % SZS status Theorem for theBenchmark
% 8.13/1.75 % SZS output start Proof for theBenchmark
% See solution above
% 8.13/1.75 % (2261919)------------------------------
% 8.13/1.75 % (2261919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.13/1.75 % (2261919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.13/1.75 % (2261919)CaDiCaL version: 2.1.3
% 8.13/1.75 % (2261919)Termination reason: Refutation
% 8.13/1.75 % (2261919)Time elapsed: 0.116 s
% 8.13/1.75 % (2261919)Peak memory usage: 14 MB
% 8.13/1.75 % (2261919)Instructions burned: 210 (million)
% 8.13/1.75 % (2261874)Success in time 1.324 s
% 8.13/1.75 % Vampire exiting
%------------------------------------------------------------------------------