%------------------------------------------------------------------------------
% 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 : 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 11:34:00 AM UTC 2026
% Result : Theorem 6.99s 1.51s
% Output : Refutation 6.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 8
% Syntax : Number of formulae : 64 ( 14 unt; 0 typ; 5 def)
% Number of atoms : 520 ( 6 equ)
% Maximal formula atoms : 36 ( 8 avg)
% Number of connectives : 393 ( 156 ~; 141 |; 37 &)
% ( 23 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 219 ( 219 fml; 0 var)
% Number of types : 4 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 22 ( 20 usr; 9 prp; 0-3 aty)
% Number of functors : 37 ( 37 usr; 6 con; 0-4 aty)
% Number of variables : 151 ( 0 sgn 129 !; 22 ?; 151 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
del: $tType ).
tff(type_def_6,type,
tp__o: $tType ).
tff(func_def_0,type,
bool: del ).
tff(func_def_1,type,
ind: del ).
tff(func_def_2,type,
arr: ( del * del ) > del ).
tff(func_def_4,type,
k: ( del * $i ) > $i ).
tff(func_def_5,type,
i: del > $i ).
tff(func_def_6,type,
inj__o: tp__o > $i ).
tff(func_def_7,type,
surj__o: $i > tp__o ).
tff(func_def_9,type,
fo__c_2Ebool_2ET: tp__o ).
tff(func_def_10,type,
c_2EquantHeuristics_2EGUESS__FORALL__GAP: ( del * del ) > $i ).
tff(func_def_11,type,
c_2EquantHeuristics_2EGUESS__EXISTS__GAP: ( del * del ) > $i ).
tff(func_def_12,type,
c_2EquantHeuristics_2EGUESS__FORALL__POINT: ( del * del ) > $i ).
tff(func_def_13,type,
c_2EquantHeuristics_2EGUESS__EXISTS__POINT: ( del * del ) > $i ).
tff(func_def_14,type,
c_2EquantHeuristics_2EGUESS__FORALL: ( del * del ) > $i ).
tff(func_def_15,type,
c_2Ebool_2E_3F: del > $i ).
tff(func_def_16,type,
c_2EquantHeuristics_2EGUESS__EXISTS: ( del * del ) > $i ).
tff(func_def_18,type,
fo__c_2Ebool_2EF: tp__o ).
tff(func_def_20,type,
fo__c_2Ebool_2E_5C_2F: ( tp__o * tp__o ) > tp__o ).
tff(func_def_22,type,
fo__c_2Ebool_2E_2F_5C: ( tp__o * tp__o ) > tp__o ).
tff(func_def_23,type,
c_2Emin_2E_3D: del > $i ).
tff(func_def_25,type,
fo__c_2Ebool_2E_7E: tp__o > tp__o ).
tff(func_def_27,type,
fo__c_2Emin_2E_3D_3D_3E: ( tp__o * tp__o ) > tp__o ).
tff(func_def_28,type,
c_2Ebool_2E_21: del > $i ).
tff(func_def_29,type,
sK0: ( del * $i * $i ) > $i ).
tff(func_def_30,type,
sK1: ( del * $i ) > $i ).
tff(func_def_31,type,
sK2: ( del * $i ) > $i ).
tff(func_def_32,type,
sK5: ( del * del * $i * $i ) > $i ).
tff(func_def_33,type,
sK6: ( del * del * $i * $i ) > $i ).
tff(func_def_34,type,
sK7: ( del * $i * $i ) > $i ).
tff(func_def_35,type,
sK8: ( del * $i * $i ) > $i ).
tff(func_def_36,type,
sK9: ( del * del * $i * $i ) > $i ).
tff(func_def_37,type,
sK10: ( del * del * $i * $i ) > $i ).
tff(func_def_38,type,
sK11: ( del * $i * $i ) > $i ).
tff(func_def_39,type,
sK12: ( del * $i * $i ) > $i ).
tff(func_def_40,type,
sK13: ( del * $i * $i ) > $i ).
tff(func_def_41,type,
sK14: ( del * $i * $i ) > $i ).
tff(func_def_42,type,
sK22: del ).
tff(func_def_43,type,
sK23: del ).
tff(pred_def_1,type,
mem: ( $i * del ) > $o ).
tff(pred_def_3,type,
sP3: ( tp__o * tp__o ) > $o ).
tff(pred_def_4,type,
sP4: ( tp__o * tp__o ) > $o ).
tff(pred_def_5,type,
sP15: ( tp__o * tp__o ) > $o ).
tff(pred_def_6,type,
sP16: ( tp__o * tp__o * tp__o ) > $o ).
tff(pred_def_7,type,
sP17: ( tp__o * tp__o * tp__o ) > $o ).
tff(pred_def_8,type,
sP18: ( tp__o * tp__o ) > $o ).
tff(pred_def_9,type,
sP19: ( tp__o * tp__o ) > $o ).
tff(pred_def_10,type,
sP20: ( tp__o * tp__o ) > $o ).
tff(pred_def_11,type,
sP21: ( tp__o * tp__o ) > $o ).
tff(f1,axiom,
! [X0: del,X1: del,X2: $i] :
( mem(X2,arr(X0,X1))
=> ! [X3: $i] :
( mem(X3,X0)
=> mem(ap(X2,X3),X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/ITP001/ITP001_2.ax',ap_tp) ).
tff(f46,axiom,
! [X0: del,X1: del,X2: $i] :
( mem(X2,arr(X0,X1))
=> ! [X3: $i] :
( mem(X3,arr(X1,bool))
=> ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X0,X1),X2),X3))
<=> ! [X4: $i] :
( mem(X4,X1)
=> ( p(ap(X3,X4))
=> ? [X5: $i] :
( mem(X5,X0)
& p(ap(X3,ap(X2,X5))) ) ) ) )
& ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL(X0,X1),X2),X3))
<=> ! [X6: $i] :
( mem(X6,X1)
=> ( ~ p(ap(X3,X6))
=> ? [X7: $i] :
( mem(X7,X0)
& ~ p(ap(X3,ap(X2,X7))) ) ) ) )
& ! [X8: $i] :
( mem(X8,arr(X0,X1))
=> ! [X9: $i] :
( mem(X9,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X8),X9))
<=> ! [X10: $i] :
( mem(X10,X0)
=> p(ap(X9,ap(X8,X10))) ) ) ) )
& ! [X11: $i] :
( mem(X11,arr(X0,X1))
=> ! [X12: $i] :
( mem(X12,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
<=> ! [X13: $i] :
( mem(X13,X0)
=> ~ p(ap(X12,ap(X11,X13))) ) ) ) )
& ! [X14: $i] :
( mem(X14,arr(X0,X1))
=> ! [X15: $i] :
( mem(X15,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X0,X1),X14),X15))
<=> ! [X16: $i] :
( mem(X16,X1)
=> ( p(ap(X15,X16))
=> ? [X17: $i] :
( mem(X17,X0)
& ( X16 = ap(X14,X17) ) ) ) ) ) ) )
& ! [X18: $i] :
( mem(X18,arr(X0,X1))
=> ! [X19: $i] :
( mem(X19,arr(X1,bool))
=> ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X0,X1),X18),X19))
<=> ! [X20: $i] :
( mem(X20,X1)
=> ( ~ p(ap(X19,X20))
=> ? [X21: $i] :
( mem(X21,X0)
& ( X20 = ap(X18,X21) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2EquantHeuristics_2EGUESS__REWRITES) ).
tff(f58,conjecture,
! [X0: del,X1: del,X2: $i] :
( mem(X2,arr(X1,X0))
=> ! [X3: $i] :
( mem(X3,arr(X0,bool))
=> ! [X4: $i] :
( mem(X4,arr(X0,bool))
=> ( ! [X5: $i] :
( 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) ).
tff(f59,negated_conjecture,
~ ! [X0: del,X1: del,X2: $i] :
( mem(X2,arr(X1,X0))
=> ! [X3: $i] :
( mem(X3,arr(X0,bool))
=> ! [X4: $i] :
( mem(X4,arr(X0,bool))
=> ( ! [X5: $i] :
( 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)],[f58]) ).
tff(f60,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f1]) ).
tff(f82,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X0,X1),X2),X3))
<=> ! [X4: $i] :
( ? [X5: $i] :
( 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: $i] :
( ? [X7: $i] :
( mem(X7,X0)
& ~ p(ap(X3,ap(X2,X7))) )
| p(ap(X3,X6))
| ~ mem(X6,X1) ) )
& ! [X8: $i] :
( ! [X9: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X8),X9))
<=> ! [X10: $i] :
( p(ap(X9,ap(X8,X10)))
| ~ mem(X10,X0) ) )
| ~ mem(X9,arr(X1,bool)) )
| ~ mem(X8,arr(X0,X1)) )
& ! [X11: $i] :
( ! [X12: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
<=> ! [X13: $i] :
( ~ p(ap(X12,ap(X11,X13)))
| ~ mem(X13,X0) ) )
| ~ mem(X12,arr(X1,bool)) )
| ~ mem(X11,arr(X0,X1)) )
& ! [X14: $i] :
( ! [X15: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X0,X1),X14),X15))
<=> ! [X16: $i] :
( ? [X17: $i] :
( 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: $i] :
( ! [X19: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X0,X1),X18),X19))
<=> ! [X20: $i] :
( ? [X21: $i] :
( 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)) ),
inference(ennf_transformation,[],[f46]) ).
tff(f83,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( ( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS(X0,X1),X2),X3))
<=> ! [X4: $i] :
( ? [X5: $i] :
( 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: $i] :
( ? [X7: $i] :
( mem(X7,X0)
& ~ p(ap(X3,ap(X2,X7))) )
| p(ap(X3,X6))
| ~ mem(X6,X1) ) )
& ! [X8: $i] :
( ! [X9: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X8),X9))
<=> ! [X10: $i] :
( p(ap(X9,ap(X8,X10)))
| ~ mem(X10,X0) ) )
| ~ mem(X9,arr(X1,bool)) )
| ~ mem(X8,arr(X0,X1)) )
& ! [X11: $i] :
( ! [X12: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
<=> ! [X13: $i] :
( ~ p(ap(X12,ap(X11,X13)))
| ~ mem(X13,X0) ) )
| ~ mem(X12,arr(X1,bool)) )
| ~ mem(X11,arr(X0,X1)) )
& ! [X14: $i] :
( ! [X15: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__GAP(X0,X1),X14),X15))
<=> ! [X16: $i] :
( ? [X17: $i] :
( 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: $i] :
( ! [X19: $i] :
( ( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__GAP(X0,X1),X18),X19))
<=> ! [X20: $i] :
( ? [X21: $i] :
( 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)) ),
inference(flattening,[],[f82]) ).
tff(f97,plain,
? [X0: del,X1: del,X2: $i] :
( ? [X3: $i] :
( ? [X4: $i] :
( ~ 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: $i] :
( 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)) ),
inference(ennf_transformation,[],[f59]) ).
tff(f98,plain,
? [X0: del,X1: del,X2: $i] :
( ? [X3: $i] :
( ? [X4: $i] :
( ~ 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: $i] :
( 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)) ),
inference(flattening,[],[f97]) ).
tff(f99,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0)
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f60]) ).
tff(f176,plain,
! [X2: $i,X3: $i,X0: del,X11: $i,X1: del,X12: $i,X13: $i] :
( ~ 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)) ),
inference(cnf_transformation,[],[f83]) ).
tff(f177,plain,
! [X2: $i,X3: $i,X0: del,X11: $i,X1: del,X12: $i] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X11,arr(X0,X1))
| ~ mem(X12,arr(X1,bool))
| mem(sK11(X0,X11,X12),X0)
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f83]) ).
tff(f178,plain,
! [X2: $i,X3: $i,X0: del,X11: $i,X1: del,X12: $i] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12))
| ~ mem(X3,arr(X1,bool))
| ~ mem(X11,arr(X0,X1))
| ~ mem(X12,arr(X1,bool))
| p(ap(X12,ap(X11,sK11(X0,X11,X12))))
| ~ mem(X2,arr(X0,X1)) ),
inference(cnf_transformation,[],[f83]) ).
tff(f256,plain,
! [X5: $i] :
( p(ap(sK25,X5))
| ~ p(ap(sK26,X5))
| ~ mem(X5,sK22) ),
inference(cnf_transformation,[],[f98]) ).
tff(f257,plain,
mem(sK26,arr(sK22,bool)),
inference(cnf_transformation,[],[f98]) ).
tff(f258,plain,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK23,sK22),sK24),sK25)),
inference(cnf_transformation,[],[f98]) ).
tff(f259,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK23,sK22),sK24),sK26)),
inference(cnf_transformation,[],[f98]) ).
tff(f260,plain,
mem(sK25,arr(sK22,bool)),
inference(cnf_transformation,[],[f98]) ).
tff(f261,plain,
mem(sK24,arr(sK23,sK22)),
inference(cnf_transformation,[],[f98]) ).
tff(f1100,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,arr(sK22,bool))
| ~ mem(sK24,arr(sK23,sK22))
| ~ mem(sK26,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23)
| ~ mem(X1,arr(sK23,sK22)) ),
inference(resolution,[],[f177,f259]) ).
tff(f1101,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,arr(sK22,bool))
| ~ mem(sK26,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23)
| ~ mem(X1,arr(sK23,sK22)) ),
inference(forward_subsumption_resolution,[],[f1100,f261]) ).
tff(f1102,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,arr(sK22,bool))
| mem(sK11(sK23,sK24,sK26),sK23)
| ~ mem(X1,arr(sK23,sK22)) ),
inference(forward_subsumption_resolution,[],[f1101,f257]) ).
tff(f1110,definition,
( spl27_10
<=> ! [X1: $i] : ~ mem(X1,arr(sK23,sK22)) ),
introduced(definition,[new_symbols(definition,[spl27_10])],[avatar_definition]) ).
tff(f1111,plain,
( ! [X1: $i] : ~ mem(X1,arr(sK23,sK22))
| ~ spl27_10 ),
inference(avatar_component_clause,[],[f1110]) ).
tff(f1113,definition,
( spl27_11
<=> mem(sK11(sK23,sK24,sK26),sK23) ),
introduced(definition,[new_symbols(definition,[spl27_11])],[avatar_definition]) ).
tff(f1115,plain,
( mem(sK11(sK23,sK24,sK26),sK23)
| ~ spl27_11 ),
inference(avatar_component_clause,[],[f1113]) ).
tff(f1117,definition,
( spl27_12
<=> ! [X0: $i] : ~ mem(X0,arr(sK22,bool)) ),
introduced(definition,[new_symbols(definition,[spl27_12])],[avatar_definition]) ).
tff(f1118,plain,
( ! [X0: $i] : ~ mem(X0,arr(sK22,bool))
| ~ spl27_12 ),
inference(avatar_component_clause,[],[f1117]) ).
tff(f1119,plain,
( spl27_10
| spl27_11
| spl27_12 ),
inference(avatar_split_clause,[],[f1102,f1117,f1113,f1110]) ).
tff(f1156,plain,
( $false
| ~ spl27_10 ),
inference(resolution,[],[f1111,f261]) ).
tff(f1161,plain,
~ spl27_10,
inference(avatar_contradiction_clause,[],[f1156]) ).
tff(f1249,plain,
! [X2: $i,X0: $i,X1: $i] :
( ~ 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)) ),
inference(resolution,[],[f176,f258]) ).
tff(f1318,plain,
! [X2: $i,X0: $i,X1: $i] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(X2,arr(sK23,sK22))
| ~ mem(X0,sK23)
| ~ mem(sK24,arr(sK23,sK22)) ),
inference(forward_subsumption_resolution,[],[f1249,f260]) ).
tff(f1319,plain,
! [X2: $i,X0: $i,X1: $i] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X1,arr(sK22,bool))
| ~ mem(X2,arr(sK23,sK22))
| ~ mem(X0,sK23) ),
inference(forward_subsumption_resolution,[],[f1318,f261]) ).
tff(f1321,definition,
( spl27_13
<=> ! [X0: $i] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X0,sK23) ) ),
introduced(definition,[new_symbols(definition,[spl27_13])],[avatar_definition]) ).
tff(f1322,plain,
( ! [X0: $i] :
( ~ p(ap(sK25,ap(sK24,X0)))
| ~ mem(X0,sK23) )
| ~ spl27_13 ),
inference(avatar_component_clause,[],[f1321]) ).
tff(f1323,plain,
( spl27_10
| spl27_12
| spl27_13 ),
inference(avatar_split_clause,[],[f1319,f1321,f1117,f1110]) ).
tff(f1325,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,arr(sK22,bool))
| ~ mem(sK24,arr(sK23,sK22))
| ~ mem(sK26,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ mem(X1,arr(sK23,sK22)) ),
inference(resolution,[],[f178,f259]) ).
tff(f1328,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,arr(sK22,bool))
| ~ mem(sK26,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ mem(X1,arr(sK23,sK22)) ),
inference(forward_subsumption_resolution,[],[f1325,f261]) ).
tff(f1329,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,arr(sK22,bool))
| p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ mem(X1,arr(sK23,sK22)) ),
inference(forward_subsumption_resolution,[],[f1328,f257]) ).
tff(f1330,plain,
( $false
| ~ spl27_12 ),
inference(resolution,[],[f1118,f257]) ).
tff(f1342,plain,
~ spl27_12,
inference(avatar_contradiction_clause,[],[f1330]) ).
tff(f1344,plain,
( ! [X0: $i] :
( ~ p(ap(sK26,ap(sK24,X0)))
| ~ mem(X0,sK23)
| ~ mem(ap(sK24,X0),sK22) )
| ~ spl27_13 ),
inference(resolution,[],[f1322,f256]) ).
tff(f1414,definition,
( spl27_14
<=> p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26)))) ),
introduced(definition,[new_symbols(definition,[spl27_14])],[avatar_definition]) ).
tff(f1416,plain,
( p(ap(sK26,ap(sK24,sK11(sK23,sK24,sK26))))
| ~ spl27_14 ),
inference(avatar_component_clause,[],[f1414]) ).
tff(f1417,plain,
( spl27_10
| spl27_14
| spl27_12 ),
inference(avatar_split_clause,[],[f1329,f1117,f1414,f1110]) ).
tff(f1527,plain,
( ~ mem(sK11(sK23,sK24,sK26),sK23)
| ~ mem(ap(sK24,sK11(sK23,sK24,sK26)),sK22)
| ~ spl27_13
| ~ spl27_14 ),
inference(resolution,[],[f1416,f1344]) ).
tff(f1530,plain,
( ~ mem(ap(sK24,sK11(sK23,sK24,sK26)),sK22)
| ~ spl27_11
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f1527,f1115]) ).
tff(f1575,plain,
( ! [X0: del] :
( ~ mem(sK11(sK23,sK24,sK26),X0)
| ~ mem(sK24,arr(X0,sK22)) )
| ~ spl27_11
| ~ spl27_13
| ~ spl27_14 ),
inference(resolution,[],[f1530,f99]) ).
tff(f1592,plain,
( ~ mem(sK24,arr(sK23,sK22))
| ~ spl27_11
| ~ spl27_13
| ~ spl27_14 ),
inference(resolution,[],[f1575,f1115]) ).
tff(f1593,plain,
( $false
| ~ spl27_11
| ~ spl27_13
| ~ spl27_14 ),
inference(forward_subsumption_resolution,[],[f1592,f261]) ).
tff(f1594,plain,
( ~ spl27_11
| ~ spl27_13
| ~ spl27_14 ),
inference(avatar_contradiction_clause,[],[f1593]) ).
cnf(s7,plain,
( spl27_10
| spl27_11
| spl27_12 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s8,plain,
~ spl27_10,
inference(sat_conversion,[],[f1161]) ).
cnf(s9,plain,
( spl27_10
| spl27_12
| spl27_13 ),
inference(sat_conversion,[],[f1323]) ).
cnf(s13,plain,
~ spl27_12,
inference(sat_conversion,[],[f1342]) ).
cnf(s14,plain,
( spl27_10
| spl27_12
| spl27_14 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s15,plain,
( ~ spl27_11
| ~ spl27_13
| ~ spl27_14 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s16,plain,
( spl27_10
| spl27_13 ),
inference(rat,[],[s9,s13]) ).
cnf(s17,plain,
spl27_14,
inference(rat,[],[s14,s13,s8]) ).
cnf(s18,plain,
spl27_13,
inference(rat,[],[s16,s8]) ).
cnf(s19,plain,
~ spl27_11,
inference(rat,[],[s15,s17,s18]) ).
cnf(s20,plain,
$false,
inference(rat,[],[s7,s13,s19,s8]) ).
tff(f1595,plain,
$false,
inference(avatar_sat_refutation,[],[s20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP006_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 11:47:50 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 Running first-order model finding
% 0.13/0.39 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
% 6.99/1.51 % (2410106)Will run a generic schedule for satisfiability detection.
% 6.99/1.51 % (2410115)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=675681972:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.99/1.51 % (2410112)% WARNING: option uhcvi not known.
% 6.99/1.51 % (2410111)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3981489748_2999 on theBenchmark for (2999ds/0Mi)
% 6.99/1.51 % (2410112)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2771753616:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.99/1.51 % (2410114)dis+10_1_sil=32000:sp=arity:random_seed=2093272482:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.99/1.51 % (2410113)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1873996450:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.99/1.51 % (2410116)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1103762906:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.99/1.51 % (2410117)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3400366357:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.99/1.51 % TRYING [1,1,1]
% 6.99/1.51 % (2410115)Instruction limit reached!
% 6.99/1.51 % (2410115)------------------------------
% 6.99/1.51 % (2410115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410115)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410115)Termination reason: Instruction limit
% 6.99/1.51 % (2410115)Termination phase: Saturation
% 6.99/1.51 % (2410115)Time elapsed: 0.036 s
% 6.99/1.51 % (2410115)Peak memory usage: 13 MB
% 6.99/1.51 % (2410115)Instructions burned: 118 (million)
% 6.99/1.51 % TRYING [1,2,1]
% 6.99/1.51 % TRYING [1,2,2]
% 6.99/1.51 % TRYING [1,3,2]
% 6.99/1.51 % (2410125)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4109501534:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.99/1.51 % TRYING [1]
% 6.99/1.51 % TRYING [2]
% 6.99/1.51 % TRYING [1,4,2]
% 6.99/1.51 % TRYING [3]
% 6.99/1.51 % (2410114)Instruction limit reached!
% 6.99/1.51 % (2410114)------------------------------
% 6.99/1.51 % (2410114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410114)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410114)Termination reason: Instruction limit
% 6.99/1.51 % (2410114)Termination phase: Saturation
% 6.99/1.51 % (2410114)Time elapsed: 0.067 s
% 6.99/1.51 % (2410114)Peak memory usage: 13 MB
% 6.99/1.51 % (2410114)Instructions burned: 104 (million)
% 6.99/1.51 % (2410116)Instruction limit reached!
% 6.99/1.51 % (2410116)------------------------------
% 6.99/1.51 % (2410116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410116)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410116)Termination reason: Instruction limit
% 6.99/1.51 % (2410116)Termination phase: Saturation
% 6.99/1.51 % (2410116)Time elapsed: 0.076 s
% 6.99/1.51 % (2410116)Peak memory usage: 13 MB
% 6.99/1.51 % (2410116)Instructions burned: 131 (million)
% 6.99/1.51 % TRYING [4]
% 6.99/1.51 % TRYING [2,4,2]
% 6.99/1.51 % (2410127)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=491566473:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.99/1.51 % (2410128)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=2717754387:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.99/1.51 % (2410117)Instruction limit reached!
% 6.99/1.51 % (2410117)------------------------------
% 6.99/1.51 % (2410117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410117)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410117)Termination reason: Instruction limit
% 6.99/1.51 % (2410117)Termination phase: Saturation
% 6.99/1.51 % (2410117)Time elapsed: 0.104 s
% 6.99/1.51 % (2410117)Peak memory usage: 14 MB
% 6.99/1.51 % (2410117)Instructions burned: 160 (million)
% 6.99/1.51 % (2410131)ott-21_1_sil=16000:fs=off:random_seed=3851128684:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.99/1.51 % TRYING [1,5,2]
% 6.99/1.51 % TRYING [5]
% 6.99/1.51 % (2410127)Instruction limit reached!
% 6.99/1.51 % (2410127)------------------------------
% 6.99/1.51 % (2410127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410127)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410127)Termination reason: Instruction limit
% 6.99/1.51 % (2410127)Termination phase: Saturation
% 6.99/1.51 % (2410127)Time elapsed: 0.081 s
% 6.99/1.51 % (2410127)Peak memory usage: 14 MB
% 6.99/1.51 % (2410127)Instructions burned: 133 (million)
% 6.99/1.51 % (2410133)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3320485455:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.99/1.51 % (2410125)Instruction limit reached!
% 6.99/1.51 % (2410125)------------------------------
% 6.99/1.51 % (2410125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410125)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410125)Termination reason: Instruction limit
% 6.99/1.51 % (2410125)Termination phase: Finite model building constraint generation
% 6.99/1.51 % (2410125)Time elapsed: 0.151 s
% 6.99/1.51 % (2410125)Peak memory usage: 37 MB
% 6.99/1.51 % (2410125)Instructions burned: 714 (million)
% 6.99/1.51 % TRYING [3,4,2]
% 6.99/1.51 % (2410135)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3956594530:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.99/1.51 % (2410131)Instruction limit reached!
% 6.99/1.51 % (2410131)------------------------------
% 6.99/1.51 % (2410131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410131)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410131)Termination reason: Instruction limit
% 6.99/1.51 % (2410131)Termination phase: Saturation
% 6.99/1.51 % (2410131)Time elapsed: 0.090 s
% 6.99/1.51 % (2410131)Peak memory usage: 13 MB
% 6.99/1.51 % (2410131)Instructions burned: 180 (million)
% 6.99/1.51 % TRYING [1,1,1]
% 6.99/1.51 % TRYING [1,2,1]
% 6.99/1.51 % TRYING [1,2,2]
% 6.99/1.51 % (2410137)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3486251154:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 6.99/1.51 % TRYING [1,3,2]
% 6.99/1.51 % TRYING [2,3,2]
% 6.99/1.51 % TRYING [2,5,2]
% 6.99/1.51 % TRYING [1,4,2]
% 6.99/1.51 % TRYING [1,6,2]
% 6.99/1.51 % (2410135)Instruction limit reached!
% 6.99/1.51 % (2410135)------------------------------
% 6.99/1.51 % (2410135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410135)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410135)Termination reason: Instruction limit
% 6.99/1.51 % (2410135)Termination phase: Finite model building SAT solving
% 6.99/1.51 % (2410135)Time elapsed: 0.187 s
% 6.99/1.51 % (2410135)Peak memory usage: 19 MB
% 6.99/1.51 % (2410135)Instructions burned: 866 (million)
% 6.99/1.51 % (2410139)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1341408101:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 6.99/1.51 % (2410128)Instruction limit reached!
% 6.99/1.51 % (2410128)------------------------------
% 6.99/1.51 % (2410128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410128)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410128)Termination reason: Instruction limit
% 6.99/1.51 % (2410128)Termination phase: Saturation
% 6.99/1.51 % (2410128)Time elapsed: 0.375 s
% 6.99/1.51 % (2410128)Peak memory usage: 18 MB
% 6.99/1.51 % (2410128)Instructions burned: 685 (million)
% 6.99/1.51 % TRYING [4,4,2]
% 6.99/1.51 % (2410133)Instruction limit reached!
% 6.99/1.51 % (2410133)------------------------------
% 6.99/1.51 % (2410133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410133)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410133)Termination reason: Instruction limit
% 6.99/1.51 % (2410133)Termination phase: Saturation
% 6.99/1.51 % (2410133)Time elapsed: 0.295 s
% 6.99/1.51 % (2410133)Peak memory usage: 13 MB
% 6.99/1.51 % (2410133)Instructions burned: 477 (million)
% 6.99/1.51 % (2410141)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=2098382696: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)
% 6.99/1.51 % (2410142)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2918129032:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 6.99/1.51 % TRYING [3,5,2]
% 6.99/1.51 % (2410139)Instruction limit reached!
% 6.99/1.51 % (2410139)------------------------------
% 6.99/1.51 % (2410139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410139)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410139)Termination reason: Instruction limit
% 6.99/1.51 % (2410139)Termination phase: Finite model building constraint generation
% 6.99/1.51 % (2410139)Time elapsed: 0.239 s
% 6.99/1.51 % (2410139)Peak memory usage: 105 MB
% 6.99/1.51 % (2410139)Instructions burned: 890 (million)
% 6.99/1.51 % (2410145)fmb+10_1_sil=64000:random_seed=2327409252:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 6.99/1.51 % TRYING [1,1,1]
% 6.99/1.51 % TRYING [1,2,1]
% 6.99/1.51 % TRYING [1,2,2]
% 6.99/1.51 % TRYING [1,3,2]
% 6.99/1.51 % TRYING [2,3,2]
% 6.99/1.51 % TRYING [1,4,2]
% 6.99/1.51 % TRYING [2,6,2]
% 6.99/1.51 % TRYING [2,4,2]
% 6.99/1.51 % TRYING [2,3,3]
% 6.99/1.51 % (2410137)Instruction limit reached!
% 6.99/1.51 % (2410137)------------------------------
% 6.99/1.51 % (2410137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410137)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410137)Termination reason: Instruction limit
% 6.99/1.51 % (2410137)Termination phase: Saturation
% 6.99/1.51 % (2410137)Time elapsed: 0.657 s
% 6.99/1.51 % (2410137)Peak memory usage: 21 MB
% 6.99/1.51 % (2410137)Instructions burned: 1179 (million)
% 6.99/1.51 % TRYING [1,5,2]
% 6.99/1.51 % (2410141)Instruction limit reached!
% 6.99/1.51 % (2410141)------------------------------
% 6.99/1.51 % (2410141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410141)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410141)Termination reason: Instruction limit
% 6.99/1.51 % (2410141)Termination phase: Saturation
% 6.99/1.51 % (2410141)Time elapsed: 0.417 s
% 6.99/1.51 % (2410141)Peak memory usage: 16 MB
% 6.99/1.51 % (2410141)Instructions burned: 693 (million)
% 6.99/1.51 % (2410147)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3545970856:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 6.99/1.51 % TRYING [1,7,2]
% 6.99/1.51 % (2410148)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2545264589:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 6.99/1.51 % TRYING [20,20,20]
% 6.99/1.51 % TRYING [8,8,8]
% 6.99/1.51 % (2410142)Instruction limit reached!
% 6.99/1.51 % (2410142)------------------------------
% 6.99/1.51 % (2410142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.51 % (2410142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.51 % (2410142)CaDiCaL version: 2.1.3
% 6.99/1.51 % (2410142)Termination reason: Instruction limit
% 6.99/1.51 % (2410142)Termination phase: Saturation
% 6.99/1.51 % (2410142)Time elapsed: 0.483 s
% 6.99/1.51 % (2410142)Peak memory usage: 19 MB
% 6.99/1.51 % (2410142)Instructions burned: 879 (million)
% 6.99/1.51 % (2410151)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1270317516:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 6.99/1.51 % TRYING [3,4,2]
% 6.99/1.51 % (2410151) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2410106-2410151"...
% 6.99/1.51 % (2410151)...printing done.
% 6.99/1.51 % (2410151)Refutation found. Thanks to Tanya!
% 6.99/1.51 % SZS status Theorem for theBenchmark
% 6.99/1.51 % SZS output start Proof for theBenchmark
% See solution above
% 6.99/1.52 % (2410151)------------------------------
% 6.99/1.52 % (2410151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.52 % (2410151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.52 % (2410151)CaDiCaL version: 2.1.3
% 6.99/1.52 % (2410151)Termination reason: Refutation
% 6.99/1.52 % (2410151)Time elapsed: 0.057 s
% 6.99/1.52 % (2410151)Peak memory usage: 13 MB
% 6.99/1.52 % (2410151)Instructions burned: 95 (million)
% 6.99/1.52 % (2410106)Success in time 1.112 s
% 6.99/1.52 % Vampire exiting
%------------------------------------------------------------------------------