%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP021_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:28:43 AM UTC 2026
% Result : Theorem 6.65s 2.71s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 47
% Syntax : Number of formulae : 389 ( 109 unt; 0 typ; 28 def)
% Number of atoms : 1897 ( 221 equ)
% Maximal formula atoms : 7 ( 4 avg)
% Number of connectives : 888 ( 373 ~; 471 |; 13 &)
% ( 20 <=>; 8 =>; 0 <=; 3 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of FOOLs : 993 ( 993 fml; 0 var)
% Number of types : 5 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 48 ( 46 usr; 33 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 8 con; 0-3 aty)
% Number of variables : 195 ( 0 sgn 186 !; 9 ?; 195 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
del: $tType ).
tff(type_def_6,type,
tp__o: $tType ).
tff(type_def_7,type,
tp__ty_2Eextreal_2Eextreal: $tType ).
tff(func_def_0,type,
bool: del ).
tff(func_def_1,type,
ind: del ).
tff(func_def_2,type,
arr: ( del * del ) > del ).
tff(func_def_4,type,
k: ( del * $i ) > $i ).
tff(func_def_5,type,
i: del > $i ).
tff(func_def_6,type,
inj__o: tp__o > $i ).
tff(func_def_7,type,
surj__o: $i > tp__o ).
tff(func_def_9,type,
fo__c_2Ebool_2ET: tp__o ).
tff(func_def_10,type,
ty_2Eextreal_2Eextreal: del ).
tff(func_def_11,type,
inj__ty_2Eextreal_2Eextreal: tp__ty_2Eextreal_2Eextreal > $i ).
tff(func_def_12,type,
surj__ty_2Eextreal_2Eextreal: $i > tp__ty_2Eextreal_2Eextreal ).
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: ( del * $i * $i ) > $i ).
tff(func_def_31,type,
sK12: ( del * $i ) > $i ).
tff(func_def_32,type,
sK13: tp__ty_2Eextreal_2Eextreal ).
tff(func_def_33,type,
sK14: tp__ty_2Eextreal_2Eextreal ).
tff(func_def_34,type,
sK15: tp__ty_2Eextreal_2Eextreal ).
tff(pred_def_1,type,
mem: ( $i * del ) > $o ).
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(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/theBenchmark.p',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/theBenchmark.p',boolext) ).
tff(f7,axiom,
! [X0: tp__o] : mem(inj__o(X0),bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_mem_o) ).
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(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(f16,axiom,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)) = ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Eextreal_2Eextreal__le) ).
tff(f19,axiom,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(X0,X1)) = ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_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_2ET)),X1),X2) = X1 )
& ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2EF)),X1),X2) = X2 ) ) ) ),
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(X0)),inj__ty_2Eextreal_2Eextreal(X1)))
& 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(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(X0)),inj__ty_2Eextreal_2Eextreal(X1)))
| 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_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(X1)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),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(X1)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(negated_conjecture,[status(cth)],[f66]) ).
tff(f86,plain,
! [X0: del,X1: del,X2: $i] :
( ! [X3: $i] :
( mem(ap(X2,X3),X1)
| ~ mem(X3,X0) )
| ~ mem(X2,arr(X0,X1)) ),
inference(ennf_transformation,[],[f1]) ).
tff(f87,plain,
! [X0: $i] :
( ! [X1: $i] :
( ( X0 = X1 )
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(ennf_transformation,[],[f2]) ).
tff(f88,plain,
! [X0: $i] :
( ! [X1: $i] :
( ( X0 = X1 )
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(flattening,[],[f87]) ).
tff(f107,plain,
! [X0: del,X1: $i] :
( ! [X2: $i] :
( ( ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2ET)),X1),X2) = X1 )
& ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2EF)),X1),X2) = X2 ) )
| ~ mem(X2,X0) )
| ~ mem(X1,X0) ),
inference(ennf_transformation,[],[f49]) ).
tff(f109,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(X0)),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(X1)),inj__ty_2Eextreal_2Eextreal(X2))) ),
inference(ennf_transformation,[],[f53]) ).
tff(f110,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(X0)),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(X1)),inj__ty_2Eextreal_2Eextreal(X2))) ),
inference(flattening,[],[f109]) ).
tff(f116,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(X1)),inj__ty_2Eextreal_2Eextreal(X0)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(ennf_transformation,[],[f67]) ).
tff(f133,plain,
! [X0: $i] :
( ! [X1: $i] :
( ( X0 = X1 )
| ( ( ~ p(X1)
| ~ p(X0) )
& ( p(X1)
| p(X0) ) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(nnf_transformation,[],[f88]) ).
tff(f201,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(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,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(X1)),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,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(nnf_transformation,[],[f116]) ).
tff(f202,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(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,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(X1)),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,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X2))),inj__ty_2Eextreal_2Eextreal(X0))) ) ),
inference(flattening,[],[f201]) ).
tff(f203,plain,
( ( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK13)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK15)),inj__ty_2Eextreal_2Eextreal(sK13)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK15))),inj__ty_2Eextreal_2Eextreal(sK13))) )
& ( ( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK13)))
& p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK15)),inj__ty_2Eextreal_2Eextreal(sK13))) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK15))),inj__ty_2Eextreal_2Eextreal(sK13))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15]),skolemize(X0,sK13),skolemize(X1,sK14),skolemize(X2,sK15)],[f202]) ).
tff(f204,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,[],[f86]) ).
tff(f205,plain,
! [X0: $i,X1: $i] :
( ~ mem(X1,bool)
| p(X1)
| p(X0)
| ( X0 = X1 )
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f133]) ).
tff(f206,plain,
! [X0: $i,X1: $i] :
( ~ mem(X1,bool)
| ~ p(X1)
| ~ p(X0)
| ( X0 = X1 )
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f133]) ).
tff(f212,plain,
! [X0: tp__o] : mem(inj__o(X0),bool),
inference(cnf_transformation,[],[f7]) ).
tff(f214,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[],[f9]) ).
tff(f215,plain,
c_2Ebool_2ET = inj__o(fo__c_2Ebool_2ET),
inference(cnf_transformation,[],[f10]) ).
tff(f216,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f11]) ).
tff(f217,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(X0)) = X0 ),
inference(cnf_transformation,[],[f12]) ).
tff(f218,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : mem(inj__ty_2Eextreal_2Eextreal(X0),ty_2Eextreal_2Eextreal),
inference(cnf_transformation,[],[f13]) ).
tff(f220,plain,
mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool))),
inference(cnf_transformation,[],[f15]) ).
tff(f221,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)) = ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)) ),
inference(cnf_transformation,[],[f16]) ).
tff(f224,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(X0,X1)) = ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)) ),
inference(cnf_transformation,[],[f19]) ).
tff(f225,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[],[f20]) ).
tff(f226,plain,
c_2Ebool_2EF = inj__o(fo__c_2Ebool_2EF),
inference(cnf_transformation,[],[f21]) ).
tff(f227,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[],[f22]) ).
tff(f282,plain,
! [X2: $i,X0: del,X1: $i] :
( ~ mem(X2,X0)
| ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2EF)),X1),X2) = X2 )
| ~ mem(X1,X0) ),
inference(cnf_transformation,[],[f107]) ).
tff(f283,plain,
! [X2: $i,X0: del,X1: $i] :
( ~ mem(X2,X0)
| ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2ET)),X1),X2) = X1 )
| ~ mem(X1,X0) ),
inference(cnf_transformation,[],[f107]) ).
tff(f302,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,[],[f110]) ).
tff(f303,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( 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(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(cnf_transformation,[],[f54]) ).
tff(f304,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(f405,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK15)),inj__ty_2Eextreal_2Eextreal(sK13)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK15))),inj__ty_2Eextreal_2Eextreal(sK13))) ),
inference(cnf_transformation,[],[f203]) ).
tff(f406,plain,
( p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK13)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK15))),inj__ty_2Eextreal_2Eextreal(sK13))) ),
inference(cnf_transformation,[],[f203]) ).
tff(f407,plain,
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK13)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(sK15)),inj__ty_2Eextreal_2Eextreal(sK13)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(sK14)),inj__ty_2Eextreal_2Eextreal(sK15))),inj__ty_2Eextreal_2Eextreal(sK13))) ),
inference(cnf_transformation,[],[f203]) ).
tff(f411,definition,
sF16 = inj__ty_2Eextreal_2Eextreal(sK14),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f412,plain,
inj__ty_2Eextreal_2Eextreal(sK14) = sF16,
inference(reorient_equations,[],[f411]) ).
tff(f413,definition,
sF17 = ap(c_2Eextreal_2Eextreal__le,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f414,plain,
ap(c_2Eextreal_2Eextreal__le,sF16) = sF17,
inference(reorient_equations,[],[f413]) ).
tff(f415,definition,
sF18 = inj__ty_2Eextreal_2Eextreal(sK13),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f416,plain,
inj__ty_2Eextreal_2Eextreal(sK13) = sF18,
inference(reorient_equations,[],[f415]) ).
tff(f417,definition,
sF19 = ap(sF17,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f418,plain,
ap(sF17,sF18) = sF19,
inference(reorient_equations,[],[f417]) ).
tff(f419,definition,
sF20 = inj__ty_2Eextreal_2Eextreal(sK15),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f420,plain,
inj__ty_2Eextreal_2Eextreal(sK15) = sF20,
inference(reorient_equations,[],[f419]) ).
tff(f421,definition,
sF21 = ap(c_2Eextreal_2Eextreal__le,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f422,plain,
ap(c_2Eextreal_2Eextreal__le,sF20) = sF21,
inference(reorient_equations,[],[f421]) ).
tff(f423,definition,
sF22 = ap(sF21,sF18),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f424,plain,
ap(sF21,sF18) = sF22,
inference(reorient_equations,[],[f423]) ).
tff(f425,definition,
sF23 = ap(c_2Eextreal_2Eextreal__max,sF16),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f426,plain,
ap(c_2Eextreal_2Eextreal__max,sF16) = sF23,
inference(reorient_equations,[],[f425]) ).
tff(f427,definition,
sF24 = ap(sF23,sF20),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f428,plain,
ap(sF23,sF20) = sF24,
inference(reorient_equations,[],[f427]) ).
tff(f429,definition,
sF25 = ap(c_2Eextreal_2Eextreal__le,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f430,plain,
ap(c_2Eextreal_2Eextreal__le,sF24) = sF25,
inference(reorient_equations,[],[f429]) ).
tff(f431,definition,
sF26 = ap(sF25,sF18),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f432,plain,
ap(sF25,sF18) = sF26,
inference(reorient_equations,[],[f431]) ).
tff(f433,plain,
( ~ p(sF19)
| ~ p(sF22)
| ~ p(sF26) ),
inference(definition_folding,[],[f407,f432,f416,f430,f428,f420,f426,f412,f424,f416,f422,f420,f418,f416,f414,f412]) ).
tff(f434,plain,
( p(sF19)
| p(sF26) ),
inference(definition_folding,[],[f406,f432,f416,f430,f428,f420,f426,f412,f418,f416,f414,f412]) ).
tff(f435,plain,
( p(sF22)
| p(sF26) ),
inference(definition_folding,[],[f405,f432,f416,f430,f428,f420,f426,f412,f424,f416,f422,f420]) ).
tff(f451,definition,
( spl27_1
<=> p(sF26) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
tff(f452,plain,
( ~ p(sF26)
| spl27_1 ),
inference(avatar_component_clause,[],[f451]) ).
tff(f453,plain,
( p(sF26)
| ~ spl27_1 ),
inference(avatar_component_clause,[],[f451]) ).
tff(f455,definition,
( spl27_2
<=> p(sF22) ),
introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition]) ).
tff(f456,plain,
( ~ p(sF22)
| spl27_2 ),
inference(avatar_component_clause,[],[f455]) ).
tff(f457,plain,
( p(sF22)
| ~ spl27_2 ),
inference(avatar_component_clause,[],[f455]) ).
tff(f458,plain,
( spl27_1
| spl27_2 ),
inference(avatar_split_clause,[],[f435,f455,f451]) ).
tff(f460,definition,
( spl27_3
<=> p(sF19) ),
introduced(definition,[new_symbols(definition,[spl27_3])],[avatar_definition]) ).
tff(f461,plain,
( ~ p(sF19)
| spl27_3 ),
inference(avatar_component_clause,[],[f460]) ).
tff(f462,plain,
( p(sF19)
| ~ spl27_3 ),
inference(avatar_component_clause,[],[f460]) ).
tff(f463,plain,
( spl27_1
| spl27_3 ),
inference(avatar_split_clause,[],[f434,f460,f451]) ).
tff(f464,plain,
( ~ spl27_1
| ~ spl27_2
| ~ spl27_3 ),
inference(avatar_split_clause,[],[f433,f460,f455,f451]) ).
tff(f471,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(sK14,X0)) = ap(ap(c_2Eextreal_2Eextreal__max,sF16),inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(superposition,[],[f224,f412]) ).
tff(f475,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(sK14,X0)) = ap(sF23,inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(forward_demodulation,[],[f471,f426]) ).
tff(f477,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,X0)) = ap(ap(c_2Eextreal_2Eextreal__le,sF20),inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(superposition,[],[f221,f420]) ).
tff(f478,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) = ap(ap(c_2Eextreal_2Eextreal__le,sF16),inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(superposition,[],[f221,f412]) ).
tff(f482,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) = ap(sF17,inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(forward_demodulation,[],[f478,f414]) ).
tff(f483,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,X0)) = ap(sF21,inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(forward_demodulation,[],[f477,f422]) ).
tff(f490,plain,
! [X2: tp__ty_2Eextreal_2Eextreal,X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)))
| ~ 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(X2)),inj__ty_2Eextreal_2Eextreal(X1))) ),
inference(superposition,[],[f302,f221]) ).
tff(f491,plain,
! [X2: tp__ty_2Eextreal_2Eextreal,X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X2,X0)))
| ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X2)),inj__ty_2Eextreal_2Eextreal(X1))) ),
inference(forward_demodulation,[],[f490,f221]) ).
tff(f498,plain,
! [X2: tp__ty_2Eextreal_2Eextreal,X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X2,X0)))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(X2,X1)))
| ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1))) ),
inference(forward_demodulation,[],[f491,f221]) ).
tff(f513,plain,
mem(sF18,ty_2Eextreal_2Eextreal),
inference(superposition,[],[f218,f416]) ).
tff(f518,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X0))),
inference(factoring,[],[f303]) ).
tff(f547,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X0))),
inference(forward_demodulation,[],[f518,f221]) ).
tff(f591,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = surj__ty_2Eextreal_2Eextreal(ap(sF23,inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(superposition,[],[f217,f475]) ).
tff(f593,plain,
sK14 = surj__ty_2Eextreal_2Eextreal(sF16),
inference(superposition,[],[f217,f412]) ).
tff(f594,plain,
sK15 = surj__ty_2Eextreal_2Eextreal(sF20),
inference(superposition,[],[f217,f420]) ).
tff(f596,plain,
ap(sF17,sF18) = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK13)),
inference(superposition,[],[f482,f416]) ).
tff(f599,plain,
sF19 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK13)),
inference(forward_demodulation,[],[f596,f418]) ).
tff(f605,plain,
ap(sF21,sF18) = inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK13)),
inference(superposition,[],[f483,f416]) ).
tff(f606,plain,
inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK14)) = ap(sF21,sF16),
inference(superposition,[],[f483,f412]) ).
tff(f608,plain,
sF22 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK13)),
inference(forward_demodulation,[],[f605,f424]) ).
tff(f624,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),inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1))),inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(superposition,[],[f304,f221]) ).
tff(f631,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,sF16),inj__ty_2Eextreal_2Eextreal(X0))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,sF16),inj__ty_2Eextreal_2Eextreal(X0))),inj__ty_2Eextreal_2Eextreal(X0)),sF16)) ),
inference(superposition,[],[f304,f412]) ).
tff(f634,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,sF16),inj__ty_2Eextreal_2Eextreal(X0))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(sF17,inj__ty_2Eextreal_2Eextreal(X0))),inj__ty_2Eextreal_2Eextreal(X0)),sF16)) ),
inference(forward_demodulation,[],[f631,f414]) ).
tff(f641,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1))),inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) = surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(X0,X1))) ),
inference(forward_demodulation,[],[f624,f224]) ).
tff(f643,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,sF16),inj__ty_2Eextreal_2Eextreal(X0))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0))),inj__ty_2Eextreal_2Eextreal(X0)),sF16)) ),
inference(forward_demodulation,[],[f634,f482]) ).
tff(f650,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( fo__c_2Eextreal_2Eextreal__max(X0,X1) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1))),inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_demodulation,[],[f641,f217]) ).
tff(f652,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( surj__ty_2Eextreal_2Eextreal(ap(sF23,inj__ty_2Eextreal_2Eextreal(X0))) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0))),inj__ty_2Eextreal_2Eextreal(X0)),sF16)) ),
inference(forward_demodulation,[],[f643,f426]) ).
tff(f660,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0))),inj__ty_2Eextreal_2Eextreal(X0)),sF16)) ),
inference(forward_demodulation,[],[f652,f591]) ).
tff(f715,plain,
fo__c_2Eextreal_2Eextreal__max(sK14,sK15) = surj__ty_2Eextreal_2Eextreal(ap(sF23,sF20)),
inference(superposition,[],[f591,f420]) ).
tff(f716,plain,
fo__c_2Eextreal_2Eextreal__max(sK14,sK15) = surj__ty_2Eextreal_2Eextreal(sF24),
inference(forward_demodulation,[],[f715,f428]) ).
tff(f717,plain,
ap(sF23,inj__ty_2Eextreal_2Eextreal(sK15)) = inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(sF24)),
inference(superposition,[],[f475,f716]) ).
tff(f718,plain,
ap(sF23,sF20) = inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(sF24)),
inference(forward_demodulation,[],[f717,f420]) ).
tff(f719,plain,
sF24 = inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(sF24)),
inference(forward_demodulation,[],[f718,f428]) ).
tff(f720,plain,
mem(sF24,ty_2Eextreal_2Eextreal),
inference(superposition,[],[f218,f719]) ).
tff(f721,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),X0)) = ap(ap(c_2Eextreal_2Eextreal__le,sF24),inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(superposition,[],[f221,f719]) ).
tff(f722,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(X0,surj__ty_2Eextreal_2Eextreal(sF24))) = ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),sF24) ),
inference(superposition,[],[f221,f719]) ).
tff(f725,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,sF24),inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),sF24))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(superposition,[],[f302,f719]) ).
tff(f730,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(ap(ap(c_2Eextreal_2Eextreal__le,sF24),inj__ty_2Eextreal_2Eextreal(X0)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),sF24)) ),
inference(superposition,[],[f303,f719]) ).
tff(f733,plain,
inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,surj__ty_2Eextreal_2Eextreal(sF24))) = ap(sF17,sF24),
inference(superposition,[],[f482,f719]) ).
tff(f734,plain,
inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,surj__ty_2Eextreal_2Eextreal(sF24))) = ap(sF21,sF24),
inference(superposition,[],[f483,f719]) ).
tff(f735,plain,
fo__c_2Eextreal_2Eextreal__max(sK14,surj__ty_2Eextreal_2Eextreal(sF24)) = surj__ty_2Eextreal_2Eextreal(ap(sF23,sF24)),
inference(superposition,[],[f591,f719]) ).
tff(f743,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),sF24)) ),
inference(forward_demodulation,[],[f730,f430]) ).
tff(f748,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),sF24))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_demodulation,[],[f725,f430]) ).
tff(f749,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),X0)) = ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(forward_demodulation,[],[f721,f430]) ).
tff(f751,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,surj__ty_2Eextreal_2Eextreal(sF24))))
| p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_demodulation,[],[f743,f722]) ).
tff(f756,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X1,surj__ty_2Eextreal_2Eextreal(sF24))))
| ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_demodulation,[],[f748,f722]) ).
tff(f759,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X1,surj__ty_2Eextreal_2Eextreal(sF24))))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(X1,X0)))
| ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_demodulation,[],[f756,f221]) ).
tff(f776,plain,
( p(ap(sF25,inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(sF24))))
| p(ap(sF25,inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(sF24)))) ),
inference(superposition,[],[f751,f749]) ).
tff(f782,plain,
p(ap(sF25,inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(sF24)))),
inference(duplicate_literal_removal,[],[f776]) ).
tff(f788,plain,
p(ap(sF25,sF24)),
inference(forward_demodulation,[],[f782,f719]) ).
tff(f824,plain,
! [X0: $i,X1: tp__ty_2Eextreal_2Eextreal] :
( ( ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Ebool_2ET)),X0),inj__ty_2Eextreal_2Eextreal(X1)) = X0 )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f283,f218]) ).
tff(f833,plain,
! [X0: $i,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| ( ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),X0),inj__ty_2Eextreal_2Eextreal(X1)) = X0 ) ),
inference(forward_demodulation,[],[f824,f215]) ).
tff(f834,plain,
! [X0: $i,X1: tp__ty_2Eextreal_2Eextreal] :
( ( inj__ty_2Eextreal_2Eextreal(X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Ebool_2EF)),X0),inj__ty_2Eextreal_2Eextreal(X1)) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f282,f218]) ).
tff(f843,plain,
! [X0: $i,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ mem(X0,ty_2Eextreal_2Eextreal)
| ( inj__ty_2Eextreal_2Eextreal(X1) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),X0),inj__ty_2Eextreal_2Eextreal(X1)) ) ),
inference(forward_demodulation,[],[f834,f226]) ).
tff(f939,plain,
mem(sF22,bool),
inference(superposition,[],[f212,f608]) ).
tff(f968,plain,
! [X0: $i] :
( mem(ap(c_2Eextreal_2Eextreal__le,X0),arr(ty_2Eextreal_2Eextreal,bool))
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f220,f204]) ).
tff(f973,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(resolution,[],[f968,f204]) ).
tff(f976,plain,
( mem(sF25,arr(ty_2Eextreal_2Eextreal,bool))
| ~ mem(sF24,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f968,f430]) ).
tff(f981,plain,
mem(sF25,arr(ty_2Eextreal_2Eextreal,bool)),
inference(forward_subsumption_resolution,[],[f976,f720]) ).
tff(f994,plain,
! [X0: $i] :
( mem(ap(sF25,X0),bool)
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f981,f204]) ).
tff(f1026,definition,
( spl27_9
<=> p(ap(sF25,sF16)) ),
introduced(definition,[new_symbols(definition,[spl27_9])],[avatar_definition]) ).
tff(f1027,plain,
( ~ p(ap(sF25,sF16))
| spl27_9 ),
inference(avatar_component_clause,[],[f1026]) ).
tff(f1028,plain,
( p(ap(sF25,sF16))
| ~ spl27_9 ),
inference(avatar_component_clause,[],[f1026]) ).
tff(f1074,plain,
! [X0: $i] :
( p(c_2Ebool_2EF)
| p(X0)
| ( c_2Ebool_2EF = X0 )
| ~ mem(X0,bool) ),
inference(resolution,[],[f205,f225]) ).
tff(f1077,plain,
! [X0: $i] :
( ~ mem(X0,bool)
| ( c_2Ebool_2EF = X0 )
| p(X0) ),
inference(forward_subsumption_resolution,[],[f1074,f227]) ).
tff(f1080,plain,
! [X0: tp__o] :
( p(inj__o(X0))
| ( inj__o(X0) = c_2Ebool_2EF ) ),
inference(resolution,[],[f1077,f212]) ).
tff(f1107,plain,
! [X2: tp__ty_2Eextreal_2Eextreal,X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(X1,X2)))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X2)))
| ( inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)) = c_2Ebool_2EF ) ),
inference(resolution,[],[f1080,f498]) ).
tff(f1142,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( inj__ty_2Eextreal_2Eextreal(X0) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)) ),
inference(resolution,[],[f833,f218]) ).
tff(f1294,plain,
mem(ap(sF21,sF16),bool),
inference(superposition,[],[f212,f606]) ).
tff(f1302,plain,
( p(ap(sF21,sF16))
| ( c_2Ebool_2EF = ap(sF21,sF16) ) ),
inference(superposition,[],[f1080,f606]) ).
tff(f1304,definition,
( spl27_15
<=> ( c_2Ebool_2EF = ap(sF21,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl27_15])],[avatar_definition]) ).
tff(f1305,plain,
( ( c_2Ebool_2EF != ap(sF21,sF16) )
| spl27_15 ),
inference(avatar_component_clause,[],[f1304]) ).
tff(f1306,plain,
( ( c_2Ebool_2EF = ap(sF21,sF16) )
| ~ spl27_15 ),
inference(avatar_component_clause,[],[f1304]) ).
tff(f1308,definition,
( spl27_16
<=> p(ap(sF21,sF16)) ),
introduced(definition,[new_symbols(definition,[spl27_16])],[avatar_definition]) ).
tff(f1310,plain,
( p(ap(sF21,sF16))
| ~ spl27_16 ),
inference(avatar_component_clause,[],[f1308]) ).
tff(f1311,plain,
( spl27_15
| spl27_16 ),
inference(avatar_split_clause,[],[f1302,f1308,f1304]) ).
tff(f1343,plain,
( mem(sF26,bool)
| ~ mem(sF18,ty_2Eextreal_2Eextreal) ),
inference(superposition,[],[f994,f432]) ).
tff(f1344,plain,
mem(sF26,bool),
inference(forward_subsumption_resolution,[],[f1343,f513]) ).
tff(f1347,plain,
( ( c_2Ebool_2EF = sF26 )
| p(sF26) ),
inference(resolution,[],[f1344,f1077]) ).
tff(f1355,plain,
( ( c_2Ebool_2EF = sF26 )
| spl27_1 ),
inference(forward_subsumption_resolution,[],[f1347,f452]) ).
tff(f1456,plain,
! [X0: $i] :
( ~ p(c_2Ebool_2ET)
| ~ p(X0)
| ( c_2Ebool_2ET = X0 )
| ~ mem(X0,bool) ),
inference(resolution,[],[f214,f206]) ).
tff(f1461,plain,
! [X0: $i] :
( ~ mem(X0,bool)
| ( c_2Ebool_2ET = X0 )
| ~ p(X0) ),
inference(forward_subsumption_resolution,[],[f1456,f216]) ).
tff(f1480,plain,
! [X0: tp__o] :
( ~ p(inj__o(X0))
| ( inj__o(X0) = c_2Ebool_2ET ) ),
inference(resolution,[],[f1461,f212]) ).
tff(f1484,plain,
( ( c_2Ebool_2ET = sF22 )
| ~ p(sF22) ),
inference(resolution,[],[f1461,f939]) ).
tff(f1485,plain,
( ( c_2Ebool_2ET = sF26 )
| ~ p(sF26) ),
inference(resolution,[],[f1461,f1344]) ).
tff(f1501,definition,
( spl27_20
<=> ( sF26 = ap(sF25,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl27_20])],[avatar_definition]) ).
tff(f1503,plain,
( ( sF26 = ap(sF25,sF16) )
| ~ spl27_20 ),
inference(avatar_component_clause,[],[f1501]) ).
tff(f1522,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(sF21,sF24))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,X0)))
| ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),X0))) ),
inference(superposition,[],[f498,f734]) ).
tff(f1532,plain,
( p(ap(sF21,sF24))
| ( c_2Ebool_2EF = ap(sF21,sF24) ) ),
inference(superposition,[],[f1080,f734]) ).
tff(f1612,plain,
( p(ap(sF17,sF24))
| p(ap(sF25,inj__ty_2Eextreal_2Eextreal(sK14))) ),
inference(superposition,[],[f751,f733]) ).
tff(f1615,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(sF17,sF24))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)))
| ~ p(inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),X0))) ),
inference(superposition,[],[f498,f733]) ).
tff(f1625,plain,
( p(ap(sF17,sF24))
| ( c_2Ebool_2EF = ap(sF17,sF24) ) ),
inference(superposition,[],[f1080,f733]) ).
tff(f1718,plain,
! [X0: $i,X1: $i] :
( ~ p(ap(ap(c_2Eextreal_2Eextreal__le,X1),X0))
| ~ mem(X1,ty_2Eextreal_2Eextreal)
| ( c_2Ebool_2ET = ap(ap(c_2Eextreal_2Eextreal__le,X1),X0) )
| ~ mem(X0,ty_2Eextreal_2Eextreal) ),
inference(resolution,[],[f973,f1461]) ).
tff(f1736,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ mem(inj__ty_2Eextreal_2Eextreal(X0),ty_2Eextreal_2Eextreal)
| ( c_2Ebool_2ET = ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)) )
| ~ mem(inj__ty_2Eextreal_2Eextreal(X1),ty_2Eextreal_2Eextreal)
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(resolution,[],[f1718,f303]) ).
tff(f1744,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ~ mem(inj__ty_2Eextreal_2Eextreal(X0),ty_2Eextreal_2Eextreal)
| ( c_2Ebool_2ET = 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(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_subsumption_resolution,[],[f1736,f218]) ).
tff(f1746,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ( c_2Ebool_2ET = 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(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_subsumption_resolution,[],[f1744,f218]) ).
tff(f1748,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)) )
| p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0))) ),
inference(forward_demodulation,[],[f1746,f221]) ).
tff(f1750,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] :
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(X1,X0)))
| ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X1)) ) ),
inference(forward_demodulation,[],[f1748,f221]) ).
tff(f1767,plain,
( p(ap(sF21,sF16))
| ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK15)) ) ),
inference(superposition,[],[f1750,f606]) ).
tff(f1778,plain,
! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( inj__ty_2Eextreal_2Eextreal(X0) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(X1)),inj__ty_2Eextreal_2Eextreal(X0)) ),
inference(resolution,[],[f843,f218]) ).
tff(f1919,plain,
( ( c_2Ebool_2ET = ap(sF21,sF16) )
| ~ p(ap(sF21,sF16)) ),
inference(resolution,[],[f1294,f1461]) ).
tff(f1924,plain,
( ( c_2Ebool_2ET = ap(sF21,sF16) )
| ~ spl27_16 ),
inference(forward_subsumption_resolution,[],[f1919,f1310]) ).
tff(f2459,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(sF19)
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,sK13)))
| ( c_2Ebool_2EF = inj__o(fo__c_2Eextreal_2Eextreal__le(X0,sK14)) ) ),
inference(superposition,[],[f1107,f599]) ).
tff(f2469,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,sK13)))
| ( c_2Ebool_2EF = inj__o(fo__c_2Eextreal_2Eextreal__le(X0,sK14)) ) )
| ~ spl27_3 ),
inference(forward_subsumption_resolution,[],[f2459,f462]) ).
tff(f2497,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(X0,sK13)))
| ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(X0,sK14)) ) )
| spl27_1
| ~ spl27_3 ),
inference(forward_demodulation,[],[f2469,f1355]) ).
tff(f2518,plain,
( p(ap(sF25,inj__ty_2Eextreal_2Eextreal(sK13)))
| ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),sK14)) )
| spl27_1
| ~ spl27_3 ),
inference(superposition,[],[f2497,f749]) ).
tff(f2519,plain,
( p(ap(sF25,sF18))
| ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),sK14)) )
| spl27_1
| ~ spl27_3 ),
inference(forward_demodulation,[],[f2518,f416]) ).
tff(f2525,plain,
( p(sF26)
| ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),sK14)) )
| spl27_1
| ~ spl27_3 ),
inference(forward_demodulation,[],[f2519,f432]) ).
tff(f2528,plain,
( ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(surj__ty_2Eextreal_2Eextreal(sF24),sK14)) )
| spl27_1
| ~ spl27_3 ),
inference(forward_subsumption_resolution,[],[f2525,f452]) ).
tff(f2531,plain,
( ( sF26 = ap(sF25,inj__ty_2Eextreal_2Eextreal(sK14)) )
| spl27_1
| ~ spl27_3 ),
inference(forward_demodulation,[],[f2528,f749]) ).
tff(f2532,plain,
( ( sF26 = ap(sF25,sF16) )
| spl27_1
| ~ spl27_3 ),
inference(forward_demodulation,[],[f2531,f412]) ).
tff(f2533,plain,
( spl27_20
| spl27_1
| ~ spl27_3 ),
inference(avatar_split_clause,[],[f2532,f460,f451,f1501]) ).
tff(f2556,plain,
( ( c_2Ebool_2ET = sF26 )
| ~ spl27_1 ),
inference(forward_subsumption_resolution,[],[f1485,f453]) ).
tff(f2558,definition,
( spl27_21
<=> ( c_2Ebool_2EF = ap(sF21,sF24) ) ),
introduced(definition,[new_symbols(definition,[spl27_21])],[avatar_definition]) ).
tff(f2560,plain,
( ( c_2Ebool_2EF = ap(sF21,sF24) )
| ~ spl27_21 ),
inference(avatar_component_clause,[],[f2558]) ).
tff(f2562,definition,
( spl27_22
<=> p(ap(sF21,sF24)) ),
introduced(definition,[new_symbols(definition,[spl27_22])],[avatar_definition]) ).
tff(f2565,plain,
( spl27_21
| spl27_22 ),
inference(avatar_split_clause,[],[f1532,f2562,f2558]) ).
tff(f2566,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(sF21,sF24))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,X0))) ),
inference(forward_demodulation,[],[f1522,f749]) ).
tff(f2573,definition,
( spl27_24
<=> ! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,X0)))
| ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl27_24])],[avatar_definition]) ).
tff(f2574,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,X0))) )
| ~ spl27_24 ),
inference(avatar_component_clause,[],[f2573]) ).
tff(f2577,plain,
( ( c_2Ebool_2ET != c_2Ebool_2EF )
| spl27_15
| ~ spl27_16 ),
inference(forward_demodulation,[],[f1305,f1924]) ).
tff(f2627,plain,
( ~ spl27_22
| spl27_24 ),
inference(avatar_split_clause,[],[f2566,f2573,f2562]) ).
tff(f2628,plain,
( ( c_2Ebool_2EF != sF26 )
| ~ spl27_1
| spl27_15
| ~ spl27_16 ),
inference(forward_demodulation,[],[f2577,f2556]) ).
tff(f2643,plain,
( p(c_2Ebool_2EF)
| ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK15)) )
| ~ spl27_15 ),
inference(forward_demodulation,[],[f1767,f1306]) ).
tff(f2653,plain,
( ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK15)) )
| ~ spl27_15 ),
inference(forward_subsumption_resolution,[],[f2643,f227]) ).
tff(f2658,plain,
( ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK15)) )
| ~ spl27_1
| ~ spl27_15 ),
inference(forward_demodulation,[],[f2653,f2556]) ).
tff(f2671,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal,X1: tp__ty_2Eextreal_2Eextreal] : ( inj__ty_2Eextreal_2Eextreal(X0) = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),sF26),inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(X1)) )
| ~ spl27_1 ),
inference(superposition,[],[f1142,f2556]) ).
tff(f2785,plain,
( ( fo__c_2Eextreal_2Eextreal__max(sK14,sK15) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),sF26),inj__ty_2Eextreal_2Eextreal(sK15)),inj__ty_2Eextreal_2Eextreal(sK14))) )
| ~ spl27_1
| ~ spl27_15 ),
inference(superposition,[],[f650,f2658]) ).
tff(f2806,plain,
( ( surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(sK15)) = fo__c_2Eextreal_2Eextreal__max(sK14,sK15) )
| ~ spl27_1
| ~ spl27_15 ),
inference(forward_demodulation,[],[f2785,f2671]) ).
tff(f2809,plain,
( ( surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(sK15)) = surj__ty_2Eextreal_2Eextreal(sF24) )
| ~ spl27_1
| ~ spl27_15 ),
inference(forward_demodulation,[],[f2806,f716]) ).
tff(f2812,plain,
( ( sK15 = surj__ty_2Eextreal_2Eextreal(sF24) )
| ~ spl27_1
| ~ spl27_15 ),
inference(forward_demodulation,[],[f2809,f217]) ).
tff(f2813,plain,
( ( inj__ty_2Eextreal_2Eextreal(sK15) = sF24 )
| ~ spl27_1
| ~ spl27_15 ),
inference(superposition,[],[f719,f2812]) ).
tff(f2825,plain,
( ( sF20 = sF24 )
| ~ spl27_1
| ~ spl27_15 ),
inference(forward_demodulation,[],[f2813,f420]) ).
tff(f2831,plain,
( ( ap(c_2Eextreal_2Eextreal__le,sF20) = sF25 )
| ~ spl27_1
| ~ spl27_15 ),
inference(superposition,[],[f430,f2825]) ).
tff(f2855,plain,
( ( sF21 = sF25 )
| ~ spl27_1
| ~ spl27_15 ),
inference(forward_demodulation,[],[f2831,f422]) ).
tff(f2858,plain,
( ( ap(sF21,sF18) = sF26 )
| ~ spl27_1
| ~ spl27_15 ),
inference(superposition,[],[f432,f2855]) ).
tff(f2865,plain,
( p(ap(sF21,sF16))
| ~ spl27_1
| ~ spl27_9
| ~ spl27_15 ),
inference(superposition,[],[f1028,f2855]) ).
tff(f2870,plain,
( p(c_2Ebool_2EF)
| ~ spl27_1
| ~ spl27_9
| ~ spl27_15 ),
inference(forward_demodulation,[],[f2865,f1306]) ).
tff(f2875,plain,
( $false
| ~ spl27_1
| ~ spl27_9
| ~ spl27_15 ),
inference(forward_subsumption_resolution,[],[f2870,f227]) ).
tff(f2876,plain,
( ~ spl27_1
| ~ spl27_9
| ~ spl27_15 ),
inference(avatar_contradiction_clause,[],[f2875]) ).
tff(f2887,plain,
( ( sF22 = sF26 )
| ~ spl27_1
| ~ spl27_15 ),
inference(superposition,[],[f424,f2858]) ).
tff(f2891,plain,
( ~ p(sF26)
| ~ spl27_1
| spl27_2
| ~ spl27_15 ),
inference(superposition,[],[f456,f2887]) ).
tff(f2896,plain,
( $false
| ~ spl27_1
| spl27_2
| ~ spl27_15 ),
inference(forward_subsumption_resolution,[],[f2891,f453]) ).
tff(f2897,plain,
( ~ spl27_1
| spl27_2
| ~ spl27_15 ),
inference(avatar_contradiction_clause,[],[f2896]) ).
tff(f2960,definition,
( spl27_38
<=> ( c_2Ebool_2EF = ap(sF17,sF24) ) ),
introduced(definition,[new_symbols(definition,[spl27_38])],[avatar_definition]) ).
tff(f2961,plain,
( ( c_2Ebool_2EF != ap(sF17,sF24) )
| spl27_38 ),
inference(avatar_component_clause,[],[f2960]) ).
tff(f2962,plain,
( ( c_2Ebool_2EF = ap(sF17,sF24) )
| ~ spl27_38 ),
inference(avatar_component_clause,[],[f2960]) ).
tff(f2964,definition,
( spl27_39
<=> p(ap(sF17,sF24)) ),
introduced(definition,[new_symbols(definition,[spl27_39])],[avatar_definition]) ).
tff(f2966,plain,
( p(ap(sF17,sF24))
| ~ spl27_39 ),
inference(avatar_component_clause,[],[f2964]) ).
tff(f2967,plain,
( spl27_38
| spl27_39 ),
inference(avatar_split_clause,[],[f1625,f2964,f2960]) ).
tff(f2968,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| ~ p(ap(sF17,sF24))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0))) ),
inference(forward_demodulation,[],[f1615,f749]) ).
tff(f2969,plain,
( p(ap(sF25,sF16))
| p(ap(sF17,sF24)) ),
inference(forward_demodulation,[],[f1612,f412]) ).
tff(f2971,definition,
( spl27_40
<=> ! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)))
| ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl27_40])],[avatar_definition]) ).
tff(f2972,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0))) )
| ~ spl27_40 ),
inference(avatar_component_clause,[],[f2971]) ).
tff(f2995,plain,
( ~ spl27_39
| spl27_40 ),
inference(avatar_split_clause,[],[f2968,f2971,f2964]) ).
tff(f2996,plain,
( p(ap(sF17,sF24))
| spl27_9 ),
inference(forward_subsumption_resolution,[],[f2969,f1027]) ).
tff(f2999,plain,
( spl27_39
| spl27_9 ),
inference(avatar_split_clause,[],[f2996,f1026,f2964]) ).
tff(f3370,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( sF16 = ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(X0)),sF16) ),
inference(superposition,[],[f1778,f412]) ).
tff(f3489,plain,
( p(sF26)
| p(ap(sF17,sF24))
| ~ spl27_20 ),
inference(forward_demodulation,[],[f2969,f1503]) ).
tff(f3636,plain,
( ~ p(ap(sF25,sF18))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK13)))
| ~ spl27_24 ),
inference(superposition,[],[f2574,f416]) ).
tff(f3640,plain,
( ~ p(sF26)
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK13)))
| ~ spl27_24 ),
inference(forward_demodulation,[],[f3636,f432]) ).
tff(f3644,plain,
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK13)))
| ~ spl27_1
| ~ spl27_24 ),
inference(forward_subsumption_resolution,[],[f3640,f453]) ).
tff(f3647,plain,
( p(sF22)
| ~ spl27_1
| ~ spl27_24 ),
inference(forward_demodulation,[],[f3644,f608]) ).
tff(f3649,plain,
( $false
| ~ spl27_1
| spl27_2
| ~ spl27_24 ),
inference(forward_subsumption_resolution,[],[f3647,f456]) ).
tff(f3650,plain,
( ~ spl27_1
| spl27_2
| ~ spl27_24 ),
inference(avatar_contradiction_clause,[],[f3649]) ).
tff(f3659,plain,
( ~ p(ap(sF25,sF18))
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK13)))
| ~ spl27_40 ),
inference(superposition,[],[f2972,f416]) ).
tff(f3663,plain,
( ~ p(sF26)
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK13)))
| ~ spl27_40 ),
inference(forward_demodulation,[],[f3659,f432]) ).
tff(f3667,plain,
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK13)))
| ~ spl27_1
| ~ spl27_40 ),
inference(forward_subsumption_resolution,[],[f3663,f453]) ).
tff(f3669,plain,
( p(sF19)
| ~ spl27_1
| ~ spl27_40 ),
inference(forward_demodulation,[],[f3667,f599]) ).
tff(f3671,plain,
( $false
| ~ spl27_1
| spl27_3
| ~ spl27_40 ),
inference(forward_subsumption_resolution,[],[f3669,f461]) ).
tff(f3672,plain,
( ~ spl27_1
| spl27_3
| ~ spl27_40 ),
inference(avatar_contradiction_clause,[],[f3671]) ).
tff(f3804,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] : ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X0)) ),
inference(resolution,[],[f1480,f547]) ).
tff(f3826,plain,
! [X0: tp__o] :
( ( inj__o(X0) = c_2Ebool_2EF )
| ( inj__o(X0) = c_2Ebool_2ET ) ),
inference(resolution,[],[f1480,f1080]) ).
tff(f3833,plain,
( ~ p(ap(sF17,sF24))
| ( c_2Ebool_2ET = ap(sF17,sF24) ) ),
inference(superposition,[],[f1480,f733]) ).
tff(f3851,plain,
( ! [X0: tp__o] :
( ( inj__o(X0) = c_2Ebool_2EF )
| ( inj__o(X0) = sF26 ) )
| ~ spl27_1 ),
inference(forward_demodulation,[],[f3826,f2556]) ).
tff(f3869,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] : ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(X0,X0)) )
| ~ spl27_1 ),
inference(forward_demodulation,[],[f3804,f2556]) ).
tff(f4105,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(X0)),sF16)) )
| ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) ) )
| ~ spl27_1 ),
inference(superposition,[],[f660,f3851]) ).
tff(f4115,plain,
( ( c_2Ebool_2EF = ap(sF21,sF16) )
| ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK14)) )
| ~ spl27_1 ),
inference(superposition,[],[f606,f3851]) ).
tff(f4125,plain,
( ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK14)) )
| ~ spl27_1
| spl27_15 ),
inference(forward_subsumption_resolution,[],[f4115,f1305]) ).
tff(f4128,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = surj__ty_2Eextreal_2Eextreal(sF16) )
| ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) ) )
| ~ spl27_1 ),
inference(forward_demodulation,[],[f4105,f3370]) ).
tff(f4155,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( sF26 = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) )
| ( sK14 = fo__c_2Eextreal_2Eextreal__max(sK14,X0) ) )
| ~ spl27_1 ),
inference(forward_demodulation,[],[f4128,f593]) ).
tff(f4202,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( ~ p(sF26)
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)))
| ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| ( sK14 = fo__c_2Eextreal_2Eextreal__max(sK14,surj__ty_2Eextreal_2Eextreal(sF24)) ) )
| ~ spl27_1 ),
inference(superposition,[],[f759,f4155]) ).
tff(f4232,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)))
| ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0)))
| ( sK14 = fo__c_2Eextreal_2Eextreal__max(sK14,surj__ty_2Eextreal_2Eextreal(sF24)) ) )
| ~ spl27_1 ),
inference(forward_subsumption_resolution,[],[f4202,f453]) ).
tff(f4254,plain,
( ! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( sK14 = surj__ty_2Eextreal_2Eextreal(ap(sF23,sF24)) )
| p(inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)))
| ~ p(ap(sF25,inj__ty_2Eextreal_2Eextreal(X0))) )
| ~ spl27_1 ),
inference(forward_demodulation,[],[f4232,f735]) ).
tff(f4262,definition,
( spl27_45
<=> ( sK14 = surj__ty_2Eextreal_2Eextreal(ap(sF23,sF24)) ) ),
introduced(definition,[new_symbols(definition,[spl27_45])],[avatar_definition]) ).
tff(f4264,plain,
( ( sK14 = surj__ty_2Eextreal_2Eextreal(ap(sF23,sF24)) )
| ~ spl27_45 ),
inference(avatar_component_clause,[],[f4262]) ).
tff(f4265,plain,
( spl27_40
| spl27_45
| ~ spl27_1 ),
inference(avatar_split_clause,[],[f4254,f451,f4262,f2971]) ).
tff(f4283,definition,
( spl27_46
<=> ( sK15 = surj__ty_2Eextreal_2Eextreal(sF24) ) ),
introduced(definition,[new_symbols(definition,[spl27_46])],[avatar_definition]) ).
tff(f4284,plain,
( ( sK15 != surj__ty_2Eextreal_2Eextreal(sF24) )
| spl27_46 ),
inference(avatar_component_clause,[],[f4283]) ).
tff(f4285,plain,
( ( sK15 = surj__ty_2Eextreal_2Eextreal(sF24) )
| ~ spl27_46 ),
inference(avatar_component_clause,[],[f4283]) ).
tff(f4287,definition,
( spl27_47
<=> ( sK14 = surj__ty_2Eextreal_2Eextreal(sF24) ) ),
introduced(definition,[new_symbols(definition,[spl27_47])],[avatar_definition]) ).
tff(f4288,plain,
( ( sK14 != surj__ty_2Eextreal_2Eextreal(sF24) )
| spl27_47 ),
inference(avatar_component_clause,[],[f4287]) ).
tff(f4289,plain,
( ( sK14 = surj__ty_2Eextreal_2Eextreal(sF24) )
| ~ spl27_47 ),
inference(avatar_component_clause,[],[f4287]) ).
tff(f4293,plain,
( ( inj__ty_2Eextreal_2Eextreal(sK14) = sF24 )
| ~ spl27_47 ),
inference(superposition,[],[f719,f4289]) ).
tff(f4294,plain,
( ( inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK14)) = ap(sF17,sF24) )
| ~ spl27_47 ),
inference(superposition,[],[f733,f4289]) ).
tff(f4295,plain,
( ( inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK14)) = ap(sF21,sF24) )
| ~ spl27_47 ),
inference(superposition,[],[f734,f4289]) ).
tff(f4302,plain,
( ( c_2Ebool_2EF = inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK14)) )
| ~ spl27_21
| ~ spl27_47 ),
inference(forward_demodulation,[],[f4295,f2560]) ).
tff(f4303,plain,
( ( c_2Ebool_2EF = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,sK14)) )
| ~ spl27_38
| ~ spl27_47 ),
inference(forward_demodulation,[],[f4294,f2962]) ).
tff(f4304,plain,
( ( sF16 = sF24 )
| ~ spl27_47 ),
inference(forward_demodulation,[],[f4293,f412]) ).
tff(f4305,plain,
( ( c_2Ebool_2EF = sF26 )
| ~ spl27_1
| spl27_15
| ~ spl27_21
| ~ spl27_47 ),
inference(forward_demodulation,[],[f4302,f4125]) ).
tff(f4306,plain,
( ( c_2Ebool_2EF = sF26 )
| ~ spl27_1
| ~ spl27_38
| ~ spl27_47 ),
inference(forward_demodulation,[],[f4303,f3869]) ).
tff(f4307,plain,
( $false
| ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_21
| ~ spl27_47 ),
inference(forward_subsumption_resolution,[],[f4305,f2628]) ).
tff(f4308,plain,
( ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_21
| ~ spl27_47 ),
inference(avatar_contradiction_clause,[],[f4307]) ).
tff(f4309,plain,
( $false
| ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_38
| ~ spl27_47 ),
inference(forward_subsumption_resolution,[],[f4306,f2628]) ).
tff(f4310,plain,
( ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_38
| ~ spl27_47 ),
inference(avatar_contradiction_clause,[],[f4309]) ).
tff(f4311,plain,
( ( sK14 != sK15 )
| ~ spl27_46
| spl27_47 ),
inference(forward_demodulation,[],[f4288,f4285]) ).
tff(f4312,plain,
( ( inj__ty_2Eextreal_2Eextreal(sK15) = sF24 )
| ~ spl27_46 ),
inference(superposition,[],[f719,f4285]) ).
tff(f4314,plain,
( ( inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK15)) = ap(sF21,sF24) )
| ~ spl27_46 ),
inference(superposition,[],[f734,f4285]) ).
tff(f4321,plain,
( ( c_2Ebool_2EF = inj__o(fo__c_2Eextreal_2Eextreal__le(sK15,sK15)) )
| ~ spl27_21
| ~ spl27_46 ),
inference(forward_demodulation,[],[f4314,f2560]) ).
tff(f4323,plain,
( ( sF20 = sF24 )
| ~ spl27_46 ),
inference(forward_demodulation,[],[f4312,f420]) ).
tff(f4324,plain,
( ( c_2Ebool_2EF = sF26 )
| ~ spl27_1
| ~ spl27_21
| ~ spl27_46 ),
inference(forward_demodulation,[],[f4321,f3869]) ).
tff(f4326,plain,
( $false
| ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_21
| ~ spl27_46 ),
inference(forward_subsumption_resolution,[],[f4324,f2628]) ).
tff(f4327,plain,
( ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_21
| ~ spl27_46 ),
inference(avatar_contradiction_clause,[],[f4326]) ).
tff(f4373,plain,
( ( c_2Ebool_2ET = sF22 )
| ~ spl27_2 ),
inference(forward_subsumption_resolution,[],[f1484,f457]) ).
tff(f4411,definition,
( spl27_51
<=> ( sF22 = sF26 ) ),
introduced(definition,[new_symbols(definition,[spl27_51])],[avatar_definition]) ).
tff(f4412,plain,
( ( sF22 != sF26 )
| spl27_51 ),
inference(avatar_component_clause,[],[f4411]) ).
tff(f4413,plain,
( ( sF22 = sF26 )
| ~ spl27_51 ),
inference(avatar_component_clause,[],[f4411]) ).
tff(f4483,plain,
( ( ap(c_2Eextreal_2Eextreal__le,sF20) = sF25 )
| ~ spl27_46 ),
inference(superposition,[],[f430,f4323]) ).
tff(f4499,plain,
( ( sK14 = surj__ty_2Eextreal_2Eextreal(ap(sF23,sF20)) )
| ~ spl27_45
| ~ spl27_46 ),
inference(superposition,[],[f4264,f4323]) ).
tff(f4501,plain,
( ( sK14 = surj__ty_2Eextreal_2Eextreal(sF24) )
| ~ spl27_45
| ~ spl27_46 ),
inference(forward_demodulation,[],[f4499,f428]) ).
tff(f4512,plain,
( ( sF21 = sF25 )
| ~ spl27_46 ),
inference(forward_demodulation,[],[f4483,f422]) ).
tff(f4513,plain,
( ( sK14 = surj__ty_2Eextreal_2Eextreal(sF20) )
| ~ spl27_45
| ~ spl27_46 ),
inference(forward_demodulation,[],[f4501,f4323]) ).
tff(f4515,plain,
( ( ap(sF21,sF18) = sF26 )
| ~ spl27_46 ),
inference(superposition,[],[f432,f4512]) ).
tff(f4541,plain,
( ( sF22 = sF26 )
| ~ spl27_46 ),
inference(superposition,[],[f424,f4515]) ).
tff(f4544,plain,
( ( sK14 = sK15 )
| ~ spl27_45
| ~ spl27_46 ),
inference(superposition,[],[f4513,f594]) ).
tff(f4548,plain,
( $false
| ~ spl27_45
| ~ spl27_46
| spl27_47 ),
inference(forward_subsumption_resolution,[],[f4544,f4311]) ).
tff(f4549,plain,
( ~ spl27_45
| ~ spl27_46
| spl27_47 ),
inference(avatar_contradiction_clause,[],[f4548]) ).
tff(f4593,plain,
( ( c_2Ebool_2EF = sF26 )
| spl27_1 ),
inference(forward_subsumption_resolution,[],[f1347,f452]) ).
tff(f4606,plain,
( p(ap(sF17,sF24))
| spl27_1
| ~ spl27_20 ),
inference(forward_subsumption_resolution,[],[f3489,f452]) ).
tff(f4631,plain,
( ( c_2Ebool_2ET = sF26 )
| ~ spl27_2
| ~ spl27_51 ),
inference(forward_demodulation,[],[f4373,f4413]) ).
tff(f4658,plain,
( p(c_2Ebool_2EF)
| spl27_1
| ~ spl27_20
| ~ spl27_38 ),
inference(forward_demodulation,[],[f4606,f2962]) ).
tff(f4677,plain,
( $false
| spl27_1
| ~ spl27_20
| ~ spl27_38 ),
inference(forward_subsumption_resolution,[],[f4658,f227]) ).
tff(f4678,plain,
( spl27_1
| ~ spl27_20
| ~ spl27_38 ),
inference(avatar_contradiction_clause,[],[f4677]) ).
tff(f4815,plain,
( p(ap(sF25,sF16))
| ~ spl27_47 ),
inference(superposition,[],[f788,f4304]) ).
tff(f4822,plain,
( p(sF26)
| ~ spl27_20
| ~ spl27_47 ),
inference(forward_demodulation,[],[f4815,f1503]) ).
tff(f4832,plain,
( $false
| spl27_1
| ~ spl27_20
| ~ spl27_47 ),
inference(forward_subsumption_resolution,[],[f4822,f452]) ).
tff(f4833,plain,
( spl27_1
| ~ spl27_20
| ~ spl27_47 ),
inference(avatar_contradiction_clause,[],[f4832]) ).
tff(f4836,plain,
( ( sF26 != ap(sF17,sF24) )
| spl27_1
| spl27_38 ),
inference(forward_demodulation,[],[f2961,f4593]) ).
tff(f4848,plain,
( ( c_2Ebool_2ET = ap(sF17,sF24) )
| ~ spl27_39 ),
inference(forward_subsumption_resolution,[],[f3833,f2966]) ).
tff(f4855,plain,
( ( sF26 = ap(sF17,sF24) )
| ~ spl27_2
| ~ spl27_39
| ~ spl27_51 ),
inference(forward_demodulation,[],[f4848,f4631]) ).
tff(f4860,plain,
( $false
| spl27_1
| ~ spl27_2
| spl27_38
| ~ spl27_39
| ~ spl27_51 ),
inference(forward_subsumption_resolution,[],[f4855,f4836]) ).
tff(f4861,plain,
( spl27_1
| ~ spl27_2
| spl27_38
| ~ spl27_39
| ~ spl27_51 ),
inference(avatar_contradiction_clause,[],[f4860]) ).
tff(f5088,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(X0)),sF16)) )
| ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) ) ),
inference(superposition,[],[f660,f3826]) ).
tff(f5112,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = surj__ty_2Eextreal_2Eextreal(sF16) )
| ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) ) ),
inference(forward_demodulation,[],[f5088,f3370]) ).
tff(f5138,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( c_2Ebool_2ET = inj__o(fo__c_2Eextreal_2Eextreal__le(sK14,X0)) )
| ( sK14 = fo__c_2Eextreal_2Eextreal__max(sK14,X0) ) ),
inference(forward_demodulation,[],[f5112,f593]) ).
tff(f7476,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),inj__ty_2Eextreal_2Eextreal(X0)),inj__ty_2Eextreal_2Eextreal(sK14))) )
| ( sK14 = fo__c_2Eextreal_2Eextreal__max(sK14,X0) ) ),
inference(superposition,[],[f650,f5138]) ).
tff(f7511,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(X0)) = fo__c_2Eextreal_2Eextreal__max(sK14,X0) )
| ( sK14 = fo__c_2Eextreal_2Eextreal__max(sK14,X0) ) ),
inference(forward_demodulation,[],[f7476,f1142]) ).
tff(f7520,plain,
! [X0: tp__ty_2Eextreal_2Eextreal] :
( ( fo__c_2Eextreal_2Eextreal__max(sK14,X0) = X0 )
| ( sK14 = fo__c_2Eextreal_2Eextreal__max(sK14,X0) ) ),
inference(forward_demodulation,[],[f7511,f217]) ).
tff(f7539,plain,
( ( sK15 = surj__ty_2Eextreal_2Eextreal(sF24) )
| ( sK14 = surj__ty_2Eextreal_2Eextreal(sF24) ) ),
inference(superposition,[],[f7520,f716]) ).
tff(f7540,plain,
( ( sK14 = surj__ty_2Eextreal_2Eextreal(sF24) )
| ( sK15 = surj__ty_2Eextreal_2Eextreal(sF24) ) ),
inference(superposition,[],[f7520,f716]) ).
tff(f7555,plain,
( ( sK15 = surj__ty_2Eextreal_2Eextreal(sF24) )
| spl27_47 ),
inference(forward_subsumption_resolution,[],[f7540,f4288]) ).
tff(f7556,plain,
( ( sK14 = surj__ty_2Eextreal_2Eextreal(sF24) )
| spl27_46 ),
inference(forward_subsumption_resolution,[],[f7539,f4284]) ).
tff(f7557,plain,
( $false
| spl27_46
| spl27_47 ),
inference(forward_subsumption_resolution,[],[f7555,f4284]) ).
tff(f7558,plain,
( spl27_46
| spl27_47 ),
inference(avatar_contradiction_clause,[],[f7557]) ).
tff(f7559,plain,
( $false
| spl27_46
| spl27_47 ),
inference(forward_subsumption_resolution,[],[f7556,f4288]) ).
tff(f7560,plain,
( spl27_46
| spl27_47 ),
inference(avatar_contradiction_clause,[],[f7559]) ).
tff(f7567,plain,
( $false
| ~ spl27_46
| spl27_51 ),
inference(forward_subsumption_resolution,[],[f4541,f4412]) ).
tff(f7568,plain,
( ~ spl27_46
| spl27_51 ),
inference(avatar_contradiction_clause,[],[f7567]) ).
cnf(s1,plain,
( spl27_1
| spl27_2 ),
inference(sat_conversion,[],[f458]) ).
cnf(s2,plain,
( spl27_1
| spl27_3 ),
inference(sat_conversion,[],[f463]) ).
cnf(s3,plain,
( ~ spl27_1
| ~ spl27_2
| ~ spl27_3 ),
inference(sat_conversion,[],[f464]) ).
cnf(s16,plain,
( spl27_15
| spl27_16 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s22,plain,
( spl27_1
| ~ spl27_3
| spl27_20 ),
inference(sat_conversion,[],[f2533]) ).
cnf(s26,plain,
( spl27_21
| spl27_22 ),
inference(sat_conversion,[],[f2565]) ).
cnf(s35,plain,
( ~ spl27_22
| spl27_24 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s42,plain,
( ~ spl27_1
| ~ spl27_9
| ~ spl27_15 ),
inference(sat_conversion,[],[f2876]) ).
cnf(s43,plain,
( ~ spl27_1
| spl27_2
| ~ spl27_15 ),
inference(sat_conversion,[],[f2897]) ).
cnf(s55,plain,
( spl27_38
| spl27_39 ),
inference(sat_conversion,[],[f2967]) ).
cnf(s60,plain,
( ~ spl27_39
| spl27_40 ),
inference(sat_conversion,[],[f2995]) ).
cnf(s61,plain,
( spl27_9
| spl27_39 ),
inference(sat_conversion,[],[f2999]) ).
cnf(s74,plain,
( ~ spl27_1
| spl27_2
| ~ spl27_24 ),
inference(sat_conversion,[],[f3650]) ).
cnf(s76,plain,
( ~ spl27_1
| spl27_3
| ~ spl27_40 ),
inference(sat_conversion,[],[f3672]) ).
cnf(s79,plain,
( ~ spl27_1
| spl27_40
| spl27_45 ),
inference(sat_conversion,[],[f4265]) ).
cnf(s86,plain,
( ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_21
| ~ spl27_47 ),
inference(sat_conversion,[],[f4308]) ).
cnf(s87,plain,
( ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_38
| ~ spl27_47 ),
inference(sat_conversion,[],[f4310]) ).
cnf(s88,plain,
( ~ spl27_1
| spl27_15
| ~ spl27_16
| ~ spl27_21
| ~ spl27_46 ),
inference(sat_conversion,[],[f4327]) ).
cnf(s113,plain,
( ~ spl27_45
| ~ spl27_46
| spl27_47 ),
inference(sat_conversion,[],[f4549]) ).
cnf(s128,plain,
( spl27_1
| ~ spl27_20
| ~ spl27_38 ),
inference(sat_conversion,[],[f4678]) ).
cnf(s132,plain,
( spl27_1
| ~ spl27_20
| ~ spl27_47 ),
inference(sat_conversion,[],[f4833]) ).
cnf(s141,plain,
( spl27_1
| ~ spl27_2
| spl27_38
| ~ spl27_39
| ~ spl27_51 ),
inference(sat_conversion,[],[f4861]) ).
cnf(s219,plain,
( spl27_46
| spl27_47 ),
inference(sat_conversion,[],[f7558]) ).
cnf(s220,plain,
( spl27_46
| spl27_47 ),
inference(sat_conversion,[],[f7560]) ).
cnf(s223,plain,
( ~ spl27_46
| spl27_51 ),
inference(sat_conversion,[],[f7568]) ).
cnf(s260,plain,
spl27_1,
inference(rat,[],[s141,s223,s55,s220,s128,s132,s22,s1,s2]) ).
cnf(s261,plain,
( ~ spl27_21
| ~ spl27_16
| spl27_15 ),
inference(rat,[],[s219,s86,s88,s260]) ).
cnf(s262,plain,
spl27_2,
inference(rat,[],[s261,s26,s35,s16,s74,s43,s260]) ).
cnf(s266,plain,
~ spl27_3,
inference(rat,[],[s3,s260,s262]) ).
cnf(s269,plain,
~ spl27_40,
inference(rat,[],[s76,s260,s266]) ).
cnf(s272,plain,
spl27_45,
inference(rat,[],[s79,s260,s269]) ).
cnf(s273,plain,
~ spl27_39,
inference(rat,[],[s60,s269]) ).
cnf(s278,plain,
spl27_9,
inference(rat,[],[s61,s273]) ).
cnf(s280,plain,
spl27_38,
inference(rat,[],[s55,s273]) ).
cnf(s281,plain,
~ spl27_15,
inference(rat,[],[s42,s260,s278]) ).
cnf(s282,plain,
spl27_16,
inference(rat,[],[s16,s281]) ).
cnf(s289,plain,
~ spl27_47,
inference(rat,[],[s87,s281,s280,s260,s282]) ).
cnf(s291,plain,
spl27_46,
inference(rat,[],[s220,s289]) ).
cnf(s292,plain,
$false,
inference(rat,[],[s113,s272,s289,s291]) ).
tff(f7737,plain,
$false,
inference(avatar_sat_refutation,[],[s292]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP021_2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 12:09:38 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.53/2.20 % (2232557)Detected formulas, will run a generic FOF schedule.
% 11.53/2.20 % (2232567)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2049596061:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.53/2.20 % (2232565)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3407391058:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.53/2.20 % (2232566)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2482110244:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.53/2.20 % (2232564)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3383291964:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.53/2.20 % (2232563)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3895382440:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.53/2.20 % (2232562)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3171303213:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.53/2.20 % (2232568)dis-21_1_sil=8000:lcm=predicate:random_seed=490768520:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.53/2.20 % (2232565)Refutation not found, incomplete strategy
% 11.53/2.20 % (2232565)------------------------------
% 11.53/2.20 % (2232565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.20 % (2232565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.20 % (2232565)CaDiCaL version: 2.1.3
% 11.53/2.20 % (2232565)Termination reason: Refutation not found, incomplete strategy
% 11.53/2.20 % (2232565)Time elapsed: 0.001 s
% 11.53/2.20 % (2232565)Peak memory usage: 88 MB
% 11.53/2.20 % (2232567)Instruction limit reached!
% 11.53/2.20 % (2232567)------------------------------
% 11.53/2.20 % (2232567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.20 % (2232567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.20 % (2232567)CaDiCaL version: 2.1.3
% 11.53/2.20 % (2232567)Termination reason: Instruction limit
% 11.53/2.20 % (2232567)Termination phase: Saturation
% 11.53/2.20 % (2232567)Time elapsed: 0.048 s
% 11.53/2.20 % (2232567)Peak memory usage: 90 MB
% 11.53/2.20 % (2232567)Instructions burned: 140 (million)
% 11.53/2.20 % (2232566)Instruction limit reached!
% 11.53/2.20 % (2232566)------------------------------
% 11.53/2.20 % (2232566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.20 % (2232566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.20 % (2232566)CaDiCaL version: 2.1.3
% 11.53/2.20 % (2232566)Termination reason: Instruction limit
% 11.53/2.20 % (2232566)Termination phase: Saturation
% 11.53/2.20 % (2232566)Time elapsed: 0.063 s
% 11.53/2.20 % (2232566)Peak memory usage: 88 MB
% 11.53/2.20 % (2232566)Instructions burned: 119 (million)
% 11.53/2.20 % (2232568)Instruction limit reached!
% 11.53/2.20 % (2232568)------------------------------
% 11.53/2.20 % (2232568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.20 % (2232568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.20 % (2232568)CaDiCaL version: 2.1.3
% 11.53/2.20 % (2232568)Termination reason: Instruction limit
% 11.53/2.20 % (2232568)Termination phase: Saturation
% 11.53/2.20 % (2232568)Time elapsed: 0.077 s
% 11.53/2.20 % (2232568)Peak memory usage: 90 MB
% 11.53/2.20 % (2232568)Instructions burned: 129 (million)
% 11.53/2.20 % (2232576)lrs+10_1_sil=8000:sp=occurrence:random_seed=2648069028:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.53/2.20 % (2232577)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2631889850:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.53/2.20 % (2232577)Refutation not found, incomplete strategy
% 11.53/2.20 % (2232577)------------------------------
% 11.53/2.20 % (2232577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.53/2.20 % (2232577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.53/2.20 % (2232577)CaDiCaL version: 2.1.3
% 11.53/2.20 % (2232577)Termination reason: Refutation not found, incomplete strategy
% 11.53/2.20 % (2232577)Time elapsed: 0.003 s
% 6.65/2.71 % (2232577)Peak memory usage: 89 MB
% 6.65/2.71 % (2232577)Instructions burned: 3 (million)
% 6.65/2.71 % (2232578)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4141423127:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.65/2.71 % (2232565)------------------------------
% 6.65/2.71 % (2232565)------------------------------
% 6.65/2.71 % (2232576)Instruction limit reached!
% 6.65/2.71 % (2232576)------------------------------
% 6.65/2.71 % (2232576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232576)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232576)Termination reason: Instruction limit
% 6.65/2.71 % (2232576)Termination phase: Saturation
% 6.65/2.71 % (2232576)Time elapsed: 0.094 s
% 6.65/2.71 % (2232576)Peak memory usage: 90 MB
% 6.65/2.71 % (2232576)Instructions burned: 288 (million)
% 6.65/2.71 % (2232578)Instruction limit reached!
% 6.65/2.71 % (2232578)------------------------------
% 6.65/2.71 % (2232578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232578)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232578)Termination reason: Instruction limit
% 6.65/2.71 % (2232578)Termination phase: Saturation
% 6.65/2.71 % (2232578)Time elapsed: 0.129 s
% 6.65/2.71 % (2232578)Peak memory usage: 89 MB
% 6.65/2.71 % (2232578)Instructions burned: 327 (million)
% 6.65/2.71 % (2232583)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4001052069:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.65/2.71 % (2232583)Refutation not found, incomplete strategy
% 6.65/2.71 % (2232583)------------------------------
% 6.65/2.71 % (2232583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232583)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232583)Termination reason: Refutation not found, incomplete strategy
% 6.65/2.71 % (2232583)Time elapsed: 0.003 s
% 6.65/2.71 % (2232583)Peak memory usage: 89 MB
% 6.65/2.71 % (2232583)Instructions burned: 6 (million)
% 6.65/2.71 % (2232582)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2555364700:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 6.65/2.71 % (2232577)------------------------------
% 6.65/2.71 % (2232577)------------------------------
% 6.65/2.71 % (2232583)------------------------------
% 6.65/2.71 % (2232583)------------------------------
% 6.65/2.71 % (2232584)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3168207800:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 6.65/2.71 % (2232582)Instruction limit reached!
% 6.65/2.71 % (2232582)------------------------------
% 6.65/2.71 % (2232582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232582)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232582)Termination reason: Instruction limit
% 6.65/2.71 % (2232582)Termination phase: Saturation
% 6.65/2.71 % (2232582)Time elapsed: 0.141 s
% 6.65/2.71 % (2232582)Peak memory usage: 92 MB
% 6.65/2.71 % (2232582)Instructions burned: 249 (million)
% 6.65/2.71 % (2232587)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3320230116:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 6.65/2.71 % (2232589)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2921611748:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 6.65/2.71 % (2232589)Instruction limit reached!
% 6.65/2.71 % (2232589)------------------------------
% 6.65/2.71 % (2232589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232589)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232589)Termination reason: Instruction limit
% 6.65/2.71 % (2232589)Termination phase: Saturation
% 6.65/2.71 % (2232589)Time elapsed: 0.030 s
% 6.65/2.71 % (2232589)Peak memory usage: 88 MB
% 6.65/2.71 % (2232589)Instructions burned: 131 (million)
% 6.65/2.71 % (2232587)Instruction limit reached!
% 6.65/2.71 % (2232587)------------------------------
% 6.65/2.71 % (2232587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232587)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232587)Termination reason: Instruction limit
% 6.65/2.71 % (2232587)Termination phase: Saturation
% 6.65/2.71 % (2232587)Time elapsed: 0.071 s
% 6.65/2.71 % (2232587)Peak memory usage: 90 MB
% 6.65/2.71 % (2232587)Instructions burned: 114 (million)
% 6.65/2.71 % (2232590)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3370577802:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 6.65/2.71 % (2232593)lrs+10_1_sil=8000:sp=occurrence:random_seed=1967651429:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 6.65/2.71 % (2232590)Instruction limit reached!
% 6.65/2.71 % (2232590)------------------------------
% 6.65/2.71 % (2232590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232590)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232590)Termination reason: Instruction limit
% 6.65/2.71 % (2232590)Termination phase: Saturation
% 6.65/2.71 % (2232590)Time elapsed: 0.059 s
% 6.65/2.71 % (2232590)Peak memory usage: 89 MB
% 6.65/2.71 % (2232590)Instructions burned: 115 (million)
% 6.65/2.71 % (2232594)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2879666189:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 6.65/2.71 % (2232594)Refutation not found, incomplete strategy
% 6.65/2.71 % (2232594)------------------------------
% 6.65/2.71 % (2232594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232594)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232594)Termination reason: Refutation not found, incomplete strategy
% 6.65/2.71 % (2232594)Time elapsed: 0.006 s
% 6.65/2.71 % (2232594)Peak memory usage: 88 MB
% 6.65/2.71 % (2232594)Instructions burned: 9 (million)
% 6.65/2.71 % (2232597)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=344657297:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 6.65/2.71 % (2232593)Instruction limit reached!
% 6.65/2.71 % (2232593)------------------------------
% 6.65/2.71 % (2232593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232593)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232593)Termination reason: Instruction limit
% 6.65/2.71 % (2232593)Termination phase: Saturation
% 6.65/2.71 % (2232593)Time elapsed: 0.276 s
% 6.65/2.71 % (2232593)Peak memory usage: 100 MB
% 6.65/2.71 % (2232593)Instructions burned: 910 (million)
% 6.65/2.71 % (2232594)------------------------------
% 6.65/2.71 % (2232594)------------------------------
% 6.65/2.71 % (2232600)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3176898057:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 6.65/2.71 % (2232600)Instruction limit reached!
% 6.65/2.71 % (2232600)------------------------------
% 6.65/2.71 % (2232600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232600)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232600)Termination reason: Instruction limit
% 6.65/2.71 % (2232600)Termination phase: Saturation
% 6.65/2.71 % (2232600)Time elapsed: 0.040 s
% 6.65/2.71 % (2232600)Peak memory usage: 90 MB
% 6.65/2.71 % (2232600)Instructions burned: 137 (million)
% 6.65/2.71 % (2232601)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1989352292:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 6.65/2.71 % (2232603)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3139393467:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 6.65/2.71 % (2232601)Instruction limit reached!
% 6.65/2.71 % (2232601)------------------------------
% 6.65/2.71 % (2232601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232601)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232601)Termination reason: Instruction limit
% 6.65/2.71 % (2232601)Termination phase: Saturation
% 6.65/2.71 % (2232601)Time elapsed: 0.206 s
% 6.65/2.71 % (2232601)Peak memory usage: 88 MB
% 6.65/2.71 % (2232601)Instructions burned: 594 (million)
% 6.65/2.71 % (2232606)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2719274452:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 6.65/2.71 % (2232584)First to succeed.
% 6.65/2.71 % (2232584)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2232557"
% 6.65/2.71 % (2232606)Instruction limit reached!
% 6.65/2.71 % (2232606)------------------------------
% 6.65/2.71 % (2232606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.65/2.71 % (2232606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.65/2.71 % (2232606)CaDiCaL version: 2.1.3
% 6.65/2.71 % (2232606)Termination reason: Instruction limit
% 6.65/2.71 % (2232606)Termination phase: Saturation
% 6.65/2.71 % (2232606)Time elapsed: 0.081 s
% 6.65/2.71 % (2232606)Peak memory usage: 90 MB
% 6.65/2.71 % (2232606)Instructions burned: 126 (million)
% 6.65/2.71 % (2232608)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2067000006:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 6.65/2.71 % (2232584)Refutation found. Thanks to Tanya!
% 6.65/2.71 % SZS status Theorem for theBenchmark
% 6.65/2.71 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/2.90 % (2232584)------------------------------
% 0.18/2.90 % (2232584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/2.90 % (2232584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/2.90 % (2232584)CaDiCaL version: 2.1.3
% 0.18/2.90 % (2232584)Termination reason: Refutation
% 0.18/2.90 % (2232584)Time elapsed: 1.185 s
% 0.18/2.90 % (2232584)Peak memory usage: 137 MB
% 0.18/2.90 % (2232584)Instructions burned: 1793 (million)
% 0.18/2.90 % (2232584)------------------------------
% 0.18/2.90 % (2232584)------------------------------
% 0.18/2.90 % (2232557)Success in time 2.111 s
% 0.18/2.90 % Vampire exiting
%------------------------------------------------------------------------------