%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ITP021_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 : n007.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:58 PM UTC 2026
% Result : Theorem 10.62s 2.73s
% Output : CNFRefutation 10.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 18
% Syntax : Number of formulae : 130 ( 48 unt; 0 typ; 0 def)
% Number of atoms : 1388 ( 78 equ)
% Maximal formula atoms : 7 ( 10 avg)
% Number of connectives : 287 ( 114 ~; 145 |; 13 &)
% ( 3 <=>; 9 =>; 0 <=; 3 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of FOOLs : 1085 (1085 fml; 0 var)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 28 ( 26 usr; 10 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 174 ( 0 sgn 165 !; 9 ?; 174 :)
% 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 ) > $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 * tp__o ) ) > $o ).
tff(func_def_14,type,
fo__c_2Eextreal_2Eextreal__le: ( tp__ty_2Eextreal_2Eextreal * tp__ty_2Eextreal_2Eextreal ) > tp__o ).
tff(func_def_15,type,
c_2Ebool_2ECOND: del > $i ).
tff(func_def_17,type,
fo__c_2Eextreal_2Eextreal__max: ( tp__ty_2Eextreal_2Eextreal * tp__ty_2Eextreal_2Eextreal ) > tp__ty_2Eextreal_2Eextreal ).
tff(func_def_19,type,
fo__c_2Ebool_2EF: tp__o ).
tff(func_def_21,type,
fo__c_2Emin_2E_3D_3D_3E: ( tp__o * tp__o ) > tp__o ).
tff(func_def_23,type,
fo__c_2Ebool_2E_5C_2F: ( tp__o * tp__o ) > tp__o ).
tff(func_def_25,type,
fo__c_2Ebool_2E_2F_5C: ( tp__o * tp__o ) > tp__o ).
tff(func_def_27,type,
fo__c_2Ebool_2E_7E: tp__o > tp__o ).
tff(func_def_28,type,
c_2Emin_2E_3D: del > $i ).
tff(func_def_29,type,
c_2Ebool_2E_21: del > $i ).
tff(func_def_30,type,
sK11: tp__ty_2Eextreal_2Eextreal ).
tff(func_def_31,type,
sK12: tp__ty_2Eextreal_2Eextreal ).
tff(func_def_32,type,
sK13: tp__ty_2Eextreal_2Eextreal ).
tff(func_def_33,type,
sK14: ( $i * ( $i * 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/sandbox2/benchmark/Axioms/ITP001/ITP001_2.ax',ap_tp) ).
tff(f2,axiom,
! [X0: $i] :
( mem(X0,bool)
=> ! [X1: $i] :
( mem(X1,bool)
=> ( ( p(X0)
<=> p(X1) )
=> ( X0 = X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/ITP001/ITP001_2.ax',boolext) ).
tff(f9,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
tff(f10,axiom,
inj__o(fo__c_2Ebool_2ET) = c_2Ebool_2ET,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Ebool_2ET) ).
tff(f11,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_true_p) ).
tff(f12,axiom,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_surj_ty_2Eextreal_2Eextreal) ).
tff(f13,axiom,
! [X0: tp__ty_2Eextreal_2Eextreal] : mem(inj__ty_2Eextreal_2Eextreal(X0),ty_2Eextreal_2Eextreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_mem_ty_2Eextreal_2Eextreal) ).
tff(f14,axiom,
! [X0: $i] :
( mem(X0,ty_2Eextreal_2Eextreal)
=> ( X0 = inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_iso_mem_ty_2Eextreal_2Eextreal) ).
tff(f15,axiom,
mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Eextreal_2Eextreal__le) ).
tff(f18,axiom,
mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Eextreal_2Eextreal__max) ).
tff(f20,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
tff(f21,axiom,
inj__o(fo__c_2Ebool_2EF) = c_2Ebool_2EF,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Ebool_2EF) ).
tff(f22,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
tff(f49,axiom,
! [X0: del,X1: $i] :
( mem(X1,X0)
=> ! [X2: $i] :
( mem(X2,X0)
=> ( ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2EF)),X1),X2) = X2 )
& ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2ET)),X1),X2) = X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Ebool_2ECOND__CLAUSES) ).
tff(f53,axiom,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1))) )
=> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eextreal_2Ele__trans) ).
tff(f54,axiom,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eextreal_2Ele__total) ).
tff(f55,axiom,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1))),inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_thm_2Eextreal_2Eextreal__max__def) ).
tff(f66,conjecture,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0)))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eextreal_2Emax__le) ).
tff(f67,negated_conjecture,
~ ! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0)))
<=> ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(negated_conjecture,[status(cth)],[f66]) ).
tff(f86,plain,
? [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0)))
<~> ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(ennf_transformation,[],[f67]) ).
tff(f98,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X2))) ),
inference(ennf_transformation,[],[f53]) ).
tff(f99,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X2))) ),
inference(flattening,[],[f98]) ).
tff(f100,plain,
! [X0: $i] :
( ~ mem(X0,bool)
| ! [X1: $i] :
( ~ mem(X1,bool)
| ( p(X0)
<~> p(X1) )
| ( X0 = X1 ) ) ),
inference(ennf_transformation,[],[f2]) ).
tff(f101,plain,
! [X0: $i] :
( ~ mem(X0,bool)
| ! [X1: $i] :
( ~ mem(X1,bool)
| ( p(X0)
<~> p(X1) )
| ( X0 = X1 ) ) ),
inference(flattening,[],[f100]) ).
tff(f105,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(f106,plain,
! [X0: $i] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| ( X0 = inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(X0)) ) ),
inference(ennf_transformation,[],[f14]) ).
tff(f107,plain,
! [X0: del,X1: $i] :
( ~ mem(X1,X0)
| ! [X2: $i] :
( ~ mem(X2,X0)
| ( ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2EF)),X1),X2) = X2 )
& ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2ET)),X1),X2) = X1 ) ) ) ),
inference(ennf_transformation,[],[f49]) ).
tff(f124,plain,
? [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0)))
| ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ) )
& ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(nnf_transformation,[],[f86]) ).
tff(f125,plain,
? [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal,X2: tp__ty_2Eextreal_2Eextreal] :
( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0)))
| ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ) )
& ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(flattening,[],[f124]) ).
tff(f126,plain,
( ( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11)))
| ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11))) ) )
& ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13)],[f125]) ).
tff(f181,plain,
! [X0: $i] :
( ~ mem(X0,bool)
| ! [X1: $i] :
( ~ mem(X1,bool)
| ( ( p(X0)
| p(X1) )
& ( ~ p(X0)
| ~ p(X1) ) )
| ( X0 = X1 ) ) ),
inference(nnf_transformation,[],[f101]) ).
tff(f184,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(cnf_transformation,[],[f126]) ).
tff(f185,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(cnf_transformation,[],[f126]) ).
tff(f186,plain,
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(cnf_transformation,[],[f126]) ).
tff(f331,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1))) ),
inference(cnf_transformation,[],[f54]) ).
tff(f332,plain,
! [X2: tp__ty_2Eextreal_2Eextreal,X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X2))) ),
inference(cnf_transformation,[],[f99]) ).
tff(f333,plain,
mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))),
inference(cnf_transformation,[],[f15]) ).
tff(f334,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1))),inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(cnf_transformation,[],[f55]) ).
tff(f335,plain,
mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))),
inference(cnf_transformation,[],[f18]) ).
tff(f337,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,bool)
| ~ mem(X1,bool)
| p(X0)
| p(X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f181]) ).
tff(f338,plain,
! [X0: $i,X1: $i] :
( ~ mem(X0,bool)
| ~ mem(X1,bool)
| ~ p(X0)
| ~ p(X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f181]) ).
tff(f343,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,[],[f105]) ).
tff(f344,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : mem(inj__ty_2Eextreal_2Eextreal(X0),ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[],[f13]) ).
tff(f345,plain,
! [X0: $i] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| ( inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(X0)) = X0 ) ),
inference(cnf_transformation,[],[f106]) ).
tff(f346,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(X0)) = X0 ),
inference(cnf_transformation,[],[f12]) ).
tff(f347,plain,
! [X2: $i,X0: del,X1: $i] :
( ~ mem(X1,X0)
| ~ mem(X2,X0)
| ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2EF)),X1),X2) = X2 ) ),
inference(cnf_transformation,[],[f107]) ).
tff(f348,plain,
! [X2: $i,X0: del,X1: $i] :
( ~ mem(X1,X0)
| ~ mem(X2,X0)
| ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2ET)),X1),X2) = X1 ) ),
inference(cnf_transformation,[],[f107]) ).
tff(f350,plain,
c_2Ebool_2ET = inj__o(fo__c_2Ebool_2ET),
inference(cnf_transformation,[],[f10]) ).
tff(f351,plain,
c_2Ebool_2EF = inj__o(fo__c_2Ebool_2EF),
inference(cnf_transformation,[],[f21]) ).
tff(f352,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f11]) ).
tff(f353,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[],[f9]) ).
tff(f354,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[],[f22]) ).
tff(f355,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[],[f20]) ).
tcf(c_49,negated_conjecture,
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_50,negated_conjecture,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_51,negated_conjecture,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_146,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_147,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X2_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_148,plain,
mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))),
inference(cnf_transformation,[],[f333]) ).
tcf(c_149,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal))) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))),
inference(cnf_transformation,[],[f334]) ).
tcf(c_150,plain,
mem(c_2Eextreal_2Eextreal__max,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))),
inference(cnf_transformation,[],[f335]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ p(X1)
| ~ p(X0)
| ~ mem(X1,bool)
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( p(X1)
| p(X0)
| ( X0 = X1 )
| ~ mem(X1,bool)
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_158,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,[],[f343]) ).
tcf(c_159,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : mem(inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[],[f344]) ).
tcf(c_160,plain,
! [X0: $i] :
( ( inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(X0)) = X0 )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_161,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)) = X0_tp__ty_2Eextreal_2Eextreal,
inference(cnf_transformation,[],[f346]) ).
tcf(c_162,plain,
! [X0: $i,X0_del: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0_del),inj__o(fo__c_2Ebool_2ET)),X0),X1) = X0 )
| ~ mem(X1,X0_del)
| ~ mem(X0,X0_del) ),
inference(cnf_transformation,[],[f348]) ).
tcf(c_163,plain,
! [X0: $i,X0_del: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0_del),inj__o(fo__c_2Ebool_2EF)),X0),X1) = X1 )
| ~ mem(X1,X0_del)
| ~ mem(X0,X0_del) ),
inference(cnf_transformation,[],[f347]) ).
tcf(c_165,plain,
inj__o(fo__c_2Ebool_2ET) = c_2Ebool_2ET,
inference(cnf_transformation,[],[f350]) ).
tcf(c_166,plain,
inj__o(fo__c_2Ebool_2EF) = c_2Ebool_2EF,
inference(cnf_transformation,[],[f351]) ).
tcf(c_167,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f352]) ).
tcf(c_168,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[],[f353]) ).
tcf(c_169,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[],[f354]) ).
tcf(c_170,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[],[f355]) ).
tcf(c_1213,plain,
! [X0: $i,X0_del: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0_del),c_2Ebool_2EF),X0),X1) = X1 )
| ~ mem(X1,X0_del)
| ~ mem(X0,X0_del) ),
inference(light_normalisation,[status(thm)],[c_163,c_166]) ).
tcf(c_1223,plain,
! [X0: $i,X0_del: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0_del),c_2Ebool_2ET),X0),X1) = X0 )
| ~ mem(X1,X0_del)
| ~ mem(X0,X0_del) ),
inference(light_normalisation,[status(thm)],[c_162,c_165]) ).
tcf(c_1991,plain,
! [X0: $i] :
( mem(ap(c_2Eextreal_2Eextreal__le,X0),arr(ty_2Eextreal_2Eextreal,bool))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_148,c_158]) ).
tcf(c_1992,plain,
! [X0: $i] :
( mem(ap(c_2Eextreal_2Eextreal__max,X0),arr(ty_2Eextreal_2Eextreal,ty_2Eextreal_2Eextreal))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_150,c_158]) ).
tcf(c_2007,plain,
! [X0: $i,X1: $i] :
( mem(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1),bool)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_1991,c_158]) ).
tcf(c_2016,plain,
! [X0: $i,X1: $i] :
( mem(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1),ty_2Eextreal_2Eextreal)
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_1992,c_158]) ).
tcf(c_2042,plain,
! [X0: $i,X1: $i] :
( ( inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,X0),X1))) = ap(ap(c_2Eextreal_2Eextreal__max,X0),X1) )
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_2016,c_160]) ).
tcf(c_2051,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal))),
inference(equality_factoring,[status(thm)],[c_146]) ).
tcf(c_2074,plain,
! [X0: $i] :
( p(c_2Ebool_2EF)
| p(X0)
| ( X0 = c_2Ebool_2EF )
| ~ mem(X0,bool) ),
inference(superposition,[status(thm)],[c_170,c_153]) ).
tcf(c_2076,plain,
! [X0: $i] :
( p(X0)
| ( X0 = c_2Ebool_2EF )
| ~ mem(X0,bool) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2074,c_169]) ).
tcf(c_2104,plain,
! [X0: $i] :
( ( X0 = c_2Ebool_2ET )
| ~ p(c_2Ebool_2ET)
| ~ p(X0)
| ~ mem(X0,bool) ),
inference(superposition,[status(thm)],[c_168,c_152]) ).
tcf(c_2107,plain,
! [X0: $i] :
( ( X0 = c_2Ebool_2ET )
| ~ p(X0)
| ~ mem(X0,bool) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2104,c_167]) ).
tcf(c_2133,plain,
! [X0: $i,X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),X0) = X0 )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_159,c_1213]) ).
tcf(c_2194,plain,
! [X0: $i,X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),X0) = inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_159,c_1223]) ).
tcf(c_2258,plain,
! [X0: $i,X1: $i] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1))
| ( ap(ap(c_2Eextreal_2Eextreal__le,X0),X1) = c_2Ebool_2EF )
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_2007,c_2076]) ).
tcf(c_2287,plain,
! [X0: $i,X1: $i] :
( ( ap(ap(c_2Eextreal_2Eextreal__le,X0),X1) = c_2Ebool_2ET )
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ~ mem(X0,ty_2Eextreal_2Eextreal)
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X0),X1)) ),
inference(superposition,[status(thm)],[c_2007,c_2107]) ).
tcf(c_2467,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X2_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) ),
inference(superposition,[status(thm)],[c_146,c_147]) ).
tcf(c_2646,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal),
inference(superposition,[status(thm)],[c_159,c_2133]) ).
tcf(c_2817,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal),
inference(superposition,[status(thm)],[c_159,c_2194]) ).
tcf(c_3178,plain,
! [X0: $i,X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),X0))) = ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),X0) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_159,c_2042]) ).
tcf(c_3355,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)))) = ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),
inference(superposition,[status(thm)],[c_159,c_3178]) ).
tcf(c_3378,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] : mem(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),ty_2Eextreal_2Eextreal),
inference(superposition,[status(thm)],[c_3355,c_159]) ).
tcf(c_3386,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X2_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X3_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X3_tp__ty_2Eextreal_2Eextreal)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal))),inj__ty_2Eextreal_2Eextreal(X3_tp__ty_2Eextreal_2Eextreal)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)))))) ),
inference(superposition,[status(thm)],[c_3355,c_147]) ).
tcf(c_4750,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X2_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2EF )
| ~ mem(inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal)
| ~ mem(inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal)
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) ),
inference(superposition,[status(thm)],[c_2258,c_147]) ).
tcf(c_4755,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X2_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2EF )
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4750,c_159,c_159]) ).
tcf(c_8715,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X2_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X3_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X3_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X3_tp__ty_2Eextreal_2Eextreal)),ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))),inj__ty_2Eextreal_2Eextreal(X2_tp__ty_2Eextreal_2Eextreal))) ),
inference(demodulation,[status(thm)],[c_3386,c_3355]) ).
tcf(c_8726,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)))) ),
inference(superposition,[status(thm)],[c_50,c_8715]) ).
tcf(c_9223,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))) = c_2Ebool_2EF )
| ~ mem(inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal)
| ~ mem(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)),ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_2258,c_8726]) ).
tcf(c_9237,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))) = c_2Ebool_2EF ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9223,c_159,c_3378]) ).
tcf(c_9406,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))) = c_2Ebool_2EF ) ),
inference(equality_factoring,[status(thm)],[c_9237]) ).
tcf(c_11900,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2EF ) ),
inference(superposition,[status(thm)],[c_2051,c_4755]) ).
tcf(c_12550,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2EF )
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2ET )
| ~ mem(inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal)
| ~ mem(inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal),ty_2Eextreal_2Eextreal) ),
inference(superposition,[status(thm)],[c_11900,c_2287]) ).
tcf(c_12640,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2EF )
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2ET ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12550,c_159,c_159]) ).
tcf(c_18153,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2ET )
| ( surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal))) ) ),
inference(superposition,[status(thm)],[c_12640,c_149]) ).
tcf(c_18220,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2ET )
| ( surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) = surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)) ) ),
inference(light_normalisation,[status(thm)],[c_18153,c_2646]) ).
tcf(c_18221,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2ET )
| ( surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal))) = X0_tp__ty_2Eextreal_2Eextreal ) ),
inference(light_normalisation,[status(thm)],[c_18220,c_161]) ).
tcf(c_19420,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal,X1_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal) )
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(X1_tp__ty_2Eextreal_2Eextreal)) = c_2Ebool_2ET ) ),
inference(superposition,[status(thm)],[c_18221,c_3355]) ).
tcf(c_19521,plain,
( ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2ET )
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(superposition,[status(thm)],[c_19420,c_49]) ).
tcf(c_19523,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2ET ) ),
inference(superposition,[status(thm)],[c_19420,c_50]) ).
tcf(c_19833,plain,
! [X0_tp__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0_tp__ty_2Eextreal_2Eextreal)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2ET ) ),
inference(superposition,[status(thm)],[c_19523,c_2467]) ).
tcf(c_20343,plain,
( ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2ET )
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(global_subsumption_just,[status(thm)],[c_19521,c_19523,c_19521]) ).
tcf(c_20778,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2ET ) ),
inference(superposition,[status(thm)],[c_19833,c_20343]) ).
tcf(c_20849,plain,
( p(c_2Ebool_2EF)
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2ET ) ),
inference(superposition,[status(thm)],[c_12640,c_20778]) ).
tcf(c_20860,plain,
ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2ET,
inference(forward_subsumption_resolution,[status(thm)],[c_20849,c_169]) ).
tcf(c_24760,plain,
surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK12))) = surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))),
inference(superposition,[status(thm)],[c_20860,c_149]) ).
tcf(c_25479,plain,
surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13))) = sK13,
inference(demodulation,[status(thm)],[c_24760,c_161,c_2817]) ).
tcf(c_25483,plain,
ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = inj__ty_2Eextreal_2Eextreal(sK13),
inference(superposition,[status(thm)],[c_25479,c_3355]) ).
tcf(c_25509,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ( ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2EF ) ),
inference(demodulation,[status(thm)],[c_9406,c_25483]) ).
tcf(c_25540,plain,
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11))) ),
inference(demodulation,[status(thm)],[c_49,c_25483]) ).
tcf(c_25541,plain,
p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK13)),inj__ty_2Eextreal_2Eextreal(sK11))),
inference(demodulation,[status(thm)],[c_51,c_25483]) ).
tcf(c_25545,plain,
~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK11))),
inference(forward_subsumption_resolution,[status(thm)],[c_25540,c_25541]) ).
tcf(c_25607,plain,
ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK12)),inj__ty_2Eextreal_2Eextreal(sK13)) = c_2Ebool_2EF,
inference(forward_subsumption_resolution,[status(thm)],[c_25509,c_25545]) ).
tcf(c_25608,plain,
c_2Ebool_2ET = c_2Ebool_2EF,
inference(light_normalisation,[status(thm)],[c_25607,c_20860]) ).
tcf(c_25678,plain,
~ p(c_2Ebool_2ET),
inference(demodulation,[status(thm)],[c_169,c_25608]) ).
tcf(c_25679,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_25678,c_167]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP021_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.10/0.37 % Computer : n007.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 : Wed Sep 23 17:44:52 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 10.62/2.73 % SZS status Started for theBenchmark.p
% 10.62/2.73 % SZS status Theorem for theBenchmark.p
% 10.62/2.73
% 10.62/2.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.62/2.73
% 10.62/2.73 % ------ iProver source info
% 10.62/2.73
% 10.62/2.73 % git: date: 2026-07-19 20:42:38 +0200
% 10.62/2.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.62/2.73 % git: non_committed_changes: false
% 10.62/2.73
% 10.62/2.73 % ------ Parsing...
% 10.62/2.73 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 10.62/2.73 %
% 10.62/2.73
% 10.62/2.73 % ------ Preprocessing... sup_sim: 2 pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 pe_s pe_e %
% 10.62/2.73
% 10.62/2.73 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 10.62/2.73 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 10.62/2.73 %
% 10.62/2.73
% 10.62/2.73 % ------ Preprocessing...
% 10.62/2.73 % ------ Proving...
% 10.62/2.73 % ------ Problem Properties
% 10.62/2.73
% 10.62/2.73 %
% 10.62/2.73 % clauses 26
% 10.62/2.73 % conjectures 3
% 10.62/2.73 % EPR 6
% 10.62/2.73 % Horn 21
% 10.62/2.73 % unary 13
% 10.62/2.73 % binary 4
% 10.62/2.73 % lits 54
% 10.62/2.73 % lits eq 12
% 10.62/2.73 % fd_pure 0
% 10.62/2.73 % fd_pseudo 0
% 10.62/2.73 % fd_cond 0
% 10.62/2.73 % fd_pseudo_cond 4
% 10.62/2.73 % AC symbols 0
% 10.62/2.73
% 10.62/2.73 % ------ Schedule dynamic 5 is on
% 10.62/2.73
% 10.62/2.73 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.62/2.73
% 10.62/2.73
% 10.62/2.73 % ------
% 10.62/2.73 % Current options:
% 10.62/2.73 % ------
% 10.62/2.73
% 10.62/2.73
% 10.62/2.73 %
% 10.62/2.73
% 10.62/2.73 % ------ Proving...
% 10.62/2.73 %
% 10.62/2.73
% 10.62/2.73 % SZS status Theorem for theBenchmark.p
% 10.62/2.73
% 10.62/2.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.62/2.73
% 10.62/2.73
%------------------------------------------------------------------------------