%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP003_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 : n003.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:27:42 AM UTC 2026
% Result : Theorem 24.32s 5.60s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 40
% Syntax : Number of formulae : 219 ( 108 unt; 0 typ; 4 def)
% Number of atoms : 1240 ( 170 equ)
% Maximal formula atoms : 7 ( 5 avg)
% Number of connectives : 372 ( 179 ~; 163 |; 12 &)
% ( 9 <=>; 7 =>; 0 <=; 2 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of FOOLs : 828 ( 828 fml; 0 var)
% Number of types : 5 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 35 ( 33 usr; 18 prp; 0-3 aty)
% Number of functors : 57 ( 57 usr; 8 con; 0-3 aty)
% Number of variables : 209 ( 0 sgn 201 !; 8 ?; 209 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
del: $tType ).
tff(type_def_6,type,
tp__ty_2Enum_2Enum: $tType ).
tff(type_def_7,type,
tp__o: $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,
ty_2Enum_2Enum: del ).
tff(func_def_7,type,
inj__ty_2Enum_2Enum: tp__ty_2Enum_2Enum > $i ).
tff(func_def_8,type,
surj__ty_2Enum_2Enum: $i > tp__ty_2Enum_2Enum ).
tff(func_def_10,type,
fo__c_2Earithmetic_2EBIT1: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
tff(func_def_11,type,
inj__o: tp__o > $i ).
tff(func_def_12,type,
surj__o: $i > tp__o ).
tff(func_def_14,type,
fo__c_2Earithmetic_2EEVEN: tp__ty_2Enum_2Enum > tp__o ).
tff(func_def_16,type,
fo__c_2Earithmetic_2EZERO: tp__ty_2Enum_2Enum ).
tff(func_def_18,type,
fo__c_2Earithmetic_2EBIT2: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
tff(func_def_20,type,
fo__c_2Earithmetic_2ENUMERAL: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
tff(func_def_22,type,
fo__c_2Earithmetic_2EODD: tp__ty_2Enum_2Enum > tp__o ).
tff(func_def_24,type,
fo__c_2Earithmetic_2EMOD: ( tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum ) > tp__ty_2Enum_2Enum ).
tff(func_def_26,type,
fo__c_2Earithmetic_2E_2A: ( tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum ) > tp__ty_2Enum_2Enum ).
tff(func_def_28,type,
fo__c_2Earithmetic_2E_2B: ( tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum ) > tp__ty_2Enum_2Enum ).
tff(func_def_30,type,
fo__c_2Ebool_2ET: tp__o ).
tff(func_def_31,type,
c_2Ebool_2ECOND: del > $i ).
tff(func_def_32,type,
c_2Ebool_2E_3F: del > $i ).
tff(func_def_34,type,
fo__c_2Enum_2ESUC: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
tff(func_def_36,type,
fo__c_2Enum_2E0: tp__ty_2Enum_2Enum ).
tff(func_def_38,type,
fo__c_2Eprim__rec_2E_3C: ( tp__ty_2Enum_2Enum * tp__ty_2Enum_2Enum ) > tp__o ).
tff(func_def_40,type,
fo__c_2Ebool_2EF: tp__o ).
tff(func_def_42,type,
fo__c_2Ebool_2E_2F_5C: ( tp__o * tp__o ) > tp__o ).
tff(func_def_43,type,
c_2Emin_2E_3D: del > $i ).
tff(func_def_45,type,
fo__c_2Ebool_2E_5C_2F: ( tp__o * tp__o ) > tp__o ).
tff(func_def_47,type,
fo__c_2Ebool_2E_7E: tp__o > tp__o ).
tff(func_def_49,type,
fo__c_2Emin_2E_3D_3D_3E: ( tp__o * tp__o ) > tp__o ).
tff(func_def_50,type,
c_2Ebool_2E_21: del > $i ).
tff(func_def_51,type,
sK13: tp__ty_2Enum_2Enum ).
tff(func_def_52,type,
sK14: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
tff(func_def_53,type,
sK15: tp__ty_2Enum_2Enum > tp__ty_2Enum_2Enum ).
tff(func_def_54,type,
sK16: ( del * $i * $i ) > $i ).
tff(func_def_55,type,
sK17: ( del * $i * $i ) > $i ).
tff(func_def_56,type,
sK18: ( del * del * $i ) > $i ).
tff(func_def_57,type,
sK19: ( del * del * $i ) > $i ).
tff(func_def_58,type,
sK20: ( del * $i ) > $i ).
tff(func_def_59,type,
sK21: ( del * tp__o * $i ) > $i ).
tff(func_def_60,type,
sK22: ( del * tp__o * $i ) > $i ).
tff(func_def_61,type,
sK23: ( del * $i ) > $i ).
tff(func_def_62,type,
sK24: ( del * $i * tp__o ) > $i ).
tff(func_def_63,type,
sK25: ( del * $i ) > $i ).
tff(func_def_64,type,
sK26: ( del * $i ) > $i ).
tff(func_def_65,type,
sK27: ( del * tp__o * $i ) > $i ).
tff(func_def_66,type,
sK28: ( del * $i ) > $i ).
tff(func_def_67,type,
sK29: ( del * $i * tp__o ) > $i ).
tff(func_def_68,type,
sK30: ( $i * $i * del ) > $i ).
tff(func_def_69,type,
sK31: ( del * $i ) > $i ).
tff(func_def_70,type,
sK32: ( del * $i ) > $i ).
tff(func_def_71,type,
sK33: ( del * $i * tp__o ) > $i ).
tff(func_def_72,type,
sK34: ( del * $i ) > $i ).
tff(func_def_73,type,
sK35: ( del * $i ) > $i ).
tff(func_def_74,type,
sK36: ( del * $i ) > $i ).
tff(func_def_75,type,
sK37: ( del * $i * $i ) > $i ).
tff(pred_def_1,type,
mem: ( $i * del ) > $o ).
tff(pred_def_3,type,
sP0: ( del * $i * $i ) > $o ).
tff(pred_def_4,type,
sP1: ( $i * $i * del ) > $o ).
tff(pred_def_5,type,
sP2: ( 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(pred_def_14,type,
sP11: ( tp__o * tp__o * tp__o ) > $o ).
tff(pred_def_15,type,
sP12: ( tp__o * tp__o * tp__o ) > $o ).
tff(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(f6,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_surj_ty_2Enum_2Enum) ).
tff(f7,axiom,
! [X0: tp__ty_2Enum_2Enum] : mem(inj__ty_2Enum_2Enum(X0),ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_mem_ty_2Enum_2Enum) ).
tff(f8,axiom,
! [X0: $i] :
( mem(X0,ty_2Enum_2Enum)
=> ( X0 = inj__ty_2Enum_2Enum(surj__ty_2Enum_2Enum(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_iso_mem_ty_2Enum_2Enum) ).
tff(f10,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(X0)) = ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2EBIT1) ).
tff(f12,axiom,
! [X0: tp__o] : mem(inj__o(X0),bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_inj_mem_o) ).
tff(f15,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( inj__o(fo__c_2Earithmetic_2EEVEN(X0)) = ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2EEVEN) ).
tff(f19,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(X0)) = ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2EBIT2) ).
tff(f21,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(X0)) = ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2ENUMERAL) ).
tff(f23,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( inj__o(fo__c_2Earithmetic_2EODD(X0)) = ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2EODD) ).
tff(f25,axiom,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EMOD(X0,X1)) = ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2EMOD) ).
tff(f27,axiom,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X0,X1)) = ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2E_2A) ).
tff(f29,axiom,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,X1)) = ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Earithmetic_2E_2B) ).
tff(f30,axiom,
mem(c_2Ebool_2ET,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2ET) ).
tff(f31,axiom,
inj__o(fo__c_2Ebool_2ET) = c_2Ebool_2ET,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Ebool_2ET) ).
tff(f32,axiom,
p(c_2Ebool_2ET),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_true_p) ).
tff(f37,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0)) = ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Enum_2ESUC) ).
tff(f38,axiom,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Enum_2E0) ).
tff(f39,axiom,
inj__ty_2Enum_2Enum(fo__c_2Enum_2E0) = c_2Enum_2E0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Enum_2E0) ).
tff(f41,axiom,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__o(fo__c_2Eprim__rec_2E_3C(X0,X1)) = ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Eprim__rec_2E_3C) ).
tff(f42,axiom,
mem(c_2Ebool_2EF,bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_c_2Ebool_2EF) ).
tff(f43,axiom,
inj__o(fo__c_2Ebool_2EF) = c_2Ebool_2EF,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stp_eq_fo_c_2Ebool_2EF) ).
tff(f44,axiom,
~ p(c_2Ebool_2EF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_false_p) ).
tff(f61,axiom,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EONE) ).
tff(f62,axiom,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2ETWO) ).
tff(f63,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EADD__0) ).
tff(f64,axiom,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X1))))
<=> p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2ELESS__MONO__EQ) ).
tff(f65,axiom,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EADD1) ).
tff(f66,axiom,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EMULT__COMM) ).
tff(f67,axiom,
! [X0: tp__ty_2Enum_2Enum] :
( p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)))
<=> ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EEVEN__ODD) ).
tff(f69,axiom,
! [X0: tp__ty_2Enum_2Enum] :
( p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)))
<=> ? [X1: tp__ty_2Enum_2Enum] : ( X0 = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EEVEN__EXISTS) ).
tff(f70,axiom,
! [X0: tp__ty_2Enum_2Enum] :
( p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0)))
<=> ? [X1: tp__ty_2Enum_2Enum] : ( X0 = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EODD__EXISTS) ).
tff(f71,axiom,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum,X2: tp__ty_2Enum_2Enum] :
( ? [X3: tp__ty_2Enum_2Enum] :
( ( X1 = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X3)),inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(X2))) )
& p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) )
=> ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X0))) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EMOD__UNIQUE) ).
tff(f86,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(f102,axiom,
! [X0: tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Eprim__rec_2ELESS__0) ).
tff(f118,conjecture,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_thm_2Earithmetic_2EMOD__2) ).
tff(f119,negated_conjecture,
~ ! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) = surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) ),
inference(negated_conjecture,[status(cth)],[f118]) ).
tff(f143,plain,
? [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) ),
inference(ennf_transformation,[],[f119]) ).
tff(f146,plain,
! [X0: $i] :
( ( X0 = inj__ty_2Enum_2Enum(surj__ty_2Enum_2Enum(X0)) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(ennf_transformation,[],[f8]) ).
tff(f147,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum,X2: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X0))) = X2 )
| ! [X3: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X3)),inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(X2))) != X1 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ) ),
inference(ennf_transformation,[],[f71]) ).
tff(f150,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,[],[f86]) ).
tff(f161,plain,
! [X0: $i] :
( ! [X1: $i] :
( ( X0 = X1 )
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(ennf_transformation,[],[f2]) ).
tff(f162,plain,
! [X0: $i] :
( ! [X1: $i] :
( ( X0 = X1 )
| ( p(X0)
<~> p(X1) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(flattening,[],[f161]) ).
tff(f205,plain,
surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(sK13))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X0,sK13)],[f143]) ).
tff(f207,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0)))
| ! [X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1)))) != X0 ) )
& ( ? [X1: tp__ty_2Enum_2Enum] : ( X0 = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1)))) )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ) ),
inference(nnf_transformation,[],[f70]) ).
tff(f208,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0)))
| ! [X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1)))) != X0 ) )
& ( ? [X2: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X2)))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ) ),
inference(rectify,[],[f207]) ).
tff(f209,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0)))
| ! [X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1)))) != X0 ) )
& ( ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK14(X0))))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0))],[f208]) ).
tff(f210,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)))
| ! [X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1))) != X0 ) )
& ( ? [X1: tp__ty_2Enum_2Enum] : ( X0 = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1))) )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ) ),
inference(nnf_transformation,[],[f69]) ).
tff(f211,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)))
| ! [X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1))) != X0 ) )
& ( ? [X2: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X2))) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ) ),
inference(rectify,[],[f210]) ).
tff(f212,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)))
| ! [X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(X1))) != X0 ) )
& ( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK15(X0)))) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X2,sK15(X0))],[f211]) ).
tff(f214,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)))
| p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) )
& ( ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0)))
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ) ),
inference(nnf_transformation,[],[f67]) ).
tff(f254,plain,
! [X0: $i] :
( ! [X1: $i] :
( ( X0 = X1 )
| ( ( ~ p(X1)
| ~ p(X0) )
& ( p(X1)
| p(X0) ) )
| ~ mem(X1,bool) )
| ~ mem(X0,bool) ),
inference(nnf_transformation,[],[f162]) ).
tff(f256,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( ( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) )
& ( p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X1)))) ) ),
inference(nnf_transformation,[],[f64]) ).
tff(f315,plain,
surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(sK13))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),
inference(cnf_transformation,[],[f205]) ).
tff(f320,plain,
mem(c_2Enum_2E0,ty_2Enum_2Enum),
inference(cnf_transformation,[],[f38]) ).
tff(f331,plain,
! [X0: $i] :
( ( inj__ty_2Enum_2Enum(surj__ty_2Enum_2Enum(X0)) = X0 )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(cnf_transformation,[],[f146]) ).
tff(f332,plain,
! [X0: tp__ty_2Enum_2Enum] : mem(inj__ty_2Enum_2Enum(X0),ty_2Enum_2Enum),
inference(cnf_transformation,[],[f7]) ).
tff(f333,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X0))) = X2 )
| ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X3)),inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(X2))) != X1 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ),
inference(cnf_transformation,[],[f147]) ).
tff(f334,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK14(X0))))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(cnf_transformation,[],[f209]) ).
tff(f336,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK15(X0)))) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ),
inference(cnf_transformation,[],[f212]) ).
tff(f338,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X1)),inj__ty_2Enum_2Enum(X0))) ),
inference(cnf_transformation,[],[f66]) ).
tff(f339,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) ),
inference(cnf_transformation,[],[f65]) ).
tff(f340,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))) = X0 ),
inference(cnf_transformation,[],[f63]) ).
tff(f341,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))),
inference(cnf_transformation,[],[f62]) ).
tff(f342,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0))),
inference(cnf_transformation,[],[f61]) ).
tff(f343,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(X0)) = X0 ),
inference(cnf_transformation,[],[f6]) ).
tff(f344,plain,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(X0)) = ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(X0)) ),
inference(cnf_transformation,[],[f10]) ).
tff(f348,plain,
! [X0: tp__ty_2Enum_2Enum] :
( p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)))
| p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(cnf_transformation,[],[f214]) ).
tff(f349,plain,
! [X0: tp__ty_2Enum_2Enum] : ( inj__o(fo__c_2Earithmetic_2EEVEN(X0)) = ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0)) ),
inference(cnf_transformation,[],[f15]) ).
tff(f351,plain,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(X0)) = ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(X0)) ),
inference(cnf_transformation,[],[f19]) ).
tff(f352,plain,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(X0)) = ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(X0)) ),
inference(cnf_transformation,[],[f21]) ).
tff(f353,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EMOD(X0,X1)) = ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
inference(cnf_transformation,[],[f25]) ).
tff(f362,plain,
! [X2: $i,X0: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2EF)),X1),X2) = X2 )
| ~ mem(X2,X0)
| ~ mem(X1,X0) ),
inference(cnf_transformation,[],[f150]) ).
tff(f363,plain,
! [X2: $i,X0: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0),inj__o(fo__c_2Ebool_2ET)),X1),X2) = X1 )
| ~ mem(X2,X0)
| ~ mem(X1,X0) ),
inference(cnf_transformation,[],[f150]) ).
tff(f365,plain,
! [X0: tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0)))),
inference(cnf_transformation,[],[f102]) ).
tff(f366,plain,
c_2Enum_2E0 = inj__ty_2Enum_2Enum(fo__c_2Enum_2E0),
inference(cnf_transformation,[],[f39]) ).
tff(f432,plain,
! [X0: tp__o] : mem(inj__o(X0),bool),
inference(cnf_transformation,[],[f12]) ).
tff(f433,plain,
! [X0: $i,X1: $i] :
( ~ mem(X1,bool)
| p(X1)
| p(X0)
| ( X0 = X1 )
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f254]) ).
tff(f434,plain,
! [X0: $i,X1: $i] :
( ~ mem(X1,bool)
| ~ p(X1)
| ~ p(X0)
| ( X0 = X1 )
| ~ mem(X0,bool) ),
inference(cnf_transformation,[],[f254]) ).
tff(f439,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))),ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) ),
inference(cnf_transformation,[],[f256]) ).
tff(f440,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__o(fo__c_2Eprim__rec_2E_3C(X0,X1)) = ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
inference(cnf_transformation,[],[f41]) ).
tff(f441,plain,
! [X0: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0)) = ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0)) ),
inference(cnf_transformation,[],[f37]) ).
tff(f442,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,X1)) = ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
inference(cnf_transformation,[],[f29]) ).
tff(f443,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X0,X1)) = ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1)) ),
inference(cnf_transformation,[],[f27]) ).
tff(f444,plain,
! [X0: tp__ty_2Enum_2Enum] : ( inj__o(fo__c_2Earithmetic_2EODD(X0)) = ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0)) ),
inference(cnf_transformation,[],[f23]) ).
tff(f609,plain,
c_2Ebool_2ET = inj__o(fo__c_2Ebool_2ET),
inference(cnf_transformation,[],[f31]) ).
tff(f610,plain,
c_2Ebool_2EF = inj__o(fo__c_2Ebool_2EF),
inference(cnf_transformation,[],[f43]) ).
tff(f611,plain,
p(c_2Ebool_2ET),
inference(cnf_transformation,[],[f32]) ).
tff(f612,plain,
mem(c_2Ebool_2ET,bool),
inference(cnf_transformation,[],[f30]) ).
tff(f613,plain,
~ p(c_2Ebool_2EF),
inference(cnf_transformation,[],[f44]) ).
tff(f614,plain,
mem(c_2Ebool_2EF,bool),
inference(cnf_transformation,[],[f42]) ).
tff(f617,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X3)),inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(X2))))),inj__ty_2Enum_2Enum(X0))) = X2 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ),
inference(equality_resolution,[],[f333]) ).
tff(f642,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( p(ap(ap(c_2Eprim__rec_2E_3C,ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) ),
inference(forward_demodulation,[],[f439,f441]) ).
tff(f697,plain,
! [X0: tp__ty_2Enum_2Enum] : p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0)))),
inference(forward_demodulation,[],[f365,f441]) ).
tff(f698,plain,
! [X2: $i,X0: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2EF),X1),X2) = X2 )
| ~ mem(X2,X0)
| ~ mem(X1,X0) ),
inference(forward_demodulation,[],[f362,f610]) ).
tff(f699,plain,
! [X2: $i,X0: del,X1: $i] :
( ( ap(ap(ap(c_2Ebool_2ECOND(X0),c_2Ebool_2ET),X1),X2) = X1 )
| ~ mem(X2,X0)
| ~ mem(X1,X0) ),
inference(forward_demodulation,[],[f363,f609]) ).
tff(f701,plain,
! [X0: tp__ty_2Enum_2Enum] :
( p(inj__o(fo__c_2Earithmetic_2EEVEN(X0)))
| p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f348,f349]) ).
tff(f704,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0))),
inference(forward_demodulation,[],[f342,f441]) ).
tff(f705,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f341,f344]) ).
tff(f706,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,fo__c_2Enum_2E0))) = X0 ),
inference(forward_demodulation,[],[f340,f442]) ).
tff(f707,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))) ),
inference(forward_demodulation,[],[f339,f344]) ).
tff(f708,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X1,X0))) ),
inference(forward_demodulation,[],[f338,f443]) ).
tff(f709,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK15(X0)))) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f336,f351]) ).
tff(f711,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK14(X0))))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f334,f351]) ).
tff(f713,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EMOD(surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X3)),inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(X2))),X0))) = X2 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f617,f353]) ).
tff(f714,plain,
surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(sK13))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f315,f344]) ).
tff(f716,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0))),inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) ),
inference(forward_demodulation,[],[f642,f441]) ).
tff(f717,plain,
! [X0: tp__ty_2Enum_2Enum] : p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2E0,fo__c_2Enum_2ESUC(X0)))),
inference(forward_demodulation,[],[f697,f440]) ).
tff(f719,plain,
! [X0: tp__ty_2Enum_2Enum] :
( p(inj__o(fo__c_2Earithmetic_2EODD(X0)))
| p(inj__o(fo__c_2Earithmetic_2EEVEN(X0))) ),
inference(forward_demodulation,[],[f701,f444]) ).
tff(f722,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT1,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = fo__c_2Enum_2ESUC(fo__c_2Enum_2E0),
inference(forward_demodulation,[],[f704,f343]) ).
tff(f723,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f705,f352]) ).
tff(f724,plain,
! [X0: tp__ty_2Enum_2Enum] : ( fo__c_2Earithmetic_2E_2B(X0,fo__c_2Enum_2E0) = X0 ),
inference(forward_demodulation,[],[f706,f343]) ).
tff(f725,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))) = surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))) ),
inference(forward_demodulation,[],[f707,f352]) ).
tff(f726,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) = fo__c_2Earithmetic_2E_2A(X1,X0) ),
inference(forward_demodulation,[],[f708,f343]) ).
tff(f727,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK15(X0)))) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f709,f352]) ).
tff(f729,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))),inj__ty_2Enum_2Enum(sK14(X0))))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f711,f352]) ).
tff(f731,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2EMOD(surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,ap(ap(c_2Earithmetic_2E_2A,inj__ty_2Enum_2Enum(X3)),inj__ty_2Enum_2Enum(X0))),inj__ty_2Enum_2Enum(X2))),X0) = X2 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f713,f343]) ).
tff(f732,plain,
surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(sK13))),inj__ty_2Enum_2Enum(fo__c_2Enum_2E0)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f714,f352]) ).
tff(f734,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2ESUC(X0),fo__c_2Enum_2ESUC(X1))))
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X0)),inj__ty_2Enum_2Enum(X1))) ),
inference(forward_demodulation,[],[f716,f440]) ).
tff(f735,plain,
fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO)))),
inference(forward_demodulation,[],[f722,f344]) ).
tff(f736,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f723,f441]) ).
tff(f737,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))) ),
inference(forward_demodulation,[],[f725,f442]) ).
tff(f738,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( fo__c_2Earithmetic_2E_2A(X1,X0) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X0,X1))) ),
inference(forward_demodulation,[],[f726,f443]) ).
tff(f739,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)),sK15(X0)))) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f727,f443]) ).
tff(f741,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)),sK14(X0))))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f729,f443]) ).
tff(f743,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2EMOD(surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2E_2B,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2A(X3,X0))),inj__ty_2Enum_2Enum(X2))),X0) = X2 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f731,f443]) ).
tff(f744,plain,
surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(sK13))),c_2Enum_2E0),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f732,f366]) ).
tff(f746,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2ESUC(X0),fo__c_2Enum_2ESUC(X1))))
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(X0,X1))) ),
inference(forward_demodulation,[],[f734,f440]) ).
tff(f747,plain,
fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO)))),
inference(forward_demodulation,[],[f735,f352]) ).
tff(f748,plain,
surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO)))) = fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))),
inference(forward_demodulation,[],[f736,f343]) ).
tff(f749,plain,
! [X0: tp__ty_2Enum_2Enum] : ( surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,inj__ty_2Enum_2Enum(X0))) = fo__c_2Earithmetic_2E_2B(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))) ),
inference(forward_demodulation,[],[f737,f343]) ).
tff(f750,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] : ( fo__c_2Earithmetic_2E_2A(X0,X1) = fo__c_2Earithmetic_2E_2A(X1,X0) ),
inference(forward_demodulation,[],[f738,f343]) ).
tff(f751,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2E_2A(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)),sK15(X0)) = X0 )
| ~ p(ap(c_2Earithmetic_2EEVEN,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f739,f343]) ).
tff(f753,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2E_2A(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)),sK14(X0))))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f741,f441]) ).
tff(f755,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2EMOD(surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2E_2B(fo__c_2Earithmetic_2E_2A(X3,X0),X2))),X0) = X2 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f743,f442]) ).
tff(f756,plain,
surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),ap(c_2Earithmetic_2ENUMERAL,ap(c_2Earithmetic_2EBIT2,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(fo__c_2Earithmetic_2EEVEN(sK13))),c_2Enum_2E0),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f744,f349]) ).
tff(f757,plain,
fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO)),
inference(forward_demodulation,[],[f747,f343]) ).
tff(f758,plain,
fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))) = surj__ty_2Enum_2Enum(ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))),
inference(forward_demodulation,[],[f748,f351]) ).
tff(f759,plain,
! [X0: tp__ty_2Enum_2Enum] : ( fo__c_2Earithmetic_2E_2B(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(X0))) ),
inference(forward_demodulation,[],[f749,f441]) ).
tff(f760,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2E_2A(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)),sK15(X0)) = X0 )
| ~ p(inj__o(fo__c_2Earithmetic_2EEVEN(X0))) ),
inference(forward_demodulation,[],[f751,f349]) ).
tff(f762,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2E_2A(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)),sK14(X0))) = X0 )
| ~ p(ap(c_2Earithmetic_2EODD,inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f753,f343]) ).
tff(f764,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2EMOD(fo__c_2Earithmetic_2E_2B(fo__c_2Earithmetic_2E_2A(X3,X0),X2),X0) = X2 )
| ~ p(ap(ap(c_2Eprim__rec_2E_3C,inj__ty_2Enum_2Enum(X2)),inj__ty_2Enum_2Enum(X0))) ),
inference(forward_demodulation,[],[f755,f343]) ).
tff(f765,plain,
surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(fo__c_2Earithmetic_2EEVEN(sK13))),c_2Enum_2E0),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),ap(c_2Earithmetic_2ENUMERAL,inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f756,f351]) ).
tff(f766,plain,
fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))) = surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))),
inference(forward_demodulation,[],[f758,f352]) ).
tff(f767,plain,
! [X0: tp__ty_2Enum_2Enum] : ( fo__c_2Enum_2ESUC(X0) = fo__c_2Earithmetic_2E_2B(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))) ),
inference(forward_demodulation,[],[f759,f343]) ).
tff(f768,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2E_2A(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)),sK14(X0))) = X0 )
| ~ p(inj__o(fo__c_2Earithmetic_2EODD(X0))) ),
inference(forward_demodulation,[],[f762,f444]) ).
tff(f770,plain,
! [X2: tp__ty_2Enum_2Enum,X3: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2EMOD(fo__c_2Earithmetic_2E_2B(fo__c_2Earithmetic_2E_2A(X3,X0),X2),X0) = X2 )
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(X2,X0))) ),
inference(forward_demodulation,[],[f764,f440]) ).
tff(f771,plain,
surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(fo__c_2Earithmetic_2EEVEN(sK13))),c_2Enum_2E0),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(ap(ap(c_2Earithmetic_2EMOD,inj__ty_2Enum_2Enum(sK13)),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f765,f352]) ).
tff(f772,plain,
fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)) = fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))),
inference(forward_demodulation,[],[f766,f343]) ).
tff(f773,plain,
! [X0: tp__ty_2Enum_2Enum] : ( fo__c_2Enum_2ESUC(X0) = fo__c_2Earithmetic_2E_2B(X0,fo__c_2Enum_2ESUC(fo__c_2Enum_2E0)) ),
inference(forward_demodulation,[],[f767,f757]) ).
tff(f774,plain,
surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(fo__c_2Earithmetic_2EEVEN(sK13))),c_2Enum_2E0),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))) != surj__ty_2Enum_2Enum(inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))))),
inference(forward_demodulation,[],[f771,f353]) ).
tff(f775,plain,
fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)) = fo__c_2Enum_2ESUC(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0)),
inference(forward_demodulation,[],[f772,f757]) ).
tff(f776,plain,
surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(fo__c_2Earithmetic_2EEVEN(sK13))),c_2Enum_2E0),inj__ty_2Enum_2Enum(fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT1(fo__c_2Earithmetic_2EZERO))))) != fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))),
inference(forward_demodulation,[],[f774,f343]) ).
tff(f777,plain,
fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(fo__c_2Earithmetic_2EEVEN(sK13))),c_2Enum_2E0),inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0)))),
inference(forward_demodulation,[],[f776,f757]) ).
tff(f827,plain,
fo__c_2Enum_2E0 = surj__ty_2Enum_2Enum(c_2Enum_2E0),
inference(superposition,[],[f343,f366]) ).
tff(f862,plain,
! [X0: tp__o,X1: $i] :
( ( inj__o(X0) = X1 )
| ~ p(X1)
| ~ p(inj__o(X0))
| ~ mem(X1,bool) ),
inference(resolution,[],[f434,f432]) ).
tff(f873,plain,
p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2E0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))))),
inference(superposition,[],[f717,f775]) ).
tff(f879,plain,
! [X2: tp__ty_2Enum_2Enum,X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( ( fo__c_2Earithmetic_2EMOD(fo__c_2Earithmetic_2E_2B(fo__c_2Earithmetic_2E_2A(X0,X1),X2),X0) = X2 )
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(X2,X0))) ),
inference(superposition,[],[f770,f750]) ).
tff(f880,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2E0 = fo__c_2Earithmetic_2EMOD(fo__c_2Earithmetic_2E_2A(X0,X1),X1) )
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2E0,X1))) ),
inference(superposition,[],[f770,f724]) ).
tff(f980,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2E0 = fo__c_2Earithmetic_2EMOD(fo__c_2Earithmetic_2E_2A(X0,X1),X0) )
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2E0,X0))) ),
inference(superposition,[],[f880,f750]) ).
tff(f992,plain,
! [X0: tp__ty_2Enum_2Enum,X1: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = fo__c_2Earithmetic_2EMOD(fo__c_2Enum_2ESUC(fo__c_2Earithmetic_2E_2A(X0,X1)),X0) )
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0),X0))) ),
inference(superposition,[],[f879,f773]) ).
tff(f995,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = fo__c_2Earithmetic_2EMOD(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) )
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0),fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))))
| ~ p(inj__o(fo__c_2Earithmetic_2EODD(X0))) ),
inference(superposition,[],[f992,f768]) ).
tff(f998,definition,
( spl38_15
<=> p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0),fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))))) ),
introduced(definition,[new_symbols(definition,[spl38_15])],[avatar_definition]) ).
tff(f1000,plain,
( ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0),fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))))
| spl38_15 ),
inference(avatar_component_clause,[],[f998]) ).
tff(f1002,definition,
( spl38_16
<=> ! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = fo__c_2Earithmetic_2EMOD(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) )
| ~ p(inj__o(fo__c_2Earithmetic_2EODD(X0))) ) ),
introduced(definition,[new_symbols(definition,[spl38_16])],[avatar_definition]) ).
tff(f1003,plain,
( ! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = fo__c_2Earithmetic_2EMOD(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) )
| ~ p(inj__o(fo__c_2Earithmetic_2EODD(X0))) )
| ~ spl38_16 ),
inference(avatar_component_clause,[],[f1002]) ).
tff(f1004,plain,
( ~ spl38_15
| spl38_16 ),
inference(avatar_split_clause,[],[f995,f1002,f998]) ).
tff(f1106,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2E0 = fo__c_2Earithmetic_2EMOD(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) )
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2E0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))))
| ~ p(inj__o(fo__c_2Earithmetic_2EEVEN(X0))) ),
inference(superposition,[],[f980,f760]) ).
tff(f1108,plain,
! [X0: tp__ty_2Enum_2Enum] :
( ( fo__c_2Enum_2E0 = fo__c_2Earithmetic_2EMOD(X0,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) )
| ~ p(inj__o(fo__c_2Earithmetic_2EEVEN(X0))) ),
inference(forward_subsumption_resolution,[],[f1106,f873]) ).
tff(f1182,plain,
! [X0: $i] :
( ( inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(surj__ty_2Enum_2Enum(X0))) = ap(c_2Enum_2ESUC,X0) )
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(superposition,[],[f441,f331]) ).
tff(f1187,plain,
inj__ty_2Enum_2Enum(fo__c_2Enum_2ESUC(fo__c_2Enum_2E0)) = ap(c_2Enum_2ESUC,c_2Enum_2E0),
inference(superposition,[],[f441,f366]) ).
tff(f1193,plain,
fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),inj__o(fo__c_2Earithmetic_2EEVEN(sK13))),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))),
inference(superposition,[],[f777,f1187]) ).
tff(f1195,plain,
fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) = surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,c_2Enum_2E0)),
inference(superposition,[],[f343,f1187]) ).
tff(f1532,plain,
! [X0: tp__ty_2Enum_2Enum] :
( p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2ESUC(X0),fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO)))))
| ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(X0,fo__c_2Enum_2ESUC(fo__c_2Enum_2E0)))) ),
inference(superposition,[],[f746,f775]) ).
tff(f1899,plain,
( ~ p(inj__o(fo__c_2Eprim__rec_2E_3C(fo__c_2Enum_2E0,fo__c_2Enum_2ESUC(fo__c_2Enum_2E0))))
| spl38_15 ),
inference(resolution,[],[f1532,f1000]) ).
tff(f1912,plain,
( $false
| spl38_15 ),
inference(forward_subsumption_resolution,[],[f1899,f717]) ).
tff(f1913,plain,
spl38_15,
inference(avatar_contradiction_clause,[],[f1912]) ).
tff(f3620,plain,
! [X0: $i] :
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),X0),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))) )
| ~ p(X0)
| ~ p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13)))
| ~ mem(X0,bool) ),
inference(superposition,[],[f1193,f862]) ).
tff(f3679,definition,
( spl38_25
<=> p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13))) ),
introduced(definition,[new_symbols(definition,[spl38_25])],[avatar_definition]) ).
tff(f3680,plain,
( p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13)))
| ~ spl38_25 ),
inference(avatar_component_clause,[],[f3679]) ).
tff(f3681,plain,
( ~ p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13)))
| spl38_25 ),
inference(avatar_component_clause,[],[f3679]) ).
tff(f3683,definition,
( spl38_26
<=> ! [X0: $i] :
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),X0),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))) )
| ~ mem(X0,bool)
| ~ p(X0) ) ),
introduced(definition,[new_symbols(definition,[spl38_26])],[avatar_definition]) ).
tff(f3684,plain,
( ! [X0: $i] :
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),X0),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))) )
| ~ mem(X0,bool)
| ~ p(X0) )
| ~ spl38_26 ),
inference(avatar_component_clause,[],[f3683]) ).
tff(f3685,plain,
( ~ spl38_25
| spl38_26 ),
inference(avatar_split_clause,[],[f3620,f3683,f3679]) ).
tff(f7331,plain,
! [X0: $i] :
( mem(ap(c_2Enum_2ESUC,X0),ty_2Enum_2Enum)
| ~ mem(X0,ty_2Enum_2Enum) ),
inference(superposition,[],[f332,f1182]) ).
tff(f8471,plain,
! [X0: $i] :
( p(c_2Ebool_2EF)
| p(X0)
| ( c_2Ebool_2EF = X0 )
| ~ mem(X0,bool) ),
inference(resolution,[],[f433,f614]) ).
tff(f8488,plain,
! [X0: $i] :
( ~ mem(X0,bool)
| ( c_2Ebool_2EF = X0 )
| p(X0) ),
inference(forward_subsumption_resolution,[],[f8471,f613]) ).
tff(f8492,plain,
! [X0: tp__o] :
( ( inj__o(X0) = c_2Ebool_2EF )
| p(inj__o(X0)) ),
inference(resolution,[],[f8488,f432]) ).
tff(f8587,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),c_2Ebool_2EF),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))) )
| p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13))) ),
inference(superposition,[],[f1193,f8492]) ).
tff(f9355,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(c_2Enum_2E0) )
| ~ mem(c_2Ebool_2ET,bool)
| ~ p(c_2Ebool_2ET)
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ spl38_26 ),
inference(superposition,[],[f3684,f699]) ).
tff(f9356,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(c_2Enum_2E0) )
| ~ mem(c_2Ebool_2ET,bool)
| ~ p(c_2Ebool_2ET)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ spl38_26 ),
inference(forward_subsumption_resolution,[],[f9355,f7331]) ).
tff(f9357,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(c_2Enum_2E0) )
| ~ p(c_2Ebool_2ET)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ spl38_26 ),
inference(forward_subsumption_resolution,[],[f9356,f612]) ).
tff(f9358,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(c_2Enum_2E0) )
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| ~ spl38_26 ),
inference(forward_subsumption_resolution,[],[f9357,f611]) ).
tff(f9359,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(c_2Enum_2E0) )
| ~ spl38_26 ),
inference(forward_subsumption_resolution,[],[f9358,f320]) ).
tff(f9360,plain,
( ( fo__c_2Enum_2E0 != fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) )
| ~ spl38_26 ),
inference(forward_demodulation,[],[f9359,f827]) ).
tff(f9502,plain,
( ( fo__c_2Enum_2E0 != fo__c_2Enum_2E0 )
| ~ p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13)))
| ~ spl38_26 ),
inference(superposition,[],[f9360,f1108]) ).
tff(f9503,plain,
( ~ p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13)))
| ~ spl38_26 ),
inference(trivial_inequality_removal,[],[f9502]) ).
tff(f9504,plain,
( $false
| ~ spl38_25
| ~ spl38_26 ),
inference(forward_subsumption_resolution,[],[f9503,f3680]) ).
tff(f9505,plain,
( ~ spl38_25
| ~ spl38_26 ),
inference(avatar_contradiction_clause,[],[f9504]) ).
tff(f9507,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(ap(ap(c_2Ebool_2ECOND(ty_2Enum_2Enum),c_2Ebool_2EF),c_2Enum_2E0),ap(c_2Enum_2ESUC,c_2Enum_2E0))) )
| spl38_25 ),
inference(forward_subsumption_resolution,[],[f8587,f3681]) ).
tff(f9513,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,c_2Enum_2E0)) )
| ~ mem(ap(c_2Enum_2ESUC,c_2Enum_2E0),ty_2Enum_2Enum)
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| spl38_25 ),
inference(superposition,[],[f9507,f698]) ).
tff(f9514,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,c_2Enum_2E0)) )
| ~ mem(c_2Enum_2E0,ty_2Enum_2Enum)
| spl38_25 ),
inference(forward_subsumption_resolution,[],[f9513,f7331]) ).
tff(f9515,plain,
( ( fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) != surj__ty_2Enum_2Enum(ap(c_2Enum_2ESUC,c_2Enum_2E0)) )
| spl38_25 ),
inference(forward_subsumption_resolution,[],[f9514,f320]) ).
tff(f9516,plain,
( ( fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) != fo__c_2Earithmetic_2EMOD(sK13,fo__c_2Earithmetic_2ENUMERAL(fo__c_2Earithmetic_2EBIT2(fo__c_2Earithmetic_2EZERO))) )
| spl38_25 ),
inference(forward_demodulation,[],[f9515,f1195]) ).
tff(f9517,plain,
( ( fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) != fo__c_2Enum_2ESUC(fo__c_2Enum_2E0) )
| ~ p(inj__o(fo__c_2Earithmetic_2EODD(sK13)))
| ~ spl38_16
| spl38_25 ),
inference(superposition,[],[f9516,f1003]) ).
tff(f9519,plain,
( ~ p(inj__o(fo__c_2Earithmetic_2EODD(sK13)))
| ~ spl38_16
| spl38_25 ),
inference(trivial_inequality_removal,[],[f9517]) ).
tff(f9520,plain,
( p(inj__o(fo__c_2Earithmetic_2EEVEN(sK13)))
| ~ spl38_16
| spl38_25 ),
inference(resolution,[],[f9519,f719]) ).
tff(f9525,plain,
( $false
| ~ spl38_16
| spl38_25 ),
inference(forward_subsumption_resolution,[],[f9520,f3681]) ).
tff(f9526,plain,
( ~ spl38_16
| spl38_25 ),
inference(avatar_contradiction_clause,[],[f9525]) ).
cnf(s15,plain,
( ~ spl38_15
| spl38_16 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s18,plain,
spl38_15,
inference(sat_conversion,[],[f1913]) ).
cnf(s28,plain,
( ~ spl38_25
| spl38_26 ),
inference(sat_conversion,[],[f3685]) ).
cnf(s186,plain,
( ~ spl38_25
| ~ spl38_26 ),
inference(sat_conversion,[],[f9505]) ).
cnf(s187,plain,
( ~ spl38_16
| spl38_25 ),
inference(sat_conversion,[],[f9526]) ).
cnf(s226,plain,
spl38_16,
inference(rat,[],[s15,s18]) ).
cnf(s227,plain,
spl38_25,
inference(rat,[],[s187,s226]) ).
cnf(s228,plain,
~ spl38_26,
inference(rat,[],[s186,s227]) ).
cnf(s231,plain,
$false,
inference(rat,[],[s28,s228,s227]) ).
tff(f9527,plain,
$false,
inference(avatar_sat_refutation,[],[s231]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP003_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.12/0.38 % Computer : n003.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 11:51:20 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 16.39/3.16 % (381960)Detected formulas, will run a generic FOF schedule.
% 16.39/3.16 % (382042)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=786770027:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 16.39/3.16 % (382046)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2220410072:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 16.39/3.16 % (382045)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2958381462:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 16.39/3.16 % (382040)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=1925848493:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 16.39/3.16 % (382047)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3308747378:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 16.39/3.16 % (382049)dis-21_1_sil=8000:lcm=predicate:random_seed=2478003343: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)
% 16.39/3.16 % (382043)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=7116059:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 16.39/3.16 % (382045)Refutation not found, incomplete strategy
% 16.39/3.16 % (382045)------------------------------
% 16.39/3.16 % (382045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.39/3.16 % (382045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.39/3.16 % (382045)CaDiCaL version: 2.1.3
% 16.39/3.16 % (382045)Termination reason: Refutation not found, incomplete strategy
% 16.39/3.16 % (382045)Time elapsed: 0.005 s
% 16.39/3.16 % (382045)Peak memory usage: 89 MB
% 16.39/3.16 % (382045)Instructions burned: 3 (million)
% 16.39/3.16 % (382049)Instruction limit reached!
% 16.39/3.16 % (382049)------------------------------
% 16.39/3.16 % (382049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.39/3.16 % (382049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.39/3.16 % (382049)CaDiCaL version: 2.1.3
% 16.39/3.16 % (382049)Termination reason: Instruction limit
% 16.39/3.16 % (382049)Termination phase: Saturation
% 16.39/3.16 % (382049)Time elapsed: 0.100 s
% 16.39/3.16 % (382049)Peak memory usage: 89 MB
% 16.39/3.16 % (382049)Instructions burned: 130 (million)
% 16.39/3.16 % (382046)Instruction limit reached!
% 16.39/3.16 % (382046)------------------------------
% 16.39/3.16 % (382046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.39/3.16 % (382046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.39/3.16 % (382046)CaDiCaL version: 2.1.3
% 16.39/3.16 % (382046)Termination reason: Instruction limit
% 16.39/3.16 % (382046)Termination phase: Saturation
% 16.39/3.16 % (382046)Time elapsed: 0.104 s
% 16.39/3.16 % (382046)Peak memory usage: 89 MB
% 16.39/3.16 % (382046)Instructions burned: 120 (million)
% 16.39/3.16 % (382047)Instruction limit reached!
% 16.39/3.16 % (382047)------------------------------
% 16.39/3.16 % (382047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.39/3.16 % (382047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.39/3.16 % (382047)CaDiCaL version: 2.1.3
% 16.39/3.16 % (382047)Termination reason: Instruction limit
% 16.39/3.16 % (382047)Termination phase: Saturation
% 16.39/3.16 % (382047)Time elapsed: 0.135 s
% 16.39/3.16 % (382047)Peak memory usage: 91 MB
% 16.39/3.16 % (382047)Instructions burned: 139 (million)
% 16.39/3.16 % (382138)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3201718948:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 16.39/3.16 % (382131)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3163755921:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 16.39/3.16 % (382130)lrs+10_1_sil=8000:sp=occurrence:random_seed=2382745026:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 16.39/3.16 % (382045)------------------------------
% 16.39/3.16 % (382045)------------------------------
% 16.39/3.16 % (382131)Instruction limit reached!
% 16.39/3.16 % (382131)------------------------------
% 16.39/3.16 % (382131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.39/3.16 % (382131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.97 % (382131)CaDiCaL version: 2.1.3
% 21.18/3.97 % (382131)Termination reason: Instruction limit
% 21.18/3.97 % (382131)Termination phase: Saturation
% 21.18/3.97 % (382131)Time elapsed: 0.140 s
% 21.18/3.97 % (382131)Peak memory usage: 91 MB
% 21.18/3.97 % (382131)Instructions burned: 157 (million)
% 21.18/3.97 % (382170)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=3068355042:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 21.18/3.97 % (382130)Instruction limit reached!
% 21.18/3.97 % (382130)------------------------------
% 21.18/3.97 % (382130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.97 % (382130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.97 % (382130)CaDiCaL version: 2.1.3
% 21.18/3.97 % (382130)Termination reason: Instruction limit
% 21.18/3.97 % (382130)Termination phase: Saturation
% 21.18/3.97 % (382130)Time elapsed: 0.284 s
% 21.18/3.97 % (382130)Peak memory usage: 93 MB
% 21.18/3.97 % (382130)Instructions burned: 285 (million)
% 21.18/3.97 % (382138)Instruction limit reached!
% 21.18/3.97 % (382138)------------------------------
% 21.18/3.97 % (382138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.97 % (382138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.97 % (382138)CaDiCaL version: 2.1.3
% 21.18/3.97 % (382138)Termination reason: Instruction limit
% 21.18/3.97 % (382138)Termination phase: Saturation
% 21.18/3.97 % (382138)Time elapsed: 0.332 s
% 21.18/3.97 % (382138)Peak memory usage: 92 MB
% 21.18/3.97 % (382138)Instructions burned: 325 (million)
% 21.18/3.97 % (382180)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=104765728:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 21.18/3.97 % (382180)Refutation not found, incomplete strategy
% 21.18/3.97 % (382180)------------------------------
% 21.18/3.97 % (382180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.97 % (382180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.97 % (382180)CaDiCaL version: 2.1.3
% 21.18/3.97 % (382180)Termination reason: Refutation not found, incomplete strategy
% 21.18/3.97 % (382180)Time elapsed: 0.013 s
% 21.18/3.97 % (382180)Peak memory usage: 88 MB
% 21.18/3.97 % (382180)Instructions burned: 13 (million)
% 21.18/3.97 % (382170)Instruction limit reached!
% 21.18/3.97 % (382170)------------------------------
% 21.18/3.97 % (382170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.97 % (382170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.97 % (382170)CaDiCaL version: 2.1.3
% 21.18/3.97 % (382170)Termination reason: Instruction limit
% 21.18/3.97 % (382170)Termination phase: Saturation
% 21.18/3.97 % (382170)Time elapsed: 0.201 s
% 21.18/3.97 % (382170)Peak memory usage: 92 MB
% 21.18/3.97 % (382170)Instructions burned: 249 (million)
% 21.18/3.97 % (382195)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=500430656:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 21.18/3.97 % (382198)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2376369080:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 21.18/3.97 % (382198)Refutation not found, incomplete strategy
% 21.18/3.97 % (382198)------------------------------
% 21.18/3.97 % (382198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.97 % (382198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.97 % (382198)CaDiCaL version: 2.1.3
% 21.18/3.97 % (382198)Termination reason: Refutation not found, incomplete strategy
% 21.18/3.97 % (382198)Time elapsed: 0.013 s
% 21.18/3.97 % (382198)Peak memory usage: 89 MB
% 21.18/3.97 % (382198)Instructions burned: 19 (million)
% 21.18/3.97 % (382043)Refutation not found, incomplete strategy
% 21.18/3.97 % (382043)------------------------------
% 21.18/3.97 % (382043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.97 % (382043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.97 % (382043)CaDiCaL version: 2.1.3
% 21.18/3.97 % (382043)Termination reason: Refutation not found, incomplete strategy
% 21.18/3.97 % (382043)Time elapsed: 1.008 s
% 21.18/3.97 % (382043)Peak memory usage: 132 MB
% 21.18/3.97 % (382043)Instructions burned: 965 (million)
% 21.18/3.97 % (382180)------------------------------
% 21.18/3.97 % (382180)------------------------------
% 32.07/5.40 % (382205)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3657699458:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 32.07/5.40 % (382205)Refutation not found, incomplete strategy
% 32.07/5.40 % (382205)------------------------------
% 32.07/5.40 % (382205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.07/5.40 % (382205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.07/5.40 % (382205)CaDiCaL version: 2.1.3
% 32.07/5.40 % (382205)Termination reason: Refutation not found, incomplete strategy
% 32.07/5.40 % (382205)Time elapsed: 0.016 s
% 32.07/5.40 % (382205)Peak memory usage: 88 MB
% 32.07/5.40 % (382205)Instructions burned: 21 (million)
% 32.07/5.40 % (382198)------------------------------
% 32.07/5.40 % (382198)------------------------------
% 32.07/5.40 % (382043)------------------------------
% 32.07/5.40 % (382043)------------------------------
% 32.07/5.40 % (382230)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3841151510:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 32.07/5.40 % (382205)------------------------------
% 32.07/5.40 % (382205)------------------------------
% 32.07/5.40 % (382236)lrs+10_1_sil=8000:sp=occurrence:random_seed=3204562862:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 32.07/5.40 % (382237)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1197247897:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 32.07/5.40 % (382230)Instruction limit reached!
% 32.07/5.40 % (382230)------------------------------
% 32.07/5.40 % (382230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.07/5.40 % (382230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.07/5.40 % (382230)CaDiCaL version: 2.1.3
% 32.07/5.40 % (382230)Termination reason: Instruction limit
% 32.07/5.40 % (382230)Termination phase: Saturation
% 32.07/5.40 % (382230)Time elapsed: 0.107 s
% 32.07/5.40 % (382230)Peak memory usage: 90 MB
% 32.07/5.40 % (382230)Instructions burned: 115 (million)
% 32.07/5.40 % (382237)Refutation not found, incomplete strategy
% 32.07/5.40 % (382237)------------------------------
% 32.07/5.40 % (382237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.07/5.40 % (382237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.07/5.40 % (382237)CaDiCaL version: 2.1.3
% 32.07/5.40 % (382237)Termination reason: Refutation not found, incomplete strategy
% 32.07/5.40 % (382237)Time elapsed: 0.017 s
% 32.07/5.40 % (382237)Peak memory usage: 89 MB
% 32.07/5.40 % (382237)Instructions burned: 17 (million)
% 32.07/5.40 % (382255)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=962596947:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 32.07/5.40 % (382258)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3473131069:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 32.07/5.40 % (382258)Instruction limit reached!
% 32.07/5.40 % (382258)------------------------------
% 32.07/5.40 % (382258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.07/5.40 % (382258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.07/5.40 % (382258)CaDiCaL version: 2.1.3
% 32.07/5.40 % (382258)Termination reason: Instruction limit
% 32.07/5.40 % (382258)Termination phase: Saturation
% 32.07/5.40 % (382258)Time elapsed: 0.070 s
% 32.07/5.40 % (382258)Peak memory usage: 91 MB
% 32.07/5.40 % (382258)Instructions burned: 135 (million)
% 32.07/5.40 % (382237)------------------------------
% 32.07/5.40 % (382237)------------------------------
% 32.07/5.40 % (382273)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1742850642:st=8:i=592:sd=3:ep=RST:ss=axioms_2979 on theBenchmark for (2979ds/592Mi)
% 32.07/5.40 % (382283)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2525043507:st=3:i=13193:sd=3:ss=axioms_2979 on theBenchmark for (2979ds/13193Mi)
% 32.07/5.40 % (382236)Instruction limit reached!
% 32.07/5.40 % (382236)------------------------------
% 32.07/5.40 % (382236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.07/5.40 % (382236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.07/5.40 % (382236)CaDiCaL version: 2.1.3
% 32.07/5.40 % (382236)Termination reason: Instruction limit
% 32.07/5.40 % (382236)Termination phase: Saturation
% 32.07/5.40 % (382236)Time elapsed: 0.517 s
% 32.07/5.40 % (382236)Peak memory usage: 99 MB
% 24.32/5.60 % (382236)Instructions burned: 908 (million)
% 24.32/5.60 % (382371)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=781215786:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 24.32/5.60 % (382273)Instruction limit reached!
% 24.32/5.60 % (382273)------------------------------
% 24.32/5.60 % (382273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382273)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382273)Termination reason: Instruction limit
% 24.32/5.60 % (382273)Termination phase: Saturation
% 24.32/5.60 % (382273)Time elapsed: 0.303 s
% 24.32/5.60 % (382273)Peak memory usage: 92 MB
% 24.32/5.60 % (382273)Instructions burned: 593 (million)
% 24.32/5.60 % (382371)Instruction limit reached!
% 24.32/5.60 % (382371)------------------------------
% 24.32/5.60 % (382371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382371)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382371)Termination reason: Instruction limit
% 24.32/5.60 % (382371)Termination phase: Saturation
% 24.32/5.60 % (382371)Time elapsed: 0.073 s
% 24.32/5.60 % (382371)Peak memory usage: 91 MB
% 24.32/5.60 % (382371)Instructions burned: 126 (million)
% 24.32/5.60 % (382404)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3806471737:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 24.32/5.60 % (382421)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2910300582:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 24.32/5.60 % (382421)Refutation not found, incomplete strategy
% 24.32/5.60 % (382421)------------------------------
% 24.32/5.60 % (382421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382421)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382421)Termination reason: Refutation not found, incomplete strategy
% 24.32/5.60 % (382421)Time elapsed: 0.002 s
% 24.32/5.60 % (382421)Peak memory usage: 88 MB
% 24.32/5.60 % (382421)Instructions burned: 2 (million)
% 24.32/5.60 % (382404)Instruction limit reached!
% 24.32/5.60 % (382404)------------------------------
% 24.32/5.60 % (382404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382404)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382404)Termination reason: Instruction limit
% 24.32/5.60 % (382404)Termination phase: Saturation
% 24.32/5.60 % (382404)Time elapsed: 0.081 s
% 24.32/5.60 % (382404)Peak memory usage: 91 MB
% 24.32/5.60 % (382404)Instructions burned: 134 (million)
% 24.32/5.60 % (382195)Instruction limit reached!
% 24.32/5.60 % (382195)------------------------------
% 24.32/5.60 % (382195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382195)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382195)Termination reason: Instruction limit
% 24.32/5.60 % (382195)Termination phase: Saturation
% 24.32/5.60 % (382195)Time elapsed: 1.709 s
% 24.32/5.60 % (382195)Peak memory usage: 145 MB
% 24.32/5.60 % (382195)Instructions burned: 2351 (million)
% 24.32/5.60 % (382424)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1556557323:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 24.32/5.60 % (382421)------------------------------
% 24.32/5.60 % (382421)------------------------------
% 24.32/5.60 % (382425)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1978783650:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 24.32/5.60 % (382427)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=589662485:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2970 on theBenchmark for (2970ds/150Mi)
% 24.32/5.60 % (382424)Instruction limit reached!
% 24.32/5.60 % (382424)------------------------------
% 24.32/5.60 % (382424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382424)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382424)Termination reason: Instruction limit
% 24.32/5.60 % (382424)Termination phase: Saturation
% 24.32/5.60 % (382424)Time elapsed: 0.239 s
% 24.32/5.60 % (382424)Peak memory usage: 94 MB
% 24.32/5.60 % (382424)Instructions burned: 431 (million)
% 24.32/5.60 % (382427)Instruction limit reached!
% 24.32/5.60 % (382427)------------------------------
% 24.32/5.60 % (382427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382427)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382427)Termination reason: Instruction limit
% 24.32/5.60 % (382427)Termination phase: Saturation
% 24.32/5.60 % (382427)Time elapsed: 0.087 s
% 24.32/5.60 % (382427)Peak memory usage: 92 MB
% 24.32/5.60 % (382427)Instructions burned: 151 (million)
% 24.32/5.60 % (382430)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3979905453:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 24.32/5.60 % (382431)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2452227455:i=667:av=off:fsr=off_2968 on theBenchmark for (2968ds/667Mi)
% 24.32/5.60 % (382431)Refutation not found, incomplete strategy
% 24.32/5.60 % (382431)------------------------------
% 24.32/5.60 % (382431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382431)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382431)Termination reason: Refutation not found, incomplete strategy
% 24.32/5.60 % (382431)Time elapsed: 0.009 s
% 24.32/5.60 % (382431)Peak memory usage: 88 MB
% 24.32/5.60 % (382431)Instructions burned: 15 (million)
% 24.32/5.60 % (382431)------------------------------
% 24.32/5.60 % (382431)------------------------------
% 24.32/5.60 % (382526)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=644328871:s2a=on:i=185:s2at=1.8:fdi=4_2963 on theBenchmark for (2963ds/185Mi)
% 24.32/5.60 % (382526)Instruction limit reached!
% 24.32/5.60 % (382526)------------------------------
% 24.32/5.60 % (382526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382526)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382526)Termination reason: Instruction limit
% 24.32/5.60 % (382526)Termination phase: Saturation
% 24.32/5.60 % (382526)Time elapsed: 0.111 s
% 24.32/5.60 % (382526)Peak memory usage: 92 MB
% 24.32/5.60 % (382526)Instructions burned: 185 (million)
% 24.32/5.60 % (382636)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4268083689:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2961 on theBenchmark for (2961ds/193Mi)
% 24.32/5.60 % (382636)Instruction limit reached!
% 24.32/5.60 % (382636)------------------------------
% 24.32/5.60 % (382636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382636)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382636)Termination reason: Instruction limit
% 24.32/5.60 % (382636)Termination phase: Saturation
% 24.32/5.60 % (382636)Time elapsed: 0.123 s
% 24.32/5.60 % (382636)Peak memory usage: 91 MB
% 24.32/5.60 % (382636)Instructions burned: 198 (million)
% 24.32/5.60 % (382638)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1590928574:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2958 on theBenchmark for (2958ds/4850Mi)
% 24.32/5.60 % (382638)Refutation not found, incomplete strategy
% 24.32/5.60 % (382638)------------------------------
% 24.32/5.60 % (382638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.32/5.60 % (382638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.32/5.60 % (382638)CaDiCaL version: 2.1.3
% 24.32/5.60 % (382638)Termination reason: Refutation not found, incomplete strategy
% 24.32/5.60 % (382638)Time elapsed: 0.008 s
% 24.32/5.60 % (382638)Peak memory usage: 88 MB
% 24.32/5.60 % (382638)Instructions burned: 15 (million)
% 24.32/5.60 % (382255)First to succeed.
% 24.32/5.60 % (382255)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-381960"
% 24.32/5.60 % (382638)------------------------------
% 24.32/5.60 % (382638)------------------------------
% 24.32/5.60 % (382255)Refutation found. Thanks to Tanya!
% 24.32/5.60 % SZS status Theorem for theBenchmark
% 24.32/5.60 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/5.80 % (382255)------------------------------
% 0.17/5.80 % (382255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/5.80 % (382255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/5.80 % (382255)CaDiCaL version: 2.1.3
% 0.17/5.80 % (382255)Termination reason: Refutation
% 0.17/5.80 % (382255)Time elapsed: 2.499 s
% 0.17/5.80 % (382255)Peak memory usage: 159 MB
% 0.17/5.80 % (382255)Instructions burned: 4159 (million)
% 0.17/5.80 % (382255)------------------------------
% 0.17/5.80 % (382255)------------------------------
% 0.17/5.80 % (381960)Success in time 4.743 s
% 0.17/5.80 % Vampire exiting
%------------------------------------------------------------------------------