Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : COM162^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39

% Computer : n012.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 07:46:17 AM UTC 2026

% Result   : Theorem 5.85s 1.97s
% Output   : Refutation 6.40s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01  % Problem  : COM162^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.05/0.13  % Computer : n012.cluster.edu
% 0.05/0.13  % Model    : x86_64 x86_64
% 0.05/0.13  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.13  % Memory   : 8046.5625MB
% 0.05/0.13  % OS       : Linux 6.8.0-71-generic
% 0.05/0.13  % CPULimit : 300
% 0.05/0.13  % WCLimit  : 300
% 0.05/0.13  % DateTime : Tue Sep 29 17:46:48 UTC 2026
% 0.05/0.13  % CPUTime  : 
% 0.05/0.13  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.41/0.41  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.24/0.62  % [INFO] 	 Parsing done (208ms). 
% 1.24/0.63  % [INFO] 	 Running in sequential loop mode. 
% 1.74/0.81  % [INFO] 	 eprover registered as external prover. 
% 1.74/0.82  % [INFO] 	 Scanning for conjecture ... 
% 1.97/0.90  % [INFO] 	 Found a conjecture (or negated_conjecture) and 369 axioms. Running axiom selection ... 
% 1.97/0.98  % [INFO] 	 Axiom selection finished. Selected 157 axioms (removed 212 axioms). 
% 2.39/1.09  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 2.39/1.10  % [INFO] 	 Type checking passed. 
% 2.39/1.10  % [CONFIG] 	 Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>.  Searching for refutation ... 
% 3.70/1.43  % [INFO] 	 [Domain constraints] Detected constraint on product_unit 
% 3.70/1.44  % [INFO] 	 [Domain constraints] dom(product_unit) ⊆ {product_Unity} 
% 3.70/1.44  % [INFO] 	 [Domain constraints] Detected constraint on product_unit 
% 3.70/1.44  % [INFO] 	 [Domain constraints] dom(product_unit) ⊆ {product_Unity} 
% 3.70/1.49  % [INFO] 	 [Domain constraints] Detected constraint on $o 
% 3.70/1.49  % [INFO] 	 [Domain constraints] dom($o) ⊆ {$true} 
% 5.85/1.97  % External prover 'e' found a proof!
% 5.85/1.97  % [INFO] 	 Killing All external provers ... 
% 5.85/1.97  % Time passed: 1767ms (effective reasoning time: 1338ms)
% 5.85/1.97  % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 5.85/1.97  % Axioms used in derivation (157): fact_117_typerep_Osize__neq, fact_173_option_Ocase__distrib, fact_228_one__natural_Orsp, fact_110_random__aux__rec, fact_145_unit_Osize_I1_J, fact_7_dag_Osimps_I4_J, fact_116_sum_Osize_I4_J, fact_6_dag_Osimps_I6_J, fact_131_sum_Osize__gen_I1_J, fact_82_dependent__nat__choice, fact_119_not__None__eq, fact_127_option_Oinducts, fact_185_num_Osize__gen_I2_J, fact_133_option_Osize__gen_I2_J, fact_249_div__1, fact_118_option_Oinject, fact_124_option_Odistinct_I1_J, fact_81_size__bool__def, fact_99_size__bool__overloaded__def, fact_225_nat__1__add__1, fact_129_split__option__all, fact_4_dag_Osimps_I7_J, fact_144_old_Ounit_Orec, fact_17_dag_Osize__gen_I2_J, fact_0_dag_Oinject, fact_146_eq__sym__Unity__conv, fact_208_numeral__2__eq__2, fact_191_nat__of__num__neq__0, fact_106_old_Obool_Osimps_I5_J, fact_192_nat__of__num_Osimps_I2_J, fact_95_natural_Oinducts, fact_152_list_Osize__gen_I2_J, fact_151_default__unit__def, fact_132_sum_Osize__gen_I2_J, fact_72_Zero__not__Suc, fact_211_Suc__nat__number__of__add, fact_142_unit_Osize_I2_J, fact_36_Nat_Oadd__0__right, fact_83_size__natural__overloaded__def, fact_90_option_Osize__neq, fact_26_old_Onat_Oinject, fact_220_Suc__eq__plus1, fact_50_nat__add__left__cancel, fact_184_num_Osize_I5_J, fact_210_Suc3__eq__add__3, fact_22_natural_Osize_I3_J, fact_65_old_Onat_Odistinct_I1_J, fact_121_Inl__Inr__False, fact_168_case__optionE, fact_37_add__Suc__right, fact_91_natural_Oinject, fact_3_dag_Oexhaust, fact_66_nat_OdiscI, fact_156_length__Cons, fact_120_not__Some__eq, fact_16_bool_Osize_I2_J, fact_157_gen__length__code_I2_J, fact_193_nat__of__num__code_I2_J, fact_160_gen__length__def, fact_71_Zero__neq__Suc, fact_115_sum_Osize_I3_J, fact_47_n__not__Suc__n, fact_79_sum_Osize__neq, fact_63_nat_Odistinct_I1_J, fact_199_add__2__eq__Suc_H, fact_207_numeral__1__eq__Suc__0, fact_189_nat__of__num_Osimps_I3_J, fact_134_option_Osize__gen_I1_J, fact_93_natural_Osimps_I7_J, fact_98_natural_Odistinct_I2_J, fact_197_num_Osize_I4_J, fact_69_zero__induct, fact_137_size__literal__def, fact_202_Suc__numeral, fact_89_size__natural__def, fact_149_old_Ounit_Oexhaust, fact_209_numeral__3__eq__3, fact_88_natural_Osize_I4_J, fact_74_old_Onat_Oinducts, fact_163_length__splice, fact_13_zero__natural_Orsp, fact_214_Suc__1, fact_136_tuple__isomorphism_Osize__neq, fact_230_Suc__div__eq__add3__div__numeral, fact_123_obj__sumE__f, fact_186_num_Osize_I6_J, fact_97_natural_Odistinct_I1_J, fact_218_One__nat__def, fact_196_num_Osize__gen_I1_J, fact_76_plus__nat_Oadd__0, fact_169_option_Odisc__eq__case_I1_J, fact_231_div__Suc__eq__div__add3, fact_171_option_Osimps_I4_J, fact_96_natural_Oexhaust, fact_73_old_Onat_Oexhaust, fact_182_disjE__realizer2, fact_24_bool_Osize_I3_J, fact_107_old_Obool_Osimps_I6_J, help_If_3_1_T, fact_78_size__bool, fact_159_length__code, fact_8_dag_Osize__gen_I1_J, fact_128_split__option__ex, fact_141_tuple__isomorphism_Osize_I2_J, fact_153_length__Suc__conv, fact_187_num_Osize__gen_I3_J, fact_77_add__eq__self__zero, fact_48_add__Suc__shift, fact_113_option_Osize_I3_J, fact_35_add__is__0, fact_148_old_Ounit_Oinducts, fact_114_option_Osize_I4_J, fact_25_nat_Oinject, fact_188_nat__of__num__code_I3_J, fact_221_Suc__eq__plus1__left, fact_130_combine__options__cases, fact_147_unit__all__impI, fact_155_list_Osize_I4_J, fact_46_Suc__inject, fact_150_tuple__isomorphism_Osize__gen, fact_38_one__is__add, fact_2_dag_Oinduct, fact_87_natural_Osize_I1_J, fact_122_Inr__Inl__False, fact_92_natural_Osimps_I6_J, fact_39_add__is__1, fact_170_option_Odisc__eq__case_I2_J, fact_94_natural_Osize_I2_J, fact_23_bool_Osize_I4_J, fact_154_Suc__length__conv, fact_51_nat__add__right__cancel, fact_10_dag_Ocase__distrib, fact_125_option_OdiscI, fact_190_nat__of__num__add, fact_68_diff__induct, fact_126_option_Oexhaust, fact_5_dag_Osimps_I5_J, fact_138_size__unit__overloaded__def, fact_67_nat__induct, fact_135_typerep_Osize_I2_J, fact_49_add__Suc, fact_18_dag_Osize_I4_J, fact_19_ntrancl__Zero, fact_75_not0__implies__Suc, fact_80_prod_Osize__neq, fact_15_bool_Osize_I1_J, fact_140_size__unit__def, fact_1_dag_Odistinct_I1_J, fact_172_option_Osimps_I5_J, fact_64_old_Onat_Odistinct_I2_J, fact_206_eval__nat__numeral_I3_J, fact_70_Suc__neq__Zero, fact_143_unit__abs__eta__conv, fact_9_dag_Osize_I3_J, fact_195_nat__of__num_Osimps_I1_J, fact_198_add__2__eq__Suc, fact_139_typerep_Osize__gen
% 5.85/1.97  % No. of inferences in proof: 318
% 5.85/1.97  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 1767 ms resp. 1338 ms w/o parsing
% 6.40/2.07  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.40/2.07  thf(binDag_Mirabelle_dag_type, type, binDag_Mirabelle_dag: $tType).
% 6.40/2.07  thf(code_natural_type, type, code_natural: $tType).
% 6.40/2.07  thf(code_term_type, type, code_term: $tType).
% 6.40/2.07  thf(product_unit_type, type, product_unit: $tType).
% 6.40/2.07  thf(typerep_type, type, typerep: $tType).
% 6.40/2.07  thf(simpl_ref_type, type, simpl_ref: $tType).
% 6.40/2.07  thf(literal_type, type, literal: $tType).
% 6.40/2.07  thf(num_type, type, num: $tType).
% 6.40/2.07  thf(nat_type, type, nat: $tType).
% 6.40/2.07  thf(basic_BNF_size_sum_decl, type, basic_BNF_size_sum: !> [TA: $tType,TB: $tType]: ((TB > nat) > ((TA > nat) > ((sum_sum @ TB @ TA) > nat)))).
% 6.40/2.07  thf(binDag476092410e_Node_decl, type, binDag476092410e_Node: (binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > binDag_Mirabelle_dag)))).
% 6.40/2.07  thf(binDag_Mirabelle_Tip_decl, type, binDag_Mirabelle_Tip: binDag_Mirabelle_dag).
% 6.40/2.07  thf(binDag1297733282se_dag_decl, type, binDag1297733282se_dag: !> [TA: $tType]: (TA > ((binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > TA))) > (binDag_Mirabelle_dag > TA)))).
% 6.40/2.07  thf(binDag1442713106ec_dag_decl, type, binDag1442713106ec_dag: !> [TA: $tType]: (TA > ((binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > (TA > (TA > TA))))) > (binDag_Mirabelle_dag > TA)))).
% 6.40/2.07  thf(binDag1924123185ze_dag_decl, type, binDag1924123185ze_dag: (binDag_Mirabelle_dag > nat)).
% 6.40/2.07  thf(code_Suc_decl, type, code_Suc: (code_natural > code_natural)).
% 6.40/2.07  thf(code_rec_natural_decl, type, code_rec_natural: !> [TA: $tType]: (TA > ((code_natural > (TA > TA)) > (code_natural > TA)))).
% 6.40/2.07  thf(code_size_natural_decl, type, code_size_natural: (code_natural > nat)).
% 6.40/2.07  thf(one_one_decl, type, one_one: !> [TA: $tType]: TA).
% 6.40/2.07  thf(plus_plus_decl, type, plus_plus: !> [TA: $tType]: (TA > (TA > TA))).
% 6.40/2.07  thf(zero_zero_decl, type, zero_zero: !> [TA: $tType]: TA).
% 6.40/2.07  thf(size_bool_decl, type, size_bool: ($o > nat)).
% 6.40/2.07  thf(default_default_decl, type, default_default: !> [TA: $tType]: TA).
% 6.40/2.07  thf(gen_length_decl, type, gen_length: !> [TA: $tType]: (nat > ((list @ TA) > nat))).
% 6.40/2.07  thf(cons_decl, type, cons: !> [TA: $tType]: (TA > ((list @ TA) > (list @ TA)))).
% 6.40/2.07  thf(size_list_decl, type, size_list: !> [TA: $tType]: ((TA > nat) > ((list @ TA) > nat))).
% 6.40/2.07  thf(splice_decl, type, splice: !> [TA: $tType]: ((list @ TA) > ((list @ TA) > (list @ TA)))).
% 6.40/2.07  thf(suc_decl, type, suc: (nat > nat)).
% 6.40/2.07  thf(size_size_decl, type, size_size: !> [TA: $tType]: (TA > nat)).
% 6.40/2.07  thf(nat_of_num_decl, type, nat_of_num: (num > nat)).
% 6.40/2.07  thf(bit0_decl, type, bit0: (num > num)).
% 6.40/2.07  thf(bit1_decl, type, bit1: (num > num)).
% 6.40/2.07  thf(one2_decl, type, one2: num).
% 6.40/2.07  thf(size_num_decl, type, size_num: (num > nat)).
% 6.40/2.07  thf(numeral_numeral_decl, type, numeral_numeral: !> [TA: $tType]: (num > TA)).
% 6.40/2.07  thf(none_decl, type, none: !> [TA: $tType]: (option @ TA)).
% 6.40/2.07  thf(some_decl, type, some: !> [TA: $tType]: (TA > (option @ TA))).
% 6.40/2.07  thf(case_option_decl, type, case_option: !> [TA: $tType,TB: $tType]: (TB > ((TA > TB) > ((option @ TA) > TB)))).
% 6.40/2.07  thf(size_option_decl, type, size_option: !> [TA: $tType]: ((TA > nat) > ((option @ TA) > nat))).
% 6.40/2.07  thf(product_Unity_decl, type, product_Unity: product_unit).
% 6.40/2.07  thf(product_rec_bool_decl, type, product_rec_bool: !> [TA: $tType]: (TA > (TA > ($o > TA)))).
% 6.40/2.07  thf(product_rec_unit_decl, type, product_rec_unit: !> [TA: $tType]: (TA > (product_unit > TA))).
% 6.40/2.07  thf(product_size_unit_decl, type, product_size_unit: (product_unit > nat)).
% 6.40/2.07  thf(tuple_742722141rphism_decl, type, tuple_742722141rphism: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > (product_prod @ TB @ TA)) > (((product_prod @ TB @ TA) > TC) > (tuple_isomorphism @ TC @ TB @ TA)))).
% 6.40/2.07  thf(tuple_1907371454rphism_decl, type, tuple_1907371454rphism: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > nat) > ((TB > nat) > ((TA > nat) > ((tuple_isomorphism @ TC @ TB @ TA) > nat))))).
% 6.40/2.07  thf(divide_divide_decl, type, divide_divide: !> [TA: $tType]: (TA > (TA > TA))).
% 6.40/2.07  thf(sum_Inl_decl, type, sum_Inl: !> [TA: $tType,TB: $tType]: (TB > (sum_sum @ TB @ TA))).
% 6.40/2.07  thf(sum_Inr_decl, type, sum_Inr: !> [TA: $tType,TB: $tType]: (TB > (sum_sum @ TA @ TB))).
% 6.40/2.07  thf(transitive_ntrancl_decl, type, transitive_ntrancl: !> [TA: $tType]: (nat > ((set @ (product_prod @ TA @ TA)) > (set @ (product_prod @ TA @ TA))))).
% 6.40/2.07  thf(typerep3_decl, type, typerep3: (literal > ((list @ typerep) > typerep))).
% 6.40/2.07  thf(size_typerep_decl, type, size_typerep: (typerep > nat)).
% 6.40/2.07  thf(a_decl, type, a: simpl_ref).
% 6.40/2.07  thf(lt_decl, type, lt: binDag_Mirabelle_dag).
% 6.40/2.07  thf(rt_decl, type, rt: binDag_Mirabelle_dag).
% 6.40/2.07  thf(139,axiom,((! [A:nat]: ((divide_divide @ nat @ A @ (suc @ (zero_zero @ nat))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_div__1)).
% 6.40/2.07  thf(645,plain,((! [A:nat]: ((divide_divide @ nat @ A @ (suc @ (zero_zero @ nat))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 6.40/2.07  thf(134,axiom,((! [TA: $tType]: ((size_size @ (option @ TA) @ (none @ TA)) = (suc @ (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_option_Osize_I3_J)).
% 6.40/2.07  thf(629,plain,((! [TA: $tType]: ((size_size @ (option @ TA) @ (none @ TA)) = (suc @ (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 6.40/2.07  thf(25,axiom,((! [A:nat]: ((plus_plus @ nat @ A @ (numeral_numeral @ nat @ (bit0 @ one2))) = (suc @ (suc @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_add__2__eq__Suc_H)).
% 6.40/2.07  thf(249,plain,((! [A:nat]: ((plus_plus @ nat @ A @ (numeral_numeral @ nat @ (bit0 @ one2))) = (suc @ (suc @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 6.40/2.07  thf(52,axiom,((! [A:code_natural]: ((zero_zero @ code_natural) != (code_Suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_natural_Odistinct_I1_J)).
% 6.40/2.07  thf(352,plain,((! [A:code_natural]: ~ ((zero_zero @ code_natural) = (code_Suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 6.40/2.07  thf(117,axiom,((! [A:typerep]: ((size_size @ typerep @ A) != (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_typerep_Osize__neq)).
% 6.40/2.07  thf(582,plain,((! [A:typerep]: ~ ((size_size @ typerep @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 6.40/2.07  thf(152,axiom,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag,D:binDag_Mirabelle_dag,E:simpl_ref,F:binDag_Mirabelle_dag]: (((binDag476092410e_Node @ A @ B @ C) = (binDag476092410e_Node @ D @ E @ F)) = ((A = D) & (B = E) & (C = F))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_dag_Oinject)).
% 6.40/2.07  thf(683,plain,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag,D:binDag_Mirabelle_dag,E:simpl_ref,F:binDag_Mirabelle_dag]: (((binDag476092410e_Node @ A @ B @ C) = (binDag476092410e_Node @ D @ E @ F)) = ((A = D) & (B = E) & (C = F))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 6.40/2.07  thf(41,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TA]: ((sum_Inl @ TB @ TA @ A) != (sum_Inr @ TA @ TB @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_Inl__Inr__False)).
% 6.40/2.07  thf(308,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TA]: ~ ((sum_Inl @ TB @ TA @ A) = (sum_Inr @ TA @ TB @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 6.40/2.07  thf(80,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) => (~ (! [B:nat]: (A != (suc @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_old_Onat_Oexhaust)).
% 6.40/2.07  thf(449,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) => (~ (! [B:nat]: ~ (A = (suc @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 6.40/2.07  thf(96,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) => (? [B:nat]: (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_not0__implies__Suc)).
% 6.40/2.07  thf(511,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) => (? [B:nat]: (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 6.40/2.07  thf(128,axiom,((! [A:num]: ((nat_of_num @ (bit1 @ A)) = (suc @ (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_nat__of__num_Osimps_I3_J)).
% 6.40/2.07  thf(614,plain,((! [A:num]: ((nat_of_num @ (bit1 @ A)) = (suc @ (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 6.40/2.07  thf(122,axiom,((! [TA: $tType]: (! [A:(TA > nat)]: ((size_option @ TA @ A @ (none @ TA)) = (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_option_Osize__gen_I1_J)).
% 6.40/2.07  thf(597,plain,((! [TA: $tType]: (! [A:(TA > nat)]: ((size_option @ TA @ (A) @ (none @ TA)) = (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 6.40/2.07  thf(103,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Suc__inject)).
% 6.40/2.07  thf(533,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 6.40/2.07  thf(108,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ A @ C)) = (B = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_nat__add__left__cancel)).
% 6.40/2.07  thf(550,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ A @ C)) = (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 6.40/2.07  thf(158,axiom,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag]: ((binDag1924123185ze_dag @ (binDag476092410e_Node @ A @ B @ C)) = (plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ A) @ (binDag1924123185ze_dag @ C)) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_dag_Osize__gen_I2_J)).
% 6.40/2.07  thf(715,plain,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag]: ((binDag1924123185ze_dag @ (binDag476092410e_Node @ A @ B @ C)) = (plus_plus @ nat @ (plus_plus @ nat @ (binDag1924123185ze_dag @ A) @ (binDag1924123185ze_dag @ C)) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 6.40/2.07  thf(48,axiom,((! [A:nat,B:num]: ((divide_divide @ nat @ (suc @ (suc @ (suc @ A))) @ (numeral_numeral @ nat @ B)) = (divide_divide @ nat @ (plus_plus @ nat @ (numeral_numeral @ nat @ (bit1 @ one2)) @ A) @ (numeral_numeral @ nat @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_Suc__div__eq__add3__div__numeral)).
% 6.40/2.07  thf(340,plain,((! [A:nat,B:num]: ((divide_divide @ nat @ (suc @ (suc @ (suc @ A))) @ (numeral_numeral @ nat @ B)) = (divide_divide @ nat @ (plus_plus @ nat @ (numeral_numeral @ nat @ (bit1 @ one2)) @ A) @ (numeral_numeral @ nat @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 6.40/2.07  thf(104,axiom,((! [A:nat]: ((plus_plus @ nat @ (zero_zero @ nat) @ A) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_plus__nat_Oadd__0)).
% 6.40/2.07  thf(538,plain,((! [A:nat]: ((plus_plus @ nat @ (zero_zero @ nat) @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 6.40/2.07  thf(74,axiom,((! [A:num]: ((size_size @ num @ (bit0 @ A)) = (plus_plus @ nat @ (size_size @ num @ A) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_num_Osize_I5_J)).
% 6.40/2.07  thf(436,plain,((! [A:num]: ((size_size @ num @ (bit0 @ A)) = (plus_plus @ nat @ (size_size @ num @ A) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 6.40/2.07  thf(141,axiom,(((size_size @ $o) = (^ [A:$o]: (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_size__bool)).
% 6.40/2.07  thf(651,plain,(((size_size @ $o) = (^ [A:$o]: (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 6.40/2.07  thf(137,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_Zero__neq__Suc)).
% 6.40/2.07  thf(638,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 6.40/2.07  thf(6,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ C @ D)) = (case_option @ TC @ TA @ (A @ B) @ (^ [E:TA]: (A @ (C @ E))) @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_option_Ocase__distrib)).
% 6.40/2.07  thf(189,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:TB,C:(TA > TB),D:(option @ TA)]: ((A @ (case_option @ TB @ TA @ B @ (C) @ D)) = (case_option @ TC @ TA @ (A @ B) @ (^ [E:TA]: (A @ (C @ E))) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 6.40/2.07  thf(125,axiom,(((one_one @ nat) = (suc @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_One__nat__def)).
% 6.40/2.07  thf(606,plain,(((one_one @ nat) = (suc @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 6.40/2.07  thf(32,axiom,((! [A:num]: ((numeral_numeral @ nat @ (bit1 @ A)) = (suc @ (numeral_numeral @ nat @ (bit0 @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_eval__nat__numeral_I3_J)).
% 6.40/2.07  thf(284,plain,((! [A:num]: ((numeral_numeral @ nat @ (bit1 @ A)) = (suc @ (numeral_numeral @ nat @ (bit0 @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 6.40/2.07  thf(68,axiom,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (suc @ (plus_plus @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_add__Suc)).
% 6.40/2.07  thf(416,plain,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (suc @ (plus_plus @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 6.40/2.07  thf(34,axiom,((! [TA: $tType]: (! [A:TA]: ((product_rec_unit @ TA @ A @ product_Unity) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_old_Ounit_Orec)).
% 6.40/2.07  thf(289,plain,((! [TA: $tType]: (! [A:TA]: ((product_rec_unit @ TA @ A @ product_Unity) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 6.40/2.07  thf(14,axiom,(((numeral_numeral @ nat @ (bit1 @ one2)) = (suc @ (suc @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_numeral__3__eq__3)).
% 6.40/2.07  thf(216,plain,(((numeral_numeral @ nat @ (bit1 @ one2)) = (suc @ (suc @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 6.40/2.07  thf(120,axiom,((! [A:code_natural]: ((code_size_natural @ (code_Suc @ A)) = (plus_plus @ nat @ (code_size_natural @ A) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_natural_Osize_I2_J)).
% 6.40/2.07  thf(591,plain,((! [A:code_natural]: ((code_size_natural @ (code_Suc @ A)) = (plus_plus @ nat @ (code_size_natural @ A) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 6.40/2.07  thf(11,axiom,((! [A:$o]: ((A = (product_Unity = product_Unity)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_eq__sym__Unity__conv)).
% 6.40/2.07  thf(211,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 6.40/2.07  thf(90,axiom,((! [TA: $tType]: (! [A:(nat > (TA > $o)),B:(nat > (TA > (TA > $o)))]: ((? [C:TA]: (A @ (zero_zero @ nat) @ C)) => ((! [C:TA,D:nat]: ((A @ D @ C) => (? [E:TA]: ((A @ (suc @ D) @ E) & (B @ D @ C @ E))))) => (? [C:(nat > TA)]: ! [D:nat]: ((A @ D @ (C @ D)) & (B @ D @ (C @ D) @ (C @ (suc @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_dependent__nat__choice)).
% 6.40/2.07  thf(485,plain,((! [TA: $tType]: (! [A:(nat > (TA > $o)),B:(nat > (TA > (TA > $o)))]: ((? [C:TA]: (A @ (zero_zero @ nat) @ C)) => ((! [C:TA,D:nat]: ((A @ D @ C) => (? [E:TA]: ((A @ (suc @ D) @ E) & (B @ D @ C @ E))))) => (? [C:(nat > TA)]: ! [D:nat]: ((A @ D @ (C @ D)) & (B @ D @ (C @ D) @ (C @ (suc @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 6.40/2.07  thf(97,axiom,((! [A:num]: ((nat_of_num @ (bit1 @ A)) = (suc @ (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_nat__of__num__code_I3_J)).
% 6.40/2.07  thf(514,plain,((! [A:num]: ((nat_of_num @ (bit1 @ A)) = (suc @ (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 6.40/2.07  thf(114,axiom,((! [A:code_natural]: ((size_size @ code_natural @ (code_Suc @ A)) = (plus_plus @ nat @ (size_size @ code_natural @ A) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_natural_Osize_I4_J)).
% 6.40/2.07  thf(574,plain,((! [A:code_natural]: ((size_size @ code_natural @ (code_Suc @ A)) = (plus_plus @ nat @ (size_size @ code_natural @ A) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 6.40/2.07  thf(88,axiom,(((size_bool @ ($false)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_bool_Osize_I2_J)).
% 6.40/2.07  thf(480,plain,(((size_bool @ ($false)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 6.40/2.07  thf(16,axiom,((! [TA: $tType]: (! [A:TA,B:(code_natural > (TA > TA))]: ((code_rec_natural @ TA @ A @ B @ (zero_zero @ code_natural)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_natural_Osimps_I6_J)).
% 6.40/2.07  thf(221,plain,((! [TA: $tType]: (! [A:TA,B:(code_natural > (TA > TA))]: ((code_rec_natural @ TA @ A @ (B) @ (zero_zero @ code_natural)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 6.40/2.07  thf(81,axiom,((! [TA: $tType]: (! [A:(set @ (product_prod @ TA @ TA))]: ((transitive_ntrancl @ TA @ (zero_zero @ nat) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_ntrancl__Zero)).
% 6.40/2.07  thf(453,plain,((! [TA: $tType]: (! [A:(set @ (product_prod @ TA @ TA))]: ((transitive_ntrancl @ TA @ (zero_zero @ nat) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 6.40/2.07  thf(63,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > nat),B:(TB > nat),C:TA]: ((basic_BNF_size_sum @ TA @ TB @ A @ B @ (sum_Inl @ TA @ TB @ C)) = (plus_plus @ nat @ (A @ C) @ (suc @ (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_sum_Osize__gen_I1_J)).
% 6.40/2.07  thf(396,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > nat),B:(TB > nat),C:TA]: ((basic_BNF_size_sum @ TA @ TB @ (A) @ (B) @ (sum_Inl @ TA @ TB @ C)) = (plus_plus @ nat @ (A @ C) @ (suc @ (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 6.40/2.07  thf(101,axiom,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = (zero_zero @ nat)) = ((A = (zero_zero @ nat)) & (B = (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_add__is__0)).
% 6.40/2.07  thf(527,plain,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = (zero_zero @ nat)) = ((A = (zero_zero @ nat)) & (B = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 6.40/2.07  thf(43,axiom,((! [A:(product_unit > $o),B:product_unit]: ((A @ product_Unity) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_old_Ounit_Oinducts)).
% 6.40/2.07  thf(312,plain,((! [A:(product_unit > $o),B:product_unit]: ((A @ product_Unity) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 6.40/2.07  thf(35,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) = (case_option @ $o @ TA @ ($false) @ (^ [B:TA]: (($true))) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_option_Odisc__eq__case_I2_J)).
% 6.40/2.07  thf(292,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) = (case_option @ $o @ TA @ ($false) @ (^ [B:TA]: (($true))) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 6.40/2.07  thf(20,axiom,((! [TA: $tType]: (! [A:nat,B:TA,C:(list @ TA)]: ((gen_length @ TA @ A @ (cons @ TA @ B @ C)) = (gen_length @ TA @ (suc @ A) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_gen__length__code_I2_J)).
% 6.40/2.07  thf(233,plain,((! [TA: $tType]: (! [A:nat,B:TA,C:(list @ TA)]: ((gen_length @ TA @ A @ (cons @ TA @ B @ C)) = (gen_length @ TA @ (suc @ A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 6.40/2.07  thf(75,axiom,(((nat_of_num @ one2) = (suc @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_nat__of__num_Osimps_I1_J)).
% 6.40/2.07  thf(439,plain,(((nat_of_num @ one2) = (suc @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 6.40/2.07  thf(150,axiom,((! [TA: $tType,TB: $tType]: (! [A:(sum_sum @ TB @ TA)]: ((size_size @ (sum_sum @ TB @ TA) @ A) != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_sum_Osize__neq)).
% 6.40/2.07  thf(678,plain,((! [TA: $tType,TB: $tType]: (! [A:(sum_sum @ TB @ TA)]: ~ ((size_size @ (sum_sum @ TB @ TA) @ A) = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 6.40/2.07  thf(51,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) = (? [B:TA]: (A = (some @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_not__None__eq)).
% 6.40/2.07  thf(349,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) = (? [B:TA]: (A = (some @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 6.40/2.07  thf(1,conjecture,(((binDag476092410e_Node @ lt @ a @ rt) != lt)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 6.40/2.07  thf(2,negated_conjecture,((~ ((binDag476092410e_Node @ lt @ a @ rt) != lt))),inference(neg_conjecture,[status(cth)],[1])).
% 6.40/2.07  thf(160,plain,((~ (~ ((binDag476092410e_Node @ lt @ a @ rt) = lt)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 6.40/2.07  thf(37,axiom,((! [A:num]: ((nat_of_num @ (bit0 @ A)) = (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_nat__of__num__code_I2_J)).
% 6.40/2.07  thf(297,plain,((! [A:num]: ((nat_of_num @ (bit0 @ A)) = (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 6.40/2.07  thf(7,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA]: ((case_option @ TB @ TA @ A @ B @ (some @ TA @ C)) = (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_option_Osimps_I5_J)).
% 6.40/2.07  thf(192,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA]: ((case_option @ TB @ TA @ A @ (B) @ (some @ TA @ C)) = (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 6.40/2.07  thf(29,axiom,((! [TA: $tType]: (((!) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) & ! [B:TA]: (A @ (some @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_split__option__all)).
% 6.40/2.07  thf(275,plain,((! [TA: $tType]: (((!) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) & ! [B:TA]: (A @ (some @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 6.40/2.07  thf(86,axiom,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ (suc @ C)) => (A @ C))) => (A @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_zero__induct)).
% 6.40/2.07  thf(467,plain,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ (suc @ C)) => (A @ C))) => (A @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 6.40/2.07  thf(26,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((product_rec_bool @ TA @ A @ B @ ($false)) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_old_Obool_Osimps_I6_J)).
% 6.40/2.07  thf(252,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((product_rec_bool @ TA @ A @ B @ ($false)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 6.40/2.07  thf(9,axiom,((! [A:(code_natural > $o),B:code_natural]: ((A @ (zero_zero @ code_natural)) => ((! [C:code_natural]: ((A @ C) => (A @ (code_Suc @ C)))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_natural_Oinducts)).
% 6.40/2.07  thf(197,plain,((! [A:(code_natural > $o),B:code_natural]: ((A @ (zero_zero @ code_natural)) => ((! [C:code_natural]: ((A @ C) => (A @ (code_Suc @ C)))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 6.40/2.07  thf(132,axiom,((size_bool = (product_rec_bool @ nat @ (zero_zero @ nat) @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_size__bool__def)).
% 6.40/2.07  thf(625,plain,(((size_bool) = (product_rec_bool @ nat @ (zero_zero @ nat) @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 6.40/2.07  thf(146,axiom,((! [A:nat]: ((suc @ A) != (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_old_Onat_Odistinct_I2_J)).
% 6.40/2.07  thf(665,plain,((! [A:nat]: ~ ((suc @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 6.40/2.07  thf(84,axiom,((! [A:nat,B:nat]: (((suc @ (zero_zero @ nat)) = (plus_plus @ nat @ A @ B)) = (((A = (suc @ (zero_zero @ nat))) & (B = (zero_zero @ nat))) | ((A = (zero_zero @ nat)) & (B = (suc @ (zero_zero @ nat)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_one__is__add)).
% 6.40/2.07  thf(461,plain,((! [A:nat,B:nat]: (((suc @ (zero_zero @ nat)) = (plus_plus @ nat @ A @ B)) = (((A = (suc @ (zero_zero @ nat))) & (B = (zero_zero @ nat))) | ((A = (zero_zero @ nat)) & (B = (suc @ (zero_zero @ nat)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 6.40/2.07  thf(91,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(tuple_isomorphism @ TC @ TB @ TA)]: ((size_size @ (tuple_isomorphism @ TC @ TB @ TA) @ A) != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_tuple__isomorphism_Osize__neq)).
% 6.40/2.07  thf(493,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(tuple_isomorphism @ TC @ TB @ TA)]: ~ ((size_size @ (tuple_isomorphism @ TC @ TB @ TA) @ A) = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 6.40/2.07  thf(82,axiom,(((size_size @ literal) = (^ [A:literal]: (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_size__literal__def)).
% 6.40/2.07  thf(456,plain,(((size_size @ literal) = (^ [A:literal]: (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 6.40/2.07  thf(17,axiom,((! [A:code_natural,B:code_natural]: (((code_Suc @ A) = (code_Suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_natural_Oinject)).
% 6.40/2.07  thf(224,plain,((! [A:code_natural,B:code_natural]: (((code_Suc @ A) = (code_Suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 6.40/2.07  thf(66,axiom,(((size_size @ product_unit) = (product_rec_unit @ nat @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_size__unit__overloaded__def)).
% 6.40/2.07  thf(403,plain,(((size_size @ product_unit) = (product_rec_unit @ nat @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 6.40/2.07  thf(53,axiom,((! [TA: $tType]: (((?) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) | ? [B:TA]: (A @ (some @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_split__option__ex)).
% 6.40/2.07  thf(356,plain,((! [TA: $tType]: (((?) @ (option @ TA)) = (^ [A:((option @ TA) > $o)]: ((A @ (none @ TA)) | ? [B:TA]: (A @ (some @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 6.40/2.07  thf(45,axiom,((! [A:nat]: ((suc @ (suc @ (suc @ A))) = (plus_plus @ nat @ (numeral_numeral @ nat @ (bit1 @ one2)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_Suc3__eq__add__3)).
% 6.40/2.07  thf(328,plain,((! [A:nat]: ((suc @ (suc @ (suc @ A))) = (plus_plus @ nat @ (numeral_numeral @ nat @ (bit1 @ one2)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 6.40/2.07  thf(147,axiom,(((numeral_numeral @ nat @ one2) = (suc @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_numeral__1__eq__Suc__0)).
% 6.40/2.07  thf(669,plain,(((numeral_numeral @ nat @ one2) = (suc @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 6.40/2.07  thf(153,axiom,((! [A:(binDag_Mirabelle_dag > $o),B:binDag_Mirabelle_dag]: ((A @ binDag_Mirabelle_Tip) => ((! [C:binDag_Mirabelle_dag,D:simpl_ref,E:binDag_Mirabelle_dag]: ((A @ C) => ((A @ E) => (A @ (binDag476092410e_Node @ C @ D @ E))))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_dag_Oinduct)).
% 6.40/2.07  thf(686,plain,((! [A:(binDag_Mirabelle_dag > $o),B:binDag_Mirabelle_dag]: ((A @ binDag_Mirabelle_Tip) => ((! [C:binDag_Mirabelle_dag,D:simpl_ref,E:binDag_Mirabelle_dag]: ((A @ C) => ((A @ E) => (A @ (binDag476092410e_Node @ C @ D @ E))))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 6.40/2.07  thf(138,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > nat),B:(TC > nat),C:(TB > nat),D:(TA > (product_prod @ TC @ TB)),E:((product_prod @ TC @ TB) > TA)]: ((tuple_1907371454rphism @ TA @ TC @ TB @ A @ B @ C @ (tuple_742722141rphism @ TA @ TC @ TB @ D @ E)) = (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_tuple__isomorphism_Osize__gen)).
% 6.40/2.07  thf(642,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > nat),B:(TC > nat),C:(TB > nat),D:(TA > (product_prod @ TC @ TB)),E:((product_prod @ TC @ TB) > TA)]: ((tuple_1907371454rphism @ TA @ TC @ TB @ (A) @ (B) @ (C) @ (tuple_742722141rphism @ TA @ TC @ TB @ (D) @ (E))) = (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 6.40/2.07  thf(12,axiom,(((one_one @ nat) = (one_one @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_one__natural_Orsp)).
% 6.40/2.07  thf(212,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 6.40/2.07  thf(131,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: ((size_size @ (list @ TA) @ (splice @ TA @ A @ B)) = (plus_plus @ nat @ (size_size @ (list @ TA) @ A) @ (size_size @ (list @ TA) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_length__splice)).
% 6.40/2.07  thf(622,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: ((size_size @ (list @ TA) @ (splice @ TA @ A @ B)) = (plus_plus @ nat @ (size_size @ (list @ TA) @ A) @ (size_size @ (list @ TA) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 6.40/2.07  thf(62,axiom,((! [A:nat,B:nat]: ((divide_divide @ nat @ A @ (suc @ (suc @ (suc @ B)))) = (divide_divide @ nat @ A @ (plus_plus @ nat @ (numeral_numeral @ nat @ (bit1 @ one2)) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_div__Suc__eq__div__add3)).
% 6.40/2.07  thf(393,plain,((! [A:nat,B:nat]: ((divide_divide @ nat @ A @ (suc @ (suc @ (suc @ B)))) = (divide_divide @ nat @ A @ (plus_plus @ nat @ (numeral_numeral @ nat @ (bit1 @ one2)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 6.40/2.07  thf(154,axiom,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag]: ((size_size @ binDag_Mirabelle_dag @ (binDag476092410e_Node @ A @ B @ C)) = (plus_plus @ nat @ (plus_plus @ nat @ (size_size @ binDag_Mirabelle_dag @ A) @ (size_size @ binDag_Mirabelle_dag @ C)) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_dag_Osize_I4_J)).
% 6.40/2.07  thf(701,plain,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag]: ((size_size @ binDag_Mirabelle_dag @ (binDag476092410e_Node @ A @ B @ C)) = (plus_plus @ nat @ (plus_plus @ nat @ (size_size @ binDag_Mirabelle_dag @ A) @ (size_size @ binDag_Mirabelle_dag @ C)) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 6.40/2.07  thf(94,axiom,((! [A:literal,B:(list @ typerep)]: ((size_typerep @ (typerep3 @ A @ B)) = (plus_plus @ nat @ (size_list @ typerep @ size_typerep @ B) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_typerep_Osize__gen)).
% 6.40/2.07  thf(503,plain,((! [A:literal,B:(list @ typerep)]: ((size_typerep @ (typerep3 @ A @ B)) = (plus_plus @ nat @ (size_list @ typerep @ (size_typerep) @ B) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 6.40/2.07  thf(49,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A != (none @ TA)) => (~ (! [B:TA]: (A != (some @ TA @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_option_Oexhaust)).
% 6.40/2.07  thf(343,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((~ (A = (none @ TA))) => (~ (! [B:TA]: ~ (A = (some @ TA @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 6.40/2.07  thf(42,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 6.40/2.07  thf(311,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 6.40/2.07  thf(105,axiom,((! [A:nat]: (A != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_n__not__Suc__n)).
% 6.40/2.07  thf(541,plain,((! [A:nat]: ~ (A = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 6.40/2.07  thf(111,axiom,(((size_bool @ ($true)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_bool_Osize_I1_J)).
% 6.40/2.07  thf(558,plain,(((size_bool @ ($true)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 6.40/2.07  thf(102,axiom,((! [A:nat,B:nat]: ((plus_plus @ nat @ A @ (suc @ B)) = (suc @ (plus_plus @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_add__Suc__right)).
% 6.40/2.07  thf(530,plain,((! [A:nat,B:nat]: ((plus_plus @ nat @ A @ (suc @ B)) = (suc @ (plus_plus @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 6.40/2.07  thf(118,axiom,(((size_size @ $o @ ($false)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_bool_Osize_I4_J)).
% 6.40/2.07  thf(586,plain,(((size_size @ $o @ ($false)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 6.40/2.07  thf(145,axiom,((! [A:num]: ((size_num @ (bit1 @ A)) = (plus_plus @ nat @ (size_num @ A) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_num_Osize__gen_I3_J)).
% 6.40/2.07  thf(662,plain,((! [A:num]: ((size_num @ (bit1 @ A)) = (plus_plus @ nat @ (size_num @ A) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 6.40/2.07  thf(159,axiom,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > (TA > (TA > TA))))),C:binDag_Mirabelle_dag,D:simpl_ref,E:binDag_Mirabelle_dag]: ((binDag1442713106ec_dag @ TA @ A @ B @ (binDag476092410e_Node @ C @ D @ E)) = (B @ C @ D @ E @ (binDag1442713106ec_dag @ TA @ A @ B @ C) @ (binDag1442713106ec_dag @ TA @ A @ B @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_dag_Osimps_I7_J)).
% 6.40/2.07  thf(718,plain,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > (TA > (TA > TA))))),C:binDag_Mirabelle_dag,D:simpl_ref,E:binDag_Mirabelle_dag]: ((binDag1442713106ec_dag @ TA @ A @ (B) @ (binDag476092410e_Node @ C @ D @ E)) = (B @ C @ D @ E @ (binDag1442713106ec_dag @ TA @ A @ (B) @ C) @ (binDag1442713106ec_dag @ TA @ A @ (B) @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 6.40/2.07  thf(72,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((size_size @ (option @ TA) @ A) != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_option_Osize__neq)).
% 6.40/2.07  thf(430,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ~ ((size_size @ (option @ TA) @ A) = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 6.40/2.07  thf(4,axiom,((! [TA: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA)]: ((case_option @ $o @ TA @ A @ B @ C) => (((C = (none @ TA)) => (~ (A))) => (~ (! [D:TA]: ((C = (some @ TA @ D)) => (~ (B @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_case__optionE)).
% 6.40/2.07  thf(166,plain,((! [TA: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA)]: ((case_option @ $o @ TA @ A @ (B) @ C) => (((C = (none @ TA)) => (~ (A))) => (~ (! [D:TA]: ((C = (some @ TA @ D)) => (~ (B @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 6.40/2.07  thf(77,axiom,(((size_size @ $o) = (product_rec_bool @ nat @ (zero_zero @ nat) @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_size__bool__overloaded__def)).
% 6.40/2.07  thf(444,plain,(((size_size @ $o) = (product_rec_bool @ nat @ (zero_zero @ nat) @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 6.40/2.07  thf(70,axiom,((! [TA: $tType]: ((gen_length @ TA) = (^ [A:nat,B:(list @ TA)]: (plus_plus @ nat @ A @ (size_size @ (list @ TA) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_gen__length__def)).
% 6.40/2.07  thf(423,plain,((! [TA: $tType]: ((gen_length @ TA) = (^ [A:nat,B:(list @ TA)]: (plus_plus @ nat @ A @ (size_size @ (list @ TA) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 6.40/2.07  thf(116,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_nat_Oinject)).
% 6.40/2.07  thf(579,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 6.40/2.07  thf(31,axiom,((! [TA: $tType]: (! [A:(code_natural > TA),B:(code_natural > TA),C:code_natural]: (((A @ (zero_zero @ code_natural)) = (B @ (zero_zero @ code_natural))) => ((! [D:code_natural]: ((A @ (code_Suc @ D)) = (B @ (code_Suc @ D)))) => ((A @ C) = (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_random__aux__rec)).
% 6.40/2.07  thf(281,plain,((! [TA: $tType]: (! [A:(code_natural > TA),B:(code_natural > TA),C:code_natural]: (((A @ (zero_zero @ code_natural)) = (B @ (zero_zero @ code_natural))) => ((! [D:code_natural]: ((A @ (code_Suc @ D)) = (B @ (code_Suc @ D)))) => ((A @ C) = (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 6.40/2.07  thf(106,axiom,((! [A:nat]: ((plus_plus @ nat @ A @ (zero_zero @ nat)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_Nat_Oadd__0__right)).
% 6.40/2.07  thf(545,plain,((! [A:nat]: ((plus_plus @ nat @ A @ (zero_zero @ nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 6.40/2.07  thf(115,axiom,((suc = (^ [A:nat]: (plus_plus @ nat @ A @ (one_one @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_Suc__eq__plus1)).
% 6.40/2.07  thf(577,plain,(((suc) = (^ [A:nat]: (plus_plus @ nat @ A @ (one_one @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 6.40/2.07  thf(157,axiom,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag]: (binDag_Mirabelle_Tip != (binDag476092410e_Node @ A @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_dag_Odistinct_I1_J)).
% 6.40/2.07  thf(711,plain,((! [A:binDag_Mirabelle_dag,B:simpl_ref,C:binDag_Mirabelle_dag]: ~ (binDag_Mirabelle_Tip = (binDag476092410e_Node @ A @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 6.40/2.07  thf(47,axiom,((! [TA: $tType]: (! [A:((option @ TA) > $o),B:(option @ TA)]: ((A @ (none @ TA)) => ((! [C:TA]: (A @ (some @ TA @ C))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_option_Oinducts)).
% 6.40/2.07  thf(335,plain,((! [TA: $tType]: (! [A:((option @ TA) > $o),B:(option @ TA)]: ((A @ (none @ TA)) => ((! [C:TA]: (A @ (some @ TA @ C))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 6.40/2.07  thf(21,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: (((suc @ A) = (size_size @ (list @ TA) @ B)) = (? [C:TA,D:(list @ TA)]: ((B = (cons @ TA @ C @ D)) & ((size_size @ (list @ TA) @ D) = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_Suc__length__conv)).
% 6.40/2.07  thf(236,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: (((suc @ A) = (size_size @ (list @ TA) @ B)) = (? [C:TA,D:(list @ TA)]: ((B = (cons @ TA @ C @ D)) & ((size_size @ (list @ TA) @ D) = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 6.40/2.07  thf(155,axiom,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > TA))),C:binDag_Mirabelle_dag,D:simpl_ref,E:binDag_Mirabelle_dag]: ((binDag1297733282se_dag @ TA @ A @ B @ (binDag476092410e_Node @ C @ D @ E)) = (B @ C @ D @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_dag_Osimps_I5_J)).
% 6.40/2.07  thf(704,plain,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > TA))),C:binDag_Mirabelle_dag,D:simpl_ref,E:binDag_Mirabelle_dag]: ((binDag1297733282se_dag @ TA @ A @ (B) @ (binDag476092410e_Node @ C @ D @ E)) = (B @ C @ D @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 6.40/2.07  thf(151,axiom,(((product_size_unit @ product_Unity) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_unit_Osize_I1_J)).
% 6.40/2.07  thf(681,plain,(((product_size_unit @ product_Unity) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 6.40/2.07  thf(69,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_nat_Odistinct_I1_J)).
% 6.40/2.07  thf(419,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 6.40/2.07  thf(19,axiom,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ((size_size @ (list @ TA) @ (cons @ TA @ A @ B)) = (suc @ (size_size @ (list @ TA) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_length__Cons)).
% 6.40/2.07  thf(230,plain,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ((size_size @ (list @ TA) @ (cons @ TA @ A @ B)) = (suc @ (size_size @ (list @ TA) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 6.40/2.07  thf(55,axiom,(((code_size_natural @ (zero_zero @ code_natural)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_natural_Osize_I1_J)).
% 6.40/2.07  thf(362,plain,(((code_size_natural @ (zero_zero @ code_natural)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 6.40/2.07  thf(44,axiom,((! [A:(product_unit > $o),B:(product_unit > $o)]: (((A @ product_Unity) => (B @ product_Unity)) => (! [C:product_unit]: ((A @ C) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_unit__all__impI)).
% 6.40/2.07  thf(318,plain,((! [A:(product_unit > $o),B:(product_unit > $o)]: (((A @ product_Unity) => (B @ product_Unity)) => (! [C:product_unit]: ((A @ C) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 6.40/2.07  thf(39,axiom,((! [A:product_unit]: (A = product_Unity))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_old_Ounit_Oexhaust)).
% 6.40/2.07  thf(303,plain,((! [A:product_unit]: (A = product_Unity))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 6.40/2.07  thf(10,axiom,((! [A:nat]: ((plus_plus @ nat @ (numeral_numeral @ nat @ (bit0 @ one2)) @ A) = (suc @ (suc @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_add__2__eq__Suc)).
% 6.40/2.07  thf(208,plain,((! [A:nat]: ((plus_plus @ nat @ (numeral_numeral @ nat @ (bit0 @ one2)) @ A) = (suc @ (suc @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 6.40/2.07  thf(60,axiom,((! [TA: $tType]: (! [A:TA]: ((none @ TA) != (some @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_option_Odistinct_I1_J)).
% 6.40/2.07  thf(387,plain,((! [TA: $tType]: (! [A:TA]: ~ ((none @ TA) = (some @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 6.40/2.07  thf(121,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > TA))),D:binDag_Mirabelle_dag]: ((A @ (binDag1297733282se_dag @ TA @ B @ C @ D)) = (binDag1297733282se_dag @ TB @ (A @ B) @ (^ [E:binDag_Mirabelle_dag,F:simpl_ref,G:binDag_Mirabelle_dag]: (A @ (C @ E @ F @ G))) @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_dag_Ocase__distrib)).
% 6.40/2.07  thf(594,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > TA))),D:binDag_Mirabelle_dag]: ((A @ (binDag1297733282se_dag @ TA @ B @ (C) @ D)) = (binDag1297733282se_dag @ TB @ (A @ B) @ (^ [E:binDag_Mirabelle_dag,F:simpl_ref,G:binDag_Mirabelle_dag]: (A @ (C @ E @ F @ G))) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 6.40/2.07  thf(13,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:nat]: (((size_size @ (list @ TA) @ A) = (suc @ B)) = (? [C:TA,D:(list @ TA)]: ((A = (cons @ TA @ C @ D)) & ((size_size @ (list @ TA) @ D) = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_length__Suc__conv)).
% 6.40/2.07  thf(213,plain,((! [TA: $tType]: (! [A:(list @ TA),B:nat]: (((size_size @ (list @ TA) @ A) = (suc @ B)) = (? [C:TA,D:(list @ TA)]: ((A = (cons @ TA @ C @ D)) & ((size_size @ (list @ TA) @ D) = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 6.40/2.07  thf(99,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_Zero__not__Suc)).
% 6.40/2.07  thf(520,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 6.40/2.07  thf(64,axiom,((suc = (plus_plus @ nat @ (one_one @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_Suc__eq__plus1__left)).
% 6.40/2.07  thf(399,plain,(((suc) = (plus_plus @ nat @ (one_one @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 6.40/2.07  thf(30,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((A = (none @ TA)) = (case_option @ $o @ TA @ ($true) @ (^ [B:TA]: (($false))) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_option_Odisc__eq__case_I1_J)).
% 6.40/2.07  thf(278,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((A = (none @ TA)) = (case_option @ $o @ TA @ ($true) @ (^ [B:TA]: (($false))) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 6.40/2.07  thf(126,axiom,((! [A:nat]: ((suc @ A) != (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_Suc__neq__Zero)).
% 6.40/2.07  thf(608,plain,((! [A:nat]: ~ ((suc @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 6.40/2.07  thf(40,axiom,(((numeral_numeral @ nat @ (bit0 @ one2)) = (suc @ (suc @ (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_numeral__2__eq__2)).
% 6.40/2.07  thf(306,plain,(((numeral_numeral @ nat @ (bit0 @ one2)) = (suc @ (suc @ (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 6.40/2.07  thf(142,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB]: ((size_size @ (sum_sum @ TB @ TA) @ (sum_Inl @ TB @ TA @ A)) = (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_sum_Osize_I3_J)).
% 6.40/2.07  thf(653,plain,((! [TA: $tType,TB: $tType]: (! [A:TB]: ((size_size @ (sum_sum @ TB @ TA) @ (sum_Inl @ TB @ TA @ A)) = (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 6.40/2.07  thf(149,axiom,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = A) => (B = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_add__eq__self__zero)).
% 6.40/2.07  thf(675,plain,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = A) => (B = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 6.40/2.07  thf(71,axiom,((! [A:num]: ((nat_of_num @ A) != (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_nat__of__num__neq__0)).
% 6.40/2.07  thf(426,plain,((! [A:num]: ~ ((nat_of_num @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 6.40/2.07  thf(107,axiom,(((size_size @ num @ one2) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_num_Osize_I4_J)).
% 6.40/2.07  thf(548,plain,(((size_size @ num @ one2) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 6.40/2.07  thf(27,axiom,((! [TA: $tType]: (! [A:(product_unit > TA)]: ((^ [B:product_unit]: (A @ product_Unity)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_unit__abs__eta__conv)).
% 6.40/2.07  thf(255,plain,((! [TA: $tType]: (! [A:(product_unit > TA)]: ((^ [B:product_unit]: (A @ product_Unity)) = (A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 6.40/2.07  thf(140,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_old_Onat_Oinject)).
% 6.40/2.07  thf(648,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 6.40/2.07  thf(129,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > nat),B:(TA > nat),C:TA]: ((basic_BNF_size_sum @ TB @ TA @ A @ B @ (sum_Inr @ TA @ TB @ C)) = (plus_plus @ nat @ (B @ C) @ (suc @ (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_sum_Osize__gen_I2_J)).
% 6.40/2.07  thf(617,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > nat),B:(TA > nat),C:TA]: ((basic_BNF_size_sum @ TB @ TA @ (A) @ (B) @ (sum_Inr @ TA @ TB @ C)) = (plus_plus @ nat @ (B @ C) @ (suc @ (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 6.40/2.07  thf(109,axiom,((! [TA: $tType]: ((size_size @ (list @ TA)) = (gen_length @ TA @ (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_length__code)).
% 6.40/2.07  thf(553,plain,((! [TA: $tType]: ((size_size @ (list @ TA)) = (gen_length @ TA @ (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 6.40/2.07  thf(83,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB]: ((size_size @ (sum_sum @ TA @ TB) @ (sum_Inr @ TB @ TA @ A)) = (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_sum_Osize_I4_J)).
% 6.40/2.07  thf(458,plain,((! [TA: $tType,TB: $tType]: (! [A:TB]: ((size_size @ (sum_sum @ TA @ TB) @ (sum_Inr @ TB @ TA @ A)) = (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 6.40/2.07  thf(36,axiom,(((suc @ (one_one @ nat)) = (numeral_numeral @ nat @ (bit0 @ one2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_Suc__1)).
% 6.40/2.07  thf(295,plain,(((suc @ (one_one @ nat)) = (numeral_numeral @ nat @ (bit0 @ one2)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 6.40/2.07  thf(156,axiom,((! [A:binDag_Mirabelle_dag]: ((A != binDag_Mirabelle_Tip) => (~ (! [B:binDag_Mirabelle_dag,C:simpl_ref,D:binDag_Mirabelle_dag]: (A != (binDag476092410e_Node @ B @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_dag_Oexhaust)).
% 6.40/2.07  thf(707,plain,((! [A:binDag_Mirabelle_dag]: ((~ (A = binDag_Mirabelle_Tip)) => (~ (! [B:binDag_Mirabelle_dag,C:simpl_ref,D:binDag_Mirabelle_dag]: ~ (A = (binDag476092410e_Node @ B @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 6.40/2.07  thf(46,axiom,((! [A:code_natural]: ((code_Suc @ A) != (zero_zero @ code_natural)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_natural_Odistinct_I2_J)).
% 6.40/2.07  thf(331,plain,((! [A:code_natural]: ~ ((code_Suc @ A) = (zero_zero @ code_natural)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 6.40/2.07  thf(76,axiom,((! [A:num]: ((size_size @ num @ (bit1 @ A)) = (plus_plus @ nat @ (size_size @ num @ A) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_num_Osize_I6_J)).
% 6.40/2.07  thf(441,plain,((! [A:num]: ((size_size @ num @ (bit1 @ A)) = (plus_plus @ nat @ (size_size @ num @ A) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 6.40/2.07  thf(58,axiom,((! [A:num]: ((suc @ (numeral_numeral @ nat @ A)) = (numeral_numeral @ nat @ (plus_plus @ num @ A @ one2))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_Suc__numeral)).
% 6.40/2.07  thf(370,plain,((! [A:num]: ((suc @ (numeral_numeral @ nat @ A)) = (numeral_numeral @ nat @ (plus_plus @ num @ A @ one2))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 6.40/2.07  thf(54,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TA]: ((sum_Inr @ TB @ TA @ A) != (sum_Inl @ TA @ TB @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_Inr__Inl__False)).
% 6.40/2.07  thf(359,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TA]: ~ ((sum_Inr @ TB @ TA @ A) = (sum_Inl @ TA @ TB @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 6.40/2.07  thf(143,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ C @ B)) = (A = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_nat__add__right__cancel)).
% 6.40/2.07  thf(656,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ C @ B)) = (A = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 6.40/2.07  thf(123,axiom,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = (suc @ (zero_zero @ nat))) = (((A = (suc @ (zero_zero @ nat))) & (B = (zero_zero @ nat))) | ((A = (zero_zero @ nat)) & (B = (suc @ (zero_zero @ nat)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_add__is__1)).
% 6.40/2.07  thf(600,plain,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = (suc @ (zero_zero @ nat))) = (((A = (suc @ (zero_zero @ nat))) & (B = (zero_zero @ nat))) | ((A = (zero_zero @ nat)) & (B = (suc @ (zero_zero @ nat)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 6.40/2.07  thf(5,axiom,((! [TA: $tType,TB: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA),D:(TB > $o),E:TB,F:(TA > TB)]: ((case_option @ $o @ TA @ A @ B @ C) => (((A) => (D @ E)) => ((! [G:TA]: ((B @ G) => (D @ (F @ G)))) => (D @ (case_option @ TB @ TA @ E @ F @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_disjE__realizer2)).
% 6.40/2.07  thf(175,plain,((! [TA: $tType,TB: $tType]: (! [A:$o,B:(TA > $o),C:(option @ TA),D:(TB > $o),E:TB,F:(TA > TB)]: ((case_option @ $o @ TA @ A @ (B) @ C) => (((A) => (D @ E)) => ((! [G:TA]: ((B @ G) => (D @ (F @ G)))) => (D @ (case_option @ TB @ TA @ E @ (F) @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 6.40/2.07  thf(127,axiom,(((size_size @ code_natural) = (code_rec_natural @ nat @ (zero_zero @ nat) @ (^ [A:code_natural,B:nat]: (plus_plus @ nat @ B @ (suc @ (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_size__natural__overloaded__def)).
% 6.40/2.07  thf(612,plain,(((size_size @ code_natural) = (code_rec_natural @ nat @ (zero_zero @ nat) @ (^ [A:code_natural,B:nat]: (plus_plus @ nat @ B @ (suc @ (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 6.40/2.07  thf(78,axiom,(((zero_zero @ nat) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_zero__natural_Orsp)).
% 6.40/2.07  thf(446,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 6.40/2.07  thf(113,axiom,((! [A:num]: ((size_num @ (bit0 @ A)) = (plus_plus @ nat @ (size_num @ A) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_num_Osize__gen_I2_J)).
% 6.40/2.07  thf(571,plain,((! [A:num]: ((size_num @ (bit0 @ A)) = (plus_plus @ nat @ (size_num @ A) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 6.40/2.07  thf(133,axiom,((product_size_unit = (product_rec_unit @ nat @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_size__unit__def)).
% 6.40/2.07  thf(627,plain,(((product_size_unit) = (product_rec_unit @ nat @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 6.40/2.07  thf(110,axiom,(((size_size @ $o @ ($true)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_bool_Osize_I3_J)).
% 6.40/2.07  thf(556,plain,(((size_size @ $o @ ($true)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 6.40/2.07  thf(89,axiom,((! [TA: $tType]: (! [A:(TA > nat),B:TA]: ((size_option @ TA @ A @ (some @ TA @ B)) = (plus_plus @ nat @ (A @ B) @ (suc @ (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_option_Osize__gen_I2_J)).
% 6.40/2.07  thf(482,plain,((! [TA: $tType]: (! [A:(TA > nat),B:TA]: ((size_option @ TA @ (A) @ (some @ TA @ B)) = (plus_plus @ nat @ (A @ B) @ (suc @ (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 6.40/2.07  thf(148,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_old_Onat_Odistinct_I1_J)).
% 6.40/2.07  thf(671,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 6.40/2.07  thf(100,axiom,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > (TA > (TA > TA)))))]: ((binDag1442713106ec_dag @ TA @ A @ B @ binDag_Mirabelle_Tip) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_dag_Osimps_I6_J)).
% 6.40/2.07  thf(524,plain,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > (TA > (TA > TA)))))]: ((binDag1442713106ec_dag @ TA @ A @ (B) @ binDag_Mirabelle_Tip) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 6.40/2.07  thf(15,axiom,((! [A:num,B:nat]: ((suc @ (plus_plus @ nat @ (numeral_numeral @ nat @ A) @ B)) = (plus_plus @ nat @ (numeral_numeral @ nat @ (plus_plus @ num @ A @ one2)) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_Suc__nat__number__of__add)).
% 6.40/2.07  thf(218,plain,((! [A:num,B:nat]: ((suc @ (plus_plus @ nat @ (numeral_numeral @ nat @ A) @ B)) = (plus_plus @ nat @ (numeral_numeral @ nat @ (plus_plus @ num @ A @ one2)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 6.40/2.07  thf(57,axiom,(((default_default @ product_unit) = product_Unity)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_default__unit__def)).
% 6.40/2.07  thf(368,plain,(((default_default @ product_unit) = product_Unity)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 6.40/2.07  thf(119,axiom,((! [TA: $tType]: (! [A:TA]: ((size_size @ (option @ TA) @ (some @ TA @ A)) = (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_option_Osize_I4_J)).
% 6.40/2.07  thf(588,plain,((! [TA: $tType]: (! [A:TA]: ((size_size @ (option @ TA) @ (some @ TA @ A)) = (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 6.40/2.07  thf(98,axiom,((! [TA: $tType]: (! [A:(TA > nat),B:TA,C:(list @ TA)]: ((size_list @ TA @ A @ (cons @ TA @ B @ C)) = (plus_plus @ nat @ (plus_plus @ nat @ (A @ B) @ (size_list @ TA @ A @ C)) @ (suc @ (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_list_Osize__gen_I2_J)).
% 6.40/2.07  thf(517,plain,((! [TA: $tType]: (! [A:(TA > nat),B:TA,C:(list @ TA)]: ((size_list @ TA @ (A) @ (cons @ TA @ B @ C)) = (plus_plus @ nat @ (plus_plus @ nat @ (A @ B) @ (size_list @ TA @ (A) @ C)) @ (suc @ (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 6.40/2.07  thf(28,axiom,((! [TA: $tType,TB: $tType]: (! [A:(option @ TB),B:((option @ TB) > ((option @ TA) > $o)),C:(option @ TA)]: (((A = (none @ TB)) => (B @ A @ C)) => (((C = (none @ TA)) => (B @ A @ C)) => ((! [D:TB,E:TA]: ((A = (some @ TB @ D)) => ((C = (some @ TA @ E)) => (B @ A @ C)))) => (B @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_combine__options__cases)).
% 6.40/2.07  thf(258,plain,((! [TA: $tType,TB: $tType]: (! [A:(option @ TB),B:((option @ TB) > ((option @ TA) > $o)),C:(option @ TA)]: (((A = (none @ TB)) => (B @ A @ C)) => (((C = (none @ TA)) => (B @ A @ C)) => ((! [D:TB,E:TA]: ((A = (some @ TB @ D)) => ((C = (some @ TA @ E)) => (B @ A @ C)))) => (B @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 6.40/2.07  thf(61,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: (((some @ TA @ A) = (some @ TA @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_option_Oinject)).
% 6.40/2.07  thf(390,plain,((! [TA: $tType]: (! [A:TA,B:TA]: (((some @ TA @ A) = (some @ TA @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 6.40/2.07  thf(135,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > (product_prod @ TC @ TB)),B:((product_prod @ TC @ TB) > TA)]: ((size_size @ (tuple_isomorphism @ TA @ TC @ TB) @ (tuple_742722141rphism @ TA @ TC @ TB @ A @ B)) = (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_tuple__isomorphism_Osize_I2_J)).
% 6.40/2.07  thf(632,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > (product_prod @ TC @ TB)),B:((product_prod @ TC @ TB) > TA)]: ((size_size @ (tuple_isomorphism @ TA @ TC @ TB) @ (tuple_742722141rphism @ TA @ TC @ TB @ (A) @ (B))) = (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 6.40/2.07  thf(65,axiom,(((size_size @ code_natural @ (zero_zero @ code_natural)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_natural_Osize_I3_J)).
% 6.40/2.07  thf(401,plain,(((size_size @ code_natural @ (zero_zero @ code_natural)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 6.40/2.07  thf(24,axiom,((! [TA: $tType]: (! [A:TA,B:(code_natural > (TA > TA)),C:code_natural]: ((code_rec_natural @ TA @ A @ B @ (code_Suc @ C)) = (B @ C @ (code_rec_natural @ TA @ A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_natural_Osimps_I7_J)).
% 6.40/2.07  thf(246,plain,((! [TA: $tType]: (! [A:TA,B:(code_natural > (TA > TA)),C:code_natural]: ((code_rec_natural @ TA @ A @ (B) @ (code_Suc @ C)) = (B @ C @ (code_rec_natural @ TA @ A @ (B) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 6.40/2.07  thf(73,axiom,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TB @ TA)]: ((size_size @ (product_prod @ TB @ TA) @ A) != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_prod_Osize__neq)).
% 6.40/2.07  thf(433,plain,((! [TA: $tType,TB: $tType]: (! [A:(product_prod @ TB @ TA)]: ~ ((size_size @ (product_prod @ TB @ TA) @ A) = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 6.40/2.07  thf(87,axiom,(((size_size @ binDag_Mirabelle_dag @ binDag_Mirabelle_Tip) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_dag_Osize_I3_J)).
% 6.40/2.07  thf(478,plain,(((size_size @ binDag_Mirabelle_dag @ binDag_Mirabelle_Tip) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 6.40/2.07  thf(50,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((product_rec_bool @ TA @ A @ B @ ($true)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_old_Obool_Osimps_I5_J)).
% 6.40/2.07  thf(346,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((product_rec_bool @ TA @ A @ B @ ($true)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 6.40/2.07  thf(33,axiom,(((size_num @ one2) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_num_Osize__gen_I1_J)).
% 6.40/2.07  thf(287,plain,(((size_num @ one2) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 6.40/2.07  thf(38,axiom,((! [A:num]: ((nat_of_num @ (bit0 @ A)) = (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_nat__of__num_Osimps_I2_J)).
% 6.40/2.07  thf(300,plain,((! [A:num]: ((nat_of_num @ (bit0 @ A)) = (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 6.40/2.07  thf(130,axiom,(((size_size @ product_unit @ product_Unity) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_unit_Osize_I2_J)).
% 6.40/2.07  thf(620,plain,(((size_size @ product_unit @ product_Unity) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 6.40/2.07  thf(79,axiom,((code_size_natural = (code_rec_natural @ nat @ (zero_zero @ nat) @ (^ [A:code_natural,B:nat]: (plus_plus @ nat @ B @ (suc @ (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_size__natural__def)).
% 6.40/2.07  thf(447,plain,(((code_size_natural) = (code_rec_natural @ nat @ (zero_zero @ nat) @ (^ [A:code_natural,B:nat]: (plus_plus @ nat @ B @ (suc @ (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 6.40/2.07  thf(67,axiom,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_old_Onat_Oinducts)).
% 6.40/2.07  thf(405,plain,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 6.40/2.07  thf(59,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:TA,B:((sum_sum @ TC @ TB) > TA),C:$o]: ((! [D:TC]: ((A = (B @ (sum_Inl @ TC @ TB @ D))) => (C))) => ((! [D:TB]: ((A = (B @ (sum_Inr @ TB @ TC @ D))) => (C))) => (! [D:(sum_sum @ TC @ TB)]: ((A = (B @ D)) => (C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_obj__sumE__f)).
% 6.40/2.07  thf(373,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:TA,B:((sum_sum @ TC @ TB) > TA),C:$o]: ((! [D:TC]: ((A = (B @ (sum_Inl @ TC @ TB @ D))) => (C))) => ((! [D:TB]: ((A = (B @ (sum_Inr @ TB @ TC @ D))) => (C))) => (! [D:(sum_sum @ TC @ TB)]: ((A = (B @ D)) => (C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 6.40/2.07  thf(124,axiom,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (plus_plus @ nat @ A @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_add__Suc__shift)).
% 6.40/2.07  thf(603,plain,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (plus_plus @ nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 6.40/2.07  thf(95,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat]: (A @ D @ (zero_zero @ nat))) => ((! [D:nat]: (A @ (zero_zero @ nat) @ (suc @ D))) => ((! [D:nat,E:nat]: ((A @ D @ E) => (A @ (suc @ D) @ (suc @ E)))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_diff__induct)).
% 6.40/2.07  thf(506,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat]: (A @ D @ (zero_zero @ nat))) => ((! [D:nat]: (A @ (zero_zero @ nat) @ (suc @ D))) => ((! [D:nat,E:nat]: ((A @ D @ E) => (A @ (suc @ D) @ (suc @ E)))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 6.40/2.07  thf(8,axiom,(((plus_plus @ nat @ (one_one @ nat) @ (one_one @ nat)) = (numeral_numeral @ nat @ (bit0 @ one2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_nat__1__add__1)).
% 6.40/2.07  thf(195,plain,(((plus_plus @ nat @ (one_one @ nat) @ (one_one @ nat)) = (numeral_numeral @ nat @ (bit0 @ one2)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 6.40/2.07  thf(136,axiom,((! [A:literal,B:(list @ typerep)]: ((size_size @ typerep @ (typerep3 @ A @ B)) = (plus_plus @ nat @ (size_list @ typerep @ (size_size @ typerep) @ B) @ (suc @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_typerep_Osize_I2_J)).
% 6.40/2.07  thf(635,plain,((! [A:literal,B:(list @ typerep)]: ((size_size @ typerep @ (typerep3 @ A @ B)) = (plus_plus @ nat @ (size_list @ typerep @ (size_size @ typerep) @ B) @ (suc @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 6.40/2.07  thf(22,axiom,((! [TA: $tType]: (! [A:(option @ TA)]: ((! [B:TA]: (A != (some @ TA @ B))) = (A = (none @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_not__Some__eq)).
% 6.40/2.07  thf(239,plain,((! [TA: $tType]: (! [A:(option @ TA)]: ((! [B:TA]: ~ (A = (some @ TA @ B))) = (A = (none @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 6.40/2.07  thf(23,axiom,((! [TA: $tType]: (! [A:(option @ TA),B:TA]: ((A = (some @ TA @ B)) => (A != (none @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_option_OdiscI)).
% 6.40/2.07  thf(242,plain,((! [TA: $tType]: (! [A:(option @ TA),B:TA]: ((A = (some @ TA @ B)) => (~ (A = (none @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 6.40/2.07  thf(85,axiom,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > TA)))]: ((binDag1297733282se_dag @ TA @ A @ B @ binDag_Mirabelle_Tip) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_dag_Osimps_I4_J)).
% 6.40/2.07  thf(464,plain,((! [TA: $tType]: (! [A:TA,B:(binDag_Mirabelle_dag > (simpl_ref > (binDag_Mirabelle_dag > TA)))]: ((binDag1297733282se_dag @ TA @ A @ (B) @ binDag_Mirabelle_Tip) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 6.40/2.07  thf(3,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(TB > TA)]: ((case_option @ TA @ TB @ A @ B @ (none @ TB)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_option_Osimps_I4_J)).
% 6.40/2.07  thf(163,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(TB > TA)]: ((case_option @ TA @ TB @ A @ (B) @ (none @ TB)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 6.40/2.07  thf(93,axiom,(((binDag1924123185ze_dag @ binDag_Mirabelle_Tip) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_dag_Osize__gen_I1_J)).
% 6.40/2.07  thf(501,plain,(((binDag1924123185ze_dag @ binDag_Mirabelle_Tip) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 6.40/2.07  thf(18,axiom,((! [A:num,B:num]: ((nat_of_num @ (plus_plus @ num @ A @ B)) = (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_nat__of__num__add)).
% 6.40/2.07  thf(227,plain,((! [A:num,B:num]: ((nat_of_num @ (plus_plus @ num @ A @ B)) = (plus_plus @ nat @ (nat_of_num @ A) @ (nat_of_num @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 6.40/2.07  thf(144,axiom,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ((size_size @ (list @ TA) @ (cons @ TA @ A @ B)) = (plus_plus @ nat @ (size_size @ (list @ TA) @ B) @ (suc @ (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_list_Osize_I4_J)).
% 6.40/2.07  thf(659,plain,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ((size_size @ (list @ TA) @ (cons @ TA @ A @ B)) = (plus_plus @ nat @ (size_size @ (list @ TA) @ B) @ (suc @ (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 6.40/2.07  thf(112,axiom,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_nat__induct)).
% 6.40/2.07  thf(560,plain,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 6.40/2.07  thf(92,axiom,((! [A:nat,B:nat]: ((A = (suc @ B)) => (A != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_nat_OdiscI)).
% 6.40/2.07  thf(496,plain,((! [A:nat,B:nat]: ((A = (suc @ B)) => (~ (A = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 6.40/2.07  thf(56,axiom,((! [A:code_natural]: ((A != (zero_zero @ code_natural)) => (~ (! [B:code_natural]: (A != (code_Suc @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_natural_Oexhaust)).
% 6.40/2.07  thf(364,plain,((! [A:code_natural]: ((~ (A = (zero_zero @ code_natural))) => (~ (! [B:code_natural]: ~ (A = (code_Suc @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 6.40/2.07  thf(723,plain,(($false)),inference(e,[status(thm)],[645,629,249,352,582,683,308,449,511,614,597,533,550,715,340,538,436,651,638,189,606,284,416,289,216,591,211,485,514,574,480,221,453,396,527,312,292,233,439,678,349,160,297,192,275,467,252,197,625,665,461,493,456,224,403,356,328,669,686,642,212,622,393,701,503,343,311,541,558,530,586,662,718,430,166,444,423,579,281,545,577,711,335,236,704,681,419,230,362,318,303,208,387,594,213,520,399,278,608,306,653,675,426,548,255,648,617,553,458,295,707,331,441,370,359,656,600,175,612,446,571,627,556,482,671,524,218,368,588,517,258,390,632,401,246,433,478,346,287,300,620,447,405,373,603,506,195,635,239,242,464,163,501,227,659,560,496,364])).
% 6.40/2.07  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.40/2.07  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------