%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP015^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 : Wed Sep 30 08:10:19 AM UTC 2026
% Result : Theorem 0.79s 0.46s
% Output : Refutation 0.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP015^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 % Computer : n009.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 19:30:17 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.24 Running first-order model finding
% 0.10/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.79/0.46 % (242813)Will run a generic schedule for satisfiability detection.
% 0.79/0.46 % (242824)% WARNING: option uhcvi not known.
% 0.79/0.46 % (242823)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1496082676_2999 on theBenchmark for (2999ds/0Mi)
% 0.79/0.46 % (242825)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1387151841:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.79/0.46 % (242824)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3251961928:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.79/0.46 % (242829)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1322680045:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.79/0.46 % (242826)dis+10_1_sil=32000:sp=arity:random_seed=2699177347:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.79/0.46 % (242827)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3196044477:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.79/0.46 % (242830)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2451753791:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.79/0.46 % (242824)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.79/0.46 % (242827)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.79/0.46 % Exception at run slice level
% 0.79/0.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.79/0.46 % (242824)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.79/0.46 % (242852)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1082175243:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.79/0.46 % Exception at run slice level
% 0.79/0.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.79/0.46 % (242826)Instruction limit reached!
% 0.79/0.46 % (242826)------------------------------
% 0.79/0.46 % (242826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.46 % (242826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.46 % (242826)CaDiCaL version: 2.1.3
% 0.79/0.46 % (242826)Termination reason: Instruction limit
% 0.79/0.46 % (242826)Termination phase: Saturation
% 0.79/0.46 % (242826)Time elapsed: 0.053 s
% 0.79/0.46 % (242826)Peak memory usage: 12 MB
% 0.79/0.46 % (242826)Instructions burned: 108 (million)
% 0.79/0.46 % (242827)Instruction limit reached!
% 0.79/0.46 % (242827)------------------------------
% 0.79/0.46 % (242827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.46 % (242827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.46 % (242827)CaDiCaL version: 2.1.3
% 0.79/0.46 % (242827)Termination reason: Instruction limit
% 0.79/0.46 % (242827)Termination phase: Saturation
% 0.79/0.46 % (242827)Time elapsed: 0.059 s
% 0.79/0.46 % (242827)Peak memory usage: 13 MB
% 0.79/0.46 % (242827)Instructions burned: 117 (million)
% 0.79/0.46 % (242867)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=822215841:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.79/0.46 % (242829)Instruction limit reached!
% 0.79/0.46 % (242829)------------------------------
% 0.79/0.46 % (242829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.46 % (242829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.46 % (242829)CaDiCaL version: 2.1.3
% 0.79/0.46 % (242829)Termination reason: Instruction limit
% 0.79/0.46 % (242829)Termination phase: Saturation
% 0.79/0.46 % (242829)Time elapsed: 0.068 s
% 0.79/0.46 % (242829)Peak memory usage: 12 MB
% 0.79/0.46 % (242829)Instructions burned: 132 (million)
% 0.79/0.46 % (242874)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1167197763:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.79/0.46 % (242874)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.79/0.46 % (242830)Instruction limit reached!
% 0.79/0.46 % (242830)------------------------------
% 0.79/0.46 % (242830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.46 % (242830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.46 % (242830)CaDiCaL version: 2.1.3
% 0.79/0.46 % (242830)Termination reason: Instruction limit
% 0.79/0.46 % (242830)Termination phase: Saturation
% 0.79/0.46 % (242830)Time elapsed: 0.079 s
% 0.79/0.46 % (242830)Peak memory usage: 13 MB
% 0.79/0.46 % (242830)Instructions burned: 159 (million)
% 0.79/0.46 % (242880)ott-21_1_sil=16000:fs=off:random_seed=3771187493:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.79/0.46 % (242874)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.79/0.46 % (242885)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=489075377:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.79/0.46 % (242892)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1976553582:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 0.79/0.46 % Exception at run slice level
% 0.79/0.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.79/0.46 % (242911)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1199618989:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 0.79/0.46 % (242867)Instruction limit reached!
% 0.79/0.46 % (242867)------------------------------
% 0.79/0.46 % (242867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.46 % (242867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.46 % (242867)CaDiCaL version: 2.1.3
% 0.79/0.46 % (242867)Termination reason: Instruction limit
% 0.79/0.46 % (242867)Termination phase: Saturation
% 0.79/0.46 % (242867)Time elapsed: 0.071 s
% 0.79/0.46 % (242867)Peak memory usage: 13 MB
% 0.79/0.46 % (242867)Instructions burned: 133 (million)
% 0.79/0.46 % (242925)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=983740010:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 0.79/0.46 % Exception at run slice level
% 0.79/0.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.79/0.46 % (242880)Instruction limit reached!
% 0.79/0.46 % (242880)------------------------------
% 0.79/0.46 % (242880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.46 % (242880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.46 % (242880)CaDiCaL version: 2.1.3
% 0.79/0.46 % (242880)Termination reason: Instruction limit
% 0.79/0.46 % (242880)Termination phase: Saturation
% 0.79/0.46 % (242880)Time elapsed: 0.083 s
% 0.79/0.46 % (242880)Peak memory usage: 12 MB
% 0.79/0.46 % (242880)Instructions burned: 181 (million)
% 0.79/0.46 % (242824) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-242813-242824"...
% 0.79/0.46 % (242824)...printing done.
% 0.79/0.46 % (242824)Refutation found. Thanks to Tanya!
% 0.79/0.46 % SZS status Theorem for theBenchmark
% 0.79/0.46 % SZS output start Proof for theBenchmark
% 0.79/0.46 thf(type_def_5, type, u: $tType).
% 0.79/0.46 thf(type_def_6, type, d: $tType).
% 0.79/0.46 thf(type_def_7, type, du: $tType).
% 0.79/0.46 thf(type_def_8, type, mono_2Etyop_2Einteger_2Eint: $tType).
% 0.79/0.46 thf(type_def_9, type, mono_2Etyop_2Enum_2Enum: $tType).
% 0.79/0.46 thf(type_def_10, type, sTfun: ($tType * $tType) > $tType).
% 0.79/0.46 thf(func_def_0, type, tyop_2Ebool_2Eitself: (d > d)).
% 0.79/0.46 thf(func_def_1, type, tyop_2Efcp_2Ecart: (d > d > d)).
% 0.79/0.46 thf(func_def_2, type, tyop_2Einteger_2Eint: d).
% 0.79/0.46 thf(func_def_3, type, tyop_2Emin_2Ebool: d).
% 0.79/0.46 thf(func_def_4, type, tyop_2Emin_2Efun: (d > d > d)).
% 0.79/0.46 thf(func_def_5, type, tyop_2Enum_2Enum: d).
% 0.79/0.46 thf(func_def_6, type, s: (d > u > du)).
% 0.79/0.46 thf(func_def_7, type, app_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_8, type, combin_i_2E0: u).
% 0.79/0.46 thf(func_def_9, type, combin_k_2E0: u).
% 0.79/0.46 thf(func_def_10, type, combin_s_2E0: u).
% 0.79/0.46 thf(func_def_11, type, c_2Ebool_2E_21_2E0: u).
% 0.79/0.46 thf(func_def_12, type, c_2Ebool_2E_21_2E1: (du > u)).
% 0.79/0.46 thf(func_def_13, type, c_2Ebool_2E_2F_5C_2E0: u).
% 0.79/0.46 thf(func_def_14, type, c_2Ebool_2E_2F_5C_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_15, type, c_2Enum_2E0_2E0: u).
% 0.79/0.46 thf(func_def_16, type, c_2Eprim__rec_2E_3C_2E0: u).
% 0.79/0.46 thf(func_def_17, type, c_2Eprim__rec_2E_3C_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_18, type, c_2Emin_2E_3D_2E0: u).
% 0.79/0.46 thf(func_def_19, type, c_2Emin_2E_3D_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_20, type, c_2Emin_2E_3D_3D_3E_2E0: u).
% 0.79/0.46 thf(func_def_21, type, c_2Emin_2E_3D_3D_3E_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_22, type, c_2Ebool_2E_3F_2E0: u).
% 0.79/0.46 thf(func_def_23, type, c_2Ebool_2E_3F_2E1: (du > u)).
% 0.79/0.46 thf(func_def_24, type, c_2Ebool_2ECOND_2E0: u).
% 0.79/0.46 thf(func_def_25, type, c_2Ebool_2ECOND_2E3: (du > du > du > u)).
% 0.79/0.46 thf(func_def_26, type, c_2Ebool_2EF_2E0: u).
% 0.79/0.46 thf(func_def_27, type, c_2Earithmetic_2EMOD_2E0: u).
% 0.79/0.46 thf(func_def_28, type, c_2Earithmetic_2EMOD_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_29, type, c_2Einteger_2ENum_2E0: u).
% 0.79/0.46 thf(func_def_30, type, c_2Einteger_2ENum_2E1: (du > u)).
% 0.79/0.46 thf(func_def_31, type, c_2Ebool_2ET_2E0: u).
% 0.79/0.46 thf(func_def_32, type, c_2Ebool_2E_5C_2F_2E0: u).
% 0.79/0.46 thf(func_def_33, type, c_2Ebool_2E_5C_2F_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_34, type, c_2Ewords_2Edimword_2E0: u).
% 0.79/0.46 thf(func_def_35, type, c_2Ewords_2Edimword_2E1: (du > u)).
% 0.79/0.46 thf(func_def_36, type, c_2Einteger__word_2Ei2w_2E0: u).
% 0.79/0.46 thf(func_def_37, type, c_2Einteger__word_2Ei2w_2E1: (du > u)).
% 0.79/0.46 thf(func_def_38, type, c_2Einteger_2Eint__lt_2E0: u).
% 0.79/0.46 thf(func_def_39, type, c_2Einteger_2Eint__lt_2E2: (du > du > u)).
% 0.79/0.46 thf(func_def_40, type, c_2Einteger_2Eint__neg_2E0: u).
% 0.79/0.46 thf(func_def_41, type, c_2Einteger_2Eint__neg_2E1: (du > u)).
% 0.79/0.46 thf(func_def_42, type, c_2Einteger_2Eint__of__num_2E0: u).
% 0.79/0.46 thf(func_def_43, type, c_2Einteger_2Eint__of__num_2E1: (du > u)).
% 0.79/0.46 thf(func_def_44, type, c_2Ewords_2En2w_2E0: u).
% 0.79/0.46 thf(func_def_45, type, c_2Ewords_2En2w_2E1: (du > u)).
% 0.79/0.46 thf(func_def_46, type, c_2Ebool_2Ethe__value_2E0: u).
% 0.79/0.46 thf(func_def_47, type, c_2Ewords_2Eword__2comp_2E0: u).
% 0.79/0.46 thf(func_def_48, type, c_2Ewords_2Eword__2comp_2E1: (du > u)).
% 0.79/0.46 thf(func_def_49, type, c_2Ebool_2E_7E_2E0: u).
% 0.79/0.46 thf(func_def_50, type, c_2Ebool_2E_7E_2E1: (du > u)).
% 0.79/0.46 thf(func_def_51, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: (($o > $o) > $o > $o)).
% 0.79/0.46 thf(func_def_52, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (($o > $o > $o) > $o > $o > $o)).
% 0.79/0.46 thf(func_def_53, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Ebool: ((mono_2Etyop_2Einteger_2Eint > $o) > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.79/0.46 thf(func_def_54, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o) > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.79/0.46 thf(func_def_55, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Einteger_2Eint: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint) > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.79/0.46 thf(func_def_56, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Enum_2Enum: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum) > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_57, type, mono_2Eapp_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool: ((mono_2Etyop_2Enum_2Enum > $o) > mono_2Etyop_2Enum_2Enum > $o)).
% 0.79/0.46 thf(func_def_58, type, mono_2Eapp_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o) > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o)).
% 0.79/0.46 thf(func_def_59, type, mono_2Eapp_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum) > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_60, type, mono_2Eapp_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Einteger_2Eint: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint) > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint)).
% 0.79/0.46 thf(func_def_61, type, mono_2Eapp_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum) > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_62, type, mono_2Ec_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 0.79/0.46 thf(func_def_63, type, mono_2Ec_2Enum_2E0: mono_2Etyop_2Enum_2Enum).
% 0.79/0.46 thf(func_def_64, type, mono_2Ec_2Eprim__rec_2E_3C: (mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o)).
% 0.79/0.46 thf(func_def_65, type, mono_2Ec_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 0.79/0.46 thf(func_def_66, type, mono_2Ec_2Ebool_2EF: $o).
% 0.79/0.46 thf(func_def_67, type, mono_2Ec_2Earithmetic_2EMOD: (mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_68, type, mono_2Ec_2Einteger_2ENum: (mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_69, type, mono_2Ec_2Ebool_2ET: $o).
% 0.79/0.46 thf(func_def_70, type, mono_2Ec_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 0.79/0.46 thf(func_def_71, type, mono_2Ec_2Einteger_2Eint__lt: (mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.79/0.46 thf(func_def_72, type, mono_2Ec_2Einteger_2Eint__neg: (mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.79/0.46 thf(func_def_73, type, mono_2Ec_2Einteger_2Eint__of__num: (mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint)).
% 0.79/0.46 thf(func_def_74, type, mono_2Ec_2Ebool_2E_7E: ($o > $o)).
% 0.79/0.46 thf(func_def_75, type, i_mono_2Etyop_2Emin_2Ebool: ($o > u)).
% 0.79/0.46 thf(func_def_76, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (($o > $o) > u)).
% 0.79/0.46 thf(func_def_77, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: (($o > $o > $o) > u)).
% 0.79/0.46 thf(func_def_78, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: ((mono_2Etyop_2Einteger_2Eint > $o) > u)).
% 0.79/0.46 thf(func_def_79, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o) > u)).
% 0.79/0.46 thf(func_def_80, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint) > u)).
% 0.79/0.46 thf(func_def_81, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum) > u)).
% 0.79/0.46 thf(func_def_82, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: ((mono_2Etyop_2Enum_2Enum > $o) > u)).
% 0.79/0.46 thf(func_def_83, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o) > u)).
% 0.79/0.46 thf(func_def_84, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum) > u)).
% 0.79/0.46 thf(func_def_85, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint) > u)).
% 0.79/0.46 thf(func_def_86, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: ((mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum) > u)).
% 0.79/0.46 thf(func_def_87, type, i_mono_2Etyop_2Einteger_2Eint: (mono_2Etyop_2Einteger_2Eint > u)).
% 0.79/0.46 thf(func_def_88, type, i_mono_2Etyop_2Enum_2Enum: (mono_2Etyop_2Enum_2Enum > u)).
% 0.79/0.46 thf(func_def_89, type, j_mono_2Etyop_2Emin_2Ebool: (du > $o)).
% 0.79/0.46 thf(func_def_90, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (du > $o > $o)).
% 0.79/0.46 thf(func_def_91, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: (du > $o > $o > $o)).
% 0.79/0.46 thf(func_def_92, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: (du > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.79/0.46 thf(func_def_93, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29: (du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.79/0.46 thf(func_def_94, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29: (du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.79/0.46 thf(func_def_95, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29: (du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_96, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: (du > mono_2Etyop_2Enum_2Enum > $o)).
% 0.79/0.46 thf(func_def_97, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29: (du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o)).
% 0.79/0.46 thf(func_def_98, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: (du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_99, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29: (du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint)).
% 0.79/0.46 thf(func_def_100, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: (du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_101, type, j_mono_2Etyop_2Einteger_2Eint: (du > mono_2Etyop_2Einteger_2Eint)).
% 0.79/0.46 thf(func_def_102, type, j_mono_2Etyop_2Enum_2Enum: (du > mono_2Etyop_2Enum_2Enum)).
% 0.79/0.46 thf(func_def_104, type, vNOT: ($o > $o)).
% 0.79/0.46 thf(func_def_107, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.79/0.46 thf(func_def_108, type, sK0: (u > u > d > d > u)).
% 0.79/0.46 thf(func_def_109, type, sK1: (u > d > u)).
% 0.79/0.46 thf(func_def_110, type, sK2: (u > d > u)).
% 0.79/0.46 thf(func_def_111, type, sK3: d).
% 0.79/0.46 thf(func_def_113, type, db0: !>[X0: $tType]:(X0)).
% 0.79/0.46 thf(func_def_114, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.79/0.46 thf(f73,axiom,(
% 0.79/0.46 ! [X0 : $o] : (mono_2Ec_2Ebool_2EF => X0)),
% 0.79/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EFALSITY)).
% 0.79/0.46 thf(f78,axiom,(
% 0.79/0.46 ! [X0 : d] : (! [X3 : u,X4 : u] : (((s @ X0 @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2EF)) @ (s @ X0 @ X3) @ (s @ X0 @ X4)))) = ((s @ X0 @ X4))) & ! [X1 : u,X2 : u] : (((s @ X0 @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2ET)) @ (s @ X0 @ X1) @ (s @ X0 @ X2)))) = ((s @ X0 @ X1))))),
% 0.79/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2Ebool__case__thm)).
% 0.79/0.46 thf(f79,axiom,(
% 0.79/0.46 (((mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0))) = ((mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))),
% 0.79/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2EINT__NEG__0)).
% 0.79/0.46 thf(f80,axiom,(
% 0.79/0.46 ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = mono_2Ec_2Ebool_2EF) & ((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)) <=> ((~ (X1 = mono_2Ec_2Enum_2E0)) | (~ (X0 = mono_2Ec_2Enum_2E0)))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X1 @ X0))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X0 @ X1))))),
% 0.79/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2EINT__LT__CALCULATE)).
% 0.79/0.46 thf(f81,axiom,(
% 0.79/0.46 ! [X0 : mono_2Etyop_2Enum_2Enum] : (((mono_2Ec_2Einteger_2ENum @ (mono_2Ec_2Einteger_2Eint__of__num @ X0))) = X0)),
% 0.79/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2ENUM__OF__INT)).
% 0.79/0.46 thf(f82,axiom,(
% 0.79/0.46 ! [X0 : d,X1 : mono_2Etyop_2Einteger_2Eint] : (((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ X1))))) = ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ (mono_2Ec_2Einteger_2Eint__lt @ X1 @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2Eword__2comp_2E1 @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ (mono_2Ec_2Einteger_2ENum @ (mono_2Ec_2Einteger_2Eint__neg @ X1)))))))) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ (mono_2Ec_2Einteger_2ENum @ X1)))))))))),
% 0.79/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger__word_2Ei2w__def)).
% 0.79/0.46 thf(f86,conjecture,(
% 0.79/0.46 ! [X0 : d] : (((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))))) = ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0))))))),
% 0.79/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger__word_2Ei2w__0)).
% 0.79/0.46 thf(f87,negated_conjecture,(
% 0.79/0.46 ~ ! [X0 : d] : (((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))))) = ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0))))))),
% 0.79/0.46 inference(negated_conjecture,[status(cth)],[f86])).
% 0.79/0.46 thf(f108,plain,(
% 0.79/0.46 ! [X0 : $o] : (mono_2Ec_2Ebool_2EF => X0)),
% 0.79/0.46 inference(rectify,[],[f73])).
% 0.79/0.46 thf(f109,plain,(
% 0.79/0.46 ! [X0 : $o] : ((mono_2Ec_2Ebool_2EF = $true) => ($true = X0))),
% 0.79/0.46 inference(fool_elimination,[],[f108])).
% 0.79/0.46 thf(f116,plain,(
% 0.79/0.46 ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = mono_2Ec_2Ebool_2EF) & ((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)) <=> ((~ (X1 = mono_2Ec_2Enum_2E0)) | (~ (X0 = mono_2Ec_2Enum_2E0)))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X1 @ X0))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X0 @ X1))))),
% 0.79/0.46 inference(rectify,[],[f80])).
% 0.79/0.46 thf(f117,plain,(
% 0.79/0.46 ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((mono_2Ec_2Ebool_2EF = ((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))))) & ((((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = $true) <=> (($true = ((~ (mono_2Ec_2Enum_2E0 = X1)))) | ($true = ((~ (mono_2Ec_2Enum_2E0 = X0)))))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X1 @ X0))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X0 @ X1))))),
% 0.79/0.46 inference(fool_elimination,[],[f116])).
% 0.79/0.46 thf(f120,plain,(
% 0.79/0.46 ! [X0 : d] : (! [X1 : u,X2 : u] : (((s @ X0 @ X2)) = ((s @ X0 @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2EF)) @ (s @ X0 @ X1) @ (s @ X0 @ X2))))) & ! [X3 : u,X4 : u] : (((s @ X0 @ X3)) = ((s @ X0 @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2ET)) @ (s @ X0 @ X3) @ (s @ X0 @ X4))))))),
% 0.79/0.46 inference(rectify,[],[f78])).
% 0.79/0.46 thf(f125,plain,(
% 0.79/0.46 ! [X0 : $o] : (($true = X0) | (mono_2Ec_2Ebool_2EF != $true))),
% 0.79/0.46 inference(ennf_transformation,[],[f109])).
% 0.79/0.46 thf(f130,plain,(
% 0.79/0.46 ? [X0 : d] : (((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0))))) != ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))))))),
% 0.79/0.46 inference(ennf_transformation,[],[f87])).
% 0.79/0.46 thf(f150,plain,(
% 0.79/0.46 ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((mono_2Ec_2Ebool_2EF = ((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))))) & (((((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = $true) | (($true != ((~ (mono_2Ec_2Enum_2E0 = X1)))) & ($true != ((~ (mono_2Ec_2Enum_2E0 = X0)))))) & ((($true = ((~ (mono_2Ec_2Enum_2E0 = X1)))) | ($true = ((~ (mono_2Ec_2Enum_2E0 = X0))))) | (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) != $true))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X1 @ X0))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X0 @ X1))))),
% 0.79/0.46 inference(nnf_transformation,[],[f117])).
% 0.79/0.46 thf(f151,plain,(
% 0.79/0.46 ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((mono_2Ec_2Ebool_2EF = ((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))))) & ((((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = $true) | (($true != ((~ (mono_2Ec_2Enum_2E0 = X1)))) & ($true != ((~ (mono_2Ec_2Enum_2E0 = X0)))))) & (($true = ((~ (mono_2Ec_2Enum_2E0 = X1)))) | ($true = ((~ (mono_2Ec_2Enum_2E0 = X0)))) | (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) != $true)) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X1 @ X0))) & (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__of__num @ X1))) = ((mono_2Ec_2Eprim__rec_2E_3C @ X0 @ X1))))),
% 0.79/0.46 inference(flattening,[],[f150])).
% 0.79/0.46 thf(f153,plain,(
% 0.79/0.46 (((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ sK3) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0))))) != ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ sK3) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))))))),
% 0.79/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f130])).
% 0.79/0.46 thf(f239,plain,(
% 0.79/0.46 ( ! [X0 : $o] : (($true = X0) | (mono_2Ec_2Ebool_2EF != $true)) )),
% 0.79/0.46 inference(cnf_transformation,[],[f125])).
% 0.79/0.46 thf(f255,plain,(
% 0.79/0.46 ( ! [X2 : u,X0 : d,X1 : u] : ((((s @ X0 @ X2)) = ((s @ X0 @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2EF)) @ (s @ X0 @ X1) @ (s @ X0 @ X2)))))) )),
% 0.79/0.46 inference(cnf_transformation,[],[f120])).
% 0.79/0.46 thf(f256,plain,(
% 0.79/0.46 (((mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)) = ((mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0))))),
% 0.79/0.46 inference(cnf_transformation,[],[f79])).
% 0.79/0.46 thf(f262,plain,(
% 0.79/0.46 ( ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((mono_2Ec_2Ebool_2EF = ((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))))) )),
% 0.79/0.46 inference(cnf_transformation,[],[f151])).
% 0.79/0.46 thf(f263,plain,(
% 0.79/0.46 ( ! [X0 : mono_2Etyop_2Enum_2Enum] : ((((mono_2Ec_2Einteger_2ENum @ (mono_2Ec_2Einteger_2Eint__of__num @ X0))) = X0)) )),
% 0.79/0.46 inference(cnf_transformation,[],[f81])).
% 0.79/0.46 thf(f264,plain,(
% 0.79/0.46 ( ! [X0 : d,X1 : mono_2Etyop_2Einteger_2Eint] : ((((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ X1))))) = ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ (mono_2Ec_2Einteger_2Eint__lt @ X1 @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2Eword__2comp_2E1 @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ (mono_2Ec_2Einteger_2ENum @ (mono_2Ec_2Einteger_2Eint__neg @ X1)))))))) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X0) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ (mono_2Ec_2Einteger_2ENum @ X1)))))))))) )),
% 0.79/0.46 inference(cnf_transformation,[],[f82])).
% 0.79/0.46 thf(f269,plain,(
% 0.79/0.46 (((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ sK3) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0))))) != ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ sK3) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))))))),
% 0.79/0.46 inference(cnf_transformation,[],[f153])).
% 0.79/0.46 thf(f270,definition,(
% 0.79/0.46 ($true != $false)),
% 0.79/0.46 introduced(theory,[fool_distinctness_axiom])).
% 0.79/0.46 thf(f271,definition,(
% 0.79/0.46 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.79/0.46 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.79/0.46 thf(f316,plain,(
% 0.79/0.46 ( ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((mono_2Ec_2Ebool_2EF = $true) | (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = $false)) )),
% 0.79/0.46 inference(iff_proxy_clausification,[],[f262])).
% 0.79/0.46 thf(f344,definition,(
% 0.79/0.46 spl4_2 <=> (mono_2Ec_2Ebool_2EF = $false)),
% 0.79/0.46 introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition])).
% 0.79/0.46 thf(f345,plain,(
% 0.79/0.46 (mono_2Ec_2Ebool_2EF != $false) | spl4_2),
% 0.79/0.46 inference(avatar_component_clause,[],[f344])).
% 0.79/0.46 thf(f346,plain,(
% 0.79/0.46 (mono_2Ec_2Ebool_2EF = $false) | ~spl4_2),
% 0.79/0.46 inference(avatar_component_clause,[],[f344])).
% 0.79/0.46 thf(f349,definition,(
% 0.79/0.46 spl4_3 <=> ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : (((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = $false)),
% 0.79/0.46 introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition])).
% 0.79/0.46 thf(f350,plain,(
% 0.79/0.46 ( ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : mono_2Etyop_2Enum_2Enum] : ((((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X1)))) = $false)) ) | ~spl4_3),
% 0.79/0.46 inference(avatar_component_clause,[],[f349])).
% 0.79/0.46 thf(f352,definition,(
% 0.79/0.46 spl4_4 <=> (mono_2Ec_2Ebool_2EF = $true)),
% 0.79/0.46 introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition])).
% 0.79/0.46 thf(f353,plain,(
% 0.79/0.46 (mono_2Ec_2Ebool_2EF != $true) | spl4_4),
% 0.79/0.46 inference(avatar_component_clause,[],[f352])).
% 0.79/0.46 thf(f355,plain,(
% 0.79/0.46 spl4_3 | spl4_4),
% 0.79/0.46 inference(avatar_split_clause,[],[f316,f352,f349])).
% 0.79/0.46 thf(f357,definition,(
% 0.79/0.46 spl4_5 <=> ! [X0 : $o] : ($true = X0)),
% 0.79/0.46 introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition])).
% 0.79/0.46 thf(f358,plain,(
% 0.79/0.46 ( ! [X0 : $o] : (($true = X0)) ) | ~spl4_5),
% 0.79/0.46 inference(avatar_component_clause,[],[f357])).
% 0.79/0.46 thf(f359,plain,(
% 0.79/0.46 ~spl4_4 | spl4_5),
% 0.79/0.46 inference(avatar_split_clause,[],[f239,f357,f352])).
% 0.79/0.46 thf(f361,definition,(
% 0.79/0.46 spl4_6 <=> ! [X0 : $o] : (($false = X0) | ($true = X0))),
% 0.79/0.46 introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition])).
% 0.79/0.46 thf(f362,plain,(
% 0.79/0.46 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) ) | ~spl4_6),
% 0.79/0.46 inference(avatar_component_clause,[],[f361])).
% 0.79/0.46 thf(f365,plain,(
% 0.79/0.46 spl4_6),
% 0.79/0.46 inference(avatar_split_clause,[],[f271,f361])).
% 0.79/0.46 thf(f586,plain,(
% 0.79/0.46 ( ! [X2 : u,X0 : d,X1 : u] : ((((s @ X0 @ X2)) = ((s @ X0 @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ $false)) @ (s @ X0 @ X1) @ (s @ X0 @ X2)))))) ) | ~spl4_2),
% 0.79/0.46 inference(forward_demodulation,[],[f255,f346])).
% 0.79/0.46 thf(f777,plain,(
% 0.79/0.46 ( ! [X0 : mono_2Etyop_2Enum_2Enum] : (($false = ((mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0))))) ) | ~spl4_3),
% 0.79/0.46 inference(constrained_superposition,[],[f350,f256])).
% 0.79/0.46 thf(f1541,plain,(
% 0.79/0.46 ( ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : d] : ((((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)))))) = ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ (mono_2Ec_2Einteger_2Eint__lt @ (mono_2Ec_2Einteger_2Eint__of__num @ X0) @ (mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0)))) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ewords_2Eword__2comp_2E1 @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ (mono_2Ec_2Einteger_2ENum @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0))))))))) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ X0))))))))) )),
% 0.79/0.47 inference(constrained_superposition,[],[f264,f263])).
% 0.79/0.47 thf(f1576,plain,(
% 0.79/0.47 ( ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : d] : ((((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)))))) = ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ebool_2ECOND_2E3 @ (s @ tyop_2Emin_2Ebool @ (i_mono_2Etyop_2Emin_2Ebool @ $false)) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ewords_2Eword__2comp_2E1 @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ (mono_2Ec_2Einteger_2ENum @ (mono_2Ec_2Einteger_2Eint__neg @ (mono_2Ec_2Einteger_2Eint__of__num @ X0))))))))) @ (s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ X0))))))))) ) | ~spl4_3),
% 0.79/0.47 inference(forward_demodulation,[],[f1541,f777])).
% 0.79/0.47 thf(f1581,plain,(
% 0.79/0.47 ( ! [X0 : mono_2Etyop_2Enum_2Enum,X1 : d] : ((((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Einteger__word_2Ei2w_2E1 @ (s @ tyop_2Einteger_2Eint @ (i_mono_2Etyop_2Einteger_2Eint @ (mono_2Ec_2Einteger_2Eint__of__num @ X0)))))) = ((s @ (tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ X1) @ (c_2Ewords_2En2w_2E1 @ (s @ tyop_2Enum_2Enum @ (i_mono_2Etyop_2Enum_2Enum @ X0))))))) ) | (~spl4_2 | ~spl4_3)),
% 0.79/0.47 inference(forward_demodulation,[],[f1576,f586])).
% 0.79/0.47 thf(f3508,plain,(
% 0.79/0.47 $false | (~spl4_2 | ~spl4_3)),
% 0.79/0.47 inference(backward_subsumption_resolution,[],[f269,f1581])).
% 0.79/0.47 thf(f3536,plain,(
% 0.79/0.47 ~spl4_2 | ~spl4_3),
% 0.79/0.47 inference(avatar_contradiction_clause,[],[f3508])).
% 0.79/0.47 thf(f3584,plain,(
% 0.79/0.47 $false | ~spl4_5),
% 0.79/0.47 inference(backward_subsumption_resolution,[],[f270,f358])).
% 0.79/0.47 thf(f3651,plain,(
% 0.79/0.47 ~spl4_5),
% 0.79/0.47 inference(avatar_contradiction_clause,[],[f3584])).
% 0.79/0.47 thf(f3672,plain,(
% 0.79/0.47 ($true != $true) | (mono_2Ec_2Ebool_2EF = $false) | (spl4_4 | ~spl4_6)),
% 0.79/0.47 inference(constrained_superposition,[],[f353,f362])).
% 0.79/0.47 thf(f3673,plain,(
% 0.79/0.47 (mono_2Ec_2Ebool_2EF = $false) | (spl4_4 | ~spl4_6)),
% 0.79/0.47 inference(trivial_inequality_removal,[],[f3672])).
% 0.79/0.47 thf(f3674,plain,(
% 0.79/0.47 $false | (spl4_2 | spl4_4 | ~spl4_6)),
% 0.79/0.47 inference(forward_subsumption_resolution,[],[f3673,f345])).
% 0.79/0.47 thf(f3675,plain,(
% 0.79/0.47 spl4_2 | spl4_4 | ~spl4_6),
% 0.79/0.47 inference(avatar_contradiction_clause,[],[f3674])).
% 0.79/0.47 cnf(s2, plain, spl4_3 | spl4_4, inference(sat_conversion,[],[f355])).
% 0.79/0.47 cnf(s3, plain, ~spl4_4 | spl4_5, inference(sat_conversion,[],[f359])).
% 0.79/0.47 cnf(s6, plain, spl4_6, inference(sat_conversion,[],[f365])).
% 0.79/0.47 cnf(s287, plain, ~spl4_2 | ~spl4_3, inference(sat_conversion,[],[f3536])).
% 0.79/0.47 cnf(s311, plain, ~spl4_5, inference(sat_conversion,[],[f3651])).
% 0.79/0.47 cnf(s316, plain, spl4_2 | spl4_4 | ~spl4_6, inference(sat_conversion,[],[f3675])).
% 0.79/0.47 cnf(s419, plain, ~spl4_4, inference(rat,[],[s3,s311])).
% 0.79/0.47 cnf(s420, plain, spl4_2, inference(rat,[],[s316,s6,s419])).
% 0.79/0.47 cnf(s421, plain, ~spl4_3, inference(rat,[],[s287,s420])).
% 0.79/0.47 cnf(s422, plain, $false, inference(rat,[],[s2,s419,s421])).
% 0.79/0.47 thf(f3676,plain,(
% 0.79/0.47 $false),
% 0.79/0.47 inference(avatar_sat_refutation,[],[s422])).
% 0.79/0.47 % SZS output end Proof for theBenchmark
% 0.79/0.47 % (242824)------------------------------
% 0.79/0.47 % (242824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.79/0.47 % (242824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.79/0.47 % (242824)CaDiCaL version: 2.1.3
% 0.79/0.47 % (242824)Termination reason: Refutation
% 0.79/0.47 % (242824)Time elapsed: 0.177 s
% 0.79/0.47 % (242824)Peak memory usage: 16 MB
% 0.79/0.47 % (242824)Instructions burned: 624 (million)
% 0.79/0.47 % (242813)Success in time 0.213 s
% 0.79/0.47 % Vampire exiting
%------------------------------------------------------------------------------