%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP020_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:47:55 PM UTC 2026
% Result : Theorem 1.68s 1.07s
% Output : CNFRefutation 1.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 6
% Syntax : Number of formulae : 47 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 338 ( 0 equ)
% Maximal formula atoms : 10 ( 7 avg)
% Number of connectives : 181 ( 84 ~; 74 |; 17 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of FOOLs : 194 ( 194 fml; 0 var)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 19 usr; 6 prp; 0-3 aty)
% Number of functors : 44 ( 44 usr; 2 con; 0-4 aty)
% Number of variables : 102 ( 0 sgn 91 !; 11 ?; 102 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
bool: del ).
tff(pred_def_1,type,
mem: ( del * $i ) > $o ).
tff(func_def_2,type,
arr: ( del * del ) > del ).
tff(pred_def_3,type,
sP0: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_4,type,
sP1: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_5,type,
sP2: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_6,type,
sP3: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_7,type,
sP4: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_8,type,
sP5: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_9,type,
sP6: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_10,type,
sP7: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_11,type,
sP8: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_12,type,
sP9: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_13,type,
sP10: ( tp__o * tp__o ) > $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,
sK11: ( $i * ( $i * del ) ) > $i ).
tff(func_def_33,type,
sK12: ( $i * del ) > $i ).
tff(func_def_34,type,
sK13: ( $i * del ) > $i ).
tff(func_def_35,type,
sK14: ( $i * del ) > $i ).
tff(func_def_36,type,
sK15: ( $i * del ) > $i ).
tff(func_def_37,type,
sK16: ( tp__o * ( $i * del ) ) > $i ).
tff(func_def_38,type,
sK17: ( $i * del ) > $i ).
tff(func_def_39,type,
sK18: ( $i * ( tp__o * del ) ) > $i ).
tff(func_def_40,type,
sK19: ( $i * del ) > $i ).
tff(func_def_41,type,
sK20: ( $i * del ) > $i ).
tff(func_def_42,type,
sK21: ( tp__o * ( $i * del ) ) > $i ).
tff(func_def_43,type,
sK22: ( $i * del ) > $i ).
tff(func_def_44,type,
sK23: ( $i * ( tp__o * del ) ) > $i ).
tff(func_def_45,type,
sK24: ( tp__o * ( $i * del ) ) > $i ).
tff(func_def_46,type,
sK25: ( $i * del ) > $i ).
tff(func_def_47,type,
sK26: ( $i * ( tp__o * del ) ) > $i ).
tff(func_def_48,type,
sK27: ( $i * del ) > $i ).
tff(func_def_49,type,
sK28: ( $i * del ) > $i ).
tff(func_def_50,type,
sK29: ( $i * ( tp__o * del ) ) > $i ).
tff(func_def_51,type,
sK30: ( $i * del ) > $i ).
tff(func_def_52,type,
sK31: ( $i * ( tp__o * del ) ) > $i ).
tff(func_def_53,type,
sK32: ( $i * ( $i * del ) ) > $i ).
tff(func_def_54,type,
sK33: ( $i * ( $i * del ) ) > $i ).
tff(func_def_55,type,
sK34: ( $i * ( del * del ) ) > $i ).
tff(func_def_56,type,
sK35: ( $i * ( del * del ) ) > $i ).
tff(func_def_57,type,
sK36: ( $i * ( $i * ( del * del ) ) ) > $i ).
tff(func_def_58,type,
sK37: ( $i * ( $i * ( del * del ) ) ) > $i ).
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(f31,axiom,
! [X0: del] : mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool)),
file('/export/starexec/sandbox/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/sandbox/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] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3))
& mem(X4,arr(X0,X1)) )
<=> ? [X5: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
& mem(X5,arr(X1,X0)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Epred__set_2EBIJ__SYM) ).
tff(f72,axiom,
? [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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ) ).
tff(f73,conjecture,
? [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))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV) ).
tff(f74,negated_conjecture,
~ ? [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(negated_conjecture,[status(cth)],[f73]) ).
tff(f92,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,X1))
| ! [X3: $i] :
( ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ) ),
inference(ennf_transformation,[],[f1]) ).
tff(f127,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,bool))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( ? [X4: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3))
& mem(X4,arr(X0,X1)) )
<=> ? [X5: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
& mem(X5,arr(X1,X0)) ) ) ) ),
inference(ennf_transformation,[],[f61]) ).
tff(f133,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(ennf_transformation,[],[f74]) ).
tff(f213,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,bool))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( ( ! [X4: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3))
| ~ mem(X4,arr(X0,X1)) )
| ? [X5: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
& mem(X5,arr(X1,X0)) ) )
& ( ! [X5: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0)) )
| ? [X4: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3))
& mem(X4,arr(X0,X1)) ) ) ) ) ),
inference(nnf_transformation,[],[f127]) ).
tff(f214,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,bool))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( ( ! [X7: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X7),X2),X3))
| ~ mem(X7,arr(X0,X1)) )
| ? [X6: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X6),X3),X2))
& mem(X6,arr(X1,X0)) ) )
& ( ! [X5: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0)) )
| ? [X4: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X4),X2),X3))
& mem(X4,arr(X0,X1)) ) ) ) ) ),
inference(rectify,[],[f213]) ).
tff(f215,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,bool))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( ( ! [X7: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X7),X2),X3))
| ~ mem(X7,arr(X0,X1)) )
| ( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),sK37(X0,X1,X2,X3)),X3),X2))
& mem(sK37(X0,X1,X2,X3),arr(X1,X0)) ) )
& ( ! [X5: $i] :
( ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0)) )
| ( p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),sK36(X0,X1,X2,X3)),X2),X3))
& mem(sK36(X0,X1,X2,X3),arr(X0,X1)) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37]),skolemize(X4,sK36(X0,X1,X2,X3)),skolemize(X6,sK37(X0,X1,X2,X3))],[f214]) ).
tff(f258,plain,
( p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK38),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(sK38,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(X0,sK38)],[f72]) ).
tff(f259,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,X0)
| mem(ap(X2,X3),X1) ),
inference(cnf_transformation,[],[f92]) ).
tff(f301,plain,
! [X0: del] : mem(c_2Epred__set_2EUNIV(X0),arr(X0,bool)),
inference(cnf_transformation,[],[f31]) ).
tff(f302,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(f413,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X7: $i] :
( ~ mem(X2,arr(X0,bool))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X7),X2),X3))
| ~ mem(X7,arr(X0,X1))
| p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),sK37(X0,X1,X2,X3)),X3),X2)) ),
inference(cnf_transformation,[],[f215]) ).
tff(f414,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X7: $i] :
( ~ mem(X2,arr(X0,bool))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),X7),X2),X3))
| ~ mem(X7,arr(X0,X1))
| mem(sK37(X0,X1,X2,X3),arr(X1,X0)) ),
inference(cnf_transformation,[],[f215]) ).
tff(f415,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X5: $i] :
( ~ mem(X2,arr(X0,bool))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X1,X0),X5),X3),X2))
| ~ mem(X5,arr(X1,X0))
| p(ap(ap(ap(c_2Epred__set_2EBIJ(X0,X1),sK36(X0,X1,X2,X3)),X2),X3)) ),
inference(cnf_transformation,[],[f215]) ).
tff(f517,plain,
p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK38),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,[],[f258]) ).
tff(f518,plain,
mem(sK38,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f258]) ).
tff(f519,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,[],[f133]) ).
tcf(c_49,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( mem(ap(X0,X1),X1_del)
| ~ mem(X1,X0_del)
| ~ mem(X0,arr(X0_del,X1_del)) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_91,plain,
! [X0_del: del] : mem(c_2Epred__set_2EUNIV(X0_del),arr(X0_del,bool)),
inference(cnf_transformation,[],[f301]) ).
tcf(c_92,plain,
! [X0_del: del,X1_del: del] : mem(c_2Epred__set_2ECROSS(X0_del,X1_del),arr(arr(X0_del,bool),arr(arr(X1_del,bool),arr(ty_2Epair_2Eprod(X0_del,X1_del),bool)))),
inference(cnf_transformation,[],[f302]) ).
tcf(c_163,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del,X2: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1_del,X0_del),sK36(X1_del,X0_del,X2,X1)),X2),X1))
| ~ mem(X2,arr(X1_del,bool))
| ~ mem(X1,arr(X0_del,bool))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0_del,X1_del),X0),X1),X2)) ),
inference(cnf_transformation,[],[f415]) ).
tcf(c_164,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del,X2: $i] :
( mem(sK37(X0_del,X1_del,X1,X2),arr(X1_del,X0_del))
| ~ mem(X2,arr(X1_del,bool))
| ~ mem(X1,arr(X0_del,bool))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0_del,X1_del),X0),X1),X2)) ),
inference(cnf_transformation,[],[f414]) ).
tcf(c_165,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del,X2: $i] :
( p(ap(ap(ap(c_2Epred__set_2EBIJ(X1_del,X0_del),sK37(X0_del,X1_del,X1,X2)),X2),X1))
| ~ mem(X2,arr(X1_del,bool))
| ~ mem(X1,arr(X0_del,bool))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ p(ap(ap(ap(c_2Epred__set_2EBIJ(X0_del,X1_del),X0),X1),X2)) ),
inference(cnf_transformation,[],[f413]) ).
tcf(c_252,plain,
mem(sK38,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum)),
inference(cnf_transformation,[],[f518]) ).
tcf(c_253,plain,
p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum),sK38),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,[],[f517]) ).
tcf(c_254,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(cnf_transformation,[],[f519]) ).
tcf(c_588,plain,
! [X0: $i,X0_del: del,X1_del: del] :
( mem(ap(c_2Epred__set_2ECROSS(X0_del,X1_del),X0),arr(arr(X1_del,bool),arr(ty_2Epair_2Eprod(X0_del,X1_del),bool)))
| ~ mem(X0,arr(X0_del,bool)) ),
inference(superposition,[status(thm)],[c_92,c_49]) ).
tcf(c_619,plain,
( mem(sK37(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),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)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(sK38,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ 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)) ),
inference(superposition,[status(thm)],[c_253,c_164]) ).
tcf(c_647,plain,
( p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),sK37(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),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)),c_2Epred__set_2EUNIV(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))))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(sK38,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ 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)) ),
inference(superposition,[status(thm)],[c_253,c_165]) ).
tcf(c_658,plain,
( p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),sK36(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)))),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(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(sK38,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ 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)) ),
inference(superposition,[status(thm)],[c_253,c_163]) ).
tcf(c_715,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( mem(ap(ap(c_2Epred__set_2ECROSS(X0_del,X1_del),X0),X1),arr(ty_2Epair_2Eprod(X0_del,X1_del),bool))
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,bool)) ),
inference(superposition,[status(thm)],[c_588,c_49]) ).
tcf(c_784,plain,
( p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),sK37(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),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)),c_2Epred__set_2EUNIV(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))))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ 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)) ),
inference(global_subsumption_just,[status(thm)],[c_647,c_252,c_647]) ).
tcf(c_789,plain,
( p(ap(ap(ap(c_2Epred__set_2EBIJ(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)),sK37(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),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)),c_2Epred__set_2EUNIV(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))))
| ~ 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)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_784,c_91]) ).
tcf(c_798,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))
| ~ mem(sK37(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),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)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum))) ),
inference(superposition,[status(thm)],[c_789,c_254]) ).
tcf(c_799,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))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool)) ),
inference(global_subsumption_just,[status(thm)],[c_658,c_252,c_619,c_798]) ).
tcf(c_800,plain,
( ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ 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)) ),
inference(renaming,[status(thm)],[c_799]) ).
tcf(c_803,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)),
inference(forward_subsumption_resolution,[status(thm)],[c_800,c_91]) ).
tcf(c_906,plain,
( mem(sK37(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),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)),c_2Epred__set_2EUNIV(ty_2Enum_2Enum)),arr(ty_2Enum_2Enum,ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum)))
| ~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool))
| ~ mem(sK38,arr(ty_2Epair_2Eprod(ty_2Enum_2Enum,ty_2Enum_2Enum),ty_2Enum_2Enum))
| ~ 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)) ),
inference(superposition,[status(thm)],[c_253,c_164]) ).
tcf(c_1051,plain,
~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool)),
inference(superposition,[status(thm)],[c_715,c_803]) ).
tcf(c_1105,plain,
~ mem(c_2Epred__set_2EUNIV(ty_2Enum_2Enum),arr(ty_2Enum_2Enum,bool)),
inference(global_subsumption_just,[status(thm)],[c_906,c_1051]) ).
tcf(c_1107,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_1105,c_91]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP020_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n015.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 17:49:24 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 1.68/1.07 % SZS status Started for theBenchmark.p
% 1.68/1.07 % SZS status Theorem for theBenchmark.p
% 1.68/1.07
% 1.68/1.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.68/1.07
% 1.68/1.07 % ------ iProver source info
% 1.68/1.07
% 1.68/1.07 % git: date: 2026-07-19 20:42:38 +0200
% 1.68/1.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.68/1.07 % git: non_committed_changes: false
% 1.68/1.07
% 1.68/1.07 % ------ Parsing...
% 1.68/1.07 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 1.68/1.07 % ------ Proving...
% 1.68/1.07 % ------ Problem Properties
% 1.68/1.07
% 1.68/1.07 %
% 1.68/1.07 % clauses 206
% 1.68/1.07 % conjectures 1
% 1.68/1.07 % EPR 14
% 1.68/1.07 % Horn 133
% 1.68/1.07 % unary 28
% 1.68/1.07 % binary 33
% 1.68/1.07 % lits 670
% 1.68/1.07 % lits eq 22
% 1.68/1.07 % fd_pure 0
% 1.68/1.07 % fd_pseudo 0
% 1.68/1.07 % fd_cond 0
% 1.68/1.07 % fd_pseudo_cond 5
% 1.68/1.07 % AC symbols 0
% 1.68/1.07
% 1.68/1.07 % ------ Input Options Time Limit: Unbounded
% 1.68/1.07
% 1.68/1.07
% 1.68/1.07 % ------
% 1.68/1.07 % Current options:
% 1.68/1.07 % ------
% 1.68/1.07
% 1.68/1.07
% 1.68/1.07 %
% 1.68/1.07
% 1.68/1.07 % ------ Proving...
% 1.68/1.07 %
% 1.68/1.07
% 1.68/1.07 % ------ Proving...
% 1.68/1.07 %
% 1.68/1.07
% 1.68/1.07 % ------ Proving...
% 1.68/1.07 %
% 1.68/1.07
% 1.68/1.07 % ------ Proving...
% 1.68/1.07 %
% 1.68/1.07
% 1.68/1.07 % ------ Proving...
% 1.68/1.07 %
% 1.68/1.07
% 1.68/1.07 % SZS status Theorem for theBenchmark.p
% 1.68/1.07
% 1.68/1.07 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.68/1.07
% 1.68/1.07
%------------------------------------------------------------------------------