%------------------------------------------------------------------------------ % File : DT2H2X---1.9.5 % Problem : LCL932^1 : TPTP v9.3.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n001.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 : Mon Sep 7 11:35:11 AM UTC 2026 % Result : CounterSatisfiable 0.10s 0.46s % Output : Saturation 0.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL932^1 : TPTP v9.3.1. Released v7.5.0. % 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.10/0.36 % Computer : n001.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 5 06:04:16 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.10/0.39 ---- Original DTF file --- % 0.10/0.39 thf(spec,logic,$$dhol). % 0.10/0.39 %------------------------------------------------------------------------------ % 0.10/0.39 % File : LCL932^1 : TPTP v9.3.1. Released v7.5.0. % 0.10/0.39 % Domain : Logic Calculi (Quantified Boolean Formulae) % 0.10/0.39 % Problem : ProofGold problem QBF_12_neg_th0 % 0.10/0.39 % Version : Especial. % 0.10/0.39 % English : % 0.10/0.39 % 0.10/0.39 % Refs : [Urb20] Urban (2020) Email to Geoff Sutcliffe % 0.10/0.39 % Source : [Urb20] % 0.10/0.39 % Names : QBF_12_neg_th0.p [Urb20] % 0.10/0.39 % 0.10/0.39 % Status : Unknown % 0.10/0.39 % Rating : 1.00 v7.5.0 % 0.10/0.39 % Syntax : Number of formulae : 213 ( 99 unt; 104 typ; 0 def) % 0.10/0.39 % Number of atoms : 895 ( 135 equ; 0 cnn) % 0.10/0.39 % Maximal formula atoms : 416 ( 8 avg) % 0.10/0.39 % Number of connectives : 1910 ( 0 ~; 0 |; 0 &;1632 @) % 0.10/0.39 % ( 0 <=>; 278 =>; 0 <=; 0 <~>) % 0.10/0.39 % Maximal formula depth : 98 ( 3 avg) % 0.10/0.39 % Number of types : 2 ( 0 usr) % 0.10/0.39 % Number of type conns : 557 ( 557 >; 0 *; 0 +; 0 <<) % 0.10/0.39 % Number of symbols : 105 ( 104 usr; 3 con; 0-14 aty) % 0.10/0.39 % Number of variables : 457 ( 275 ^; 145 !; 37 ?; 457 :) % 0.10/0.39 % SPC : TH0_UNK_EQU_NAR_NDT % 0.10/0.39 % 0.10/0.39 % Comments : See https://proofgold.org % 0.10/0.39 %------------------------------------------------------------------------------ % 0.10/0.39 thf(c_Eps_i_tp,type, % 0.10/0.39 c_Eps_i: ( $i > $o ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_False_tp,type, % 0.10/0.39 c_False: $o ). % 0.10/0.39 % 0.10/0.39 thf(c_True_tp,type, % 0.10/0.39 c_True: $o ). % 0.10/0.39 % 0.10/0.39 thf(c_not_tp,type, % 0.10/0.39 c_not: $o > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_and_tp,type, % 0.10/0.39 c_and: $o > $o > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_or_tp,type, % 0.10/0.39 c_or: $o > $o > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_iff_tp,type, % 0.10/0.39 c_iff: $o > $o > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_In_tp,type, % 0.10/0.39 c_In: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_Subq_tp,type, % 0.10/0.39 c_Subq: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_Empty_tp,type, % 0.10/0.39 c_Empty: $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Union_tp,type, % 0.10/0.39 c_Union: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Power_tp,type, % 0.10/0.39 c_Power: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Repl_tp,type, % 0.10/0.39 c_Repl: $i > ( $i > $i ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_TransSet_tp,type, % 0.10/0.39 c_TransSet: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_atleast2_tp,type, % 0.10/0.39 c_atleast2: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_atleast3_tp,type, % 0.10/0.39 c_atleast3: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_atleast4_tp,type, % 0.10/0.39 c_atleast4: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_atleast5_tp,type, % 0.10/0.39 c_atleast5: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_atleast6_tp,type, % 0.10/0.39 c_atleast6: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_exactly2_tp,type, % 0.10/0.39 c_exactly2: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_exactly3_tp,type, % 0.10/0.39 c_exactly3: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_exactly4_tp,type, % 0.10/0.39 c_exactly4: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_exactly5_tp,type, % 0.10/0.39 c_exactly5: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_exu_i_tp,type, % 0.10/0.39 c_exu_i: ( $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_reflexive_i_tp,type, % 0.10/0.39 c_reflexive_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_irreflexive_i_tp,type, % 0.10/0.39 c_irreflexive_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_symmetric_i_tp,type, % 0.10/0.39 c_symmetric_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_antisymmetric_i_tp,type, % 0.10/0.39 c_antisymmetric_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_transitive_i_tp,type, % 0.10/0.39 c_transitive_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_eqreln_i_tp,type, % 0.10/0.39 c_eqreln_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_per_i_tp,type, % 0.10/0.39 c_per_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_linear_i_tp,type, % 0.10/0.39 c_linear_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_trichotomous_or_i_tp,type, % 0.10/0.39 c_trichotomous_or_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_partialorder_i_tp,type, % 0.10/0.39 c_partialorder_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_totalorder_i_tp,type, % 0.10/0.39 c_totalorder_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_strictpartialorder_i_tp,type, % 0.10/0.39 c_strictpartialorder_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_stricttotalorder_i_tp,type, % 0.10/0.39 c_stricttotalorder_i: ( $i > $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_If_i_tp,type, % 0.10/0.39 c_If_i: $o > $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_exactly1of2_tp,type, % 0.10/0.39 c_exactly1of2: $o > $o > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_exactly1of3_tp,type, % 0.10/0.39 c_exactly1of3: $o > $o > $o > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_nIn_tp,type, % 0.10/0.39 c_nIn: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_nSubq_tp,type, % 0.10/0.39 c_nSubq: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_UPair_tp,type, % 0.10/0.39 c_UPair: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Sing_tp,type, % 0.10/0.39 c_Sing: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_binunion_tp,type, % 0.10/0.39 c_binunion: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_SetAdjoin_tp,type, % 0.10/0.39 c_SetAdjoin: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_famunion_tp,type, % 0.10/0.39 c_famunion: $i > ( $i > $i ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Sep_tp,type, % 0.10/0.39 c_Sep: $i > ( $i > $o ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_ReplSep_tp,type, % 0.10/0.39 c_ReplSep: $i > ( $i > $o ) > ( $i > $i ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_binintersect_tp,type, % 0.10/0.39 c_binintersect: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_setminus_tp,type, % 0.10/0.39 c_setminus: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_inj_tp,type, % 0.10/0.39 c_inj: $i > $i > ( $i > $i ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_bij_tp,type, % 0.10/0.39 c_bij: $i > $i > ( $i > $i ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_atleastp_tp,type, % 0.10/0.39 c_atleastp: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_equip_tp,type, % 0.10/0.39 c_equip: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_In_rec_poly_G_i_tp,type, % 0.10/0.39 c_In_rec_poly_G_i: ( $i > ( $i > $i ) > $i ) > $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_In_rec_poly_i_tp,type, % 0.10/0.39 c_In_rec_poly_i: ( $i > ( $i > $i ) > $i ) > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_ordsucc_tp,type, % 0.10/0.39 c_ordsucc: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_nat_p_tp,type, % 0.10/0.39 c_nat_p: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_nat_primrec_tp,type, % 0.10/0.39 c_nat_primrec: $i > ( $i > $i > $i ) > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_add_nat_tp,type, % 0.10/0.39 c_add_nat: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_mul_nat_tp,type, % 0.10/0.39 c_mul_nat: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_ordinal_tp,type, % 0.10/0.39 c_ordinal: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_V__tp,type, % 0.10/0.39 c_V_: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Inj1_tp,type, % 0.10/0.39 c_Inj1: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Inj0_tp,type, % 0.10/0.39 c_Inj0: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Unj_tp,type, % 0.10/0.39 c_Unj: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_combine_funcs_tp,type, % 0.10/0.39 c_combine_funcs: $i > $i > ( $i > $i ) > ( $i > $i ) > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_setsum_tp,type, % 0.10/0.39 c_setsum: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_proj0_tp,type, % 0.10/0.39 c_proj0: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_proj1_tp,type, % 0.10/0.39 c_proj1: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_binrep_tp,type, % 0.10/0.39 c_binrep: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_lam_tp,type, % 0.10/0.39 c_lam: $i > ( $i > $i ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_setprod_tp,type, % 0.10/0.39 c_setprod: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_ap_tp,type, % 0.10/0.39 c_ap: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_setsum_p_tp,type, % 0.10/0.39 c_setsum_p: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_tuple_p_tp,type, % 0.10/0.39 c_tuple_p: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_Pi_tp,type, % 0.10/0.39 c_Pi: $i > ( $i > $i ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_setexp_tp,type, % 0.10/0.39 c_setexp: $i > $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_Sep2_tp,type, % 0.10/0.39 c_Sep2: $i > ( $i > $i ) > ( $i > $i > $o ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_set_of_pairs_tp,type, % 0.10/0.39 c_set_of_pairs: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_lam2_tp,type, % 0.10/0.39 c_lam2: $i > ( $i > $i ) > ( $i > $i > $i ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_PNoEq__tp,type, % 0.10/0.39 c_PNoEq_: $i > ( $i > $o ) > ( $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_PNoLt__tp,type, % 0.10/0.39 c_PNoLt_: $i > ( $i > $o ) > ( $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_PNoLt_tp,type, % 0.10/0.39 c_PNoLt: $i > ( $i > $o ) > $i > ( $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_PNoLe_tp,type, % 0.10/0.39 c_PNoLe: $i > ( $i > $o ) > $i > ( $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_PNo_downc_tp,type, % 0.10/0.39 c_PNo_downc: ( $i > ( $i > $o ) > $o ) > $i > ( $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_PNo_upc_tp,type, % 0.10/0.39 c_PNo_upc: ( $i > ( $i > $o ) > $o ) > $i > ( $i > $o ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_SNoElts__tp,type, % 0.10/0.39 c_SNoElts_: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_SNo__tp,type, % 0.10/0.39 c_SNo_: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_PSNo_tp,type, % 0.10/0.39 c_PSNo: $i > ( $i > $o ) > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_SNo_tp,type, % 0.10/0.39 c_SNo: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_SNoLev_tp,type, % 0.10/0.39 c_SNoLev: $i > $i ). % 0.10/0.39 % 0.10/0.39 thf(c_SNoEq__tp,type, % 0.10/0.39 c_SNoEq_: $i > $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_SNoLt_tp,type, % 0.10/0.39 c_SNoLt: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_SNoLe_tp,type, % 0.10/0.39 c_SNoLe: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_binop_on_tp,type, % 0.10/0.39 c_binop_on: $i > ( $i > $i > $i ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_Loop_tp,type, % 0.10/0.39 c_Loop: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_Loop_with_defs_tp,type, % 0.10/0.39 c_Loop_with_defs: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $i > ( $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_Loop_with_defs_cex1_tp,type, % 0.10/0.39 c_Loop_with_defs_cex1: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $i > ( $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_Loop_with_defs_cex2_tp,type, % 0.10/0.39 c_Loop_with_defs_cex2: $i > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $i > ( $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > ( $i > $i > $i ) > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_combinator_tp,type, % 0.10/0.39 c_combinator: $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_combinator_equiv_tp,type, % 0.10/0.39 c_combinator_equiv: $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(c_equip_mod_tp,type, % 0.10/0.39 c_equip_mod: $i > $i > $i > $o ). % 0.10/0.39 % 0.10/0.39 thf(ax1,axiom, % 0.10/0.39 ! [X0: $i > $o,X1: $i] : % 0.10/0.39 ( ( X0 @ X1 ) % 0.10/0.39 => ( X0 @ ( c_Eps_i @ X0 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax2,axiom, % 0.10/0.39 ! [X0: $o] : % 0.10/0.39 ( ( c_not @ ( c_not @ X0 ) ) % 0.10/0.39 => X0 ) ). % 0.10/0.39 % 0.10/0.39 thf(ax3,axiom, % 0.10/0.39 ! [X0: $o,X1: $o] : % 0.10/0.39 ( ( c_iff @ X0 @ X1 ) % 0.10/0.39 => ( X0 = X1 ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax4,axiom, % 0.10/0.39 ! [X0: $i,X1: $i] : % 0.10/0.39 ( ( c_Subq @ X0 @ X1 ) % 0.10/0.39 => ( ( c_Subq @ X1 @ X0 ) % 0.10/0.39 => ( X0 = X1 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax5,axiom, % 0.10/0.39 ( c_not % 0.10/0.39 @ ? [X0: $i] : ( c_In @ X0 @ c_Empty ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax6,axiom, % 0.10/0.39 ! [X0: $i,X1: $i] : % 0.10/0.39 ( c_iff @ ( c_In @ X1 @ ( c_Union @ X0 ) ) % 0.10/0.39 @ ? [X2: $i] : ( c_and @ ( c_In @ X1 @ X2 ) @ ( c_In @ X2 @ X0 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax7,axiom, % 0.10/0.39 ! [X0: $i,X1: $i] : ( c_iff @ ( c_In @ X1 @ ( c_Power @ X0 ) ) @ ( c_Subq @ X1 @ X0 ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax8,axiom, % 0.10/0.39 ! [X0: $i,X1: $i > $i,X2: $i] : % 0.10/0.39 ( c_iff % 0.10/0.39 @ ( c_In @ X2 % 0.10/0.39 @ ( c_Repl @ X0 % 0.10/0.39 @ ^ [X3: $i] : ( X1 @ X3 ) ) ) % 0.10/0.39 @ ? [X3: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X3 @ X0 ) % 0.10/0.39 @ ( X2 % 0.10/0.39 = ( X1 @ X3 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax9,axiom, % 0.10/0.39 ! [X0: $i > $o] : % 0.10/0.39 ( ! [X1: $i] : % 0.10/0.39 ( ( X0 @ X1 ) % 0.10/0.39 => ! [X2: $i] : % 0.10/0.39 ( ( c_In @ X2 @ X1 ) % 0.10/0.39 => ( X0 @ X2 ) ) ) % 0.10/0.39 => ( ( X0 @ c_Empty ) % 0.10/0.39 => ( ! [X1: $i] : % 0.10/0.39 ( ( X0 @ X1 ) % 0.10/0.39 => ( X0 @ ( c_Union @ X1 ) ) ) % 0.10/0.39 => ( ! [X1: $i] : % 0.10/0.39 ( ( X0 @ X1 ) % 0.10/0.39 => ( X0 @ ( c_Power @ X1 ) ) ) % 0.10/0.39 => ( ! [X1: $i] : % 0.10/0.39 ( ( X0 @ X1 ) % 0.10/0.39 => ! [X2: $i > $i] : % 0.10/0.39 ( ! [X3: $i] : % 0.10/0.39 ( ( c_In @ X3 @ X1 ) % 0.10/0.39 => ( X0 @ ( X2 @ X3 ) ) ) % 0.10/0.39 => ( X0 % 0.10/0.39 @ ( c_Repl @ X1 % 0.10/0.39 @ ^ [X3: $i] : ( X2 @ X3 ) ) ) ) ) % 0.10/0.39 => ! [X1: $i] : ( X0 @ X1 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax10,axiom, % 0.10/0.39 ! [X0: $i > $o] : % 0.10/0.39 ( ! [X1: $i] : % 0.10/0.39 ( ! [X2: $i] : % 0.10/0.39 ( ( c_In @ X2 @ X1 ) % 0.10/0.39 => ( X0 @ X2 ) ) % 0.10/0.39 => ( X0 @ X1 ) ) % 0.10/0.39 => ! [X1: $i] : ( X0 @ X1 ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax11,axiom, % 0.10/0.39 ( c_False % 0.10/0.39 = ( ! [X0: $o] : X0 ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax12,axiom, % 0.10/0.39 ( c_True % 0.10/0.39 = ( ! [X0: $o] : % 0.10/0.39 ( X0 % 0.10/0.39 => X0 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax13,axiom, % 0.10/0.39 ( c_not % 0.10/0.39 = ( ^ [X0: $o] : % 0.10/0.39 ( X0 % 0.10/0.39 => c_False ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax14,axiom, % 0.10/0.39 ( c_and % 0.10/0.39 = ( ^ [X0: $o,X1: $o] : % 0.10/0.39 ! [X2: $o] : % 0.10/0.39 ( ( X0 % 0.10/0.39 => ( X1 % 0.10/0.39 => X2 ) ) % 0.10/0.39 => X2 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax15,axiom, % 0.10/0.39 ( c_or % 0.10/0.39 = ( ^ [X0: $o,X1: $o] : % 0.10/0.39 ! [X2: $o] : % 0.10/0.39 ( ( X0 % 0.10/0.39 => X2 ) % 0.10/0.39 => ( ( X1 % 0.10/0.39 => X2 ) % 0.10/0.39 => X2 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax16,axiom, % 0.10/0.39 ( c_iff % 0.10/0.39 = ( ^ [X0: $o,X1: $o] : % 0.10/0.39 ( c_and % 0.10/0.39 @ ( X0 % 0.10/0.39 => X1 ) % 0.10/0.39 @ ( X1 % 0.10/0.39 => X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax17,axiom, % 0.10/0.39 ( c_Subq % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ! [X2: $i] : % 0.10/0.39 ( ( c_In @ X2 @ X0 ) % 0.10/0.39 => ( c_In @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax18,axiom, % 0.10/0.39 ( c_TransSet % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ! [X1: $i] : % 0.10/0.39 ( ( c_In @ X1 @ X0 ) % 0.10/0.39 => ( c_Subq @ X1 @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax19,axiom, % 0.10/0.39 ( c_atleast2 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ? [X1: $i] : ( c_and @ ( c_In @ X1 @ X0 ) @ ( c_not @ ( c_Subq @ X0 @ ( c_Power @ X1 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax20,axiom, % 0.10/0.39 ( c_atleast3 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ? [X1: $i] : ( c_and @ ( c_Subq @ X1 @ X0 ) @ ( c_and @ ( c_not @ ( c_Subq @ X0 @ X1 ) ) @ ( c_atleast2 @ X1 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax21,axiom, % 0.10/0.39 ( c_atleast4 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ? [X1: $i] : ( c_and @ ( c_Subq @ X1 @ X0 ) @ ( c_and @ ( c_not @ ( c_Subq @ X0 @ X1 ) ) @ ( c_atleast3 @ X1 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax22,axiom, % 0.10/0.39 ( c_atleast5 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ? [X1: $i] : ( c_and @ ( c_Subq @ X1 @ X0 ) @ ( c_and @ ( c_not @ ( c_Subq @ X0 @ X1 ) ) @ ( c_atleast4 @ X1 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax23,axiom, % 0.10/0.39 ( c_atleast6 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ? [X1: $i] : ( c_and @ ( c_Subq @ X1 @ X0 ) @ ( c_and @ ( c_not @ ( c_Subq @ X0 @ X1 ) ) @ ( c_atleast5 @ X1 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax24,axiom, % 0.10/0.39 ( c_exactly2 % 0.10/0.39 = ( ^ [X0: $i] : ( c_and @ ( c_atleast2 @ X0 ) @ ( c_not @ ( c_atleast3 @ X0 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax25,axiom, % 0.10/0.39 ( c_exactly3 % 0.10/0.39 = ( ^ [X0: $i] : ( c_and @ ( c_atleast3 @ X0 ) @ ( c_not @ ( c_atleast4 @ X0 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax26,axiom, % 0.10/0.39 ( c_exactly4 % 0.10/0.39 = ( ^ [X0: $i] : ( c_and @ ( c_atleast4 @ X0 ) @ ( c_not @ ( c_atleast5 @ X0 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax27,axiom, % 0.10/0.39 ( c_exactly5 % 0.10/0.39 = ( ^ [X0: $i] : ( c_and @ ( c_atleast5 @ X0 ) @ ( c_not @ ( c_atleast6 @ X0 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax28,axiom, % 0.10/0.39 ( c_exu_i % 0.10/0.39 = ( ^ [X0: $i > $o] : % 0.10/0.39 ( c_and % 0.10/0.39 @ ? [X1: $i] : ( X0 @ X1 ) % 0.10/0.39 @ ! [X1: $i,X2: $i] : % 0.10/0.39 ( ( X0 @ X1 ) % 0.10/0.39 => ( ( X0 @ X2 ) % 0.10/0.39 => ( X1 = X2 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax29,axiom, % 0.10/0.39 ( c_reflexive_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : % 0.10/0.39 ! [X1: $i] : ( X0 @ X1 @ X1 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax30,axiom, % 0.10/0.39 ( c_irreflexive_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : % 0.10/0.39 ! [X1: $i] : ( c_not @ ( X0 @ X1 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax31,axiom, % 0.10/0.39 ( c_symmetric_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : % 0.10/0.39 ! [X1: $i,X2: $i] : % 0.10/0.39 ( ( X0 @ X1 @ X2 ) % 0.10/0.39 => ( X0 @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax32,axiom, % 0.10/0.39 ( c_antisymmetric_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : % 0.10/0.39 ! [X1: $i,X2: $i] : % 0.10/0.39 ( ( X0 @ X1 @ X2 ) % 0.10/0.39 => ( ( X0 @ X2 @ X1 ) % 0.10/0.39 => ( X1 = X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax33,axiom, % 0.10/0.39 ( c_transitive_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : % 0.10/0.39 ! [X1: $i,X2: $i,X3: $i] : % 0.10/0.39 ( ( X0 @ X1 @ X2 ) % 0.10/0.39 => ( ( X0 @ X2 @ X3 ) % 0.10/0.39 => ( X0 @ X1 @ X3 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax34,axiom, % 0.10/0.39 ( c_eqreln_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : ( c_and @ ( c_and @ ( c_reflexive_i @ X0 ) @ ( c_symmetric_i @ X0 ) ) @ ( c_transitive_i @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax35,axiom, % 0.10/0.39 ( c_per_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : ( c_and @ ( c_symmetric_i @ X0 ) @ ( c_transitive_i @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax36,axiom, % 0.10/0.39 ( c_linear_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : % 0.10/0.39 ! [X1: $i,X2: $i] : ( c_or @ ( X0 @ X1 @ X2 ) @ ( X0 @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax37,axiom, % 0.10/0.39 ( c_trichotomous_or_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : % 0.10/0.39 ! [X1: $i,X2: $i] : ( c_or @ ( c_or @ ( X0 @ X1 @ X2 ) @ ( X1 = X2 ) ) @ ( X0 @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax38,axiom, % 0.10/0.39 ( c_partialorder_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : ( c_and @ ( c_and @ ( c_reflexive_i @ X0 ) @ ( c_antisymmetric_i @ X0 ) ) @ ( c_transitive_i @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax39,axiom, % 0.10/0.39 ( c_totalorder_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : ( c_and @ ( c_partialorder_i @ X0 ) @ ( c_linear_i @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax40,axiom, % 0.10/0.39 ( c_strictpartialorder_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : ( c_and @ ( c_irreflexive_i @ X0 ) @ ( c_transitive_i @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax41,axiom, % 0.10/0.39 ( c_stricttotalorder_i % 0.10/0.39 = ( ^ [X0: $i > $i > $o] : ( c_and @ ( c_strictpartialorder_i @ X0 ) @ ( c_trichotomous_or_i @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax42,axiom, % 0.10/0.39 ( c_If_i % 0.10/0.39 = ( ^ [X0: $o,X1: $i,X2: $i] : % 0.10/0.39 ( c_Eps_i % 0.10/0.39 @ ^ [X3: $i] : ( c_or @ ( c_and @ X0 @ ( X3 = X1 ) ) @ ( c_and @ ( c_not @ X0 ) @ ( X3 = X2 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax43,axiom, % 0.10/0.39 ( c_exactly1of2 % 0.10/0.39 = ( ^ [X0: $o,X1: $o] : ( c_or @ ( c_and @ X0 @ ( c_not @ X1 ) ) @ ( c_and @ ( c_not @ X0 ) @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax44,axiom, % 0.10/0.39 ( c_exactly1of3 % 0.10/0.39 = ( ^ [X0: $o,X1: $o,X2: $o] : ( c_or @ ( c_and @ ( c_exactly1of2 @ X0 @ X1 ) @ ( c_not @ X2 ) ) @ ( c_and @ ( c_and @ ( c_not @ X0 ) @ ( c_not @ X1 ) ) @ X2 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax45,axiom, % 0.10/0.39 ( c_nIn % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : ( c_not @ ( c_In @ X0 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax46,axiom, % 0.10/0.39 ( c_nSubq % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : ( c_not @ ( c_Subq @ X0 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax47,axiom, % 0.10/0.39 ( c_UPair % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_Repl @ ( c_Power @ ( c_Power @ c_Empty ) ) % 0.10/0.39 @ ^ [X2: $i] : ( c_If_i @ ( c_In @ c_Empty @ X2 ) @ X0 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax48,axiom, % 0.10/0.39 ( c_Sing % 0.10/0.39 = ( ^ [X0: $i] : ( c_UPair @ X0 @ X0 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax49,axiom, % 0.10/0.39 ( c_binunion % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : ( c_Union @ ( c_UPair @ X0 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax50,axiom, % 0.10/0.39 ( c_SetAdjoin % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : ( c_binunion @ X0 @ ( c_Sing @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax51,axiom, % 0.10/0.39 ( c_famunion % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i] : % 0.10/0.39 ( c_Union % 0.10/0.39 @ ( c_Repl @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( X1 @ X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax52,axiom, % 0.10/0.39 ( c_Sep % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $o] : % 0.10/0.39 ( c_If_i % 0.10/0.39 @ ? [X2: $i] : ( c_and @ ( c_In @ X2 @ X0 ) @ ( X1 @ X2 ) ) % 0.10/0.39 @ ( c_Repl @ X0 % 0.10/0.39 @ ^ [X2: $i] : % 0.10/0.39 ( ^ [X3: $i] : % 0.10/0.39 ( c_If_i @ ( X1 @ X3 ) @ X3 % 0.10/0.39 @ ( c_Eps_i % 0.10/0.39 @ ^ [X4: $i] : ( c_and @ ( c_In @ X4 @ X0 ) @ ( X1 @ X4 ) ) ) ) % 0.10/0.39 @ X2 ) ) % 0.10/0.39 @ c_Empty ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax53,axiom, % 0.10/0.39 ( c_ReplSep % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $o,X2: $i > $i] : % 0.10/0.39 ( c_Repl % 0.10/0.39 @ ( c_Sep @ X0 % 0.10/0.39 @ ^ [X3: $i] : ( X1 @ X3 ) ) % 0.10/0.39 @ ^ [X3: $i] : ( X2 @ X3 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax54,axiom, % 0.10/0.39 ( c_binintersect % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_Sep @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( c_In @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax55,axiom, % 0.10/0.39 ( c_setminus % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_Sep @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( c_nIn @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax56,axiom, % 0.10/0.39 ( c_inj % 0.10/0.39 = ( ^ [X0: $i,X1: $i,X2: $i > $i] : % 0.10/0.39 ( c_and % 0.10/0.39 @ ! [X3: $i] : % 0.10/0.39 ( ( c_In @ X3 @ X0 ) % 0.10/0.39 => ( c_In @ ( X2 @ X3 ) @ X1 ) ) % 0.10/0.39 @ ! [X3: $i] : % 0.10/0.39 ( ( c_In @ X3 @ X0 ) % 0.10/0.39 => ! [X4: $i] : % 0.10/0.39 ( ( c_In @ X4 @ X0 ) % 0.10/0.39 => ( ( ( X2 @ X3 ) % 0.10/0.39 = ( X2 @ X4 ) ) % 0.10/0.39 => ( X3 = X4 ) ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax57,axiom, % 0.10/0.39 ( c_bij % 0.10/0.39 = ( ^ [X0: $i,X1: $i,X2: $i > $i] : % 0.10/0.39 ( c_and @ ( c_inj @ X0 @ X1 @ X2 ) % 0.10/0.39 @ ! [X3: $i] : % 0.10/0.39 ( ( c_In @ X3 @ X1 ) % 0.10/0.39 => ? [X4: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X4 @ X0 ) % 0.10/0.39 @ ( ( X2 @ X4 ) % 0.10/0.39 = X3 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax58,axiom, % 0.10/0.39 ( c_atleastp % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ? [X2: $i > $i] : ( c_inj @ X0 @ X1 @ X2 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax59,axiom, % 0.10/0.39 ( c_equip % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ? [X2: $i > $i] : ( c_bij @ X0 @ X1 @ X2 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax60,axiom, % 0.10/0.39 ( c_In_rec_poly_G_i % 0.10/0.39 = ( ^ [X0: $i > ( $i > $i ) > $i,X1: $i,X2: $i] : % 0.10/0.39 ! [X3: $i > $i > $o] : % 0.10/0.39 ( ! [X4: $i,X5: $i > $i] : % 0.10/0.39 ( ! [X6: $i] : % 0.10/0.39 ( ( c_In @ X6 @ X4 ) % 0.10/0.39 => ( X3 @ X6 @ ( X5 @ X6 ) ) ) % 0.10/0.39 => ( X3 @ X4 @ ( X0 @ X4 @ X5 ) ) ) % 0.10/0.39 => ( X3 @ X1 @ X2 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax61,axiom, % 0.10/0.39 ( c_In_rec_poly_i % 0.10/0.39 = ( ^ [X0: $i > ( $i > $i ) > $i,X1: $i] : % 0.10/0.39 ( c_Eps_i % 0.10/0.39 @ ^ [X2: $i] : ( c_In_rec_poly_G_i @ X0 @ X1 @ X2 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax62,axiom, % 0.10/0.39 ( c_ordsucc % 0.10/0.39 = ( ^ [X0: $i] : ( c_binunion @ X0 @ ( c_Sing @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax63,axiom, % 0.10/0.39 ( c_nat_p % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ! [X1: $i > $o] : % 0.10/0.39 ( ( X1 @ c_Empty ) % 0.10/0.39 => ( ! [X2: $i] : % 0.10/0.39 ( ( X1 @ X2 ) % 0.10/0.39 => ( X1 @ ( c_ordsucc @ X2 ) ) ) % 0.10/0.39 => ( X1 @ X0 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax64,axiom, % 0.10/0.39 ( c_nat_primrec % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i > $i] : % 0.10/0.39 ( c_In_rec_poly_i % 0.10/0.39 @ ^ [X2: $i,X3: $i > $i] : ( c_If_i @ ( c_In @ ( c_Union @ X2 ) @ X2 ) @ ( X1 @ ( c_Union @ X2 ) @ ( X3 @ ( c_Union @ X2 ) ) ) @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax65,axiom, % 0.10/0.39 ( c_add_nat % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_nat_primrec @ X0 % 0.10/0.39 @ ^ [X2: $i,X3: $i] : ( c_ordsucc @ X3 ) % 0.10/0.39 @ X1 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax66,axiom, % 0.10/0.39 ( c_mul_nat % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_nat_primrec @ c_Empty % 0.10/0.39 @ ^ [X2: $i,X3: $i] : ( c_add_nat @ X0 @ X3 ) % 0.10/0.39 @ X1 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax67,axiom, % 0.10/0.39 ( c_ordinal % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ( c_and @ ( c_TransSet @ X0 ) % 0.10/0.39 @ ! [X1: $i] : % 0.10/0.39 ( ( c_In @ X1 @ X0 ) % 0.10/0.39 => ( c_TransSet @ X1 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax68,axiom, % 0.10/0.39 ( c_V_ % 0.10/0.39 = ( c_In_rec_poly_i % 0.10/0.39 @ ^ [X0: $i,X1: $i > $i] : % 0.10/0.39 ( c_famunion @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( c_Power @ ( X1 @ X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax69,axiom, % 0.10/0.39 ( c_Inj1 % 0.10/0.39 = ( c_In_rec_poly_i % 0.10/0.39 @ ^ [X0: $i,X1: $i > $i] : % 0.10/0.39 ( c_binunion @ ( c_Sing @ c_Empty ) % 0.10/0.39 @ ( c_Repl @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( X1 @ X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax70,axiom, % 0.10/0.39 ( c_Inj0 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ( c_Repl @ X0 % 0.10/0.39 @ ^ [X1: $i] : ( c_Inj1 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax71,axiom, % 0.10/0.39 ( c_Unj % 0.10/0.39 = ( c_In_rec_poly_i % 0.10/0.39 @ ^ [X0: $i,X1: $i > $i] : % 0.10/0.39 ( c_Repl @ ( c_setminus @ X0 @ ( c_Sing @ c_Empty ) ) % 0.10/0.39 @ ^ [X2: $i] : ( X1 @ X2 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax72,axiom, % 0.10/0.39 ( c_combine_funcs % 0.10/0.39 = ( ^ [X0: $i,X1: $i,X2: $i > $i,X3: $i > $i,X4: $i] : % 0.10/0.39 ( c_If_i % 0.10/0.39 @ ( X4 % 0.10/0.39 = ( c_Inj0 @ ( c_Unj @ X4 ) ) ) % 0.10/0.39 @ ( X2 @ ( c_Unj @ X4 ) ) % 0.10/0.39 @ ( X3 @ ( c_Unj @ X4 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax73,axiom, % 0.10/0.39 ( c_setsum % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_binunion % 0.10/0.39 @ ( c_Repl @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( c_Inj0 @ X2 ) ) % 0.10/0.39 @ ( c_Repl @ X1 % 0.10/0.39 @ ^ [X2: $i] : ( c_Inj1 @ X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax74,axiom, % 0.10/0.39 ( c_proj0 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ( c_ReplSep @ X0 % 0.10/0.39 @ ^ [X1: $i] : % 0.10/0.39 ? [X2: $i] : % 0.10/0.39 ( ( c_Inj0 @ X2 ) % 0.10/0.39 = X1 ) % 0.10/0.39 @ ^ [X1: $i] : ( c_Unj @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax75,axiom, % 0.10/0.39 ( c_proj1 % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ( c_ReplSep @ X0 % 0.10/0.39 @ ^ [X1: $i] : % 0.10/0.39 ? [X2: $i] : % 0.10/0.39 ( ( c_Inj1 @ X2 ) % 0.10/0.39 = X1 ) % 0.10/0.39 @ ^ [X1: $i] : ( c_Unj @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax76,axiom, % 0.10/0.39 ( c_binrep % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : ( c_setsum @ X0 @ ( c_Power @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax77,axiom, % 0.10/0.39 ( c_lam % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i] : % 0.10/0.39 ( c_famunion @ X0 % 0.10/0.39 @ ^ [X2: $i] : % 0.10/0.39 ( c_Repl @ ( X1 @ X2 ) % 0.10/0.39 @ ^ [X3: $i] : ( c_setsum @ X2 @ X3 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax78,axiom, % 0.10/0.39 ( c_setprod % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_lam @ X0 % 0.10/0.39 @ ^ [X2: $i] : X1 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax79,axiom, % 0.10/0.39 ( c_ap % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_ReplSep @ X0 % 0.10/0.39 @ ^ [X2: $i] : % 0.10/0.39 ? [X3: $i] : % 0.10/0.39 ( X2 % 0.10/0.39 = ( c_setsum @ X1 @ X3 ) ) % 0.10/0.39 @ ^ [X2: $i] : ( c_proj1 @ X2 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax80,axiom, % 0.10/0.39 ( c_setsum_p % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ( ( c_setsum @ ( c_ap @ X0 @ c_Empty ) @ ( c_ap @ X0 @ ( c_ordsucc @ c_Empty ) ) ) % 0.10/0.39 = X0 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax81,axiom, % 0.10/0.39 ( c_tuple_p % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ! [X2: $i] : % 0.10/0.39 ( ( c_In @ X2 @ X1 ) % 0.10/0.39 => ? [X3: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X3 @ X0 ) % 0.10/0.39 @ ? [X4: $i] : % 0.10/0.39 ( X2 % 0.10/0.39 = ( c_setsum @ X3 @ X4 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax82,axiom, % 0.10/0.39 ( c_Pi % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i] : % 0.10/0.39 ( c_Sep % 0.10/0.39 @ ( c_Power % 0.10/0.39 @ ( c_lam @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( c_Union @ ( X1 @ X2 ) ) ) ) % 0.10/0.39 @ ^ [X2: $i] : % 0.10/0.39 ! [X3: $i] : % 0.10/0.39 ( ( c_In @ X3 @ X0 ) % 0.10/0.39 => ( c_In @ ( c_ap @ X2 @ X3 ) @ ( X1 @ X3 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax83,axiom, % 0.10/0.39 ( c_setexp % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_Pi @ X1 % 0.10/0.39 @ ^ [X2: $i] : X0 ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax84,axiom, % 0.10/0.39 ( c_Sep2 % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i,X2: $i > $i > $o] : % 0.10/0.39 ( c_Sep % 0.10/0.39 @ ( c_lam @ X0 % 0.10/0.39 @ ^ [X3: $i] : ( X1 @ X3 ) ) % 0.10/0.39 @ ^ [X3: $i] : ( X2 @ ( c_ap @ X3 @ c_Empty ) @ ( c_ap @ X3 @ ( c_ordsucc @ c_Empty ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax85,axiom, % 0.10/0.39 ( c_set_of_pairs % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ! [X1: $i] : % 0.10/0.39 ( ( c_In @ X1 @ X0 ) % 0.10/0.39 => ? [X2: $i,X3: $i] : % 0.10/0.39 ( X1 % 0.10/0.39 = ( c_lam @ ( c_ordsucc @ ( c_ordsucc @ c_Empty ) ) % 0.10/0.39 @ ^ [X4: $i] : ( c_If_i @ ( X4 = c_Empty ) @ X2 @ X3 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax86,axiom, % 0.10/0.39 ( c_lam2 % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i,X2: $i > $i > $i] : % 0.10/0.39 ( c_lam @ X0 % 0.10/0.39 @ ^ [X3: $i] : % 0.10/0.39 ( c_lam @ ( X1 @ X3 ) % 0.10/0.39 @ ^ [X4: $i] : ( X2 @ X3 @ X4 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax87,axiom, % 0.10/0.39 ( c_PNoEq_ % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $o,X2: $i > $o] : % 0.10/0.39 ! [X3: $i] : % 0.10/0.39 ( ( c_In @ X3 @ X0 ) % 0.10/0.39 => ( c_iff @ ( X1 @ X3 ) @ ( X2 @ X3 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax88,axiom, % 0.10/0.39 ( c_PNoLt_ % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $o,X2: $i > $o] : % 0.10/0.39 ? [X3: $i] : ( c_and @ ( c_In @ X3 @ X0 ) @ ( c_and @ ( c_and @ ( c_PNoEq_ @ X3 @ X1 @ X2 ) @ ( c_not @ ( X1 @ X3 ) ) ) @ ( X2 @ X3 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax89,axiom, % 0.10/0.39 ( c_PNoLt % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $o,X2: $i,X3: $i > $o] : ( c_or @ ( c_or @ ( c_PNoLt_ @ ( c_binintersect @ X0 @ X2 ) @ X1 @ X3 ) @ ( c_and @ ( c_and @ ( c_In @ X0 @ X2 ) @ ( c_PNoEq_ @ X0 @ X1 @ X3 ) ) @ ( X3 @ X0 ) ) ) @ ( c_and @ ( c_and @ ( c_In @ X2 @ X0 ) @ ( c_PNoEq_ @ X2 @ X1 @ X3 ) ) @ ( c_not @ ( X1 @ X2 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax90,axiom, % 0.10/0.39 ( c_PNoLe % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $o,X2: $i,X3: $i > $o] : ( c_or @ ( c_PNoLt @ X0 @ X1 @ X2 @ X3 ) @ ( c_and @ ( X0 = X2 ) @ ( c_PNoEq_ @ X0 @ X1 @ X3 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax91,axiom, % 0.10/0.39 ( c_PNo_downc % 0.10/0.39 = ( ^ [X0: $i > ( $i > $o ) > $o,X1: $i,X2: $i > $o] : % 0.10/0.39 ? [X3: $i] : % 0.10/0.39 ( c_and @ ( c_ordinal @ X3 ) % 0.10/0.39 @ ? [X4: $i > $o] : ( c_and @ ( X0 @ X3 @ X4 ) @ ( c_PNoLe @ X1 @ X2 @ X3 @ X4 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax92,axiom, % 0.10/0.39 ( c_PNo_upc % 0.10/0.39 = ( ^ [X0: $i > ( $i > $o ) > $o,X1: $i,X2: $i > $o] : % 0.10/0.39 ? [X3: $i] : % 0.10/0.39 ( c_and @ ( c_ordinal @ X3 ) % 0.10/0.39 @ ? [X4: $i > $o] : ( c_and @ ( X0 @ X3 @ X4 ) @ ( c_PNoLe @ X3 @ X4 @ X1 @ X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax93,axiom, % 0.10/0.39 ( c_SNoElts_ % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ( c_binunion @ X0 % 0.10/0.39 @ ( c_Repl @ X0 % 0.10/0.39 @ ^ [X1: $i] : % 0.10/0.39 ( ^ [X2: $i] : ( c_SetAdjoin @ X2 @ ( c_Sing @ ( c_ordsucc @ c_Empty ) ) ) % 0.10/0.39 @ X1 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax94,axiom, % 0.10/0.39 ( c_SNo_ % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_and @ ( c_Subq @ X1 @ ( c_SNoElts_ @ X0 ) ) % 0.10/0.39 @ ! [X2: $i] : % 0.10/0.39 ( ( c_In @ X2 @ X0 ) % 0.10/0.39 => ( c_exactly1of2 % 0.10/0.39 @ ( c_In % 0.10/0.39 @ ( ^ [X3: $i] : ( c_SetAdjoin @ X3 @ ( c_Sing @ ( c_ordsucc @ c_Empty ) ) ) % 0.10/0.39 @ X2 ) % 0.10/0.39 @ X1 ) % 0.10/0.39 @ ( c_In @ X2 @ X1 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax95,axiom, % 0.10/0.39 ( c_PSNo % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $o] : % 0.10/0.39 ( c_binunion % 0.10/0.39 @ ( c_Sep @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( X1 @ X2 ) ) % 0.10/0.39 @ ( c_ReplSep @ X0 % 0.10/0.39 @ ^ [X2: $i] : ( c_not @ ( X1 @ X2 ) ) % 0.10/0.39 @ ^ [X2: $i] : % 0.10/0.39 ( ^ [X3: $i] : ( c_SetAdjoin @ X3 @ ( c_Sing @ ( c_ordsucc @ c_Empty ) ) ) % 0.10/0.39 @ X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax96,axiom, % 0.10/0.39 ( c_SNo % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ? [X1: $i] : ( c_and @ ( c_ordinal @ X1 ) @ ( c_SNo_ @ X1 @ X0 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax97,axiom, % 0.10/0.39 ( c_SNoLev % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ( c_Eps_i % 0.10/0.39 @ ^ [X1: $i] : ( c_and @ ( c_ordinal @ X1 ) @ ( c_SNo_ @ X1 @ X0 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax98,axiom, % 0.10/0.39 ( c_SNoEq_ % 0.10/0.39 = ( ^ [X0: $i,X1: $i,X2: $i] : % 0.10/0.39 ( c_PNoEq_ @ X0 % 0.10/0.39 @ ^ [X3: $i] : ( c_In @ X3 @ X1 ) % 0.10/0.39 @ ^ [X3: $i] : ( c_In @ X3 @ X2 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax99,axiom, % 0.10/0.39 ( c_SNoLt % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_PNoLt @ ( c_SNoLev @ X0 ) % 0.10/0.39 @ ^ [X2: $i] : ( c_In @ X2 @ X0 ) % 0.10/0.39 @ ( c_SNoLev @ X1 ) % 0.10/0.39 @ ^ [X2: $i] : ( c_In @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax100,axiom, % 0.10/0.39 ( c_SNoLe % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ( c_PNoLe @ ( c_SNoLev @ X0 ) % 0.10/0.39 @ ^ [X2: $i] : ( c_In @ X2 @ X0 ) % 0.10/0.39 @ ( c_SNoLev @ X1 ) % 0.10/0.39 @ ^ [X2: $i] : ( c_In @ X2 @ X1 ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax101,axiom, % 0.10/0.39 ( c_binop_on % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i > $i] : % 0.10/0.39 ! [X2: $i] : % 0.10/0.39 ( ( c_In @ X2 @ X0 ) % 0.10/0.39 => ! [X3: $i] : % 0.10/0.39 ( ( c_In @ X3 @ X0 ) % 0.10/0.39 => ( c_In @ ( X1 @ X2 @ X3 ) @ X0 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax102,axiom, % 0.10/0.39 ( c_Loop % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i > $i,X2: $i > $i > $i,X3: $i > $i > $i,X4: $i] : % 0.10/0.39 ( c_and % 0.10/0.39 @ ( c_and @ ( c_and @ ( c_and @ ( c_binop_on @ X0 @ X1 ) @ ( c_binop_on @ X0 @ X2 ) ) @ ( c_binop_on @ X0 @ X3 ) ) % 0.10/0.39 @ ! [X5: $i] : % 0.10/0.39 ( ( c_In @ X5 @ X0 ) % 0.10/0.39 => ( c_and % 0.10/0.39 @ ( ( X1 @ X4 @ X5 ) % 0.10/0.39 = X5 ) % 0.10/0.39 @ ( ( X1 @ X5 @ X4 ) % 0.10/0.39 = X5 ) ) ) ) % 0.10/0.39 @ ! [X5: $i] : % 0.10/0.39 ( ( c_In @ X5 @ X0 ) % 0.10/0.39 => ! [X6: $i] : % 0.10/0.39 ( ( c_In @ X6 @ X0 ) % 0.10/0.39 => ( c_and % 0.10/0.39 @ ( c_and % 0.10/0.39 @ ( c_and % 0.10/0.39 @ ( ( X2 @ X5 @ ( X1 @ X5 @ X6 ) ) % 0.10/0.39 = X6 ) % 0.10/0.39 @ ( ( X1 @ X5 @ ( X2 @ X5 @ X6 ) ) % 0.10/0.39 = X6 ) ) % 0.10/0.39 @ ( ( X3 @ ( X1 @ X5 @ X6 ) @ X6 ) % 0.10/0.39 = X5 ) ) % 0.10/0.39 @ ( ( X1 @ ( X3 @ X5 @ X6 ) @ X6 ) % 0.10/0.39 = X5 ) ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax103,axiom, % 0.10/0.39 ( c_Loop_with_defs % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i > $i,X2: $i > $i > $i,X3: $i > $i > $i,X4: $i,X5: $i > $i > $i,X6: $i > $i > $i > $i,X7: $i > $i > $i,X8: $i > $i > $i > $i,X9: $i > $i > $i > $i,X10: $i > $i > $i,X11: $i > $i > $i,X12: $i > $i > $i,X13: $i > $i > $i] : % 0.10/0.39 ( c_and % 0.10/0.39 @ ( c_and % 0.10/0.39 @ ( c_and % 0.10/0.39 @ ( c_and @ ( c_Loop @ X0 @ X1 @ X2 @ X3 @ X4 ) % 0.10/0.39 @ ! [X14: $i] : % 0.10/0.39 ( ( c_In @ X14 @ X0 ) % 0.10/0.39 => ! [X15: $i] : % 0.10/0.39 ( ( c_In @ X15 @ X0 ) % 0.10/0.39 => ( ( X5 @ X14 @ X15 ) % 0.10/0.39 = ( X2 @ ( X1 @ X15 @ X14 ) @ ( X1 @ X14 @ X15 ) ) ) ) ) ) % 0.10/0.39 @ ! [X14: $i] : % 0.10/0.39 ( ( c_In @ X14 @ X0 ) % 0.10/0.39 => ! [X15: $i] : % 0.10/0.39 ( ( c_In @ X15 @ X0 ) % 0.10/0.39 => ! [X16: $i] : % 0.10/0.39 ( ( c_In @ X16 @ X0 ) % 0.10/0.39 => ( ( X6 @ X14 @ X15 @ X16 ) % 0.10/0.39 = ( X2 @ ( X1 @ X14 @ ( X1 @ X15 @ X16 ) ) @ ( X1 @ ( X1 @ X14 @ X15 ) @ X16 ) ) ) ) ) ) ) % 0.10/0.39 @ ! [X14: $i] : % 0.10/0.39 ( ( c_In @ X14 @ X0 ) % 0.10/0.39 => ! [X15: $i] : % 0.10/0.39 ( ( c_In @ X15 @ X0 ) % 0.10/0.39 => ( c_and % 0.10/0.39 @ ( c_and % 0.10/0.39 @ ( c_and % 0.10/0.39 @ ( c_and % 0.10/0.39 @ ( ( X7 @ X14 @ X15 ) % 0.10/0.39 = ( X2 @ X14 @ ( X1 @ X15 @ X14 ) ) ) % 0.10/0.39 @ ( ( X10 @ X14 @ X15 ) % 0.10/0.39 = ( X1 @ X14 @ ( X1 @ X15 @ ( X2 @ X14 @ X4 ) ) ) ) ) % 0.10/0.39 @ ( ( X11 @ X14 @ X15 ) % 0.10/0.39 = ( X1 @ ( X1 @ ( X3 @ X4 @ X14 ) @ X15 ) @ X14 ) ) ) % 0.10/0.39 @ ( ( X12 @ X14 @ X15 ) % 0.10/0.39 = ( X1 @ ( X2 @ X14 @ X15 ) @ ( X2 @ ( X2 @ X14 @ X4 ) @ X4 ) ) ) ) % 0.10/0.39 @ ( ( X13 @ X14 @ X15 ) % 0.10/0.39 = ( X1 @ ( X3 @ X4 @ ( X3 @ X4 @ X14 ) ) @ ( X3 @ X15 @ X14 ) ) ) ) ) ) ) % 0.10/0.39 @ ! [X14: $i] : % 0.10/0.39 ( ( c_In @ X14 @ X0 ) % 0.10/0.39 => ! [X15: $i] : % 0.10/0.39 ( ( c_In @ X15 @ X0 ) % 0.10/0.39 => ! [X16: $i] : % 0.10/0.39 ( ( c_In @ X16 @ X0 ) % 0.10/0.39 => ( c_and % 0.10/0.39 @ ( ( X8 @ X14 @ X15 @ X16 ) % 0.10/0.39 = ( X2 @ ( X1 @ X15 @ X14 ) @ ( X1 @ X15 @ ( X1 @ X14 @ X16 ) ) ) ) % 0.10/0.39 @ ( ( X9 @ X14 @ X15 @ X16 ) % 0.10/0.39 = ( X3 @ ( X1 @ ( X1 @ X16 @ X14 ) @ X15 ) @ ( X1 @ X14 @ X15 ) ) ) ) ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax104,axiom, % 0.10/0.39 ( c_Loop_with_defs_cex1 % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i > $i,X2: $i > $i > $i,X3: $i > $i > $i,X4: $i,X5: $i > $i > $i,X6: $i > $i > $i > $i,X7: $i > $i > $i,X8: $i > $i > $i > $i,X9: $i > $i > $i > $i,X10: $i > $i > $i,X11: $i > $i > $i,X12: $i > $i > $i,X13: $i > $i > $i] : % 0.10/0.39 ( c_and @ ( c_Loop_with_defs @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 ) % 0.10/0.39 @ ? [X14: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X14 @ X0 ) % 0.10/0.39 @ ? [X15: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X15 @ X0 ) % 0.10/0.39 @ ? [X16: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X16 @ X0 ) % 0.10/0.39 @ ? [X17: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X17 @ X0 ) % 0.10/0.39 @ ( c_not % 0.10/0.39 @ ( ( X5 @ ( X1 @ ( X2 @ ( X8 @ X15 @ X16 @ X14 ) @ X4 ) @ X14 ) @ X17 ) % 0.10/0.39 = X4 ) ) ) ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax105,axiom, % 0.10/0.39 ( c_Loop_with_defs_cex2 % 0.10/0.39 = ( ^ [X0: $i,X1: $i > $i > $i,X2: $i > $i > $i,X3: $i > $i > $i,X4: $i,X5: $i > $i > $i,X6: $i > $i > $i > $i,X7: $i > $i > $i,X8: $i > $i > $i > $i,X9: $i > $i > $i > $i,X10: $i > $i > $i,X11: $i > $i > $i,X12: $i > $i > $i,X13: $i > $i > $i] : % 0.10/0.39 ( c_and @ ( c_Loop_with_defs @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 ) % 0.10/0.39 @ ? [X14: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X14 @ X0 ) % 0.10/0.39 @ ? [X15: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X15 @ X0 ) % 0.10/0.39 @ ? [X16: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X16 @ X0 ) % 0.10/0.39 @ ? [X17: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X17 @ X0 ) % 0.10/0.39 @ ? [X18: $i] : % 0.10/0.39 ( c_and @ ( c_In @ X18 @ X0 ) % 0.10/0.39 @ ( c_not % 0.10/0.39 @ ( ( X6 @ X18 @ ( X1 @ ( X3 @ X4 @ X14 ) @ ( X9 @ X15 @ X16 @ X14 ) ) @ X17 ) % 0.10/0.39 = X4 ) ) ) ) ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax106,axiom, % 0.10/0.39 ( c_combinator % 0.10/0.39 = ( ^ [X0: $i] : % 0.10/0.39 ! [X1: $i > $o] : % 0.10/0.39 ( ( X1 @ ( c_Inj0 @ c_Empty ) ) % 0.10/0.39 => ( ( X1 @ ( c_Inj0 @ ( c_Power @ c_Empty ) ) ) % 0.10/0.39 => ( ! [X2: $i,X3: $i] : % 0.10/0.39 ( ( X1 @ X2 ) % 0.10/0.39 => ( ( X1 @ X3 ) % 0.10/0.39 => ( X1 @ ( c_Inj1 @ ( c_setsum @ X2 @ X3 ) ) ) ) ) % 0.10/0.39 => ( X1 @ X0 ) ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax107,axiom, % 0.10/0.39 ( c_combinator_equiv % 0.10/0.39 = ( ^ [X0: $i,X1: $i] : % 0.10/0.39 ! [X2: $i > $i > $o] : % 0.10/0.39 ( ^ [X3: $i,X4: $i,X5: $i > $i > $i] : % 0.10/0.39 ( ( c_per_i @ X2 ) % 0.10/0.39 => ( ! [X6: $i] : % 0.10/0.39 ( ( c_combinator @ X6 ) % 0.10/0.39 => ( X2 @ X6 @ X6 ) ) % 0.10/0.39 => ( ! [X6: $i,X7: $i,X8: $i,X9: $i] : % 0.10/0.39 ( ( c_combinator @ X6 ) % 0.10/0.39 => ( ( c_combinator @ X7 ) % 0.10/0.39 => ( ( c_combinator @ X8 ) % 0.10/0.39 => ( ( c_combinator @ X9 ) % 0.10/0.39 => ( ( X2 @ X6 @ X8 ) % 0.10/0.39 => ( ( X2 @ X7 @ X9 ) % 0.10/0.39 => ( X2 @ ( X5 @ X6 @ X7 ) @ ( X5 @ X8 @ X9 ) ) ) ) ) ) ) ) % 0.10/0.39 => ( ! [X6: $i,X7: $i] : ( X2 @ ( X5 @ ( X5 @ X3 @ X6 ) @ X7 ) @ X6 ) % 0.10/0.39 => ( ! [X6: $i,X7: $i,X8: $i] : ( X2 @ ( X5 @ ( X5 @ ( X5 @ X4 @ X6 ) @ X7 ) @ X8 ) @ ( X5 @ ( X5 @ X6 @ X8 ) @ ( X5 @ X7 @ X8 ) ) ) % 0.10/0.39 => ( X2 @ X0 @ X1 ) ) ) ) ) ) % 0.10/0.39 @ ( c_Inj0 @ c_Empty ) % 0.10/0.39 @ ( c_Inj0 @ ( c_Power @ c_Empty ) ) % 0.10/0.39 @ ^ [X3: $i,X4: $i] : ( c_Inj1 @ ( c_setsum @ X3 @ X4 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(ax108,axiom, % 0.10/0.39 ( c_equip_mod % 0.10/0.39 = ( ^ [X0: $i,X1: $i,X2: $i] : % 0.10/0.39 ? [X3: $i,X4: $i] : ( c_or @ ( c_and @ ( c_equip @ ( c_setsum @ X0 @ X3 ) @ X1 ) @ ( c_equip @ ( c_setprod @ X4 @ X3 ) @ X2 ) ) @ ( c_and @ ( c_equip @ ( c_setsum @ X1 @ X3 ) @ X0 ) @ ( c_equip @ ( c_setprod @ X4 @ X3 ) @ X2 ) ) ) ) ) ). % 0.10/0.39 % 0.10/0.39 thf(conj,conjecture, % 0.10/0.39 ( c_not % 0.10/0.39 @ ( c_not % 0.10/0.39 @ ! [X0: $o,X1: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X2: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X3: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X4: $o,X5: $o,X6: $o,X7: $o,X8: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X9: $o,X10: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X11: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X12: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X13: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X14: $o,X15: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X16: $o,X17: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X18: $o,X19: $o,X20: $o,X21: $o,X22: $o,X23: $o,X24: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X25: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X26: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X27: $o,X28: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X29: $o,X30: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X31: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X32: $o,X33: $o,X34: $o,X35: $o,X36: $o,X37: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X38: $o,X39: $o,X40: $o,X41: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X42: $o,X43: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X44: $o,X45: $o,X46: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X47: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X48: $o,X49: $o,X50: $o] : % 0.10/0.39 ( c_not % 0.10/0.39 @ ! [X51: $o] : % 0.10/0.39 ( c_iff % 0.10/0.39 @ ( ( c_iff % 0.10/0.39 @ ( c_iff % 0.10/0.39 @ ( c_iff % 0.10/0.39 @ ( c_not % 0.10/0.39 @ ( ( c_iff @ X31 @ ( c_iff @ ( c_not @ X22 ) @ X29 ) ) % 0.10/0.39 => ( ( c_not % 0.10/0.39 @ ( c_iff @ X39 % 0.10/0.39 @ ( ( c_not @ X29 ) % 0.10/0.39 => ( ( c_not @ X22 ) % 0.10/0.39 => X31 ) ) ) ) % 0.10/0.39 => ( c_not % 0.10/0.39 @ ( ( c_not @ X31 ) % 0.10/0.39 => ( X29 % 0.10/0.39 => ( ( c_not @ X11 ) % 0.10/0.39 => X39 ) ) ) ) ) ) ) % 0.10/0.39 @ ( c_not % 0.10/0.39 @ ( ( c_iff % 0.10/0.39 @ ( X31 % 0.10/0.40 => ( X22 % 0.10/0.40 => ( c_iff @ X6 @ X49 ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( X31 % 0.10/0.40 => ( c_iff @ X6 @ X29 ) ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ X49 % 0.10/0.40 @ ( X31 % 0.10/0.40 => ( X22 % 0.10/0.40 => X27 ) ) ) ) ) ) ) % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( ( X50 % 0.10/0.40 => ( X48 % 0.10/0.40 => ( ( c_not @ X39 ) % 0.10/0.40 => X51 ) ) ) % 0.10/0.40 => ( c_not @ ( c_iff @ X39 @ X25 ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( X32 % 0.10/0.40 => ( c_iff @ X29 % 0.10/0.40 @ ( X12 % 0.10/0.40 => X39 ) ) ) % 0.10/0.40 @ ( c_not @ ( c_iff @ X31 @ X32 ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X29 % 0.10/0.40 => ( ( c_not @ X0 ) % 0.10/0.40 => X50 ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X48 % 0.10/0.40 => ( X32 % 0.10/0.40 => ( c_iff @ X13 @ c_False ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( c_iff @ X19 % 0.10/0.40 @ ( c_iff @ X13 % 0.10/0.40 @ ( X0 % 0.10/0.40 => X39 ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ X50 % 0.10/0.40 @ ( c_iff @ X39 % 0.10/0.40 @ ( X13 % 0.10/0.40 => c_False ) ) ) ) ) ) ) ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff @ ( c_iff @ X50 @ ( c_iff @ X38 @ ( c_iff @ X1 @ X16 ) ) ) % 0.10/0.40 @ ( c_iff @ ( c_iff @ X47 @ ( c_iff @ X34 @ ( c_iff @ ( c_not @ X16 ) @ X51 ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not @ X38 ) % 0.10/0.40 => ( c_iff @ ( c_not @ X33 ) % 0.10/0.40 @ ( X16 % 0.10/0.40 => X47 ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X47 % 0.10/0.40 => ( X38 % 0.10/0.40 => ( X1 % 0.10/0.40 => c_False ) ) ) ) ) % 0.10/0.40 @ ( c_iff @ ( c_not @ X38 ) % 0.10/0.40 @ ( X16 % 0.10/0.40 => X47 ) ) ) % 0.10/0.40 @ ( c_iff @ ( c_not @ X34 ) % 0.10/0.40 @ ( ( c_not @ X33 ) % 0.10/0.40 => ( c_iff @ X16 @ X38 ) ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( c_iff @ X42 @ ( c_iff @ X30 @ X28 ) ) ) ) % 0.10/0.40 => ( c_iff @ ( c_not @ X37 ) % 0.10/0.40 @ ( X30 % 0.10/0.40 => X42 ) ) ) ) % 0.10/0.40 @ ( X51 % 0.10/0.40 => ( X49 % 0.10/0.40 => ( X38 % 0.10/0.40 => ( X37 % 0.10/0.40 => c_False ) ) ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not @ X34 ) % 0.10/0.40 => ( ( c_not @ X26 ) % 0.10/0.40 => ( ( c_not @ X14 ) % 0.10/0.40 => X42 ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff @ X14 @ X34 ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_iff @ X34 @ ( c_iff @ ( c_not @ X17 ) @ ( c_iff @ X14 @ X49 ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( X38 % 0.10/0.40 => ( c_iff @ X34 % 0.10/0.40 @ ( ( c_not @ X14 ) % 0.10/0.40 => X49 ) ) ) ) ) ) ) ) ) ) ) ) ) % 0.10/0.40 => ( ( c_not % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( X46 % 0.10/0.40 => ( c_iff @ X43 @ ( c_iff @ X35 @ c_False ) ) ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( X45 % 0.10/0.40 => X23 ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X45 % 0.10/0.40 => ( ( c_not @ X23 ) % 0.10/0.40 => ( c_iff @ X10 @ X49 ) ) ) ) % 0.10/0.40 @ ( ( c_not @ X21 ) % 0.10/0.40 => ( ( c_not @ X10 ) % 0.10/0.40 => X23 ) ) ) ) % 0.10/0.40 @ ( ( c_not @ X10 ) % 0.10/0.40 => X23 ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff @ ( c_not @ X35 ) % 0.10/0.40 @ ( X21 % 0.10/0.40 => ( X10 % 0.10/0.40 => X43 ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ X49 % 0.10/0.40 @ ( X35 % 0.10/0.40 => ( c_iff @ ( c_not @ X10 ) @ X43 ) ) ) ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff @ ( c_not @ X46 ) % 0.10/0.40 @ ( X8 % 0.10/0.40 => ( c_iff @ ( c_not @ X7 ) @ X49 ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( c_iff @ X21 % 0.10/0.40 @ ( X9 % 0.10/0.40 => ( c_iff @ X8 @ X49 ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( X21 % 0.10/0.40 => ( c_iff @ X9 % 0.10/0.40 @ ( X8 % 0.10/0.40 => X46 ) ) ) ) ) ) % 0.10/0.40 @ ( c_not @ ( c_iff @ X21 @ X49 ) ) ) ) ) ) % 0.10/0.40 => ( ( c_not % 0.10/0.40 @ ( c_iff @ X45 % 0.10/0.40 @ ( X43 % 0.10/0.40 => ( X41 % 0.10/0.40 => X5 ) ) ) ) % 0.10/0.40 => ( c_iff @ X45 % 0.10/0.40 @ ( ( c_not @ X18 ) % 0.10/0.40 => ( c_iff @ ( c_not @ X5 ) @ X49 ) ) ) ) ) ) % 0.10/0.40 => ( ( c_not % 0.10/0.40 @ ( ( ( c_not % 0.10/0.40 @ ( c_iff @ X51 % 0.10/0.40 @ ( X40 % 0.10/0.40 => ( c_iff @ X36 @ c_False ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ X49 % 0.10/0.40 @ ( ( c_not @ X46 ) % 0.10/0.40 => ( c_iff @ ( c_not @ X40 ) @ X51 ) ) ) ) ) % 0.10/0.40 => ( ( c_iff % 0.10/0.40 @ ( X36 % 0.10/0.40 => ( c_iff @ X15 @ ( c_iff @ X2 @ X46 ) ) ) % 0.10/0.40 @ ( c_iff @ ( c_iff @ ( c_not @ X46 ) @ ( c_iff @ ( c_not @ X36 ) @ X51 ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( ( c_not @ X44 ) % 0.10/0.40 => ( c_iff @ ( c_not @ X36 ) @ ( c_iff @ X15 @ X46 ) ) ) ) % 0.10/0.40 => ( c_not @ ( c_iff @ X51 @ ( c_iff @ X36 @ X46 ) ) ) ) % 0.10/0.40 @ ( c_iff @ X44 @ c_False ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X46 % 0.10/0.40 => c_False ) ) ) ) ) % 0.10/0.40 => ( X46 % 0.10/0.40 => ( X36 % 0.10/0.40 => ( X24 % 0.10/0.40 => ( c_iff @ X15 @ c_False ) ) ) ) ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( c_iff @ X44 % 0.10/0.40 @ ( ( c_not @ X20 ) % 0.10/0.40 => ( c_iff @ X3 @ X45 ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff @ ( c_not @ X3 ) @ X4 ) % 0.10/0.40 => ( c_not @ ( c_iff @ X49 @ ( c_iff @ X20 @ X46 ) ) ) ) ) % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( c_iff @ ( c_not @ X45 ) @ X46 ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff @ ( c_not @ X45 ) % 0.10/0.40 @ ( ( c_not @ X3 ) % 0.10/0.40 => X46 ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_iff @ X49 @ ( c_iff @ ( c_not @ X45 ) @ X50 ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ ( c_not @ X46 ) % 0.10/0.40 @ ( ( c_not @ X45 ) % 0.10/0.40 => ( X3 % 0.10/0.40 => X50 ) ) ) ) ) ) ) ) ) % 0.10/0.40 => ( X46 % 0.10/0.40 => ( c_iff @ ( c_not @ X45 ) @ X49 ) ) ) ) ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( X48 % 0.10/0.40 => ( ( c_not @ X46 ) % 0.10/0.40 => ( c_iff @ X32 @ X47 ) ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X50 % 0.10/0.40 => ( c_iff @ X21 @ ( c_iff @ X16 @ X48 ) ) ) ) % 0.10/0.40 @ ( X47 % 0.10/0.40 => X21 ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( c_iff @ X50 % 0.10/0.40 @ ( X44 % 0.10/0.40 => X47 ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ X50 % 0.10/0.40 @ ( X46 % 0.10/0.40 => ( c_iff @ X29 @ c_False ) ) ) ) ) ) % 0.10/0.40 => ( c_iff @ X46 @ ( c_iff @ ( c_not @ X29 ) @ X44 ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ ( c_not @ X48 ) % 0.10/0.40 @ ( c_iff @ ( c_not @ X46 ) % 0.10/0.40 @ ( X29 % 0.10/0.40 => X50 ) ) ) ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( ( ( c_not @ X47 ) % 0.10/0.40 => ( c_iff @ X27 @ X48 ) ) % 0.10/0.40 => ( X48 % 0.10/0.40 => ( c_iff @ X38 @ X50 ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( X50 % 0.10/0.40 => ( c_iff @ X48 % 0.10/0.40 @ ( X36 % 0.10/0.40 => X47 ) ) ) ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( ( ( c_not @ ( c_iff @ X47 @ ( c_iff @ X22 @ X18 ) ) ) % 0.10/0.40 => ( X48 % 0.10/0.40 => ( c_iff @ X18 @ X51 ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( X48 % 0.10/0.40 => ( c_iff @ X47 @ ( c_iff @ ( c_not @ X22 ) @ X50 ) ) ) ) ) % 0.10/0.40 @ ( ( c_iff @ X51 % 0.10/0.40 @ ( X35 % 0.10/0.40 => ( X18 % 0.10/0.40 => c_False ) ) ) % 0.10/0.40 => ( c_iff @ X31 @ ( c_iff @ X22 @ ( c_iff @ ( c_not @ X18 ) @ X35 ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( c_iff @ X48 % 0.10/0.40 @ ( c_iff @ X47 % 0.10/0.40 @ ( X2 % 0.10/0.40 => X51 ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( X19 % 0.10/0.40 => ( c_iff @ ( c_not @ X0 ) @ X47 ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X48 % 0.10/0.40 => ( X19 % 0.10/0.40 => ( c_iff @ ( c_not @ X0 ) @ X1 ) ) ) ) ) % 0.10/0.40 @ ( c_not @ ( c_iff @ X48 @ ( c_iff @ X1 @ X19 ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( c_iff @ X2 % 0.10/0.40 @ ( c_iff @ ( c_not @ X1 ) % 0.10/0.40 @ ( ( c_not @ X0 ) % 0.10/0.40 => X48 ) ) ) ) ) ) ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( X48 % 0.10/0.40 => ( X35 % 0.10/0.40 => X4 ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( ( c_not @ X48 ) % 0.10/0.40 => ( ( c_not @ X24 ) % 0.10/0.40 => ( X13 % 0.10/0.40 => X50 ) ) ) ) % 0.10/0.40 => ( X50 % 0.10/0.40 => ( ( c_not @ X8 ) % 0.10/0.40 => X13 ) ) ) ) ) ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( c_iff @ X49 % 0.10/0.40 @ ( X43 % 0.10/0.40 => ( c_iff @ X11 @ ( c_iff @ X7 @ c_False ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( c_iff @ X45 % 0.10/0.40 @ ( X11 % 0.10/0.40 => c_False ) ) ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( ( c_not @ ( c_iff @ X49 @ ( c_iff @ X43 @ X33 ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_iff @ ( c_not @ X43 ) @ ( c_iff @ ( c_not @ X33 ) @ ( c_iff @ X15 @ X45 ) ) ) % 0.10/0.40 => ( ( c_not @ X45 ) % 0.10/0.40 => ( c_iff @ ( c_not @ X43 ) % 0.10/0.40 @ ( ( c_not @ X15 ) % 0.10/0.40 => X49 ) ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X47 % 0.10/0.40 => ( c_iff @ X17 @ ( c_iff @ X15 @ X49 ) ) ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( ( c_iff @ X46 @ ( c_iff @ X43 @ ( c_iff @ X20 @ X45 ) ) ) % 0.10/0.40 => ( c_not % 0.10/0.40 @ ( ( c_not @ X28 ) % 0.10/0.40 => X43 ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( c_iff @ X45 % 0.10/0.40 @ ( c_iff @ X43 % 0.10/0.40 @ ( X42 % 0.10/0.40 => c_False ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff @ X45 % 0.10/0.40 @ ( X43 % 0.10/0.40 => ( X42 % 0.10/0.40 => ( c_iff @ X37 @ c_False ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not @ ( c_iff @ ( c_not @ X42 ) @ ( c_iff @ ( c_not @ X10 ) @ X49 ) ) ) % 0.10/0.40 => ( c_not @ ( c_iff @ X37 @ X45 ) ) ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( X42 % 0.10/0.40 => ( c_iff @ ( c_not @ X14 ) @ ( c_iff @ ( c_not @ X6 ) @ X45 ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( ( c_not @ X42 ) % 0.10/0.40 => ( ( c_not @ X28 ) % 0.10/0.40 => ( X14 % 0.10/0.40 => X45 ) ) ) ) % 0.10/0.40 => ( c_iff @ X28 % 0.10/0.40 @ ( ( c_not @ X14 ) % 0.10/0.40 => X49 ) ) ) ) ) % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( X42 % 0.10/0.40 => X45 ) ) ) ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_iff % 0.10/0.40 @ ( ( X46 % 0.10/0.40 => ( ( c_not @ X34 ) % 0.10/0.40 => ( c_iff @ X30 @ X41 ) ) ) % 0.10/0.40 => ( X34 % 0.10/0.40 => ( c_iff @ ( c_not @ X30 ) @ ( c_iff @ X26 @ X40 ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_iff @ X46 % 0.10/0.40 @ ( c_iff @ ( c_not @ X39 ) % 0.10/0.40 @ ( ( c_not @ X26 ) % 0.10/0.40 => X41 ) ) ) % 0.10/0.40 @ ( ( c_not @ ( c_iff @ ( c_not @ X41 ) @ ( c_iff @ ( c_not @ X26 ) @ ( c_iff @ ( c_not @ X12 ) @ X46 ) ) ) ) % 0.10/0.40 => ( X46 % 0.10/0.40 => ( c_iff @ X26 % 0.10/0.40 @ ( X3 % 0.10/0.40 => X12 ) ) ) ) ) ) % 0.10/0.40 => ( c_iff % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( X45 % 0.10/0.40 => ( X5 % 0.10/0.40 => c_False ) ) ) ) % 0.10/0.40 => ( c_iff @ X34 @ ( c_iff @ X30 @ X49 ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( ( c_not @ X46 ) % 0.10/0.40 => ( ( c_not @ X30 ) % 0.10/0.40 => ( X23 % 0.10/0.40 => X49 ) ) ) % 0.10/0.40 @ ( c_not @ ( c_iff @ X45 @ ( c_iff @ X30 @ X23 ) ) ) ) ) % 0.10/0.40 @ ( c_iff % 0.10/0.40 @ ( ( c_iff @ ( c_iff @ X46 @ ( c_iff @ X45 @ ( c_iff @ ( c_not @ X9 ) @ X44 ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( c_iff @ X46 % 0.10/0.40 @ ( X45 % 0.10/0.40 => ( X44 % 0.10/0.40 => ( X25 % 0.10/0.40 => c_False ) ) ) ) ) ) % 0.10/0.40 => ( X44 % 0.10/0.40 => ( c_iff @ X9 @ X25 ) ) ) % 0.10/0.40 @ ( c_not % 0.10/0.40 @ ( X49 % 0.10/0.40 => ( c_iff @ X46 % 0.10/0.40 @ ( c_iff @ X45 % 0.10/0.40 @ ( X44 % 0.10/0.40 => c_False ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.10/0.40 % 0.10/0.40 %------------------------------------------------------------------------------ % 0.10/0.40 ------------------------ % 0.10/0.40 /starexec/sw/sutcliffe/jdk-11.0.2/bin/java: Command not found. % 0.10/0.40 ---- Embedded in THF --- % 0.10/0.40 ------------------------ % 0.10/0.42 ---- Cleaned THF --- % 0.10/0.42 ------------------------ % 0.10/0.45 % (1882718)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_1882698 for (2999ds/2Mi) % 0.10/0.45 % (1882718)Refutation not found, incomplete strategy % 0.10/0.45 % (1882718)------------------------------ % 0.10/0.45 % (1882718)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100) % 0.10/0.45 % (1882718)Termination reason: Refutation not found, incomplete strategy % 0.10/0.45 % 0.10/0.45 % 0.10/0.45 % (1882718)Memory used [KB]: 5373 % 0.10/0.45 % (1882718)Time elapsed: 0.002 s % 0.10/0.45 % (1882718)Instructions burned: 1 (million) % 0.10/0.45 % (1882718)------------------------------ % 0.10/0.45 % (1882718)------------------------------ % 0.10/0.46 % (1882714)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_1882698 for (2999ds/183Mi) % 0.10/0.46 % (1882715)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_1882698 for (2999ds/4Mi) % 0.10/0.46 % (1882716)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_1882698 for (2999ds/27Mi) % 0.10/0.46 % (1882714)First to succeed. % 0.10/0.46 % (1882717)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_1882698 for (2999ds/2Mi) % 0.10/0.46 % (1882715)Also succeeded, but the first one will report. % 0.10/0.46 % (1882716)Refutation not found, incomplete strategy % 0.10/0.46 % (1882716)------------------------------ % 0.10/0.46 % (1882716)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100) % 0.10/0.46 % (1882716)Termination reason: Refutation not found, incomplete strategy % 0.10/0.46 % 0.10/0.46 % 0.10/0.46 % (1882716)Memory used [KB]: 5373 % 0.10/0.46 % (1882716)Time elapsed: 0.003 s % 0.10/0.46 % (1882716)Instructions burned: 1 (million) % 0.10/0.46 % (1882716)------------------------------ % 0.10/0.46 % (1882716)------------------------------ % 0.10/0.46 % (1882720)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_1882698 for (2999ds/18Mi) % 0.10/0.46 % SZS status Satisfiable for DTF2THF_1882698 % 0.10/0.46 % (1882714)# SZS output start Saturation. % 0.10/0.46 % (1882714)# SZS output end Saturation. % 0.10/0.46 % (1882714)------------------------------ % 0.10/0.46 % (1882714)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100) % 0.10/0.46 % (1882714)Termination reason: Satisfiable % 0.10/0.46 % 0.10/0.46 % (1882714)Memory used [KB]: 5373 % 0.10/0.46 % (1882714)Time elapsed: 0.003 s % 0.10/0.46 % (1882714)Instructions burned: 1 (million) % 0.10/0.46 % (1882714)------------------------------ % 0.10/0.46 % (1882714)------------------------------ % 0.10/0.46 % (1882713)Success in time 0.019 s %------------------------------------------------------------------------------