%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP006_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:34 PM UTC 2026
% Result : Theorem 4.31s 1.27s
% Output : CNFRefutation 4.31s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f113ERROR: Could not build tree for root c_796ERROR: MakeTreeStats fails)
% 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 * tp__o ) ) ) > $o ).
tff(pred_def_4,type,
sP1: ( del * del ) > $o ).
tff(pred_def_5,type,
sP2: ( del * del ) > $o ).
tff(pred_def_6,type,
sP3: ( del * ( $i * ( $i * del ) ) ) > $o ).
tff(pred_def_7,type,
sP4: ( del * ( $i * ( $i * del ) ) ) > $o ).
tff(pred_def_8,type,
sP5: ( del * del ) > $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 * tp__o ) ) > $o ).
tff(pred_def_14,type,
sP11: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_15,type,
sP12: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_16,type,
sP13: ( tp__o * ( tp__o * tp__o ) ) > $o ).
tff(pred_def_17,type,
sP14: ( tp__o * tp__o ) > $o ).
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,
sK15: ( $i * ( $i * del ) ) > $i ).
tff(func_def_30,type,
sK16: ( $i * del ) > $i ).
tff(func_def_31,type,
sK17: ( $i * del ) > $i ).
tff(func_def_32,type,
sK18: ( $i * ( $i * del ) ) > $i ).
tff(func_def_33,type,
sK19: ( del * ( $i * ( $i * del ) ) ) > $i ).
tff(func_def_34,type,
sK20: ( $i * ( $i * del ) ) > $i ).
tff(func_def_35,type,
sK21: ( del * ( $i * ( $i * del ) ) ) > $i ).
tff(func_def_36,type,
sK22: ( $i * ( $i * del ) ) > $i ).
tff(func_def_37,type,
sK23: ( $i * ( $i * ( del * del ) ) ) > $i ).
tff(func_def_38,type,
sK24: ( $i * ( $i * del ) ) > $i ).
tff(func_def_39,type,
sK25: ( $i * ( $i * ( del * del ) ) ) > $i ).
tff(func_def_40,type,
sK26: ( $i * ( $i * del ) ) > $i ).
tff(func_def_41,type,
sK27: ( $i * ( $i * del ) ) > $i ).
tff(func_def_42,type,
sK28: del ).
tff(func_def_43,type,
sK29: del ).
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(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/sandbox2/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(f73,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(f105,plain,
? [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(ennf_transformation,[],[f59]) ).
tff(f106,plain,
? [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(flattening,[],[f105]) ).
tff(f157,plain,
! [X0: del,X1: del] :
( ~ sP5(X0,X1)
| ! [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))) ) )
& ( ? [X13: $i] :
( mem(X13,X0)
& p(ap(X12,ap(X11,X13))) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X11),X12)) ) ) ) ) ),
inference(nnf_transformation,[],[f113]) ).
tff(f158,plain,
! [X0: del,X1: del] :
( ~ sP5(X0,X1)
| ! [X2: $i] :
( ~ mem(X2,arr(X0,X1))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( ( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X2),X3))
| ! [X5: $i] :
( ~ mem(X5,X0)
| ~ p(ap(X3,ap(X2,X5))) ) )
& ( ? [X4: $i] :
( mem(X4,X0)
& p(ap(X3,ap(X2,X4))) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X2),X3)) ) ) ) ) ),
inference(rectify,[],[f157]) ).
tff(f159,plain,
! [X0: del,X1: del] :
( ~ sP5(X0,X1)
| ! [X2: $i] :
( ~ mem(X2,arr(X0,X1))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( ( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X2),X3))
| ! [X5: $i] :
( ~ mem(X5,X0)
| ~ p(ap(X3,ap(X2,X5))) ) )
& ( ( mem(sK18(X0,X2,X3),X0)
& p(ap(X3,ap(X2,sK18(X0,X2,X3)))) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X2),X3)) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X4,sK18(X0,X2,X3))],[f158]) ).
tff(f172,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,X1))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( sP1(X0,X1)
& sP2(X0,X1)
& sP5(X0,X1)
& ! [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))) ) )
& ( ? [X10: $i] :
( mem(X10,X0)
& ~ p(ap(X9,ap(X8,X10))) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X8),X9)) ) ) ) )
& sP3(X0,X2,X3,X1)
& sP4(X0,X2,X3,X1) ) ) ),
inference(nnf_transformation,[],[f114]) ).
tff(f173,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,X1))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( sP1(X0,X1)
& sP2(X0,X1)
& sP5(X0,X1)
& ! [X4: $i] :
( ~ mem(X4,arr(X0,X1))
| ! [X5: $i] :
( ~ mem(X5,arr(X1,bool))
| ( ( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X4),X5))
| ! [X7: $i] :
( ~ mem(X7,X0)
| p(ap(X5,ap(X4,X7))) ) )
& ( ? [X6: $i] :
( mem(X6,X0)
& ~ p(ap(X5,ap(X4,X6))) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X4),X5)) ) ) ) )
& sP3(X0,X2,X3,X1)
& sP4(X0,X2,X3,X1) ) ) ),
inference(rectify,[],[f172]) ).
tff(f174,plain,
! [X0: del,X1: del,X2: $i] :
( ~ mem(X2,arr(X0,X1))
| ! [X3: $i] :
( ~ mem(X3,arr(X1,bool))
| ( sP1(X0,X1)
& sP2(X0,X1)
& sP5(X0,X1)
& ! [X4: $i] :
( ~ mem(X4,arr(X0,X1))
| ! [X5: $i] :
( ~ mem(X5,arr(X1,bool))
| ( ( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X4),X5))
| ! [X7: $i] :
( ~ mem(X7,X0)
| p(ap(X5,ap(X4,X7))) ) )
& ( ( mem(sK27(X0,X4,X5),X0)
& ~ p(ap(X5,ap(X4,sK27(X0,X4,X5)))) )
| p(ap(ap(c_2EquantHeuristics_2EGUESS__EXISTS__POINT(X0,X1),X4),X5)) ) ) ) )
& sP3(X0,X2,X3,X1)
& sP4(X0,X2,X3,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(X6,sK27(X0,X4,X5))],[f173]) ).
tff(f210,plain,
( mem(sK30,arr(sK29,sK28))
& mem(sK31,arr(sK28,bool))
& mem(sK32,arr(sK28,bool))
& ! [X5: $i] :
( ~ mem(X5,sK28)
| ~ p(ap(sK32,X5))
| p(ap(sK31,X5)) )
& p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK29,sK28),sK30),sK31))
& ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK29,sK28),sK30),sK32)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28,sK29,sK30,sK31,sK32]),skolemize(X0,sK28),skolemize(X1,sK29),skolemize(X2,sK30),skolemize(X3,sK31),skolemize(X4,sK32)],[f106]) ).
tff(f211,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,[],[f73]) ).
tff(f296,plain,
! [X2: $i,X3: $i,X0: del,X1: del,X5: $i] :
( ~ sP5(X0,X1)
| ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X2),X3))
| ~ mem(X5,X0)
| ~ p(ap(X3,ap(X2,X5))) ),
inference(cnf_transformation,[],[f159]) ).
tff(f297,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( ~ sP5(X0,X1)
| ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| mem(sK18(X0,X2,X3),X0)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X2),X3)) ),
inference(cnf_transformation,[],[f159]) ).
tff(f298,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( ~ sP5(X0,X1)
| ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| p(ap(X3,ap(X2,sK18(X0,X2,X3))))
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0,X1),X2),X3)) ),
inference(cnf_transformation,[],[f159]) ).
tff(f321,plain,
! [X2: $i,X3: $i,X0: del,X1: del] :
( ~ mem(X2,arr(X0,X1))
| ~ mem(X3,arr(X1,bool))
| sP5(X0,X1) ),
inference(cnf_transformation,[],[f174]) ).
tff(f412,plain,
mem(sK30,arr(sK29,sK28)),
inference(cnf_transformation,[],[f210]) ).
tff(f413,plain,
mem(sK31,arr(sK28,bool)),
inference(cnf_transformation,[],[f210]) ).
tff(f414,plain,
mem(sK32,arr(sK28,bool)),
inference(cnf_transformation,[],[f210]) ).
tff(f415,plain,
! [X5: $i] :
( ~ mem(X5,sK28)
| ~ p(ap(sK32,X5))
| p(ap(sK31,X5)) ),
inference(cnf_transformation,[],[f210]) ).
tff(f416,plain,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK29,sK28),sK30),sK31)),
inference(cnf_transformation,[],[f210]) ).
tff(f417,plain,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK29,sK28),sK30),sK32)),
inference(cnf_transformation,[],[f210]) ).
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,[],[f211]) ).
tcf(c_112,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1))
| p(ap(X1,ap(X0,sK18(X0_del,X0,X1))))
| ~ sP5(X0_del,X1_del)
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del)) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_113,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( mem(sK18(X0_del,X0,X1),X0_del)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1))
| ~ sP5(X0_del,X1_del)
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del)) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_114,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del,X2: $i] :
( ~ sP5(X0_del,X1_del)
| ~ mem(X2,X0_del)
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ p(ap(X1,ap(X0,X2)))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1)) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_140,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( sP5(X0_del,X1_del)
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del)) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_212,negated_conjecture,
~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK29,sK28),sK30),sK32)),
inference(cnf_transformation,[],[f417]) ).
tcf(c_213,negated_conjecture,
p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(sK29,sK28),sK30),sK31)),
inference(cnf_transformation,[],[f416]) ).
tcf(c_214,negated_conjecture,
! [X0: $i] :
( p(ap(sK31,X0))
| ~ mem(X0,sK28)
| ~ p(ap(sK32,X0)) ),
inference(cnf_transformation,[],[f415]) ).
tcf(c_215,negated_conjecture,
mem(sK32,arr(sK28,bool)),
inference(cnf_transformation,[],[f414]) ).
tcf(c_216,negated_conjecture,
mem(sK31,arr(sK28,bool)),
inference(cnf_transformation,[],[f413]) ).
tcf(c_217,negated_conjecture,
mem(sK30,arr(sK29,sK28)),
inference(cnf_transformation,[],[f412]) ).
tcf(c_262,plain,
! [X0: $i] :
( ~ sP5(sK29,sK28)
| ~ mem(X0,sK29)
| ~ mem(sK31,arr(sK28,bool))
| ~ mem(sK30,arr(sK29,sK28))
| ~ p(ap(sK31,ap(sK30,X0))) ),
inference(superposition,[status(thm)],[c_213,c_114]) ).
tcf(c_282,plain,
! [X0: $i] :
( ~ sP5(sK29,sK28)
| ~ mem(X0,sK29)
| ~ p(ap(sK31,ap(sK30,X0))) ),
inference(global_subsumption_just,[status(thm)],[c_262,c_217,c_216,c_262]) ).
tcf(c_310,plain,
! [X0: $i] :
( sP5(sK29,sK28)
| ~ mem(X0,arr(sK28,bool)) ),
inference(superposition,[status(thm)],[c_217,c_140]) ).
tcf(c_343,plain,
sP5(sK29,sK28),
inference(superposition,[status(thm)],[c_215,c_310]) ).
tcf(c_463,plain,
! [X0: $i] :
( mem(ap(sK30,X0),sK28)
| ~ mem(X0,sK29) ),
inference(superposition,[status(thm)],[c_217,c_49]) ).
tcf(c_464,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( mem(sK18(X0_del,X0,X1),X0_del)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ mem(X1,arr(X1_del,bool)) ),
inference(global_subsumption_just,[status(thm)],[c_113,c_140,c_113]) ).
tcf(c_465,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( mem(sK18(X0_del,X0,X1),X0_del)
| p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1))
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del)) ),
inference(renaming,[status(thm)],[c_464]) ).
tcf(c_476,plain,
( mem(sK18(sK29,sK30,sK32),sK29)
| ~ mem(sK32,arr(sK28,bool))
| ~ mem(sK30,arr(sK29,sK28)) ),
inference(superposition,[status(thm)],[c_465,c_212]) ).
tcf(c_478,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1))
| p(ap(X1,ap(X0,sK18(X0_del,X0,X1))))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ mem(X1,arr(X1_del,bool)) ),
inference(global_subsumption_just,[status(thm)],[c_112,c_140,c_112]) ).
tcf(c_479,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1))
| p(ap(X1,ap(X0,sK18(X0_del,X0,X1))))
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del)) ),
inference(renaming,[status(thm)],[c_478]) ).
tcf(c_489,plain,
( p(ap(sK32,ap(sK30,sK18(sK29,sK30,sK32))))
| ~ mem(sK32,arr(sK28,bool))
| ~ mem(sK30,arr(sK29,sK28)) ),
inference(superposition,[status(thm)],[c_479,c_212]) ).
tcf(c_490,plain,
! [X0: $i,X0_del: del,X1_del: del] :
( p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),sK32))
| p(ap(sK31,ap(X0,sK18(X0_del,X0,sK32))))
| ~ mem(sK32,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ mem(ap(X0,sK18(X0_del,X0,sK32)),sK28) ),
inference(superposition,[status(thm)],[c_479,c_214]) ).
tcf(c_492,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del,X2: $i] :
( ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1))
| ~ p(ap(X1,ap(X0,X2)))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X2,X0_del) ),
inference(global_subsumption_just,[status(thm)],[c_114,c_114,c_140]) ).
tcf(c_493,plain,
! [X0: $i,X0_del: del,X1: $i,X1_del: del,X2: $i] :
( ~ mem(X2,X0_del)
| ~ mem(X1,arr(X1_del,bool))
| ~ mem(X0,arr(X0_del,X1_del))
| ~ p(ap(X1,ap(X0,X2)))
| ~ p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(X0_del,X1_del),X0),X1)) ),
inference(renaming,[status(thm)],[c_492]) ).
tcf(c_507,plain,
! [X0: $i] :
( ~ mem(X0,sK29)
| ~ mem(sK31,arr(sK28,bool))
| ~ mem(sK30,arr(sK29,sK28))
| ~ p(ap(sK31,ap(sK30,X0))) ),
inference(superposition,[status(thm)],[c_213,c_493]) ).
tcf(c_541,plain,
mem(sK18(sK29,sK30,sK32),sK29),
inference(global_subsumption_just,[status(thm)],[c_476,c_217,c_215,c_476]) ).
tcf(c_557,plain,
p(ap(sK32,ap(sK30,sK18(sK29,sK30,sK32)))),
inference(global_subsumption_just,[status(thm)],[c_489,c_217,c_215,c_489]) ).
tcf(c_559,plain,
( p(ap(sK31,ap(sK30,sK18(sK29,sK30,sK32))))
| ~ mem(ap(sK30,sK18(sK29,sK30,sK32)),sK28) ),
inference(superposition,[status(thm)],[c_557,c_214]) ).
tcf(c_583,plain,
( p(ap(sK31,ap(sK30,sK18(sK29,sK30,sK32))))
| ~ mem(sK32,arr(sK28,bool))
| ~ mem(sK30,arr(sK29,sK28))
| ~ mem(ap(sK30,sK18(sK29,sK30,sK32)),sK28) ),
inference(superposition,[status(thm)],[c_490,c_212]) ).
tcf(c_585,plain,
! [X0: $i] :
( ~ mem(X0,sK29)
| ~ p(ap(sK31,ap(sK30,X0))) ),
inference(global_subsumption_just,[status(thm)],[c_507,c_282,c_343]) ).
tcf(c_778,plain,
( ~ mem(sK18(sK29,sK30,sK32),sK29)
| ~ mem(ap(sK30,sK18(sK29,sK30,sK32)),sK28) ),
inference(superposition,[status(thm)],[c_559,c_585]) ).
tcf(c_793,plain,
~ mem(ap(sK30,sK18(sK29,sK30,sK32)),sK28),
inference(global_subsumption_just,[status(thm)],[c_583,c_217,c_215,c_476,c_778]) ).
tcf(c_795,plain,
~ mem(sK18(sK29,sK30,sK32),sK29),
inference(superposition,[status(thm)],[c_463,c_793]) ).
tcf(c_796,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_541,c_795]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP006_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 17:30:14 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 4.31/1.27 % SZS status Started for theBenchmark.p
% 4.31/1.27 % SZS status Theorem for theBenchmark.p
% 4.31/1.27
% 4.31/1.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.31/1.27
% 4.31/1.27 % ------ iProver source info
% 4.31/1.27
% 4.31/1.27 % git: date: 2026-07-19 20:42:38 +0200
% 4.31/1.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.31/1.27 % git: non_committed_changes: false
% 4.31/1.27
% 4.31/1.27 % ------ Parsing...
% 4.31/1.27 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 4.31/1.27 % ------ Proving...
% 4.31/1.27 % ------ Problem Properties
% 4.31/1.27
% 4.31/1.27 %
% 4.31/1.27 % clauses 169
% 4.31/1.27 % conjectures 6
% 4.31/1.27 % EPR 13
% 4.31/1.27 % Horn 112
% 4.31/1.27 % unary 30
% 4.31/1.27 % binary 26
% 4.31/1.27 % lits 541
% 4.31/1.27 % lits eq 22
% 4.31/1.27 % fd_pure 0
% 4.31/1.27 % fd_pseudo 0
% 4.31/1.27 % fd_cond 0
% 4.31/1.27 % fd_pseudo_cond 5
% 4.31/1.27 % AC symbols 0
% 4.31/1.27
% 4.31/1.27 % ------ Input Options Time Limit: Unbounded
% 4.31/1.27
% 4.31/1.27
% 4.31/1.27 % ------
% 4.31/1.27 % Current options:
% 4.31/1.27 % ------
% 4.31/1.27
% 4.31/1.27
% 4.31/1.27 %
% 4.31/1.27
% 4.31/1.27 % ------ Proving...
% 4.31/1.27 %
% 4.31/1.27
% 4.31/1.27 % ------ Proving...
% 4.31/1.27 %
% 4.31/1.27
% 4.31/1.27 % ------ Proving...
% 4.31/1.27 %
% 4.31/1.27
% 4.31/1.27 % SZS status Theorem for theBenchmark.p
% 4.31/1.27
% 4.31/1.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.31/1.27
% 4.31/1.27
%------------------------------------------------------------------------------