%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP020_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:35:52 AM UTC 2026
% Result : Theorem 7.80s 1.69s
% Output : Refutation 7.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 7
% Syntax : Number of formulae : 38 ( 12 unt; 0 typ; 1 def)
% Number of atoms : 183 ( 0 equ)
% Maximal formula atoms : 6 ( 4 avg)
% Number of connectives : 105 ( 50 ~; 41 |; 7 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of FOOLs : 90 ( 90 fml; 0 var)
% Number of types : 6 ( 4 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 12 usr; 3 prp; 0-3 aty)
% Number of functors : 52 ( 52 usr; 5 con; 0-4 aty)
% Number of variables : 52 ( 0 sgn 45 !; 7 ?; 52 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
del: $tType ).
tff(type_def_6,type,
tp__o: $tType ).
tff(type_def_7,type,
tp__ty_2Enum_2Enum: $tType ).
tff(type_def_8,type,
tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: $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_11,type,
fo__c_2Ebool_2EF: tp__o ).
tff(func_def_13,type,
fo__c_2Emin_2E_3D_3D_3E: ( tp__o * tp__o ) > tp__o ).
tff(func_def_15,type,
fo__c_2Ebool_2E_5C_2F: ( tp__o * tp__o ) > tp__o ).
tff(func_def_17,type,
fo__c_2Ebool_2E_2F_5C: ( tp__o * tp__o ) > tp__o ).
tff(func_def_19,type,
fo__c_2Ebool_2E_7E: tp__o > tp__o ).
tff(func_def_20,type,
c_2Emin_2E_3D: del > $i ).
tff(func_def_21,type,
c_2Ebool_2E_21: del > $i ).
tff(func_def_22,type,
c_2Epred__set_2EUNIV: del > $i ).
tff(func_def_23,type,
ty_2Epair_2Eprod: ( del * del ) > del ).
tff(func_def_24,type,
c_2Epred__set_2ECROSS: ( del * del ) > $i ).
tff(func_def_25,type,
c_2Epred__set_2EBIJ: ( del * del ) > $i ).
tff(func_def_26,type,
ty_2Enum_2Enum: del ).
tff(func_def_27,type,
inj__ty_2Enum_2Enum: tp__ty_2Enum_2Enum > $i ).
tff(func_def_28,type,
surj__ty_2Enum_2Enum: $i > tp__ty_2Enum_2Enum ).
tff(func_def_29,type,
inj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum > $i ).
tff(func_def_30,type,
surj__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum: $i > tp__c_ty_2Epair_2Eprod_ty_2Enum_2Enum_ty_2Enum_2Enum ).
tff(func_def_31,type,
c_2Ebool_2E_3F: del > $i ).
tff(func_def_32,type,
sK0: ( del * $i * $i ) > $i ).
tff(func_def_33,type,
sK1: ( del * $i ) > $i ).
tff(func_def_34,type,
sK2: ( del * $i ) > $i ).
tff(func_def_35,type,
sK3: ( del * $i ) > $i ).
tff(func_def_36,type,
sK4: ( del * $i ) > $i ).
tff(func_def_37,type,
sK5: ( del * $i * tp__o ) > $i ).
tff(func_def_38,type,
sK6: ( del * $i ) > $i ).
tff(func_def_39,type,
sK7: ( del * tp__o * $i ) > $i ).
tff(func_def_40,type,
sK8: ( del * $i ) > $i ).
tff(func_def_41,type,
sK9: ( del * $i * tp__o ) > $i ).
tff(func_def_42,type,
sK10: ( del * $i ) > $i ).
tff(func_def_43,type,
sK11: ( del * tp__o * $i ) > $i ).
tff(func_def_44,type,
sK12: ( del * $i ) > $i ).
tff(func_def_45,type,
sK13: ( del * $i * tp__o ) > $i ).
tff(func_def_46,type,
sK14: ( del * $i ) > $i ).
tff(func_def_47,type,
sK15: ( del * tp__o * $i ) > $i ).
tff(func_def_48,type,
sK16: ( del * $i ) > $i ).
tff(func_def_49,type,
sK17: ( del * tp__o * $i ) > $i ).
tff(func_def_50,type,
sK18: ( del * $i ) > $i ).
tff(func_def_51,type,
sK19: ( del * tp__o * $i ) > $i ).
tff(func_def_52,type,
sK20: ( del * $i ) > $i ).
tff(func_def_53,type,
sK21: ( del * del * $i ) > $i ).
tff(func_def_54,type,
sK22: ( del * del * $i ) > $i ).
tff(func_def_55,type,
sK23: ( del * $i * $i ) > $i ).
tff(func_def_56,type,
sK24: ( del * $i * $i ) > $i ).
tff(func_def_57,type,
sK25: ( del * del * $i * $i ) > $i ).
tff(func_def_58,type,
sK26: ( del * del * $i * $i ) > $i ).
tff(pred_def_1,type,
mem: ( $i * del ) > $o ).
tff(pred_def_3,type,
sP27: ( tp__o * tp__o ) > $o ).
tff(pred_def_4,type,
sP28: ( tp__o * tp__o * tp__o ) > $o ).
tff(pred_def_5,type,
sP29: ( tp__o * tp__o * tp__o ) > $o ).
tff(pred_def_6,type,
sP30: ( tp__o * tp__o ) > $o ).
tff(pred_def_7,type,
sP31: ( tp__o * tp__o ) > $o ).
tff(pred_def_8,type,
sP32: ( tp__o * tp__o ) > $o ).
tff(pred_def_9,type,
sP33: ( 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/sandbox2/benchmark/Axioms/ITP001/ITP001_2.ax',ap_tp) ).
tff(f31,axiom,
! [X0: del] : mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Epred__set_2EUNIV) ).
tff(f32,axiom,
! [X0: del,X1: del] : mem(c_2Epred__set_2ECROSS(X0,X1),arr(arr(X0,bool),arr(arr(X1,bool),arr(ty_2Epair_2Eprod(X0,X1),bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Epred__set_2ECROSS) ).
tff(f61,axiom,
! [X0: del,X1: del,X2: $i] :
( mem(X2,arr(X0,bool))
=> ! [X3: $i] :
( mem(X3,arr(X1,bool))
=> ( ? [X4: $i] :
( mem(X4,arr(X0,X1))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3)) )
<=> ? [X5: $i] :
( mem(X5,arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EBIJ__SYM) ).
tff(f72,axiom,
? [X0: $i] :
( mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ) ).
tff(f73,conjecture,
? [X0: $i] :
( mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV) ).
tff(f74,negated_conjecture,
~ ? [X0: $i] :
( mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) ),
inference(negated_conjecture,[status(cth)],[f73]) ).
tff(f75,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(f112,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( ( ? [X4: $i] :
( mem(X4,arr(X0,X1))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3)) )
<=> ? [X5: $i] :
( mem(X5,arr(X1,X0))
& p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2)) ) )
| ~ mem(X3,arr(X1,bool)) )
| ~ mem(X2,arr(X0,bool)) ),
inference(ennf_transformation,[],[f61]) ).
tff(f122,plain,
! [X0: $i] :
( ~ mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))) ),
inference(ennf_transformation,[],[f74]) ).
tff(f123,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,[],[f75]) ).
tff(f165,plain,
! [X0: del] : mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool)),
inference(cnf_transformation,[],[f31]) ).
tff(f166,plain,
! [X0: del,X1: del] : mem(c_2Epred__set_2ECROSS(X0,X1),arr(arr(X0,bool),arr(arr(X1,bool),arr(ty_2Epair_2Eprod(X0,X1),bool)))),
inference(cnf_transformation,[],[f32]) ).
tff(f226,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X5: $i] :
( mem(sK25(X0,X1,X2,X3),arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0))
| ~ mem(X2,arr(X0,bool)) ),
inference(cnf_transformation,[],[f112]) ).
tff(f227,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X5: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),sK25(X0,X1,X2,X3)),X2),X3))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0))
| ~ mem(X2,arr(X0,bool)) ),
inference(cnf_transformation,[],[f112]) ).
tff(f293,plain,
p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK34),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),
inference(cnf_transformation,[],[f72]) ).
tff(f294,plain,
mem(sK34,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f72]) ).
tff(f295,plain,
! [X0: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),X0),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))))
| ~ mem(X0,arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) ),
inference(cnf_transformation,[],[f122]) ).
tff(f1026,definition,
( spl35_1
<=> mem(ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)) ),
introduced(definition,[new_symbols(definition,[spl35_1])],[avatar_definition]) ).
tff(f1027,plain,
( mem(ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ spl35_1 ),
inference(avatar_component_clause,[],[f1026]) ).
tff(f1028,plain,
( ~ mem(ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| spl35_1 ),
inference(avatar_component_clause,[],[f1026]) ).
tff(f1034,plain,
( ! [X0: del] :
( ~ mem(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool)))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),X0) )
| spl35_1 ),
inference(resolution,[],[f1028,f123]) ).
tff(f1047,plain,
( ! [X0: del,X1: del] :
( ~ mem(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),arr(X1,arr(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),X1)
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),X0) )
| spl35_1 ),
inference(resolution,[],[f1034,f123]) ).
tff(f1048,plain,
( ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| spl35_1 ),
inference(resolution,[],[f1047,f166]) ).
tff(f1049,plain,
( ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| spl35_1 ),
inference(duplicate_literal_removal,[],[f1048]) ).
tff(f1050,plain,
( $false
| spl35_1 ),
inference(forward_subsumption_resolution,[],[f1049,f165]) ).
tff(f1051,plain,
spl35_1,
inference(avatar_contradiction_clause,[],[f1050]) ).
tff(f2394,plain,
! [X0: $i] :
( ~ mem(ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(sK25(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) ),
inference(resolution,[],[f227,f295]) ).
tff(f2395,plain,
! [X0: $i] :
( ~ mem(ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool)) ),
inference(forward_subsumption_resolution,[],[f2394,f226]) ).
tff(f2396,plain,
( ! [X0: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool)) )
| ~ spl35_1 ),
inference(forward_subsumption_resolution,[],[f2395,f1027]) ).
tff(f2397,plain,
( ! [X0: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),X0),ap(ap(c_2Epred__set_2ECROSS(ty_2Enum_2Enum,ty_2Enum_2Enum),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum))),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)))
| ~ mem(X0,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) )
| ~ spl35_1 ),
inference(forward_subsumption_resolution,[],[f2396,f165]) ).
tff(f2398,plain,
( ~ mem(sK34,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ spl35_1 ),
inference(resolution,[],[f2397,f293]) ).
tff(f2419,plain,
( $false
| ~ spl35_1 ),
inference(forward_subsumption_resolution,[],[f2398,f294]) ).
tff(f2420,plain,
~ spl35_1,
inference(avatar_contradiction_clause,[],[f2419]) ).
cnf(s2,plain,
spl35_1,
inference(sat_conversion,[],[f1051]) ).
cnf(s31,plain,
~ spl35_1,
inference(sat_conversion,[],[f2420]) ).
cnf(s48,plain,
$false,
inference(rat,[],[s2,s31]) ).
tff(f2421,plain,
$false,
inference(avatar_sat_refutation,[],[s48]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP020_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 12:09:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.80/1.69 % (3424273)Will run a generic schedule for satisfiability detection.
% 7.80/1.69 % (3424278)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3647947531_2999 on theBenchmark for (2999ds/0Mi)
% 7.80/1.69 % (3424279)% WARNING: option uhcvi not known.
% 7.80/1.69 % (3424279)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=556337899:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.80/1.69 % (3424280)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2998570800:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.80/1.69 % (3424281)dis+10_1_sil=32000:sp=arity:random_seed=3320997943:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.80/1.69 % (3424282)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1906173967:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.80/1.69 % (3424284)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4026363319:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.80/1.69 % (3424283)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=692360164:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.80/1.69 % TRYING [1,1,1,1,1]
% 7.80/1.69 % TRYING [1,2,1,1,1]
% 7.80/1.69 % TRYING [1,2,2,1,1]
% 7.80/1.69 % TRYING [2,2,2,1,1]
% 7.80/1.69 % TRYING [2,3,2,1,1]
% 7.80/1.69 % TRYING [2,4,2,1,1]
% 7.80/1.69 % (3424281)Instruction limit reached!
% 7.80/1.69 % (3424281)------------------------------
% 7.80/1.69 % (3424281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424281)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424281)Termination reason: Instruction limit
% 7.80/1.69 % (3424281)Termination phase: Saturation
% 7.80/1.69 % (3424281)Time elapsed: 0.066 s
% 7.80/1.69 % (3424281)Peak memory usage: 13 MB
% 7.80/1.69 % (3424281)Instructions burned: 104 (million)
% 7.80/1.69 % (3424282)Instruction limit reached!
% 7.80/1.69 % (3424282)------------------------------
% 7.80/1.69 % (3424282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424282)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424282)Termination reason: Instruction limit
% 7.80/1.69 % (3424282)Termination phase: Saturation
% 7.80/1.69 % (3424282)Time elapsed: 0.069 s
% 7.80/1.69 % (3424282)Peak memory usage: 13 MB
% 7.80/1.69 % (3424282)Instructions burned: 116 (million)
% 7.80/1.69 % (3424283)Instruction limit reached!
% 7.80/1.69 % (3424283)------------------------------
% 7.80/1.69 % (3424283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424283)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424283)Termination reason: Instruction limit
% 7.80/1.69 % (3424283)Termination phase: Saturation
% 7.80/1.69 % (3424283)Time elapsed: 0.071 s
% 7.80/1.69 % (3424283)Peak memory usage: 13 MB
% 7.80/1.69 % (3424283)Instructions burned: 131 (million)
% 7.80/1.69 % TRYING [3,4,2,1,1]
% 7.80/1.69 % (3424292)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1505981369:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.80/1.69 % (3424293)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4234939274:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.80/1.69 % (3424294)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=1240769940:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.80/1.69 % (3424284)Instruction limit reached!
% 7.80/1.69 % (3424284)------------------------------
% 7.80/1.69 % (3424284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424284)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424284)Termination reason: Instruction limit
% 7.80/1.69 % (3424284)Termination phase: Saturation
% 7.80/1.69 % (3424284)Time elapsed: 0.100 s
% 7.80/1.69 % (3424284)Peak memory usage: 14 MB
% 7.80/1.69 % (3424284)Instructions burned: 159 (million)
% 7.80/1.69 % TRYING [1]
% 7.80/1.69 % TRYING [2]
% 7.80/1.69 % TRYING [2,5,2,1,1]
% 7.80/1.69 % (3424298)ott-21_1_sil=16000:fs=off:random_seed=2174271620:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.80/1.69 % TRYING [3]
% 7.80/1.69 % TRYING [4]
% 7.80/1.69 % (3424293)Instruction limit reached!
% 7.80/1.69 % (3424293)------------------------------
% 7.80/1.69 % (3424293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424293)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424293)Termination reason: Instruction limit
% 7.80/1.69 % (3424293)Termination phase: Saturation
% 7.80/1.69 % (3424293)Time elapsed: 0.080 s
% 7.80/1.69 % (3424293)Peak memory usage: 13 MB
% 7.80/1.69 % (3424293)Instructions burned: 131 (million)
% 7.80/1.69 % TRYING [4,4,2,1,1]
% 7.80/1.69 % (3424300)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2287048408:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 7.80/1.69 % (3424298)Instruction limit reached!
% 7.80/1.69 % (3424298)------------------------------
% 7.80/1.69 % (3424298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424298)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424298)Termination reason: Instruction limit
% 7.80/1.69 % (3424298)Termination phase: Saturation
% 7.80/1.69 % (3424298)Time elapsed: 0.089 s
% 7.80/1.69 % (3424298)Peak memory usage: 13 MB
% 7.80/1.69 % (3424298)Instructions burned: 182 (million)
% 7.80/1.69 % (3424302)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2800623845:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 7.80/1.69 % TRYING [3,5,2,1,1]
% 7.80/1.69 % TRYING [1,1,1,1,1]
% 7.80/1.69 % TRYING [5]
% 7.80/1.69 % TRYING [1,2,1,1,1]
% 7.80/1.69 % TRYING [1,2,2,1,1]
% 7.80/1.69 % TRYING [2,2,2,1,1]
% 7.80/1.69 % TRYING [2,6,2,1,1]
% 7.80/1.69 % (3424292)Instruction limit reached!
% 7.80/1.69 % (3424292)------------------------------
% 7.80/1.69 % (3424292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424292)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424292)Termination reason: Instruction limit
% 7.80/1.69 % (3424292)Termination phase: Finite model building constraint generation
% 7.80/1.69 % (3424292)Time elapsed: 0.279 s
% 7.80/1.69 % (3424292)Peak memory usage: 36 MB
% 7.80/1.69 % (3424292)Instructions burned: 716 (million)
% 7.80/1.69 % TRYING [2,3,2,1,1]
% 7.80/1.69 % (3424304)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1419702205:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 7.80/1.69 % TRYING [5,4,2,1,1]
% 7.80/1.69 % (3424294)Instruction limit reached!
% 7.80/1.69 % (3424294)------------------------------
% 7.80/1.69 % (3424294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424294)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424294)Termination reason: Instruction limit
% 7.80/1.69 % (3424294)Termination phase: Saturation
% 7.80/1.69 % (3424294)Time elapsed: 0.379 s
% 7.80/1.69 % (3424294)Peak memory usage: 19 MB
% 7.80/1.69 % (3424294)Instructions burned: 685 (million)
% 7.80/1.69 % TRYING [2,4,2,1,1]
% 7.80/1.69 % (3424306)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1076811418:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 7.80/1.69 % (3424300)Instruction limit reached!
% 7.80/1.69 % (3424300)------------------------------
% 7.80/1.69 % (3424300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424300)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424300)Termination reason: Instruction limit
% 7.80/1.69 % (3424300)Termination phase: Saturation
% 7.80/1.69 % (3424300)Time elapsed: 0.306 s
% 7.80/1.69 % (3424300)Peak memory usage: 13 MB
% 7.80/1.69 % (3424300)Instructions burned: 477 (million)
% 7.80/1.69 % (3424308)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=3332248064: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)
% 7.80/1.69 % TRYING [3,6,2,1,1]
% 7.80/1.69 % (3424302)Instruction limit reached!
% 7.80/1.69 % (3424302)------------------------------
% 7.80/1.69 % (3424302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424302)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424302)Termination reason: Instruction limit
% 7.80/1.69 % (3424302)Termination phase: Finite model building SAT solving
% 7.80/1.69 % (3424302)Time elapsed: 0.381 s
% 7.80/1.69 % (3424302)Peak memory usage: 22 MB
% 7.80/1.69 % (3424302)Instructions burned: 866 (million)
% 7.80/1.69 % (3424310)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=279498678:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 7.80/1.69 % TRYING [6,4,2,1,1]
% 7.80/1.69 % (3424308)Instruction limit reached!
% 7.80/1.69 % (3424308)------------------------------
% 7.80/1.69 % (3424308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424308)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424308)Termination reason: Instruction limit
% 7.80/1.69 % (3424308)Termination phase: Saturation
% 7.80/1.69 % (3424308)Time elapsed: 0.384 s
% 7.80/1.69 % (3424308)Peak memory usage: 16 MB
% 7.80/1.69 % (3424308)Instructions burned: 692 (million)
% 7.80/1.69 % TRYING [5,5,2,1,1]
% 7.80/1.69 % (3424306)Instruction limit reached!
% 7.80/1.69 % (3424306)------------------------------
% 7.80/1.69 % (3424306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424306)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424306)Termination reason: Instruction limit
% 7.80/1.69 % (3424306)Termination phase: Finite model building constraint generation
% 7.80/1.69 % (3424306)Time elapsed: 0.421 s
% 7.80/1.69 % (3424306)Peak memory usage: 105 MB
% 7.80/1.69 % (3424306)Instructions burned: 892 (million)
% 7.80/1.69 % (3424312)fmb+10_1_sil=64000:random_seed=4056186650:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 7.80/1.69 % (3424314)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=429423019:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 7.80/1.69 % TRYING [1,1,1,1,1]
% 7.80/1.69 % TRYING [1,2,1,1,1]
% 7.80/1.69 % TRYING [1,2,2,1,1]
% 7.80/1.69 % TRYING [20,20,20,20,20]
% 7.80/1.69 % TRYING [2,2,2,1,1]
% 7.80/1.69 % TRYING [2,3,2,1,1]
% 7.80/1.69 % (3424304)Instruction limit reached!
% 7.80/1.69 % (3424304)------------------------------
% 7.80/1.69 % (3424304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424304)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424304)Termination reason: Instruction limit
% 7.80/1.69 % (3424304)Termination phase: Saturation
% 7.80/1.69 % (3424304)Time elapsed: 0.654 s
% 7.80/1.69 % (3424304)Peak memory usage: 22 MB
% 7.80/1.69 % (3424304)Instructions burned: 1179 (million)
% 7.80/1.69 % (3424316)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=416751692:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 7.80/1.69 % TRYING [2,7,2,1,1]
% 7.80/1.69 % TRYING [2,4,2,1,1]
% 7.80/1.69 % TRYING [8,8,8,8,8]
% 7.80/1.69 % (3424310)Instruction limit reached!
% 7.80/1.69 % (3424310)------------------------------
% 7.80/1.69 % (3424310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.69 % (3424310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.69 % (3424310)CaDiCaL version: 2.1.3
% 7.80/1.69 % (3424310)Termination reason: Instruction limit
% 7.80/1.69 % (3424310)Termination phase: Saturation
% 7.80/1.69 % (3424310)Time elapsed: 0.487 s
% 7.80/1.69 % (3424310)Peak memory usage: 20 MB
% 7.80/1.69 % (3424310)Instructions burned: 881 (million)
% 7.80/1.69 % (3424318)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2722036531:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 7.80/1.69 % TRYING [2,3,3,1,1]
% 7.80/1.69 % (3424318) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3424273-3424318"...
% 7.80/1.69 % (3424318)...printing done.
% 7.80/1.69 % (3424318)Refutation found. Thanks to Tanya!
% 7.80/1.69 % SZS status Theorem for theBenchmark
% 7.80/1.69 % SZS output start Proof for theBenchmark
% See solution above
% 7.80/1.70 % (3424318)------------------------------
% 7.80/1.70 % (3424318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.80/1.70 % (3424318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.70 % (3424318)CaDiCaL version: 2.1.3
% 7.80/1.70 % (3424318)Termination reason: Refutation
% 7.80/1.70 % (3424318)Time elapsed: 0.082 s
% 7.80/1.70 % (3424318)Peak memory usage: 14 MB
% 7.80/1.70 % (3424318)Instructions burned: 137 (million)
% 7.80/1.70 % (3424273)Success in time 1.281 s
% 7.80/1.70 % Vampire exiting
%------------------------------------------------------------------------------