%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP053^1 : TPTP v9.3.1. Released v7.5.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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:34 AM UTC 2026
% Result : Theorem 98.50s 42.34s
% Output : Refutation 99.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP053^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % 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.08/0.23 % Computer : n008.cluster.edu
% 0.08/0.23 % Model : x86_64 x86_64
% 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.23 % Memory : 8046.5625MB
% 0.08/0.23 % OS : Linux 6.8.0-71-generic
% 0.08/0.24 % CPULimit : 300
% 0.08/0.24 % WCLimit : 300
% 0.08/0.24 % DateTime : Tue Sep 29 19:44:24 UTC 2026
% 0.08/0.24 % CPUTime :
% 0.08/0.24 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
% 1.04/0.84 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.30/1.28 % [INFO] Parsing done (434ms).
% 2.77/1.30 % [INFO] Running in sequential loop mode.
% 3.79/1.60 % [INFO] eprover registered as external prover.
% 3.79/1.60 % [INFO] Scanning for conjecture ...
% 3.79/1.67 % [INFO] Found a conjecture (or negated_conjecture) and 254 axioms. Running axiom selection ...
% 4.10/1.75 % [INFO] Axiom selection finished. Selected 228 axioms (removed 26 axioms).
% 4.91/1.91 % [INFO] Problem is higher-order (TPTP THF).
% 4.91/1.94 % [INFO] Type checking passed.
% 4.91/1.94 % [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 ...
% 98.50/42.33 % External prover 'e' found a proof!
% 98.50/42.33 % [INFO] Killing All external provers ...
% 98.50/42.33 % Time passed: 41941ms (effective reasoning time: 41024ms)
% 98.50/42.33 % 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)>
% 98.50/42.34 % Axioms used in derivation (228): fact_175_old_Oprod_Oexhaust, fact_152_add__le__less__mono, fact_2__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_Au_At_A_061_A1_A_L_Alength_Ap2_092_060close_062, fact_183_le__antisym, fact_56_add__le__cancel__right, fact_146_add__mono__thms__linordered__field_I5_J, fact_84_add__mono, fact_149_Graph_OshortestPath__is__simple, fact_39_assms_I4_J, fact_221_dual__order_Otrans, fact_212_isPath_Osimps_I1_J, fact_101_min__dist__less, fact_139_add__less__imp__less__right, fact_248_order_Ostrict__trans, fact_199_discrete, fact_235_antisym, fact_144_add__mono__thms__linordered__field_I1_J, fact_66_Graph_Oconnected__refl, fact_231_order_Otrans, fact_193_add__leD2, fact_135_less__irrefl__nat, fact_127_add__less__mono1, fact_227_ord__eq__le__trans, fact_81_add__mono__thms__linordered__semiring_I3_J, fact_91_Graph_Omin__dist__minD, fact_247_less__imp__not__less, fact_198_isSPath__nt__parallel, fact_190_add__le__mono1, fact_38_shortestPath__is__path, fact_70_Graph_OisShortestPath__level__edge_I2_J, fact_54_isShortestPath__level__edge_I3_J, fact_8_min__dist__split_I1_J, fact_131_nat__neq__iff, fact_213_order__refl, fact_116_Graph_OisSimplePath_Ocong, fact_166_Pair__inject, fact_34_min__distI__eq, fact_179_size__neq__size__imp__neq, fact_233_eq__refl, fact_59_isShortestPath__level__edge_I4_J, fact_118_le__neq__implies__less, fact_238_ord__eq__le__subst, fact_178_old_Oprod_Oinducts, fact_242_order_Ostrict__implies__not__eq, fact_58_isShortestPath__level__edge_I5_J, fact_145_add__mono__thms__linordered__field_I2_J, fact_23_add_Ocommute, fact_14_isPath__distD, fact_22_add_Oleft__commute, fact_5__092_060open_062u_A_092_060noteq_062_Av_092_060close_062, fact_181_le__trans, fact_71_Graph_OisShortestPath__level__edge_I3_J, fact_250_linorder__cases, fact_78_Graph_OisShortestPath__level__edge_I4_J, fact_61_connected__distI, fact_229_antisym__conv, fact_93_Graph_Omin__dist__is__dist, fact_60_connected__refl, fact_226_ord__le__eq__trans, fact_103_isSPath__sg__incoming, fact_40_connected__def, fact_129_trans__less__add2, fact_32_Graph_Odist__def, fact_16_DISTS_I2_J, fact_141_add__strict__right__mono, fact_83_add__mono__thms__linordered__semiring_I1_J, fact_223_dual__order_Orefl, fact_128_trans__less__add1, fact_37_min__dist__is__dist, fact_104_isSPath__sg__outgoing, fact_192_le__Suc__ex, fact_20_add__right__imp__eq, fact_243_not__less__iff__gr__or__eq, fact_187_nat__le__iff__add, fact_51_isShortestPath__def, fact_125_not__add__less1, fact_151_add__mono__thms__linordered__field_I3_J, fact_107_old_Oprod_Oinject, fact_123_add__lessD1, fact_119_less__or__eq__imp__le, fact_6_MDSV, fact_224_order__trans, fact_111_isSPath__pathLE, fact_44_Collect__cong, fact_64_Graph_Oobtain__shortest__path, fact_33_min__dist__minD, fact_55_add__le__cancel__left, fact_218_Graph_OisPath_Osimps_I1_J, fact_186_Graph_OisShortestPath__alt, fact_79_Graph_Omin__distI2, fact_62_Graph_OisPath__ex__edge1, fact_80_Graph_OisShortestPath__def, fact_47_isPath__ex__edge1, fact_21_add__left__imp__eq, fact_88_le__iff__add, fact_99_nat__add__left__cancel__le, fact_206_bounded__Max__nat, fact_188_trans__le__add2, fact_102_isSPath__no__selfloop, fact_25_group__cancel_Oadd2, fact_237_ord__le__eq__subst, fact_148_Graph_OisSPath__pathLE, fact_130_less__add__eq__less, fact_120_le__eq__less__or__eq, fact_87_add__right__mono, fact_160_surj__pair, fact_197_add__leE, fact_134_less__not__refl3, fact_215_simplePath__same__conv, fact_27_add__mono__thms__linordered__semiring_I4_J, fact_0_MIN_H, fact_228_order__class_Oorder_Oeq__iff, fact_69_Graph_OisShortestPath__level__edge_I1_J, fact_57_isShortestPath__level__edge_I6_J, fact_72_Graph_Oconnected__def, fact_36_Graph_Omin__dist__split_I2_J, fact_113_add__less__cancel__right, fact_191_add__le__mono, fact_35_Graph_Omin__dist__split_I1_J, fact_133_less__not__refl2, fact_3__092_060open_062min__dist_Av_At_A_061_Alength_Ap2_092_060close_062, fact_52_isShortestPath__level__edge_I1_J, fact_31_Graph_OisPath__distD, fact_219_dual__order_Oantisym, fact_194_add__leD1, fact_43_Collect__mem__eq, fact_92_Graph_Omin__distI__eq, fact_100_isShortestPath__alt, fact_63_Graph_OisPath__ex__edge2, fact_68_Graph_Omin__dist__le, fact_154_Graph_Omin__dist__less, fact_217_Graph_OsimplePath__same__conv, fact_117_less__mono__imp__le__mono, fact_121_less__imp__le__nat, fact_98_Graph_Odist__trans, fact_115_nat__add__left__cancel__less, fact_95_Graph_OisPath_Ocong, fact_200_swap__swap, fact_220_dual__order_Oeq__iff, fact_209_Graph_OisSPath__nt__parallel, fact_65_Graph_OisShortestPath_Ocong, fact_94_Graph_OisShortestPath__min__dist__def, fact_1__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_As_Au_A_061_Alength_Ap1_092_060close_062, fact_184_nat__le__linear, fact_124_add__less__mono, fact_9_add__left__cancel, fact_153_add__less__le__mono, fact_147_mono__nat__linear__lb, fact_10_add__right__cancel, fact_89_add__le__imp__le__left, fact_86_less__eqE, fact_142_add__strict__left__mono, fact_74_Graph_Oconnected__distI, fact_75_Graph_OshortestPath__is__path, fact_12_assms_I3_J, fact_230_le__cases3, fact_137_infinite__descent, fact_29_one__reorient, fact_205_swap__simp, fact_251_less__imp__triv, fact_156_Graph_OisSPath__sg__incoming, fact_241_dual__order_Ostrict__implies__not__eq, fact_195_le__add2, fact_143_add__strict__mono, fact_13_DISTS_I1_J, fact_225_order__class_Oorder_Oantisym, fact_132_less__not__refl, fact_48_isPath__ex__edge2, fact_96_Graph_Omin__dist_Ocong, fact_253_antisym__conv3, fact_4_MIN, fact_76_Graph_OisShortestPath__level__edge_I6_J, fact_140_add__less__imp__less__left, fact_30_isShortestPath__min__dist__def, fact_73_Graph_Oconnected__by__dist, fact_246_exists__least__iff, fact_77_Graph_OisShortestPath__level__edge_I5_J, fact_126_not__add__less2, fact_114_add__less__cancel__left, fact_110_prod_Oinject, fact_240_order__subst1, fact_28_ab__semigroup__add__class_Oadd__ac_I1_J, fact_24_add_Oassoc, fact_7_min__dist__split_I2_J, fact_236_eq__iff, fact_196_le__add1, fact_67_Graph_Oconnected_Ocong, fact_90_add__le__imp__le__right, fact_157_Graph_OisSPath__sg__outgoing, fact_42_mem__Collect__eq, fact_53_isShortestPath__level__edge_I2_J, fact_19_assms_I1_J, fact_26_group__cancel_Oadd1, fact_122_nat__less__le, fact_222_linorder__wlog, fact_216_Graph_OsimplePath__empty__conv, fact_136_nat__less__induct, fact_244_dual__order_Ostrict__trans, fact_112_shortestPath__is__simple, fact_214_simplePath__empty__conv, fact_189_trans__le__add1, fact_11_dist__trans, fact_41_connected__by__dist, fact_15_dist__def, fact_17_P, fact_239_order__subst2, fact_210_less__add__one, fact_234_linear, fact_180_le__refl, fact_155_Graph_OisSPath__no__selfloop, fact_18_DISTS_I3_J, fact_82_add__mono__thms__linordered__semiring_I2_J, fact_45_obtain__shortest__path, fact_245_linorder__less__wlog, fact_46_assms_I2_J, fact_252_less__imp__not__eq2, fact_185_Nat_Oex__has__greatest__nat, fact_85_add__left__mono, fact_211_add__mono1, fact_249_dual__order_Oirrefl, fact_49_min__dist__le, fact_150_add__mono__thms__linordered__field_I4_J, fact_138_linorder__neqE__nat, fact_182_eq__imp__le, fact_97_Graph_Odist_Ocong, fact_163_prod__cases, fact_50_min__distI2, fact_232_le__cases
% 98.50/42.34 % No. of inferences in proof: 721
% 98.50/42.34 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 41941 ms resp. 41024 ms w/o parsing
% 99.43/42.65 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 99.43/42.65 thf(produc1864880952at_nat_type, type, produc1864880952at_nat: $tType).
% 99.43/42.65 thf(produc787001653at_nat_type, type, produc787001653at_nat: $tType).
% 99.43/42.65 thf(produc2082277813at_nat_type, type, produc2082277813at_nat: $tType).
% 99.43/42.65 thf(produc1190591575at_nat_type, type, produc1190591575at_nat: $tType).
% 99.43/42.65 thf(produc1271302400at_nat_type, type, produc1271302400at_nat: $tType).
% 99.43/42.65 thf(produc1695820582at_nat_type, type, produc1695820582at_nat: $tType).
% 99.43/42.65 thf(list_P559422087at_nat_type, type, list_P559422087at_nat: $tType).
% 99.43/42.65 thf(set_Pr1986765409at_nat_type, type, set_Pr1986765409at_nat: $tType).
% 99.43/42.65 thf(product_prod_nat_nat_type, type, product_prod_nat_nat: $tType).
% 99.43/42.65 thf(capacity_type, type, capacity: $tType).
% 99.43/42.65 thf(nat_type, type, nat: $tType).
% 99.43/42.65 thf(connected_capacity_decl, type, connected_capacity: ((product_prod_nat_nat > capacity) > (nat > (nat > $o)))).
% 99.43/42.65 thf(dist_capacity_decl, type, dist_capacity: ((product_prod_nat_nat > capacity) > (nat > (nat > (nat > $o))))).
% 99.43/42.65 thf(isPath_capacity_decl, type, isPath_capacity: ((product_prod_nat_nat > capacity) > (nat > (list_P559422087at_nat > (nat > $o))))).
% 99.43/42.65 thf(isShor1936442771pacity_decl, type, isShor1936442771pacity: ((product_prod_nat_nat > capacity) > (nat > (list_P559422087at_nat > (nat > $o))))).
% 99.43/42.65 thf(isSimp1359852763pacity_decl, type, isSimp1359852763pacity: ((product_prod_nat_nat > capacity) > (nat > (list_P559422087at_nat > (nat > $o))))).
% 99.43/42.65 thf(min_dist_capacity_decl, type, min_dist_capacity: ((product_prod_nat_nat > capacity) > (nat > (nat > nat)))).
% 99.43/42.65 thf(one_one_nat_decl, type, one_one_nat: nat).
% 99.43/42.65 thf(plus_plus_nat_decl, type, plus_plus_nat: (nat > (nat > nat))).
% 99.43/42.65 thf(nil_Pr1308055047at_nat_decl, type, nil_Pr1308055047at_nat: list_P559422087at_nat).
% 99.43/42.65 thf(set_Pr2131844118at_nat_decl, type, set_Pr2131844118at_nat: (list_P559422087at_nat > set_Pr1986765409at_nat)).
% 99.43/42.65 thf(size_s1990949619at_nat_decl, type, size_s1990949619at_nat: (list_P559422087at_nat > nat)).
% 99.43/42.65 thf(ord_less_nat_decl, type, ord_less_nat: (nat > (nat > $o))).
% 99.43/42.65 thf(ord_less_eq_nat_decl, type, ord_less_eq_nat: (nat > (nat > $o))).
% 99.43/42.65 thf(product_Pair_nat_nat_decl, type, product_Pair_nat_nat: (nat > (nat > product_prod_nat_nat))).
% 99.43/42.65 thf(product_swap_nat_nat_decl, type, product_swap_nat_nat: (product_prod_nat_nat > product_prod_nat_nat)).
% 99.43/42.65 thf(collec7649004at_nat_decl, type, collec7649004at_nat: ((product_prod_nat_nat > $o) > set_Pr1986765409at_nat)).
% 99.43/42.65 thf(member701585322at_nat_decl, type, member701585322at_nat: (product_prod_nat_nat > (set_Pr1986765409at_nat > $o))).
% 99.43/42.65 thf(c_decl, type, c: (product_prod_nat_nat > capacity)).
% 99.43/42.65 thf(p_decl, type, p: list_P559422087at_nat).
% 99.43/42.65 thf(p1_decl, type, p1: list_P559422087at_nat).
% 99.43/42.65 thf(p2_decl, type, p2: list_P559422087at_nat).
% 99.43/42.65 thf(p3_decl, type, p3: list_P559422087at_nat).
% 99.43/42.65 thf(s_decl, type, s: nat).
% 99.43/42.65 thf(t_decl, type, t: nat).
% 99.43/42.65 thf(u_decl, type, u: nat).
% 99.43/42.65 thf(v_decl, type, v: nat).
% 99.43/42.65 thf(sk1_decl, type, sk1: ((product_prod_nat_nat > $o) > ((product_prod_nat_nat > $o) > product_prod_nat_nat))).
% 99.43/42.65 thf(sk2_decl, type, sk2: ((nat > (nat > $o)) > nat)).
% 99.43/42.65 thf(sk3_decl, type, sk3: ((nat > (nat > $o)) > nat)).
% 99.43/42.65 thf(sk4_decl, type, sk4: ((nat > (nat > $o)) > nat)).
% 99.43/42.65 thf(sk5_decl, type, sk5: ((nat > (nat > $o)) > nat)).
% 99.43/42.65 thf(sk6_decl, type, sk6: ((nat > (nat > $o)) > nat)).
% 99.43/42.65 thf(sk7_decl, type, sk7: (nat > ((nat > $o) > nat))).
% 99.43/42.65 thf(sk8_decl, type, sk8: ((nat > $o) > nat)).
% 99.43/42.65 thf(sk9_decl, type, sk9: (nat > (product_prod_nat_nat > nat))).
% 99.43/42.65 thf(sk26_decl, type, sk26: (product_prod_nat_nat > nat)).
% 99.43/42.65 thf(sk27_decl, type, sk27: (product_prod_nat_nat > nat)).
% 99.43/42.65 thf(sk30_decl, type, sk30: (product_prod_nat_nat > nat)).
% 99.43/42.65 thf(sk31_decl, type, sk31: (product_prod_nat_nat > nat)).
% 99.43/42.65 thf(sk66_decl, type, sk66: product_prod_nat_nat).
% 99.43/42.65 thf(sk67_decl, type, sk67: product_prod_nat_nat).
% 99.43/42.65 thf(sk68_decl, type, sk68: product_prod_nat_nat).
% 99.43/42.65 thf(sk69_decl, type, sk69: product_prod_nat_nat).
% 99.43/42.65 thf(sk1_def, definition, sk1 = (^ [A:(product_prod_nat_nat > $o),B:(product_prod_nat_nat > $o)]: (@+ [C:product_prod_nat_nat]: ~ ((B @ C) = (A @ C)))) ).
% 99.43/42.65 thf(sk2_def, definition, sk2 = (^ [A:(nat > (nat > $o))]: (@+ [B:nat]: ~ (! [C:nat]: ((ord_less_nat @ B @ C) => (A @ B @ C))))) ).
% 99.43/42.65 thf(sk3_def, definition, sk3 = (^ [A:(nat > (nat > $o))]: (@+ [B:nat]: ~ ((ord_less_nat @ (sk2 @ A) @ B) => (A @ (sk2 @ A) @ B)))) ).
% 99.43/42.65 thf(sk4_def, definition, sk4 = (^ [A:(nat > (nat > $o))]: (@+ [B:nat]: ~ (A @ B @ B))) ).
% 99.43/42.65 thf(sk5_def, definition, sk5 = (^ [A:(nat > (nat > $o))]: (@+ [B:nat]: ~ (! [C:nat]: ((A @ C @ B) => (A @ B @ C))))) ).
% 99.43/42.65 thf(sk6_def, definition, sk6 = (^ [A:(nat > (nat > $o))]: (@+ [B:nat]: ~ ((A @ B @ (sk5 @ A)) => (A @ (sk5 @ A) @ B)))) ).
% 99.43/42.65 thf(sk7_def, definition, sk7 = (^ [A:nat,B:(nat > $o)]: (@+ [C:nat]: ~ ((B @ C) => (ord_less_eq_nat @ C @ A)))) ).
% 99.43/42.65 thf(sk8_def, definition, sk8 = (^ [A:(nat > $o)]: (@+ [B:nat]: ((A @ B) & ! [C:nat]: ((A @ C) => (ord_less_eq_nat @ C @ B))))) ).
% 99.43/42.65 thf(sk9_def, definition, sk9 = (@+ [A:(nat > (product_prod_nat_nat > nat))]: ! [B:nat,C:nat]: ((A @ C @ (product_Pair_nat_nat @ B @ C)) = B)) ).
% 99.43/42.65 thf(sk26_def, definition, sk26 = (^ [A:product_prod_nat_nat]: (@+ [B:nat]: ? [C:nat]: (A = (product_Pair_nat_nat @ B @ C)))) ).
% 99.43/42.65 thf(sk27_def, definition, sk27 = (^ [A:product_prod_nat_nat]: (@+ [B:nat]: (A = (product_Pair_nat_nat @ (sk26 @ A) @ B)))) ).
% 99.43/42.65 thf(sk30_def, definition, sk30 = (^ [A:product_prod_nat_nat]: (@+ [B:nat]: ? [C:nat]: (A = (product_Pair_nat_nat @ B @ C)))) ).
% 99.43/42.65 thf(sk31_def, definition, sk31 = (^ [A:product_prod_nat_nat]: (@+ [B:nat]: (A = (product_Pair_nat_nat @ (sk30 @ A) @ B)))) ).
% 99.43/42.65 thf(33,axiom,((isShor1936442771pacity = isShor1936442771pacity)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_Graph_OisShortestPath_Ocong)).
% 99.43/42.65 thf(365,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 99.43/42.65 thf(147,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) => (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_add__less__imp__less__right)).
% 99.43/42.65 thf(760,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) => (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 99.43/42.65 thf(67,axiom,((! [A:product_prod_nat_nat]: ? [B:nat,C:nat]: (A = (product_Pair_nat_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_surj__pair)).
% 99.43/42.65 thf(477,plain,((! [A:product_prod_nat_nat]: ? [B:nat,C:nat]: (A = (product_Pair_nat_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 99.43/42.65 thf(478,plain,(! [A:product_prod_nat_nat] : ((A = (product_Pair_nat_nat @ (sk30 @ A) @ (sk31 @ A))))),inference(cnf,[status(esa)],[477])).
% 99.43/42.65 thf(479,plain,(! [A:product_prod_nat_nat] : (((product_Pair_nat_nat @ (sk30 @ A) @ (sk31 @ A)) = A))),inference(lifteq,[status(thm)],[478])).
% 99.43/42.65 thf(28,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_less__not__refl2)).
% 99.43/42.65 thf(347,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 99.43/42.65 thf(187,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((min_dist_capacity @ A @ B @ D) = (plus_plus_nat @ (plus_plus_nat @ (min_dist_capacity @ A @ B @ E) @ one_one_nat) @ (min_dist_capacity @ A @ F @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_Graph_OisShortestPath__level__edge_I6_J)).
% 99.43/42.65 thf(893,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((min_dist_capacity @ (A) @ B @ D) = (plus_plus_nat @ (plus_plus_nat @ (min_dist_capacity @ (A) @ B @ E) @ one_one_nat) @ (min_dist_capacity @ (A) @ F @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 99.43/42.65 thf(81,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_less__imp__not__eq2)).
% 99.43/42.65 thf(518,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 99.43/42.65 thf(153,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_nat__add__left__cancel__less)).
% 99.43/42.65 thf(777,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 99.43/42.65 thf(68,axiom,((connected_capacity = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:nat]: (dist_capacity @ A @ B @ D @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_Graph_Oconnected__by__dist)).
% 99.43/42.65 thf(480,plain,(((connected_capacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:nat]: (dist_capacity @ A @ B @ D @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 99.43/42.65 thf(481,plain,(((connected_capacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:nat]: (dist_capacity @ A @ B @ D @ C)))),inference(lifteq,[status(thm)],[480])).
% 99.43/42.65 thf(192,axiom,((! [A:nat,B:nat]: ((connected_capacity @ c @ A @ B) => (~ (! [C:list_P559422087at_nat]: ~ (isShor1936442771pacity @ c @ A @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_obtain__shortest__path)).
% 99.43/42.65 thf(909,plain,((! [A:nat,B:nat]: ((connected_capacity @ (c) @ A @ B) => (~ (! [C:list_P559422087at_nat]: ~ (isShor1936442771pacity @ (c) @ A @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 99.43/42.65 thf(104,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ? [C:nat]: (B = (plus_plus_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_nat__le__iff__add)).
% 99.43/42.65 thf(628,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ? [C:nat]: (B = (plus_plus_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 99.43/42.65 thf(25,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_dual__order_Oeq__iff)).
% 99.43/42.65 thf(341,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 99.43/42.65 thf(342,plain,(((^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))) = ((=) @ nat))),inference(lifteq,[status(thm)],[341])).
% 99.43/42.65 thf(1031,plain,(! [A:nat] : (((^ [B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))) = ((=) @ nat @ A)))),inference(func_ext,[status(esa)],[342])).
% 99.43/42.65 thf(148,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => (connected_capacity @ c @ E @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_isShortestPath__level__edge_I3_J)).
% 99.43/42.65 thf(762,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => (connected_capacity @ (c) @ E @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 99.43/42.65 thf(123,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => (((plus_plus_nat @ C @ B) = (plus_plus_nat @ A @ D)) => (ord_less_nat @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_less__add__eq__less)).
% 99.43/42.65 thf(683,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => (((plus_plus_nat @ C @ B) = (plus_plus_nat @ A @ D)) => (ord_less_nat @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 99.43/42.65 thf(62,axiom,((! [A:product_prod_nat_nat]: ~ (! [B:nat,C:nat]: (A != (product_Pair_nat_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_old_Oprod_Oexhaust)).
% 99.43/42.65 thf(459,plain,((! [A:product_prod_nat_nat]: ~ (! [B:nat,C:nat]: ~ (A = (product_Pair_nat_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 99.43/42.65 thf(460,plain,((~ (~ (! [A:product_prod_nat_nat]: ? [B:nat,C:nat]: (A = (product_Pair_nat_nat @ B @ C)))))),inference(miniscope,[status(thm)],[459])).
% 99.43/42.65 thf(461,plain,(! [A:product_prod_nat_nat] : ((A = (product_Pair_nat_nat @ (sk26 @ A) @ (sk27 @ A))))),inference(cnf,[status(esa)],[460])).
% 99.43/42.65 thf(462,plain,(! [A:product_prod_nat_nat] : (((product_Pair_nat_nat @ (sk26 @ A) @ (sk27 @ A)) = A))),inference(lifteq,[status(thm)],[461])).
% 99.43/42.65 thf(8,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) => (~ ((A = C) => (B != D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_Pair__inject)).
% 99.43/42.65 thf(276,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) => (~ ((A = C) => (~ (B = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 99.43/42.65 thf(277,plain,(! [D:nat,C:nat,B:nat,A:nat] : (((~ ((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) | (A = C)) & (~ ((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) | (B = D))))),inference(cnf,[status(esa)],[276])).
% 99.43/42.65 thf(278,plain,(! [D:nat,C:nat,B:nat,A:nat] : ((~ ((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D))) | (A = C))),inference(cnfConj,[status(thm)],[277])).
% 99.43/42.65 thf(280,plain,(! [D:nat,C:nat,B:nat,A:nat] : (((product_Pair_nat_nat @ A @ B) != (product_Pair_nat_nat @ C @ D)) | (A = C))),inference(lifteq,[status(thm)],[278])).
% 99.43/42.65 thf(160,axiom,((u != v)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5__092_060open_062u_A_092_060noteq_062_Av_092_060close_062)).
% 99.43/42.65 thf(797,plain,((~ (u = v))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 99.43/42.65 thf(798,plain,((~ (u = v))),inference(polarity_switch,[status(thm)],[797])).
% 99.43/42.65 thf(799,plain,((v != u)),inference(lifteq,[status(thm)],[798])).
% 99.43/42.65 thf(11383,plain,(! [D:nat,C:nat,B:nat,A:nat] : (((product_Pair_nat_nat @ A @ B) != (product_Pair_nat_nat @ C @ D)) | (C != u) | (A != v))),inference(paramod_ordered,[status(thm)],[280,799])).
% 99.43/42.65 thf(11384,plain,(! [C:nat,B:nat,A:nat] : (((product_Pair_nat_nat @ v @ A) != (product_Pair_nat_nat @ B @ C)) | (B != u))),inference(pattern_uni,[status(thm)],[11383:[bind(A, $thf(v))]])).
% 99.43/42.65 thf(11785,plain,(! [B:nat,A:nat] : (((product_Pair_nat_nat @ v @ A) != (product_Pair_nat_nat @ u @ B)))),inference(simp,[status(thm)],[11384])).
% 99.43/42.65 thf(12284,plain,(! [C:nat,B:nat,A:product_prod_nat_nat] : ((A != (product_Pair_nat_nat @ u @ C)) | ((product_Pair_nat_nat @ (sk26 @ A) @ (sk27 @ A)) != (product_Pair_nat_nat @ v @ B)))),inference(paramod_ordered,[status(thm)],[462,11785])).
% 99.43/42.65 thf(12291,plain,(! [B:nat,A:nat] : (((sk26 @ (product_Pair_nat_nat @ u @ B)) != v) | ((sk27 @ (product_Pair_nat_nat @ u @ B)) != A))),inference(simp,[status(thm)],[12284])).
% 99.43/42.65 thf(12299,plain,(! [A:nat] : (((sk26 @ (product_Pair_nat_nat @ u @ A)) != v))),inference(simp,[status(thm)],[12291])).
% 99.43/42.65 thf(222,axiom,(((min_dist_capacity @ c @ s @ v) = (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_MDSV)).
% 99.43/42.65 thf(993,plain,(((min_dist_capacity @ (c) @ s @ v) = (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 99.43/42.65 thf(994,plain,(((min_dist_capacity @ (c) @ s @ v) = (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat))),inference(lifteq,[status(thm)],[993])).
% 99.43/42.65 thf(142,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (ord_less_nat @ (A @ D) @ (A @ E)))) => (ord_less_eq_nat @ (plus_plus_nat @ (A @ B) @ C) @ (A @ (plus_plus_nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_mono__nat__linear__lb)).
% 99.43/42.65 thf(741,plain,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (ord_less_nat @ (A @ D) @ (A @ E)))) => (ord_less_eq_nat @ (plus_plus_nat @ (A @ B) @ C) @ (A @ (plus_plus_nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 99.43/42.65 thf(72,axiom,((! [A:product_prod_nat_nat,B:(product_prod_nat_nat > $o)]: ((member701585322at_nat @ A @ (collec7649004at_nat @ B)) = (B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_mem__Collect__eq)).
% 99.43/42.65 thf(489,plain,((! [A:product_prod_nat_nat,B:(product_prod_nat_nat > $o)]: ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 99.43/42.65 thf(490,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : (((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) = (B @ A)))),inference(cnf,[status(esa)],[489])).
% 99.43/42.65 thf(491,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : (((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) = (B @ A)))),inference(lifteq,[status(thm)],[490])).
% 99.43/42.65 thf(69,axiom,((! [A:set_Pr1986765409at_nat]: ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_Collect__mem__eq)).
% 99.43/42.65 thf(482,plain,((! [A:set_Pr1986765409at_nat]: ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 99.43/42.65 thf(483,plain,(! [A:set_Pr1986765409at_nat] : (((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) = A))),inference(cnf,[status(esa)],[482])).
% 99.43/42.65 thf(484,plain,(! [A:set_Pr1986765409at_nat] : (((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) = A))),inference(lifteq,[status(thm)],[483])).
% 99.43/42.65 thf(157,axiom,((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (set_Pr2131844118at_nat @ p))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_assms_I2_J)).
% 99.43/42.65 thf(788,plain,((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (set_Pr2131844118at_nat @ p))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 99.43/42.65 thf(121,axiom,(((min_dist_capacity @ c @ s @ t) = (plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_MIN_H)).
% 99.43/42.65 thf(679,plain,(((min_dist_capacity @ (c) @ s @ t) = (plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 99.43/42.65 thf(680,plain,(((min_dist_capacity @ (c) @ s @ t) = (plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)))),inference(lifteq,[status(thm)],[679])).
% 99.43/42.65 thf(156,axiom,(((min_dist_capacity @ c @ s @ t) = (size_s1990949619at_nat @ p))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_MIN)).
% 99.43/42.65 thf(786,plain,(((min_dist_capacity @ (c) @ s @ t) = (size_s1990949619at_nat @ p))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 99.43/42.65 thf(787,plain,(((min_dist_capacity @ (c) @ s @ t) = (size_s1990949619at_nat @ p))),inference(lifteq,[status(thm)],[786])).
% 99.43/42.65 thf(3324,plain,(((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) = (size_s1990949619at_nat @ p))),inference(rewrite,[status(thm)],[680,787])).
% 99.43/42.65 thf(162,axiom,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_not__add__less2)).
% 99.43/42.65 thf(803,plain,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 99.43/42.65 thf(804,plain,((~ (? [A:nat,B:nat]: (ord_less_nat @ (plus_plus_nat @ A @ B) @ B)))),inference(miniscope,[status(thm)],[803])).
% 99.43/42.65 thf(805,plain,(! [B:nat,A:nat] : ((~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ B)))),inference(cnf,[status(esa)],[804])).
% 99.43/42.65 thf(3331,plain,(! [B:nat,A:nat] : ((~ (ord_less_nat @ (size_s1990949619at_nat @ p) @ B)) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ A @ B)))),inference(paramod_ordered,[status(thm)],[3324,805])).
% 99.43/42.65 thf(3332,plain,((~ (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2)))),inference(pattern_uni,[status(thm)],[3331:[bind(A, $thf(plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat)),bind(B, $thf(size_s1990949619at_nat @ p2))]])).
% 99.43/42.65 thf(6226,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((~ (member701585322at_nat @ A @ (collec7649004at_nat @ (B)))) | ((B @ A) != (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2))))),inference(paramod_ordered,[status(thm)],[491,3332])).
% 99.43/42.65 thf(6570,plain,(! [A:product_prod_nat_nat] : ((~ (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2)))))))),inference(pre_uni,[status(thm)],[6226:[bind(A, $thf(A)),bind(B, $thf(^ [C:product_prod_nat_nat]: (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2))))]])).
% 99.43/42.65 thf(6757,plain,(! [A:product_prod_nat_nat] : ((~ (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(rewrite,[status(thm)],[6570,3332])).
% 99.43/42.65 thf(6763,plain,(! [A:product_prod_nat_nat] : (~ (($true)) | ((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (set_Pr2131844118at_nat @ p)) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(paramod_ordered,[status(thm)],[788,6757])).
% 99.43/42.65 thf(6764,plain,(! [A:product_prod_nat_nat] : (((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (set_Pr2131844118at_nat @ p)) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(simp,[status(thm)],[6763])).
% 99.43/42.65 thf(6838,plain,(! [A:product_prod_nat_nat] : (((product_Pair_nat_nat @ u @ v) != A) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))) != (set_Pr2131844118at_nat @ p)))),inference(simp,[status(thm)],[6764])).
% 99.43/42.65 thf(6881,plain,(((collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (($false)))) != (set_Pr2131844118at_nat @ p))),inference(simp,[status(thm)],[6838])).
% 99.43/42.65 thf(7674,plain,(! [A:set_Pr1986765409at_nat] : ((A != (set_Pr2131844118at_nat @ p)) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) != (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false))))))),inference(paramod_ordered,[status(thm)],[484,6881])).
% 99.43/42.65 thf(7709,plain,(((^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p))) != (^ [A:product_prod_nat_nat]: (($false))))),inference(simp,[status(thm)],[7674])).
% 99.43/42.65 thf(7739,plain,((member701585322at_nat @ sk67 @ (set_Pr2131844118at_nat @ p))),inference(func_ext,[status(esa)],[7709])).
% 99.43/42.65 thf(7872,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((B @ A) != (member701585322at_nat @ sk67 @ (set_Pr2131844118at_nat @ p))))),inference(paramod_ordered,[status(thm)],[491,7739])).
% 99.43/42.65 thf(7896,plain,((member701585322at_nat @ sk67 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p)))))),inference(pre_uni,[status(thm)],[7872:[bind(A, $thf(sk67)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p))))]])).
% 99.43/42.65 thf(8965,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((B @ A) != (member701585322at_nat @ sk67 @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p)))))))),inference(paramod_ordered,[status(thm)],[491,7896])).
% 99.43/42.65 thf(8991,plain,((member701585322at_nat @ sk67 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p))))))))),inference(pre_uni,[status(thm)],[8965:[bind(A, $thf(sk67)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (collec7649004at_nat @ (^ [D:product_prod_nat_nat]: (member701585322at_nat @ D @ (set_Pr2131844118at_nat @ p)))))))]])).
% 99.43/42.65 thf(10175,plain,(! [A:product_prod_nat_nat] : (~ (($true)) | ((member701585322at_nat @ sk67 @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p)))))))) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(paramod_ordered,[status(thm)],[8991,6757])).
% 99.43/42.65 thf(10176,plain,(! [A:product_prod_nat_nat] : (((member701585322at_nat @ sk67 @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p)))))))) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(simp,[status(thm)],[10175])).
% 99.43/42.65 thf(10213,plain,(! [A:product_prod_nat_nat] : ((sk67 != A) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p))))))) != (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false))))))),inference(simp,[status(thm)],[10176])).
% 99.43/42.65 thf(10219,plain,(((collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p))))))) != (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (($false)))))),inference(simp,[status(thm)],[10213])).
% 99.43/42.65 thf(10819,plain,(((^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p)))))) != (^ [A:product_prod_nat_nat]: (($false))))),inference(simp,[status(thm)],[10219])).
% 99.43/42.65 thf(10837,plain,((member701585322at_nat @ sk69 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p)))))),inference(func_ext,[status(esa)],[10819])).
% 99.43/42.65 thf(181,axiom,((! [A:nat,B:nat]: ((connected_capacity @ c @ A @ B) = (? [C:list_P559422087at_nat]: (isPath_capacity @ c @ A @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_connected__def)).
% 99.43/42.65 thf(873,plain,((! [A:nat,B:nat]: ((connected_capacity @ (c) @ A @ B) = (? [C:list_P559422087at_nat]: (isPath_capacity @ (c) @ A @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 99.43/42.65 thf(6,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_linorder__less__wlog)).
% 99.43/42.65 thf(241,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 99.43/42.65 thf(242,plain,((! [A:(nat > (nat > $o))]: ((! [B:nat,C:nat]: ((ord_less_nat @ B @ C) => (A @ B @ C))) => ((! [B:nat]: (A @ B @ B)) => ((! [B:nat,C:nat]: ((A @ C @ B) => (A @ B @ C))) => (! [B:nat,C:nat]: (A @ B @ C))))))),inference(miniscope,[status(thm)],[241])).
% 99.43/42.65 thf(243,plain,(! [C:nat,B:nat,A:(nat > (nat > $o))] : ((((ord_less_nat @ (sk2 @ (A)) @ (sk3 @ (A))) | ~ (A @ (sk4 @ (A)) @ (sk4 @ (A))) | (A @ (sk6 @ (A)) @ (sk5 @ (A))) | (A @ B @ C)) & ((ord_less_nat @ (sk2 @ (A)) @ (sk3 @ (A))) | ~ (A @ (sk4 @ (A)) @ (sk4 @ (A))) | ~ (A @ (sk5 @ (A)) @ (sk6 @ (A))) | (A @ B @ C)) & (~ (A @ (sk2 @ (A)) @ (sk3 @ (A))) | ~ (A @ (sk4 @ (A)) @ (sk4 @ (A))) | (A @ (sk6 @ (A)) @ (sk5 @ (A))) | (A @ B @ C)) & (~ (A @ (sk2 @ (A)) @ (sk3 @ (A))) | ~ (A @ (sk4 @ (A)) @ (sk4 @ (A))) | ~ (A @ (sk5 @ (A)) @ (sk6 @ (A))) | (A @ B @ C))))),inference(cnf,[status(esa)],[242])).
% 99.43/42.65 thf(247,plain,(! [C:nat,B:nat,A:(nat > (nat > $o))] : ((~ (A @ (sk2 @ (A)) @ (sk3 @ (A)))) | (~ (A @ (sk4 @ (A)) @ (sk4 @ (A)))) | (~ (A @ (sk5 @ (A)) @ (sk6 @ (A)))) | (A @ B @ C))),inference(cnfConj,[status(thm)],[243])).
% 99.43/42.65 thf(38,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat]: (connected_capacity @ A @ B @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_Graph_Oconnected__refl)).
% 99.43/42.65 thf(378,plain,((! [A:(product_prod_nat_nat > capacity),B:nat]: (connected_capacity @ (A) @ B @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 99.43/42.65 thf(379,plain,(! [B:nat,A:(product_prod_nat_nat > capacity)] : ((connected_capacity @ (A) @ B @ B))),inference(cnf,[status(esa)],[378])).
% 99.43/42.65 thf(120,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (ord_less_eq_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_add__mono__thms__linordered__field_I3_J)).
% 99.43/42.65 thf(677,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (ord_less_eq_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 99.43/42.65 thf(138,axiom,((dist_capacity = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ? [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) & ((size_s1990949619at_nat @ E) = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_Graph_Odist__def)).
% 99.43/42.65 thf(730,plain,(((dist_capacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ? [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) & ((size_s1990949619at_nat @ E) = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 99.43/42.65 thf(221,axiom,((isShor1936442771pacity = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_Graph_OisShortestPath__alt)).
% 99.43/42.65 thf(991,plain,(((isShor1936442771pacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 99.43/42.65 thf(992,plain,(((isShor1936442771pacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))))),inference(lifteq,[status(thm)],[991])).
% 99.43/42.65 thf(105,axiom,((isShor1936442771pacity = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_Graph_OisShortestPath__min__dist__def)).
% 99.43/42.65 thf(630,plain,(((isShor1936442771pacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 99.43/42.65 thf(631,plain,(((isShor1936442771pacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))))),inference(lifteq,[status(thm)],[630])).
% 99.43/42.65 thf(1305,plain,(((^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))))),inference(rewrite,[status(thm)],[992,631])).
% 99.43/42.65 thf(96,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((connected_capacity @ A @ B @ C) => (~ (! [D:list_P559422087at_nat]: ~ (isShor1936442771pacity @ A @ B @ D @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_Graph_Oobtain__shortest__path)).
% 99.43/42.65 thf(597,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((connected_capacity @ (A) @ B @ C) => (~ (! [D:list_P559422087at_nat]: ~ (isShor1936442771pacity @ (A) @ B @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 99.43/42.65 thf(132,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_add__less__le__mono)).
% 99.43/42.65 thf(715,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 99.43/42.65 thf(200,axiom,((member701585322at_nat @ (product_Pair_nat_nat @ v @ u) @ (set_Pr2131844118at_nat @ p3))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_assms_I4_J)).
% 99.43/42.65 thf(934,plain,((member701585322at_nat @ (product_Pair_nat_nat @ v @ u) @ (set_Pr2131844118at_nat @ p3))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 99.43/42.65 thf(6761,plain,(! [A:product_prod_nat_nat] : (~ (($true)) | ((member701585322at_nat @ (product_Pair_nat_nat @ v @ u) @ (set_Pr2131844118at_nat @ p3)) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(paramod_ordered,[status(thm)],[934,6757])).
% 99.43/42.65 thf(6762,plain,(! [A:product_prod_nat_nat] : (((member701585322at_nat @ (product_Pair_nat_nat @ v @ u) @ (set_Pr2131844118at_nat @ p3)) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(simp,[status(thm)],[6761])).
% 99.43/42.65 thf(6834,plain,(! [A:product_prod_nat_nat] : (((product_Pair_nat_nat @ v @ u) != A) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))) != (set_Pr2131844118at_nat @ p3)))),inference(simp,[status(thm)],[6762])).
% 99.43/42.65 thf(6878,plain,(((collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (($false)))) != (set_Pr2131844118at_nat @ p3))),inference(simp,[status(thm)],[6834])).
% 99.43/42.65 thf(6893,plain,(! [A:set_Pr1986765409at_nat] : ((A != (set_Pr2131844118at_nat @ p3)) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) != (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false))))))),inference(paramod_ordered,[status(thm)],[484,6878])).
% 99.43/42.65 thf(6933,plain,(((^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p3))) != (^ [A:product_prod_nat_nat]: (($false))))),inference(simp,[status(thm)],[6893])).
% 99.43/42.65 thf(7737,plain,((member701585322at_nat @ sk66 @ (set_Pr2131844118at_nat @ p3))),inference(func_ext,[status(esa)],[6933])).
% 99.43/42.65 thf(7771,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((B @ A) != (member701585322at_nat @ sk66 @ (set_Pr2131844118at_nat @ p3))))),inference(paramod_ordered,[status(thm)],[491,7737])).
% 99.43/42.65 thf(7786,plain,(! [A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ sk66 @ (set_Pr2131844118at_nat @ p3))))))),inference(pre_uni,[status(thm)],[7771:[bind(A, $thf(A)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ sk66 @ (set_Pr2131844118at_nat @ p3))))]])).
% 99.43/42.65 thf(12522,plain,(! [A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($true))))))),inference(rewrite,[status(thm)],[7786,7737])).
% 99.43/42.65 thf(85,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_antisym__conv3)).
% 99.43/42.65 thf(538,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 99.43/42.65 thf(199,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (ord_less_eq_nat @ C @ D)) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_add__mono__thms__linordered__semiring_I2_J)).
% 99.43/42.65 thf(930,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (ord_less_eq_nat @ C @ D)) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 99.43/42.65 thf(165,axiom,((plus_plus_nat = (^ [A:nat,B:nat]: (plus_plus_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_add_Ocommute)).
% 99.43/42.65 thf(813,plain,(((plus_plus_nat) = (^ [A:nat,B:nat]: (plus_plus_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 99.43/42.65 thf(814,plain,(((plus_plus_nat) = (^ [A:nat,B:nat]: (plus_plus_nat @ B @ A)))),inference(lifteq,[status(thm)],[813])).
% 99.43/42.65 thf(1,conjecture,(((min_dist_capacity @ c @ u @ t) = (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 99.43/42.65 thf(2,negated_conjecture,((~ ((min_dist_capacity @ c @ u @ t) = (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))))),inference(neg_conjecture,[status(cth)],[1])).
% 99.43/42.65 thf(231,plain,((~ ((min_dist_capacity @ (c) @ u @ t) = (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 99.43/42.65 thf(232,plain,(((min_dist_capacity @ (c) @ u @ t) != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))),inference(lifteq,[status(thm)],[231])).
% 99.43/42.65 thf(1318,plain,(((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))) | ((min_dist_capacity @ (c) @ u @ t) != (min_dist_capacity @ (c) @ s @ v))),inference(paramod_ordered,[status(thm)],[994,232])).
% 99.43/42.65 thf(1321,plain,(((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))) | ((c) != (c)) | (u != s) | (v != t)),inference(simp,[status(thm)],[1318])).
% 99.43/42.65 thf(1327,plain,(((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))) | (u != s) | (v != t)),inference(simp,[status(thm)],[1321])).
% 99.43/42.65 thf(226,axiom,((dist_capacity @ c @ v @ (size_s1990949619at_nat @ p2) @ t)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_DISTS_I3_J)).
% 99.43/42.65 thf(1001,plain,((dist_capacity @ (c) @ v @ (size_s1990949619at_nat @ p2) @ t)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 99.43/42.65 thf(48,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isPath_capacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((E != B) => (? [G:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ G @ E) @ (set_Pr2131844118at_nat @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_Graph_OisPath__ex__edge1)).
% 99.43/42.65 thf(417,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isPath_capacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((~ (E = B)) => (? [G:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ G @ E) @ (set_Pr2131844118at_nat @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 99.43/42.65 thf(12,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_nat__le__linear)).
% 99.43/42.65 thf(301,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 99.43/42.65 thf(244,plain,(! [C:nat,B:nat,A:(nat > (nat > $o))] : ((ord_less_nat @ (sk2 @ (A)) @ (sk3 @ (A))) | (~ (A @ (sk4 @ (A)) @ (sk4 @ (A)))) | (A @ (sk6 @ (A)) @ (sk5 @ (A))) | (A @ B @ C))),inference(cnfConj,[status(thm)],[243])).
% 99.43/42.65 thf(1159,plain,(! [C:nat,B:nat,A:(nat > (nat > $o))] : ((ord_less_nat @ (sk2 @ (A)) @ (sk3 @ (A))) | (~ (A @ (sk4 @ (A)) @ (sk4 @ (A)))) | (A @ (sk6 @ (A)) @ (sk5 @ (A))) | ((A @ B @ C) != (A @ (sk6 @ (A)) @ (sk5 @ (A)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[244])).
% 99.43/42.65 thf(1188,plain,(! [B:nat,A:nat] : ((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | (~ ((sk4 @ ((=) @ nat)) = (sk4 @ ((=) @ nat)))) | ((sk6 @ ((=) @ nat)) = (sk5 @ ((=) @ nat))) | ((A = B) != ((sk6 @ ((=) @ nat)) = (sk5 @ ((=) @ nat)))) | ~ (($true)))),inference(replace_andrewseq,[status(thm)],[1159:[bind(A, $thf((=) @ nat))]])).
% 99.43/42.65 thf(1207,plain,(! [B:nat,A:nat] : (((sk4 @ ((=) @ nat)) != (sk4 @ ((=) @ nat))) | ((sk6 @ ((=) @ nat)) = (sk5 @ ((=) @ nat))) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | ((A = B) != ((sk6 @ ((=) @ nat)) = (sk5 @ ((=) @ nat)))) | ~ (($true)))),inference(lifteq,[status(thm)],[1188])).
% 99.43/42.65 thf(1232,plain,(~ (($true)) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | ((sk6 @ ((=) @ nat)) = (sk5 @ ((=) @ nat)))),inference(pattern_uni,[status(thm)],[1207:[bind(A, $thf(sk6 @ ((=) @ nat))),bind(B, $thf(sk5 @ ((=) @ nat)))]])).
% 99.43/42.65 thf(1290,plain,((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | ((sk6 @ ((=) @ nat)) = (sk5 @ ((=) @ nat)))),inference(simp,[status(thm)],[1232])).
% 99.43/42.65 thf(245,plain,(! [C:nat,B:nat,A:(nat > (nat > $o))] : ((ord_less_nat @ (sk2 @ (A)) @ (sk3 @ (A))) | (~ (A @ (sk4 @ (A)) @ (sk4 @ (A)))) | (~ (A @ (sk5 @ (A)) @ (sk6 @ (A)))) | (A @ B @ C))),inference(cnfConj,[status(thm)],[243])).
% 99.43/42.65 thf(249,plain,(! [B:nat,A:nat] : ((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | (~ ((sk4 @ ((=) @ nat)) = (sk4 @ ((=) @ nat)))) | (~ ((sk5 @ ((=) @ nat)) = (sk6 @ ((=) @ nat)))) | (A = B))),inference(replace_andrewseq,[status(thm)],[245:[bind(A, $thf((=) @ nat))]])).
% 99.43/42.65 thf(252,plain,(! [B:nat,A:nat] : (((sk4 @ ((=) @ nat)) != (sk4 @ ((=) @ nat))) | ((sk6 @ ((=) @ nat)) != (sk5 @ ((=) @ nat))) | (A = B) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))))),inference(lifteq,[status(thm)],[249])).
% 99.43/42.65 thf(253,plain,(! [B:nat,A:nat] : (((sk6 @ ((=) @ nat)) != (sk5 @ ((=) @ nat))) | (A = B) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))))),inference(simp,[status(thm)],[252])).
% 99.43/42.65 thf(3840,plain,(! [B:nat,A:nat] : (((sk6 @ ((=) @ nat)) != (sk5 @ ((=) @ nat))) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | (B != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))) | (A != (min_dist_capacity @ (c) @ u @ t)))),inference(paramod_ordered,[status(thm)],[253,232])).
% 99.43/42.65 thf(3841,plain,(! [A:nat] : (((sk6 @ ((=) @ nat)) != (sk5 @ ((=) @ nat))) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | (A != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))))),inference(pattern_uni,[status(thm)],[3840:[bind(A, $thf(min_dist_capacity @ (c) @ u @ t)),bind(B, $thf(B))]])).
% 99.43/42.65 thf(4026,plain,(((sk6 @ ((=) @ nat)) != (sk5 @ ((=) @ nat))) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat)))),inference(simp,[status(thm)],[3841])).
% 99.43/42.65 thf(4378,plain,((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | ((sk5 @ ((=) @ nat)) != (sk5 @ ((=) @ nat))) | (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | ((sk6 @ ((=) @ nat)) != (sk6 @ ((=) @ nat)))),inference(paramod_ordered,[status(thm)],[1290,4026])).
% 99.43/42.65 thf(4379,plain,((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) | ((sk6 @ ((=) @ nat)) != (sk6 @ ((=) @ nat)))),inference(simp,[status(thm)],[4378])).
% 99.43/42.65 thf(4380,plain,((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat)))),inference(pattern_uni,[status(thm)],[4379:[]])).
% 99.43/42.65 thf(9,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_less__not__refl3)).
% 99.43/42.65 thf(286,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 99.43/42.65 thf(287,plain,(! [B:nat,A:nat] : ((~ (ord_less_nat @ A @ B)) | (~ (A = B)))),inference(cnf,[status(esa)],[286])).
% 99.43/42.65 thf(288,plain,(! [B:nat,A:nat] : ((A != B) | (~ (ord_less_nat @ A @ B)))),inference(lifteq,[status(thm)],[287])).
% 99.43/42.65 thf(289,plain,(! [A:nat] : ((~ (ord_less_nat @ A @ A)))),inference(simp,[status(thm)],[288])).
% 99.43/42.65 thf(4434,plain,(! [A:nat] : (~ (($true)) | ((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) != (ord_less_nat @ A @ A)))),inference(paramod_ordered,[status(thm)],[4380,289])).
% 99.43/42.65 thf(4435,plain,(! [A:nat] : (((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) != (ord_less_nat @ A @ A)))),inference(simp,[status(thm)],[4434])).
% 99.43/42.65 thf(4458,plain,(! [A:nat] : (((sk2 @ ((=) @ nat)) != A) | ((sk3 @ ((=) @ nat)) != A))),inference(simp,[status(thm)],[4435])).
% 99.43/42.65 thf(4467,plain,(((sk3 @ ((=) @ nat)) != (sk2 @ ((=) @ nat)))),inference(simp,[status(thm)],[4458])).
% 99.43/42.65 thf(186,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((connected_capacity @ c @ A @ B) => ((! [D:nat]: ((dist_capacity @ c @ A @ D @ B) => ((! [E:nat]: ((dist_capacity @ c @ A @ E @ B) => (ord_less_eq_nat @ D @ E))) => (C @ D)))) => (C @ (min_dist_capacity @ c @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_min__distI2)).
% 99.43/42.65 thf(885,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((connected_capacity @ (c) @ A @ B) => ((! [D:nat]: ((dist_capacity @ (c) @ A @ D @ B) => ((! [E:nat]: ((dist_capacity @ (c) @ A @ E @ B) => (ord_less_eq_nat @ D @ E))) => (C @ D)))) => (C @ (min_dist_capacity @ (c) @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 99.43/42.65 thf(12285,plain,(! [C:nat,B:nat,A:product_prod_nat_nat] : ((A != (product_Pair_nat_nat @ v @ B)) | ((product_Pair_nat_nat @ (sk26 @ A) @ (sk27 @ A)) != (product_Pair_nat_nat @ u @ C)))),inference(paramod_ordered,[status(thm)],[462,11785])).
% 99.43/42.65 thf(12295,plain,(! [B:nat,A:nat] : (((sk26 @ (product_Pair_nat_nat @ v @ A)) != u) | ((sk27 @ (product_Pair_nat_nat @ v @ A)) != B))),inference(simp,[status(thm)],[12285])).
% 99.43/42.65 thf(12303,plain,(! [A:nat] : (((sk26 @ (product_Pair_nat_nat @ v @ A)) != u))),inference(simp,[status(thm)],[12295])).
% 99.43/42.65 thf(122,axiom,((! [A:nat]: (ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_less__add__one)).
% 99.43/42.65 thf(681,plain,((! [A:nat]: (ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 99.43/42.65 thf(682,plain,(! [A:nat] : ((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)))),inference(cnf,[status(esa)],[681])).
% 99.43/42.65 thf(119,axiom,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_not__add__less1)).
% 99.43/42.65 thf(674,plain,((! [A:nat,B:nat]: ~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 99.43/42.65 thf(675,plain,((~ (? [A:nat,B:nat]: (ord_less_nat @ (plus_plus_nat @ A @ B) @ A)))),inference(miniscope,[status(thm)],[674])).
% 99.43/42.65 thf(676,plain,(! [B:nat,A:nat] : ((~ (ord_less_nat @ (plus_plus_nat @ A @ B) @ A)))),inference(cnf,[status(esa)],[675])).
% 99.43/42.65 thf(2128,plain,(! [C:nat,B:nat,A:nat] : (~ (($true)) | ((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ (plus_plus_nat @ B @ C) @ B)))),inference(paramod_ordered,[status(thm)],[682,676])).
% 99.43/42.65 thf(2129,plain,(! [C:nat,B:nat,A:nat] : (((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ (plus_plus_nat @ B @ C) @ B)))),inference(simp,[status(thm)],[2128])).
% 99.43/42.65 thf(2157,plain,(! [C:nat,B:nat,A:nat] : ((A != (plus_plus_nat @ B @ C)) | ((plus_plus_nat @ A @ one_one_nat) != B))),inference(simp,[status(thm)],[2129])).
% 99.43/42.65 thf(2191,plain,(! [B:nat,A:nat] : (((plus_plus_nat @ (plus_plus_nat @ A @ B) @ one_one_nat) != A))),inference(simp,[status(thm)],[2157])).
% 99.43/42.65 thf(3339,plain,(! [B:nat,A:nat] : (((plus_plus_nat @ (size_s1990949619at_nat @ p) @ one_one_nat) != A) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ A @ B)))),inference(paramod_ordered,[status(thm)],[3324,2191])).
% 99.43/42.65 thf(3340,plain,(((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != (plus_plus_nat @ (size_s1990949619at_nat @ p) @ one_one_nat))),inference(pattern_uni,[status(thm)],[3339:[bind(A, $thf(plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat)),bind(B, $thf(size_s1990949619at_nat @ p2))]])).
% 99.43/42.65 thf(4331,plain,(((size_s1990949619at_nat @ p1) != (size_s1990949619at_nat @ p)) | (one_one_nat != one_one_nat)),inference(simp,[status(thm)],[3340])).
% 99.43/42.65 thf(4348,plain,(((size_s1990949619at_nat @ p1) != (size_s1990949619at_nat @ p))),inference(simp,[status(thm)],[4331])).
% 99.43/42.65 thf(2093,plain,(! [B:nat,A:nat] : (~ (($true)) | ((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ B @ B)))),inference(paramod_ordered,[status(thm)],[682,289])).
% 99.43/42.65 thf(2094,plain,(! [B:nat,A:nat] : (((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ B @ B)))),inference(simp,[status(thm)],[2093])).
% 99.43/42.65 thf(2105,plain,(! [B:nat,A:nat] : ((A != B) | ((plus_plus_nat @ A @ one_one_nat) != B))),inference(simp,[status(thm)],[2094])).
% 99.43/42.65 thf(2120,plain,(! [A:nat] : (((plus_plus_nat @ A @ one_one_nat) != A))),inference(simp,[status(thm)],[2105])).
% 99.43/42.65 thf(3335,plain,(! [A:nat] : (((size_s1990949619at_nat @ p) != A) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ A @ one_one_nat)))),inference(paramod_ordered,[status(thm)],[3324,2120])).
% 99.43/42.65 thf(3342,plain,(((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != (size_s1990949619at_nat @ p)) | ((size_s1990949619at_nat @ p2) != one_one_nat)),inference(simp,[status(thm)],[3335])).
% 99.43/42.65 thf(172,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat]: ((connected_capacity @ A @ B @ C) => (((min_dist_capacity @ A @ B @ C) = D) => ((ord_less_nat @ E @ D) => (? [F:nat]: ((connected_capacity @ A @ B @ F) & ((min_dist_capacity @ A @ B @ F) = E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_Graph_Omin__dist__less)).
% 99.43/42.65 thf(838,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat]: ((connected_capacity @ (A) @ B @ C) => (((min_dist_capacity @ (A) @ B @ C) = D) => ((ord_less_nat @ E @ D) => (? [F:nat]: ((connected_capacity @ (A) @ B @ F) & ((min_dist_capacity @ (A) @ B @ F) = E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 99.43/42.65 thf(206,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ C @ D)) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_add__mono__thms__linordered__semiring_I1_J)).
% 99.43/42.65 thf(949,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ C @ D)) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 99.43/42.65 thf(49,axiom,((! [A:(product_prod_nat_nat > $o),B:product_prod_nat_nat]: ((! [C:nat,D:nat]: (A @ (product_Pair_nat_nat @ C @ D))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_old_Oprod_Oinducts)).
% 99.43/42.65 thf(421,plain,((! [A:(product_prod_nat_nat > $o),B:product_prod_nat_nat]: ((! [C:nat,D:nat]: (A @ (product_Pair_nat_nat @ C @ D))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 99.43/42.65 thf(98,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_add__le__mono1)).
% 99.43/42.65 thf(606,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 99.43/42.65 thf(1013,plain,(! [A:nat] : (((plus_plus_nat @ A) = (^ [B:nat]: (plus_plus_nat @ B @ A))))),inference(func_ext,[status(esa)],[814])).
% 99.43/42.65 thf(73,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_dual__order_Oirrefl)).
% 99.43/42.65 thf(492,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 99.43/42.65 thf(158,axiom,((! [A:nat,B:nat,C:nat,D:nat,E:nat]: ((dist_capacity @ c @ A @ B @ C) => ((dist_capacity @ c @ C @ D @ E) => (((min_dist_capacity @ c @ A @ E) = (plus_plus_nat @ B @ D)) => ((min_dist_capacity @ c @ A @ C) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_min__dist__split_I1_J)).
% 99.43/42.65 thf(789,plain,((! [A:nat,B:nat,C:nat,D:nat,E:nat]: ((dist_capacity @ (c) @ A @ B @ C) => ((dist_capacity @ (c) @ C @ D @ E) => (((min_dist_capacity @ (c) @ A @ E) = (plus_plus_nat @ B @ D)) => ((min_dist_capacity @ (c) @ A @ C) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 99.43/42.65 thf(18,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_linorder__neqE__nat)).
% 99.43/42.65 thf(321,plain,((! [A:nat,B:nat]: ((~ (A = B)) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 99.43/42.65 thf(1322,plain,(((size_s1990949619at_nat @ p1) != one_one_nat) | ((size_s1990949619at_nat @ p2) != one_one_nat) | ((c) != (c)) | (u != s) | (v != t)),inference(simp,[status(thm)],[1318])).
% 99.43/42.65 thf(1328,plain,(((size_s1990949619at_nat @ p1) != one_one_nat) | ((size_s1990949619at_nat @ p2) != one_one_nat) | (u != s) | (v != t)),inference(simp,[status(thm)],[1322])).
% 99.43/42.65 thf(1332,plain,(((size_s1990949619at_nat @ p1) != one_one_nat) | (u != s) | (v != t) | ((size_s1990949619at_nat @ p2) != (size_s1990949619at_nat @ p1)) | (one_one_nat != one_one_nat)),inference(eqfactor_ordered,[status(thm)],[1328])).
% 99.43/42.65 thf(1334,plain,(((size_s1990949619at_nat @ p1) != one_one_nat) | (u != s) | (v != t) | (p2 != p1)),inference(simp,[status(thm)],[1332])).
% 99.43/42.65 thf(70,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_le__refl)).
% 99.43/42.65 thf(485,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 99.43/42.65 thf(5,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_dual__order_Otrans)).
% 99.43/42.65 thf(238,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 99.43/42.65 thf(202,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_add__mono)).
% 99.43/42.65 thf(937,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 99.43/42.65 thf(163,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isPath_capacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((E != C) => (? [F:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_isPath__ex__edge2)).
% 99.43/42.65 thf(806,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isPath_capacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((~ (E = C)) => (? [F:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 99.43/42.65 thf(124,axiom,((isShor1936442771pacity = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ! [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) => (ord_less_eq_nat @ (size_s1990949619at_nat @ C) @ (size_s1990949619at_nat @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_Graph_OisShortestPath__def)).
% 99.43/42.65 thf(687,plain,(((isShor1936442771pacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ! [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) => (ord_less_eq_nat @ (size_s1990949619at_nat @ C) @ (size_s1990949619at_nat @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 99.43/42.65 thf(107,axiom,((! [A:nat,B:list_P559422087at_nat]: ((isSimp1359852763pacity @ c @ A @ B @ A) = (B = nil_Pr1308055047at_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_simplePath__same__conv)).
% 99.43/42.65 thf(634,plain,((! [A:nat,B:list_P559422087at_nat]: ((isSimp1359852763pacity @ (c) @ A @ B @ A) = (B = nil_Pr1308055047at_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 99.43/42.65 thf(183,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) => (dist_capacity @ A @ B @ (size_s1990949619at_nat @ C) @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_Graph_OisPath__distD)).
% 99.43/42.65 thf(877,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ (A) @ B @ C @ D) => (dist_capacity @ (A) @ B @ (size_s1990949619at_nat @ C) @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 99.43/42.65 thf(178,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (? [C:nat]: (B = (plus_plus_nat @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_le__Suc__ex)).
% 99.43/42.65 thf(866,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (? [C:nat]: (B = (plus_plus_nat @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 99.43/42.65 thf(6932,plain,(((collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p3)))) != (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (($false)))))),inference(simp,[status(thm)],[6893])).
% 99.43/42.65 thf(51,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_eq_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_linorder__wlog)).
% 99.43/42.65 thf(428,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_eq_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 99.43/42.65 thf(7,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq_nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq_nat @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_Nat_Oex__has__greatest__nat)).
% 99.43/42.65 thf(260,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq_nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq_nat @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 99.43/42.65 thf(261,plain,((! [A:(nat > $o)]: ((? [B:nat]: (A @ B)) => ((? [B:nat]: ! [C:nat]: ((A @ C) => (ord_less_eq_nat @ C @ B))) => (? [B:nat]: ((A @ B) & ! [C:nat]: ((A @ C) => (ord_less_eq_nat @ C @ B)))))))),inference(miniscope,[status(thm)],[260])).
% 99.43/42.65 thf(262,plain,(! [D:nat,C:nat,B:nat,A:(nat > $o)] : (((~ (A @ B) | (A @ (sk7 @ C @ (A))) | (A @ (sk8 @ (A)))) & (~ (A @ B) | (A @ (sk7 @ C @ (A))) | ~ (A @ D) | (ord_less_eq_nat @ D @ (sk8 @ (A)))) & (~ (A @ B) | ~ (ord_less_eq_nat @ (sk7 @ C @ (A)) @ C) | (A @ (sk8 @ (A)))) & (~ (A @ B) | ~ (ord_less_eq_nat @ (sk7 @ C @ (A)) @ C) | ~ (A @ D) | (ord_less_eq_nat @ D @ (sk8 @ (A))))))),inference(cnf,[status(esa)],[261])).
% 99.43/42.65 thf(265,plain,(! [C:nat,B:nat,A:(nat > $o)] : ((~ (A @ B)) | (~ (ord_less_eq_nat @ (sk7 @ C @ (A)) @ C)) | (A @ (sk8 @ (A))))),inference(cnfConj,[status(thm)],[262])).
% 99.43/42.65 thf(77,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((A != B) => (ord_less_nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_le__neq__implies__less)).
% 99.43/42.65 thf(507,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((~ (A = B)) => (ord_less_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 99.43/42.65 thf(80,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_nat__less__le)).
% 99.43/42.65 thf(516,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 99.43/42.65 thf(517,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(lifteq,[status(thm)],[516])).
% 99.43/42.65 thf(1072,plain,(! [A:nat] : (((ord_less_nat @ A) = (^ [B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B)))))),inference(func_ext,[status(esa)],[517])).
% 99.43/42.65 thf(60,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => (connected_capacity @ A @ B @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_Graph_OisShortestPath__level__edge_I1_J)).
% 99.43/42.65 thf(453,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => (connected_capacity @ (A) @ B @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 99.43/42.65 thf(83,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_order__class_Oorder_Oeq__iff)).
% 99.43/42.65 thf(527,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 99.43/42.65 thf(15,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_eq__imp__le)).
% 99.43/42.65 thf(309,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 99.43/42.65 thf(310,plain,(! [B:nat,A:nat] : ((~ (A = B)) | (ord_less_eq_nat @ A @ B))),inference(cnf,[status(esa)],[309])).
% 99.43/42.65 thf(311,plain,(! [B:nat,A:nat] : ((A != B) | (ord_less_eq_nat @ A @ B))),inference(lifteq,[status(thm)],[310])).
% 99.43/42.65 thf(312,plain,(! [A:nat] : ((ord_less_eq_nat @ A @ A))),inference(simp,[status(thm)],[311])).
% 99.43/42.65 thf(3,axiom,((! [A:(product_prod_nat_nat > $o),B:(product_prod_nat_nat > $o)]: ((! [C:product_prod_nat_nat]: ((A @ C) = (B @ C))) => ((collec7649004at_nat @ A) = (collec7649004at_nat @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_Collect__cong)).
% 99.43/42.65 thf(233,plain,((! [A:(product_prod_nat_nat > $o),B:(product_prod_nat_nat > $o)]: ((! [C:product_prod_nat_nat]: ((A @ C) = (B @ C))) => ((collec7649004at_nat @ (A)) = (collec7649004at_nat @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 99.43/42.65 thf(39,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:product_prod_nat_nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) => ((member701585322at_nat @ E @ (set_Pr2131844118at_nat @ C)) => (~ (member701585322at_nat @ (product_swap_nat_nat @ E) @ (set_Pr2131844118at_nat @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_Graph_OisSPath__nt__parallel)).
% 99.43/42.65 thf(380,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:product_prod_nat_nat]: ((isSimp1359852763pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ E @ (set_Pr2131844118at_nat @ C)) => (~ (member701585322at_nat @ (product_swap_nat_nat @ E) @ (set_Pr2131844118at_nat @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 99.43/42.65 thf(84,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_ord__eq__le__subst)).
% 99.43/42.65 thf(529,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 99.43/42.65 thf(159,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat,F:nat]: ((isSimp1359852763pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((D != F) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ F @ E) @ (set_Pr2131844118at_nat @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_isSPath__sg__incoming)).
% 99.43/42.65 thf(793,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat,F:nat]: ((isSimp1359852763pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((~ (D = F)) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ F @ E) @ (set_Pr2131844118at_nat @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 99.43/42.65 thf(197,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => (connected_capacity @ c @ D @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_isShortestPath__level__edge_I2_J)).
% 99.43/42.65 thf(925,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => (connected_capacity @ (c) @ D @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 99.43/42.65 thf(164,axiom,((((min_dist_capacity @ c @ s @ t) = (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))) => ((min_dist_capacity @ c @ u @ t) = (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_Au_At_A_061_A1_A_L_Alength_Ap2_092_060close_062)).
% 99.43/42.65 thf(810,plain,((((min_dist_capacity @ (c) @ s @ t) = (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))) => ((min_dist_capacity @ (c) @ u @ t) = (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 99.43/42.65 thf(7787,plain,((member701585322at_nat @ sk66 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p3)))))),inference(pre_uni,[status(thm)],[7771:[bind(A, $thf(sk66)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p3))))]])).
% 99.43/42.65 thf(8864,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((member701585322at_nat @ sk66 @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p3))))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[7787,491])).
% 99.43/42.65 thf(8884,plain,((member701585322at_nat @ sk66 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p3))))))))),inference(pre_uni,[status(thm)],[8864:[bind(A, $thf(sk66)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (collec7649004at_nat @ (^ [D:product_prod_nat_nat]: (member701585322at_nat @ D @ (set_Pr2131844118at_nat @ p3)))))))]])).
% 99.43/42.65 thf(9522,plain,(! [A:product_prod_nat_nat] : (~ (($true)) | ((member701585322at_nat @ sk66 @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p3)))))))) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(paramod_ordered,[status(thm)],[8884,6757])).
% 99.43/42.65 thf(9523,plain,(! [A:product_prod_nat_nat] : (((member701585322at_nat @ sk66 @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p3)))))))) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(simp,[status(thm)],[9522])).
% 99.43/42.65 thf(9560,plain,(! [A:product_prod_nat_nat] : ((sk66 != A) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p3))))))) != (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false))))))),inference(simp,[status(thm)],[9523])).
% 99.43/42.65 thf(9567,plain,(((collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p3))))))) != (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (($false)))))),inference(simp,[status(thm)],[9560])).
% 99.43/42.65 thf(9570,plain,(((^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p3)))))) != (^ [A:product_prod_nat_nat]: (($false))))),inference(simp,[status(thm)],[9567])).
% 99.43/42.65 thf(9588,plain,((member701585322at_nat @ sk68 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p3)))))),inference(func_ext,[status(esa)],[9570])).
% 99.43/42.65 thf(34,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((B = C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_ord__le__eq__trans)).
% 99.43/42.65 thf(366,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((B = C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 99.43/42.65 thf(131,axiom,((! [A:nat,B:nat]: (ord_less_eq_nat @ A @ (plus_plus_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_le__add1)).
% 99.43/42.65 thf(713,plain,((! [A:nat,B:nat]: (ord_less_eq_nat @ A @ (plus_plus_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 99.43/42.65 thf(714,plain,(! [B:nat,A:nat] : ((ord_less_eq_nat @ A @ (plus_plus_nat @ A @ B)))),inference(cnf,[status(esa)],[713])).
% 99.43/42.65 thf(11,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_ord__le__eq__subst)).
% 99.43/42.65 thf(292,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 99.43/42.65 thf(6241,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (set_Pr2131844118at_nat @ p)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[788,491])).
% 99.43/42.65 thf(6439,plain,((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p)))))),inference(pre_uni,[status(thm)],[6241:[bind(A, $thf(product_Pair_nat_nat @ u @ v)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p))))]])).
% 99.43/42.65 thf(6792,plain,(! [A:product_prod_nat_nat] : (~ (($true)) | ((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p))))) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(paramod_ordered,[status(thm)],[6439,6757])).
% 99.43/42.65 thf(6793,plain,(! [A:product_prod_nat_nat] : (((member701585322at_nat @ (product_Pair_nat_nat @ u @ v) @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p))))) != (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false)))))))),inference(simp,[status(thm)],[6792])).
% 99.43/42.65 thf(6849,plain,(! [A:product_prod_nat_nat] : (((product_Pair_nat_nat @ u @ v) != A) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p)))) != (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (($false))))))),inference(simp,[status(thm)],[6793])).
% 99.43/42.65 thf(6856,plain,(((collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p)))) != (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (($false)))))),inference(simp,[status(thm)],[6849])).
% 99.43/42.65 thf(204,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_20_add__right__imp__eq)).
% 99.43/42.65 thf(942,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)],[204])).
% 99.43/42.65 thf(54,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_less__not__refl)).
% 99.43/42.65 thf(439,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 99.43/42.65 thf(209,axiom,((dist_capacity @ c @ s @ (size_s1990949619at_nat @ p1) @ u)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_DISTS_I1_J)).
% 99.43/42.65 thf(957,plain,((dist_capacity @ (c) @ s @ (size_s1990949619at_nat @ p1) @ u)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 99.43/42.65 thf(143,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((min_dist_capacity @ A @ E @ D) = (plus_plus_nat @ one_one_nat @ (min_dist_capacity @ A @ F @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Graph_OisShortestPath__level__edge_I5_J)).
% 99.43/42.65 thf(746,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((min_dist_capacity @ (A) @ E @ D) = (plus_plus_nat @ one_one_nat @ (min_dist_capacity @ (A) @ F @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 99.43/42.65 thf(166,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((min_dist_capacity @ A @ B @ F) = (plus_plus_nat @ (min_dist_capacity @ A @ B @ E) @ one_one_nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_Graph_OisShortestPath__level__edge_I4_J)).
% 99.43/42.65 thf(815,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((min_dist_capacity @ (A) @ B @ F) = (plus_plus_nat @ (min_dist_capacity @ (A) @ B @ E) @ one_one_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 99.43/42.65 thf(126,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_add__mono__thms__linordered__field_I2_J)).
% 99.43/42.65 thf(693,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 99.43/42.65 thf(264,plain,(! [D:nat,C:nat,B:nat,A:(nat > $o)] : ((~ (A @ B)) | (A @ (sk7 @ C @ (A))) | (~ (A @ D)) | (ord_less_eq_nat @ D @ (sk8 @ (A))))),inference(cnfConj,[status(thm)],[262])).
% 99.43/42.65 thf(268,plain,(! [C:nat,B:nat,A:nat] : ((~ (A = A)) | (A = (sk7 @ B @ ((=) @ nat @ A))) | (~ (A = C)) | (ord_less_eq_nat @ C @ (sk8 @ ((=) @ nat @ A))))),inference(replace_leibeq,[status(thm)],[264:[bind(A, $thf((=) @ nat @ B))]])).
% 99.43/42.65 thf(274,plain,(! [C:nat,B:nat,A:nat] : ((A != A) | (A = (sk7 @ B @ ((=) @ nat @ A))) | (A != C) | (ord_less_eq_nat @ C @ (sk8 @ ((=) @ nat @ A))))),inference(lifteq,[status(thm)],[268])).
% 99.43/42.65 thf(275,plain,(! [B:nat,A:nat] : ((B = (sk7 @ A @ ((=) @ nat @ B))) | (ord_less_eq_nat @ B @ (sk8 @ ((=) @ nat @ B))))),inference(simp,[status(thm)],[274])).
% 99.43/42.65 thf(64,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_dual__order_Orefl)).
% 99.43/42.65 thf(467,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 99.43/42.65 thf(102,axiom,((! [A:nat,B:nat]: (ord_less_eq_nat @ A @ (plus_plus_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_le__add2)).
% 99.43/42.65 thf(624,plain,((! [A:nat,B:nat]: (ord_less_eq_nat @ A @ (plus_plus_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 99.43/42.65 thf(625,plain,(! [B:nat,A:nat] : ((ord_less_eq_nat @ A @ (plus_plus_nat @ B @ A)))),inference(cnf,[status(esa)],[624])).
% 99.43/42.65 thf(52,axiom,((! [A:nat,B:nat]: ((product_swap_nat_nat @ (product_Pair_nat_nat @ A @ B)) = (product_Pair_nat_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_swap__simp)).
% 99.43/42.65 thf(435,plain,((! [A:nat,B:nat]: ((product_swap_nat_nat @ (product_Pair_nat_nat @ A @ B)) = (product_Pair_nat_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 99.43/42.65 thf(21,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_le__antisym)).
% 99.43/42.65 thf(329,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 99.43/42.65 thf(4552,plain,(! [B:nat,A:nat] : ((ord_less_eq_nat @ A @ (size_s1990949619at_nat @ p)) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ B @ A)))),inference(paramod_ordered,[status(thm)],[3324,625])).
% 99.43/42.65 thf(4553,plain,((ord_less_eq_nat @ (size_s1990949619at_nat @ p2) @ (size_s1990949619at_nat @ p))),inference(pattern_uni,[status(thm)],[4552:[bind(A, $thf(size_s1990949619at_nat @ p2)),bind(B, $thf(plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat))]])).
% 99.43/42.65 thf(82,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_ord__eq__le__trans)).
% 99.43/42.65 thf(522,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 99.43/42.65 thf(146,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_10_add__right__cancel)).
% 99.43/42.65 thf(757,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)],[146])).
% 99.43/42.65 thf(89,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_nat__less__induct)).
% 99.43/42.65 thf(551,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 99.43/42.65 thf(4432,plain,(~ (($true)) | ((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) != (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2)))),inference(paramod_ordered,[status(thm)],[4380,3332])).
% 99.43/42.65 thf(4433,plain,(((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) != (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2)))),inference(simp,[status(thm)],[4432])).
% 99.43/42.65 thf(4461,plain,(((sk2 @ ((=) @ nat)) != (size_s1990949619at_nat @ p)) | ((sk3 @ ((=) @ nat)) != (size_s1990949619at_nat @ p2))),inference(simp,[status(thm)],[4433])).
% 99.43/42.65 thf(61,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_dual__order_Ostrict__trans)).
% 99.43/42.65 thf(456,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 99.43/42.65 thf(173,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat,F:nat]: ((isSimp1359852763pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((E != F) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ D @ F) @ (set_Pr2131844118at_nat @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_isSPath__sg__outgoing)).
% 99.43/42.65 thf(847,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat,F:nat]: ((isSimp1359852763pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((~ (E = F)) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ D @ F) @ (set_Pr2131844118at_nat @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 99.43/42.65 thf(9638,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((member701585322at_nat @ sk68 @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p3))))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[9588,491])).
% 99.43/42.65 thf(9658,plain,((member701585322at_nat @ sk68 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p3))))))))),inference(pre_uni,[status(thm)],[9638:[bind(A, $thf(sk68)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (collec7649004at_nat @ (^ [D:product_prod_nat_nat]: (member701585322at_nat @ D @ (set_Pr2131844118at_nat @ p3)))))))]])).
% 99.43/42.65 thf(184,axiom,((dist_capacity @ c @ u @ one_one_nat @ v)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_DISTS_I2_J)).
% 99.43/42.65 thf(879,plain,((dist_capacity @ (c) @ u @ one_one_nat @ v)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 99.43/42.65 thf(19,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_dual__order_Oantisym)).
% 99.43/42.65 thf(324,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 99.43/42.65 thf(215,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) => (ord_less_eq_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_add__le__imp__le__left)).
% 99.43/42.65 thf(974,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) => (ord_less_eq_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 99.43/42.65 thf(127,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_trans__le__add1)).
% 99.43/42.65 thf(697,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 99.43/42.65 thf(112,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_add__less__cancel__right)).
% 99.43/42.65 thf(650,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 99.43/42.65 thf(136,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_add__le__mono)).
% 99.43/42.65 thf(725,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 99.43/42.65 thf(47,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq_nat @ D @ C))) => (~ (! [D:nat]: ((A @ D) => (~ (! [E:nat]: ((A @ E) => (ord_less_eq_nat @ E @ D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_bounded__Max__nat)).
% 99.43/42.65 thf(403,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq_nat @ D @ C))) => (~ (! [D:nat]: ((A @ D) => (~ (! [E:nat]: ((A @ E) => (ord_less_eq_nat @ E @ D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 99.43/42.65 thf(42,axiom,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_less__imp__triv)).
% 99.43/42.65 thf(388,plain,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 99.43/42.65 thf(179,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_add__less__mono1)).
% 99.43/42.65 thf(869,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 99.43/42.65 thf(155,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_add__less__mono)).
% 99.43/42.65 thf(783,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 99.43/42.65 thf(220,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ one_one_nat) @ (plus_plus_nat @ B @ one_one_nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_add__mono1)).
% 99.43/42.65 thf(989,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ one_one_nat) @ (plus_plus_nat @ B @ one_one_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 99.43/42.65 thf(175,axiom,((((min_dist_capacity @ c @ s @ t) = (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))) => ((min_dist_capacity @ c @ s @ u) = (size_s1990949619at_nat @ p1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_As_Au_A_061_Alength_Ap1_092_060close_062)).
% 99.43/42.65 thf(857,plain,((((min_dist_capacity @ (c) @ s @ t) = (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))) => ((min_dist_capacity @ (c) @ s @ u) = (size_s1990949619at_nat @ p1)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 99.43/42.65 thf(228,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_add__le__less__mono)).
% 99.43/42.65 thf(1006,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 99.43/42.65 thf(20,axiom,((connected_capacity = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:list_P559422087at_nat]: (isPath_capacity @ A @ B @ D @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_Graph_Oconnected__def)).
% 99.43/42.65 thf(327,plain,(((connected_capacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:list_P559422087at_nat]: (isPath_capacity @ A @ B @ D @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 99.43/42.65 thf(328,plain,(((connected_capacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:list_P559422087at_nat]: (isPath_capacity @ A @ B @ D @ C)))),inference(lifteq,[status(thm)],[327])).
% 99.43/42.65 thf(10,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_eq__iff)).
% 99.43/42.65 thf(290,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 99.43/42.65 thf(291,plain,(((^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))) = ((=) @ nat))),inference(lifteq,[status(thm)],[290])).
% 99.43/42.65 thf(1074,plain,(((ord_less_nat) = ((=) @ nat)) | ((^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))) != (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(paramod_ordered,[status(thm)],[517,291])).
% 99.43/42.65 thf(1078,plain,(((ord_less_nat) = ((=) @ nat)) | ((ord_less_eq_nat) != (ord_less_eq_nat)) | ((^ [A:nat,B:nat]: (ord_less_eq_nat @ B @ A)) != (^ [A:nat,B:nat]: ~ (A = B)))),inference(simp,[status(thm)],[1074])).
% 99.43/42.65 thf(1082,plain,(((ord_less_nat) = ((=) @ nat)) | ((^ [A:nat,B:nat]: (ord_less_eq_nat @ B @ A)) != (^ [A:nat,B:nat]: ~ (A = B)))),inference(simp,[status(thm)],[1078])).
% 99.43/42.65 thf(117,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isPath_capacity @ c @ A @ B @ C) => (? [D:list_P559422087at_nat]: (isSimp1359852763pacity @ c @ A @ D @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_isSPath__pathLE)).
% 99.43/42.65 thf(669,plain,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isPath_capacity @ (c) @ A @ B @ C) => (? [D:list_P559422087at_nat]: (isSimp1359852763pacity @ (c) @ A @ D @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 99.43/42.65 thf(108,axiom,((! [A:list_P559422087at_nat,B:list_P559422087at_nat]: (((size_s1990949619at_nat @ A) != (size_s1990949619at_nat @ B)) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_size__neq__size__imp__neq)).
% 99.43/42.65 thf(637,plain,((! [A:list_P559422087at_nat,B:list_P559422087at_nat]: ((~ ((size_s1990949619at_nat @ A) = (size_s1990949619at_nat @ B))) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 99.43/42.65 thf(87,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_less__imp__le__nat)).
% 99.43/42.65 thf(547,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 99.43/42.65 thf(129,axiom,((! [A:nat]: (connected_capacity @ c @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_connected__refl)).
% 99.43/42.65 thf(705,plain,((! [A:nat]: (connected_capacity @ (c) @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 99.43/42.65 thf(706,plain,(! [A:nat] : ((connected_capacity @ (c) @ A @ A))),inference(cnf,[status(esa)],[705])).
% 99.43/42.65 thf(3341,plain,(((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ (size_s1990949619at_nat @ p) @ one_one_nat))),inference(simp,[status(thm)],[3335])).
% 99.43/42.65 thf(4530,plain,(((plus_plus_nat @ (size_s1990949619at_nat @ p) @ one_one_nat) != (size_s1990949619at_nat @ p))),inference(rewrite,[status(thm)],[3341,3324])).
% 99.43/42.65 thf(281,plain,((? [A:(nat > (product_prod_nat_nat > nat))]: ! [B:nat,C:nat]: ((A @ C @ (product_Pair_nat_nat @ B @ C)) = B))),inference(detectInverse,[status(thm)],[280])).
% 99.43/42.65 thf(282,plain,(! [B:nat,A:nat] : (((sk9 @ B @ (product_Pair_nat_nat @ A @ B)) = A))),inference(cnf,[status(esa)],[281])).
% 99.43/42.65 thf(12410,plain,(! [B:nat,A:nat] : (((sk9 @ B @ (product_Pair_nat_nat @ A @ B)) = A))),inference(lifteq,[status(thm)],[282])).
% 99.43/42.65 thf(141,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_add__strict__right__mono)).
% 99.43/42.65 thf(738,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 99.43/42.65 thf(1320,plain,(((size_s1990949619at_nat @ p1) != one_one_nat) | ((size_s1990949619at_nat @ p2) != one_one_nat) | ((min_dist_capacity @ (c) @ u @ t) != (min_dist_capacity @ (c) @ s @ v))),inference(simp,[status(thm)],[1318])).
% 99.43/42.65 thf(1668,plain,(((size_s1990949619at_nat @ p1) != one_one_nat) | ((size_s1990949619at_nat @ p2) != one_one_nat) | ((min_dist_capacity @ (c) @ u @ t) != (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat))),inference(rewrite,[status(thm)],[1320,994])).
% 99.43/42.65 thf(227,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isPath_capacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((D != A) => (? [F:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ F @ D) @ (set_Pr2131844118at_nat @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_isPath__ex__edge1)).
% 99.43/42.65 thf(1002,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isPath_capacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((~ (D = A)) => (? [F:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ F @ D) @ (set_Pr2131844118at_nat @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 99.43/42.65 thf(9606,plain,(! [A:set_Pr1986765409at_nat] : ((member701585322at_nat @ sk68 @ A) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) != (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p3))))))),inference(paramod_ordered,[status(thm)],[484,9588])).
% 99.43/42.65 thf(9607,plain,((member701585322at_nat @ sk68 @ (set_Pr2131844118at_nat @ p3))),inference(pattern_uni,[status(thm)],[9606:[bind(A, $thf(set_Pr2131844118at_nat @ p3))]])).
% 99.43/42.65 thf(11051,plain,(! [D:nat,C:nat,B:nat,A:nat] : (((product_Pair_nat_nat @ A @ B) != (product_Pair_nat_nat @ C @ D)) | (C != (sk2 @ ((=) @ nat))) | (A != (sk3 @ ((=) @ nat))))),inference(paramod_ordered,[status(thm)],[280,4467])).
% 99.43/42.65 thf(11052,plain,(! [C:nat,B:nat,A:nat] : (((product_Pair_nat_nat @ (sk3 @ ((=) @ nat)) @ A) != (product_Pair_nat_nat @ B @ C)) | (B != (sk2 @ ((=) @ nat))))),inference(pattern_uni,[status(thm)],[11051:[bind(A, $thf(sk3 @ ((=) @ nat))),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D))]])).
% 99.43/42.65 thf(11927,plain,(! [B:nat,A:nat] : (((product_Pair_nat_nat @ (sk3 @ ((=) @ nat)) @ A) != (product_Pair_nat_nat @ (sk2 @ ((=) @ nat)) @ B)))),inference(simp,[status(thm)],[11052])).
% 99.43/42.65 thf(35,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat]: ((isSimp1359852763pacity @ A @ B @ C @ B) = (C = nil_Pr1308055047at_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_Graph_OsimplePath__same__conv)).
% 99.43/42.65 thf(371,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat]: ((isSimp1359852763pacity @ (A) @ B @ C @ B) = (C = nil_Pr1308055047at_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 99.43/42.65 thf(111,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_add__less__cancel__left)).
% 99.43/42.65 thf(647,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 99.43/42.65 thf(224,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_ab__semigroup__add__class_Oadd__ac_I1_J)).
% 99.43/42.65 thf(997,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 99.43/42.65 thf(1333,plain,(((size_s1990949619at_nat @ p1) != one_one_nat) | (u != s) | (v != t) | ((size_s1990949619at_nat @ p2) != (size_s1990949619at_nat @ p1))),inference(simp,[status(thm)],[1332])).
% 99.43/42.65 thf(266,plain,(! [D:nat,C:nat,B:nat,A:(nat > $o)] : ((~ (A @ B)) | (~ (ord_less_eq_nat @ (sk7 @ C @ (A)) @ C)) | (~ (A @ D)) | (ord_less_eq_nat @ D @ (sk8 @ (A))))),inference(cnfConj,[status(thm)],[262])).
% 99.43/42.65 thf(196,axiom,((! [A:nat,B:nat,C:nat,D:nat,E:nat]: ((dist_capacity @ c @ A @ B @ C) => ((dist_capacity @ c @ C @ D @ E) => (((min_dist_capacity @ c @ A @ E) = (plus_plus_nat @ B @ D)) => ((min_dist_capacity @ c @ C @ E) = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_min__dist__split_I2_J)).
% 99.43/42.65 thf(921,plain,((! [A:nat,B:nat,C:nat,D:nat,E:nat]: ((dist_capacity @ (c) @ A @ B @ C) => ((dist_capacity @ (c) @ C @ D @ E) => (((min_dist_capacity @ (c) @ A @ E) = (plus_plus_nat @ B @ D)) => ((min_dist_capacity @ (c) @ C @ E) = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 99.43/42.65 thf(86,axiom,((! [A:nat,B:nat]: (((ord_less_nat @ A @ B) | (A = B)) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_less__or__eq__imp__le)).
% 99.43/42.65 thf(541,plain,((! [A:nat,B:nat]: (((ord_less_nat @ A @ B) | (A = B)) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 99.43/42.65 thf(114,axiom,(((min_dist_capacity @ c @ v @ t) = (size_s1990949619at_nat @ p2))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3__092_060open_062min__dist_Av_At_A_061_Alength_Ap2_092_060close_062)).
% 99.43/42.65 thf(656,plain,(((min_dist_capacity @ (c) @ v @ t) = (size_s1990949619at_nat @ p2))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 99.43/42.65 thf(657,plain,(((min_dist_capacity @ (c) @ v @ t) = (size_s1990949619at_nat @ p2))),inference(lifteq,[status(thm)],[656])).
% 99.43/42.65 thf(149,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ A @ (plus_plus_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_trans__le__add2)).
% 99.43/42.65 thf(765,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ A @ (plus_plus_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 99.43/42.65 thf(45,axiom,((connected_capacity = connected_capacity)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_Graph_Oconnected_Ocong)).
% 99.43/42.65 thf(398,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 99.43/42.65 thf(208,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (C = D)) => ((plus_plus_nat @ A @ C) = (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_add__mono__thms__linordered__semiring_I4_J)).
% 99.43/42.65 thf(953,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((A = B) & (C = D)) => ((plus_plus_nat @ A @ C) = (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 99.43/42.65 thf(93,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_not__less__iff__gr__or__eq)).
% 99.43/42.65 thf(586,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 99.43/42.65 thf(133,axiom,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ c @ A @ B @ C) => (ord_less_eq_nat @ (min_dist_capacity @ c @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_min__dist__minD)).
% 99.43/42.65 thf(718,plain,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ (c) @ A @ B @ C) => (ord_less_eq_nat @ (min_dist_capacity @ (c) @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 99.43/42.65 thf(26,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_le__eq__less__or__eq)).
% 99.43/42.65 thf(343,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 99.43/42.65 thf(4,axiom,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_exists__least__iff)).
% 99.43/42.65 thf(236,plain,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 99.43/42.65 thf(237,plain,(((^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))) = ((?) @ nat))),inference(lifteq,[status(thm)],[236])).
% 99.43/42.65 thf(191,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) = ((isPath_capacity @ c @ A @ B @ C) & ((size_s1990949619at_nat @ B) = (min_dist_capacity @ c @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_isShortestPath__min__dist__def)).
% 99.43/42.65 thf(906,plain,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) = ((isPath_capacity @ (c) @ A @ B @ C) & ((size_s1990949619at_nat @ B) = (min_dist_capacity @ (c) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 99.43/42.65 thf(144,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ C) => (~ ((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_add__leE)).
% 99.43/42.65 thf(750,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ C) => (~ ((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 99.43/42.65 thf(100,axiom,((! [A:nat,B:nat]: ((connected_capacity @ c @ A @ B) = (? [C:nat]: (dist_capacity @ c @ A @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_connected__by__dist)).
% 99.43/42.65 thf(618,plain,((! [A:nat,B:nat]: ((connected_capacity @ (c) @ A @ B) = (? [C:nat]: (dist_capacity @ (c) @ A @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 99.43/42.65 thf(125,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((min_dist_capacity @ c @ A @ C) = (plus_plus_nat @ (plus_plus_nat @ (min_dist_capacity @ c @ A @ D) @ one_one_nat) @ (min_dist_capacity @ c @ E @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_isShortestPath__level__edge_I6_J)).
% 99.43/42.65 thf(689,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((min_dist_capacity @ (c) @ A @ C) = (plus_plus_nat @ (plus_plus_nat @ (min_dist_capacity @ (c) @ A @ D) @ one_one_nat) @ (min_dist_capacity @ (c) @ E @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 99.43/42.65 thf(56,axiom,((! [A:nat,B:nat]: ((A != B) = ((ord_less_nat @ A @ B) | (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_nat__neq__iff)).
% 99.43/42.65 thf(444,plain,((! [A:nat,B:nat]: ((~ (A = B)) = ((ord_less_nat @ A @ B) | (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 99.43/42.65 thf(37,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((A != B) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_linorder__cases)).
% 99.43/42.65 thf(375,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (A = B)) => (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 99.43/42.65 thf(79,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_old_Oprod_Oinject)).
% 99.43/42.65 thf(513,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 99.43/42.65 thf(139,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (plus_plus_nat @ C @ A) @ (plus_plus_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_add__left__mono)).
% 99.43/42.65 thf(732,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (plus_plus_nat @ C @ A) @ (plus_plus_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 99.43/42.65 thf(12271,plain,(! [C:nat,B:nat,A:product_prod_nat_nat] : ((A != (product_Pair_nat_nat @ v @ B)) | ((product_Pair_nat_nat @ (sk30 @ A) @ (sk31 @ A)) != (product_Pair_nat_nat @ u @ C)))),inference(paramod_ordered,[status(thm)],[479,11785])).
% 99.43/42.65 thf(12293,plain,(! [B:nat,A:nat] : (((sk30 @ (product_Pair_nat_nat @ v @ A)) != u) | ((sk31 @ (product_Pair_nat_nat @ v @ A)) != B))),inference(simp,[status(thm)],[12271])).
% 99.43/42.65 thf(12301,plain,(! [A:nat] : (((sk30 @ (product_Pair_nat_nat @ v @ A)) != u))),inference(simp,[status(thm)],[12293])).
% 99.43/42.65 thf(92,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less_nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_infinite__descent)).
% 99.43/42.65 thf(577,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less_nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 99.43/42.65 thf(210,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((connected_capacity @ A @ B @ C) => (dist_capacity @ A @ B @ (min_dist_capacity @ A @ B @ C) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_Graph_Omin__dist__is__dist)).
% 99.43/42.65 thf(958,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((connected_capacity @ (A) @ B @ C) => (dist_capacity @ (A) @ B @ (min_dist_capacity @ (A) @ B @ C) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 99.43/42.65 thf(167,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat,F:nat]: ((dist_capacity @ A @ B @ C @ D) => ((dist_capacity @ A @ D @ E @ F) => (((min_dist_capacity @ A @ B @ F) = (plus_plus_nat @ C @ E)) => ((min_dist_capacity @ A @ B @ D) = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_Graph_Omin__dist__split_I1_J)).
% 99.43/42.65 thf(819,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat,F:nat]: ((dist_capacity @ (A) @ B @ C @ D) => ((dist_capacity @ (A) @ D @ E @ F) => (((min_dist_capacity @ (A) @ B @ F) = (plus_plus_nat @ C @ E)) => ((min_dist_capacity @ (A) @ B @ D) = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 99.43/42.65 thf(91,axiom,((! [A:nat,B:nat,C:nat]: (((ord_less_eq_nat @ A @ B) => (~ (ord_less_eq_nat @ B @ C))) => (((ord_less_eq_nat @ B @ A) => (~ (ord_less_eq_nat @ A @ C))) => (((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ C @ B))) => (((ord_less_eq_nat @ C @ B) => (~ (ord_less_eq_nat @ B @ A))) => (((ord_less_eq_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))) => (~ ((ord_less_eq_nat @ C @ A) => (~ (ord_less_eq_nat @ A @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_le__cases3)).
% 99.43/42.65 thf(562,plain,((! [A:nat,B:nat,C:nat]: (((ord_less_eq_nat @ A @ B) => (~ (ord_less_eq_nat @ B @ C))) => (((ord_less_eq_nat @ B @ A) => (~ (ord_less_eq_nat @ A @ C))) => (((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ C @ B))) => (((ord_less_eq_nat @ C @ B) => (~ (ord_less_eq_nat @ B @ A))) => (((ord_less_eq_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))) => (~ ((ord_less_eq_nat @ C @ A) => (~ (ord_less_eq_nat @ A @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 99.43/42.65 thf(190,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((dist_capacity @ A @ B @ C @ D) => (ord_less_eq_nat @ (min_dist_capacity @ A @ B @ D) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_Graph_Omin__dist__minD)).
% 99.43/42.65 thf(904,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((dist_capacity @ (A) @ B @ C @ D) => (ord_less_eq_nat @ (min_dist_capacity @ (A) @ B @ D) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 99.43/42.65 thf(109,axiom,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ c @ A @ B @ C) = (? [D:list_P559422087at_nat]: ((isPath_capacity @ c @ A @ D @ C) & ((size_s1990949619at_nat @ D) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_dist__def)).
% 99.43/42.65 thf(641,plain,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ (c) @ A @ B @ C) = (? [D:list_P559422087at_nat]: ((isPath_capacity @ (c) @ A @ D @ C) & ((size_s1990949619at_nat @ D) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 99.43/42.65 thf(43,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((isSimp1359852763pacity @ A @ B @ nil_Pr1308055047at_nat @ C) = (B = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_Graph_OsimplePath__empty__conv)).
% 99.43/42.65 thf(391,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((isSimp1359852763pacity @ (A) @ B @ nil_Pr1308055047at_nat @ C) = (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 99.43/42.65 thf(16,axiom,((! [A:(product_prod_nat_nat > $o),B:product_prod_nat_nat]: ((! [C:nat,D:nat]: (A @ (product_Pair_nat_nat @ C @ D))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_prod__cases)).
% 99.43/42.65 thf(313,plain,((! [A:(product_prod_nat_nat > $o),B:product_prod_nat_nat]: ((! [C:nat,D:nat]: (A @ (product_Pair_nat_nat @ C @ D))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 99.43/42.65 thf(23,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_order_Ostrict__trans)).
% 99.43/42.65 thf(335,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 99.43/42.65 thf(10856,plain,(! [A:set_Pr1986765409at_nat] : ((member701585322at_nat @ sk69 @ A) | ((collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ A))) != (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p))))))),inference(paramod_ordered,[status(thm)],[484,10837])).
% 99.43/42.65 thf(10857,plain,((member701585322at_nat @ sk69 @ (set_Pr2131844118at_nat @ p))),inference(pattern_uni,[status(thm)],[10856:[bind(A, $thf(set_Pr2131844118at_nat @ p))]])).
% 99.43/42.65 thf(75,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_dual__order_Ostrict__implies__not__eq)).
% 99.43/42.65 thf(498,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 99.43/42.65 thf(205,axiom,((! [A:nat,B:nat]: ((connected_capacity @ c @ A @ B) => (dist_capacity @ c @ A @ (min_dist_capacity @ c @ A @ B) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_min__dist__is__dist)).
% 99.43/42.65 thf(947,plain,((! [A:nat,B:nat]: ((connected_capacity @ (c) @ A @ B) => (dist_capacity @ (c) @ A @ (min_dist_capacity @ (c) @ A @ B) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 99.43/42.65 thf(217,axiom,((! [A:nat,B:nat,C:nat,D:nat,E:nat]: ((dist_capacity @ c @ A @ B @ C) => ((dist_capacity @ c @ C @ D @ E) => (dist_capacity @ c @ A @ (plus_plus_nat @ B @ D) @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_dist__trans)).
% 99.43/42.65 thf(979,plain,((! [A:nat,B:nat,C:nat,D:nat,E:nat]: ((dist_capacity @ (c) @ A @ B @ C) => ((dist_capacity @ (c) @ C @ D @ E) => (dist_capacity @ (c) @ A @ (plus_plus_nat @ B @ D) @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 99.43/42.65 thf(169,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => (isPath_capacity @ c @ A @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_shortestPath__is__path)).
% 99.43/42.65 thf(831,plain,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => (isPath_capacity @ (c) @ A @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 99.43/42.65 thf(12270,plain,(! [C:nat,B:nat,A:product_prod_nat_nat] : ((A != (product_Pair_nat_nat @ u @ C)) | ((product_Pair_nat_nat @ (sk30 @ A) @ (sk31 @ A)) != (product_Pair_nat_nat @ v @ B)))),inference(paramod_ordered,[status(thm)],[479,11785])).
% 99.43/42.65 thf(12289,plain,(! [B:nat,A:nat] : (((sk30 @ (product_Pair_nat_nat @ u @ B)) != v) | ((sk31 @ (product_Pair_nat_nat @ u @ B)) != A))),inference(simp,[status(thm)],[12270])).
% 99.43/42.65 thf(12297,plain,(! [A:nat] : (((sk30 @ (product_Pair_nat_nat @ u @ A)) != v))),inference(simp,[status(thm)],[12289])).
% 99.43/42.65 thf(17,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_antisym__conv)).
% 99.43/42.65 thf(318,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 99.43/42.65 thf(185,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ A @ D) = (plus_plus_nat @ B @ (plus_plus_nat @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_group__cancel_Oadd1)).
% 99.43/42.65 thf(880,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ A @ D) = (plus_plus_nat @ B @ (plus_plus_nat @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 99.43/42.65 thf(13,axiom,((! [A:product_prod_nat_nat]: ((product_swap_nat_nat @ (product_swap_nat_nat @ A)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_swap__swap)).
% 99.43/42.65 thf(303,plain,((! [A:product_prod_nat_nat]: ((product_swap_nat_nat @ (product_swap_nat_nat @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 99.43/42.65 thf(269,plain,(! [B:nat,A:nat] : ((~ (A = A)) | (~ (ord_less_eq_nat @ (sk7 @ B @ ((=) @ nat @ A)) @ B)) | (A = (sk8 @ ((=) @ nat @ A))))),inference(replace_leibeq,[status(thm)],[265:[bind(A, $thf((=) @ nat @ B))]])).
% 99.43/42.65 thf(270,plain,(! [B:nat,A:nat] : ((A != A) | (A = (sk8 @ ((=) @ nat @ A))) | (~ (ord_less_eq_nat @ (sk7 @ B @ ((=) @ nat @ A)) @ B)))),inference(lifteq,[status(thm)],[269])).
% 99.43/42.65 thf(271,plain,(! [B:nat,A:nat] : ((A = (sk8 @ ((=) @ nat @ A))) | (~ (ord_less_eq_nat @ (sk7 @ B @ ((=) @ nat @ A)) @ B)))),inference(simp,[status(thm)],[270])).
% 99.43/42.65 thf(177,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_add__strict__mono)).
% 99.43/42.65 thf(863,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ D) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 99.43/42.65 thf(189,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((min_dist_capacity @ c @ D @ C) = (plus_plus_nat @ one_one_nat @ (min_dist_capacity @ c @ E @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_isShortestPath__level__edge_I5_J)).
% 99.43/42.65 thf(900,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((min_dist_capacity @ (c) @ D @ C) = (plus_plus_nat @ one_one_nat @ (min_dist_capacity @ (c) @ E @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 99.43/42.65 thf(118,axiom,((! [A:nat]: ((one_one_nat = A) = (A = one_one_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_one__reorient)).
% 99.43/42.65 thf(671,plain,((! [A:nat]: ((one_one_nat = A) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 99.43/42.65 thf(672,plain,(! [A:nat] : (((one_one_nat = A) = (A = one_one_nat)))),inference(cnf,[status(esa)],[671])).
% 99.43/42.65 thf(673,plain,(! [A:nat] : (((one_one_nat = A) = (A = one_one_nat)))),inference(lifteq,[status(thm)],[672])).
% 99.43/42.65 thf(263,plain,(! [C:nat,B:nat,A:(nat > $o)] : ((~ (A @ B)) | (A @ (sk7 @ C @ (A))) | (A @ (sk8 @ (A))))),inference(cnfConj,[status(thm)],[262])).
% 99.43/42.65 thf(4843,plain,(! [D:nat,C:nat,B:(nat > $o),A:nat] : ((~ (A = one_one_nat)) | (B @ (sk7 @ D @ (B))) | (B @ (sk8 @ (B))) | ((one_one_nat = A) != (B @ C)))),inference(paramod_ordered,[status(thm)],[673,263])).
% 99.43/42.65 thf(4948,plain,(! [D:nat,C:nat,B:(nat > $o),A:nat] : ((A != one_one_nat) | (B @ (sk7 @ D @ (B))) | (B @ (sk8 @ (B))) | ((one_one_nat = A) != (B @ C)))),inference(lifteq,[status(thm)],[4843])).
% 99.43/42.65 thf(4972,plain,(! [A:nat] : (((sk8 @ (^ [B:nat]: (B = one_one_nat))) = one_one_nat) | ((sk7 @ A @ (^ [B:nat]: (B = one_one_nat))) = one_one_nat))),inference(pre_uni,[status(thm)],[4948:[bind(A, $thf(one_one_nat)),bind(B, $thf(^ [E:nat]: (E = one_one_nat))),bind(C, $thf(one_one_nat)),bind(D, $thf(D))]])).
% 99.43/42.65 thf(5142,plain,(! [A:nat] : (((sk8 @ (^ [B:nat]: (B = one_one_nat))) = one_one_nat) | ((sk7 @ A @ (^ [B:nat]: (B = one_one_nat))) = one_one_nat))),inference(lifteq,[status(thm)],[4972])).
% 99.43/42.65 thf(5143,plain,(! [A:nat] : (((sk8 @ (^ [B:nat]: (B = one_one_nat))) = one_one_nat) | ((sk7 @ A @ (^ [B:nat]: (B = one_one_nat))) = one_one_nat))),inference(simp,[status(thm)],[5142])).
% 99.43/42.65 thf(32,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => (connected_capacity @ A @ F @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_Graph_OisShortestPath__level__edge_I3_J)).
% 99.43/42.65 thf(362,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => (connected_capacity @ (A) @ F @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 99.43/42.65 thf(59,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_linear)).
% 99.43/42.65 thf(451,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 99.43/42.65 thf(27,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_less__imp__not__less)).
% 99.43/42.65 thf(345,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 99.43/42.65 thf(101,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) = ((isPath_capacity @ c @ A @ B @ C) & ! [D:list_P559422087at_nat]: ((isPath_capacity @ c @ A @ D @ C) => (ord_less_eq_nat @ (size_s1990949619at_nat @ B) @ (size_s1990949619at_nat @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_isShortestPath__def)).
% 99.43/42.65 thf(621,plain,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) = ((isPath_capacity @ (c) @ A @ B @ C) & ! [D:list_P559422087at_nat]: ((isPath_capacity @ (c) @ A @ D @ C) => (ord_less_eq_nat @ (size_s1990949619at_nat @ B) @ (size_s1990949619at_nat @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 99.43/42.65 thf(128,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ D @ A) = (plus_plus_nat @ B @ (plus_plus_nat @ D @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_group__cancel_Oadd2)).
% 99.43/42.65 thf(700,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((A = (plus_plus_nat @ B @ C)) => ((plus_plus_nat @ D @ A) = (plus_plus_nat @ B @ (plus_plus_nat @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 99.43/42.65 thf(1029,plain,(! [A:nat] : (((^ [B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))) = ((=) @ nat @ A)))),inference(func_ext,[status(esa)],[291])).
% 99.43/42.65 thf(212,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (! [C:nat]: (B != (plus_plus_nat @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_less__eqE)).
% 99.43/42.65 thf(964,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (! [C:nat]: ~ (B = (plus_plus_nat @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 99.43/42.65 thf(103,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) => (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_add__less__imp__less__left)).
% 99.43/42.65 thf(626,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) => (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 99.43/42.65 thf(1021,plain,(((^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:nat]: (dist_capacity @ A @ B @ D @ C)) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:list_P559422087at_nat]: (isPath_capacity @ A @ B @ D @ C))) | ((connected_capacity) != (connected_capacity))),inference(paramod_ordered,[status(thm)],[481,328])).
% 99.43/42.65 thf(1022,plain,(((^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:nat]: (dist_capacity @ A @ B @ D @ C)) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ? [D:list_P559422087at_nat]: (isPath_capacity @ A @ B @ D @ C)))),inference(pattern_uni,[status(thm)],[1021:[]])).
% 99.43/42.65 thf(3336,plain,(! [B:nat,A:nat] : ((~ (ord_less_nat @ (size_s1990949619at_nat @ p) @ A)) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ A @ B)))),inference(paramod_ordered,[status(thm)],[3324,676])).
% 99.43/42.65 thf(3337,plain,((~ (ord_less_nat @ (size_s1990949619at_nat @ p) @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat)))),inference(pattern_uni,[status(thm)],[3336:[bind(A, $thf(plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat)),bind(B, $thf(size_s1990949619at_nat @ p2))]])).
% 99.43/42.65 thf(4424,plain,(~ (($true)) | ((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) != (ord_less_nat @ (size_s1990949619at_nat @ p) @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat)))),inference(paramod_ordered,[status(thm)],[4380,3337])).
% 99.43/42.65 thf(4425,plain,(((ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat))) != (ord_less_nat @ (size_s1990949619at_nat @ p) @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat)))),inference(simp,[status(thm)],[4424])).
% 99.43/42.65 thf(4462,plain,(((sk2 @ ((=) @ nat)) != (size_s1990949619at_nat @ p)) | ((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != (sk3 @ ((=) @ nat)))),inference(simp,[status(thm)],[4425])).
% 99.43/42.65 thf(99,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((connected_capacity @ c @ A @ B) => (((min_dist_capacity @ c @ A @ B) = C) => ((ord_less_nat @ D @ C) => (? [E:nat]: ((connected_capacity @ c @ A @ E) & ((min_dist_capacity @ c @ A @ E) = D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_min__dist__less)).
% 99.43/42.65 thf(609,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((connected_capacity @ (c) @ A @ B) => (((min_dist_capacity @ (c) @ A @ B) = C) => ((ord_less_nat @ D @ C) => (? [E:nat]: ((connected_capacity @ (c) @ A @ E) & ((min_dist_capacity @ (c) @ A @ E) = D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 99.43/42.65 thf(239,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (! [C:nat]: ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B)))))),inference(miniscope,[status(thm)],[238])).
% 99.43/42.65 thf(240,plain,(! [C:nat,B:nat,A:nat] : ((~ (ord_less_eq_nat @ A @ B)) | (~ (ord_less_eq_nat @ C @ A)) | (ord_less_eq_nat @ C @ B))),inference(cnf,[status(esa)],[239])).
% 99.43/42.65 thf(193,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => (isSimp1359852763pacity @ c @ A @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_shortestPath__is__simple)).
% 99.43/42.65 thf(912,plain,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => (isSimp1359852763pacity @ (c) @ A @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 99.43/42.65 thf(46,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isPath_capacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((F != D) => (? [G:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ F @ G) @ (set_Pr2131844118at_nat @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_Graph_OisPath__ex__edge2)).
% 99.43/42.65 thf(399,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isPath_capacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((~ (F = D)) => (? [G:nat]: (member701585322at_nat @ (product_Pair_nat_nat @ F @ G) @ (set_Pr2131844118at_nat @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 99.43/42.65 thf(150,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (plus_plus_nat @ B @ C)) = (plus_plus_nat @ B @ (plus_plus_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_add_Oleft__commute)).
% 99.43/42.65 thf(768,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ A @ (plus_plus_nat @ B @ C)) = (plus_plus_nat @ B @ (plus_plus_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 99.43/42.65 thf(629,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ? [C:nat]: (B = (plus_plus_nat @ A @ C))))),inference(lifteq,[status(thm)],[628])).
% 99.43/42.65 thf(344,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(lifteq,[status(thm)],[343])).
% 99.43/42.65 thf(1044,plain,(((^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))) = (^ [A:nat,B:nat]: ? [C:nat]: (B = (plus_plus_nat @ A @ C))))),inference(rewrite,[status(thm)],[629,344])).
% 99.43/42.65 thf(154,axiom,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_add_Oassoc)).
% 99.43/42.65 thf(780,plain,((! [A:nat,B:nat,C:nat]: ((plus_plus_nat @ (plus_plus_nat @ A @ B) @ C) = (plus_plus_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 99.43/42.65 thf(1015,plain,(! [A:(product_prod_nat_nat > capacity)] : (((connected_capacity @ A) = (^ [B:nat,C:nat]: ? [D:list_P559422087at_nat]: (isPath_capacity @ A @ B @ D @ C))))),inference(func_ext,[status(esa)],[328])).
% 99.43/42.65 thf(225,axiom,((min_dist_capacity = min_dist_capacity)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_Graph_Omin__dist_Ocong)).
% 99.43/42.65 thf(1000,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 99.43/42.65 thf(174,axiom,((! [A:nat,B:nat,C:nat]: ((connected_capacity @ c @ A @ B) => ((ord_less_eq_nat @ C @ (min_dist_capacity @ c @ A @ B)) => (? [D:nat]: ((connected_capacity @ c @ A @ D) & ((min_dist_capacity @ c @ A @ D) = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_min__dist__le)).
% 99.43/42.65 thf(851,plain,((! [A:nat,B:nat,C:nat]: ((connected_capacity @ (c) @ A @ B) => ((ord_less_eq_nat @ C @ (min_dist_capacity @ (c) @ A @ B)) => (? [D:nat]: ((connected_capacity @ (c) @ A @ D) & ((min_dist_capacity @ (c) @ A @ D) = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 99.43/42.65 thf(53,axiom,((isPath_capacity = isPath_capacity)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_Graph_OisPath_Ocong)).
% 99.43/42.65 thf(438,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 99.43/42.65 thf(115,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_21_add__left__imp__eq)).
% 99.43/42.65 thf(658,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)],[115])).
% 99.43/42.65 thf(44,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat,G:nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((E != G) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ G @ F) @ (set_Pr2131844118at_nat @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_Graph_OisSPath__sg__incoming)).
% 99.43/42.65 thf(394,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat,G:nat]: ((isSimp1359852763pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((~ (E = G)) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ G @ F) @ (set_Pr2131844118at_nat @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 99.43/42.65 thf(219,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:product_prod_nat_nat]: ((isSimp1359852763pacity @ c @ A @ B @ C) => ((member701585322at_nat @ D @ (set_Pr2131844118at_nat @ B)) => (~ (member701585322at_nat @ (product_swap_nat_nat @ D) @ (set_Pr2131844118at_nat @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_isSPath__nt__parallel)).
% 99.43/42.65 thf(986,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:product_prod_nat_nat]: ((isSimp1359852763pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ D @ (set_Pr2131844118at_nat @ B)) => (~ (member701585322at_nat @ (product_swap_nat_nat @ D) @ (set_Pr2131844118at_nat @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 99.43/42.65 thf(14,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_order_Otrans)).
% 99.43/42.65 thf(306,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 99.43/42.65 thf(113,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => (connected_capacity @ c @ A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_isShortestPath__level__edge_I1_J)).
% 99.43/42.65 thf(653,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => (connected_capacity @ (c) @ A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 99.43/42.65 thf(94,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_prod_Oinject)).
% 99.43/42.65 thf(589,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((product_Pair_nat_nat @ A @ B) = (product_Pair_nat_nat @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 99.43/42.65 thf(12356,plain,(! [C:nat,B:nat,A:product_prod_nat_nat] : ((A != (product_Pair_nat_nat @ (sk3 @ ((=) @ nat)) @ B)) | ((product_Pair_nat_nat @ (sk26 @ A) @ (sk27 @ A)) != (product_Pair_nat_nat @ (sk2 @ ((=) @ nat)) @ C)))),inference(paramod_ordered,[status(thm)],[462,11927])).
% 99.43/42.65 thf(12360,plain,(! [B:nat,A:nat] : (((sk26 @ (product_Pair_nat_nat @ (sk3 @ ((=) @ nat)) @ A)) != (sk2 @ ((=) @ nat))) | ((sk27 @ (product_Pair_nat_nat @ (sk3 @ ((=) @ nat)) @ A)) != B))),inference(simp,[status(thm)],[12356])).
% 99.43/42.65 thf(12368,plain,(! [A:nat] : (((sk26 @ (product_Pair_nat_nat @ (sk3 @ ((=) @ nat)) @ A)) != (sk2 @ ((=) @ nat))))),inference(simp,[status(thm)],[12360])).
% 99.43/42.65 thf(116,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((connected_capacity @ A @ B @ C) => ((ord_less_eq_nat @ D @ (min_dist_capacity @ A @ B @ C)) => (? [E:nat]: ((connected_capacity @ A @ B @ E) & ((min_dist_capacity @ A @ B @ E) = D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_Graph_Omin__dist__le)).
% 99.43/42.65 thf(663,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((connected_capacity @ (A) @ B @ C) => ((ord_less_eq_nat @ D @ (min_dist_capacity @ (A) @ B @ C)) => (? [E:nat]: ((connected_capacity @ (A) @ B @ E) & ((min_dist_capacity @ (A) @ B @ E) = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 99.43/42.65 thf(36,axiom,((isSimp1359852763pacity = isSimp1359852763pacity)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_Graph_OisSimplePath_Ocong)).
% 99.43/42.65 thf(374,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 99.43/42.65 thf(71,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_order__refl)).
% 99.43/42.65 thf(487,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 99.43/42.65 thf(1018,plain,(! [A:(product_prod_nat_nat > capacity)] : (((connected_capacity @ A) = (^ [B:nat,C:nat]: ? [D:nat]: (dist_capacity @ A @ B @ D @ C))))),inference(func_ext,[status(esa)],[481])).
% 99.43/42.65 thf(30,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ E @ E) @ (set_Pr2131844118at_nat @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_Graph_OisSPath__no__selfloop)).
% 99.43/42.65 thf(355,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat]: ((isSimp1359852763pacity @ (A) @ B @ C @ D) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ E @ E) @ (set_Pr2131844118at_nat @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 99.43/42.65 thf(145,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_add__le__cancel__left)).
% 99.43/42.65 thf(754,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 99.43/42.65 thf(50,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => (isPath_capacity @ A @ B @ C @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_Graph_OshortestPath__is__path)).
% 99.43/42.65 thf(426,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => (isPath_capacity @ (A) @ B @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 99.43/42.65 thf(213,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) = ((isSimp1359852763pacity @ c @ A @ B @ C) & ((size_s1990949619at_nat @ B) = (min_dist_capacity @ c @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_isShortestPath__alt)).
% 99.43/42.65 thf(968,plain,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) = ((isSimp1359852763pacity @ (c) @ A @ B @ C) & ((size_s1990949619at_nat @ B) = (min_dist_capacity @ (c) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 99.43/42.65 thf(168,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:(nat > $o)]: ((connected_capacity @ A @ B @ C) => ((! [E:nat]: ((dist_capacity @ A @ B @ E @ C) => ((! [F:nat]: ((dist_capacity @ A @ B @ F @ C) => (ord_less_eq_nat @ E @ F))) => (D @ E)))) => (D @ (min_dist_capacity @ A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_Graph_Omin__distI2)).
% 99.43/42.65 thf(823,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:(nat > $o)]: ((connected_capacity @ (A) @ B @ C) => ((! [E:nat]: ((dist_capacity @ (A) @ B @ E @ C) => ((! [F:nat]: ((dist_capacity @ (A) @ B @ F @ C) => (ord_less_eq_nat @ E @ F))) => (D @ E)))) => (D @ (min_dist_capacity @ (A) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 99.43/42.65 thf(6232,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((member701585322at_nat @ (product_Pair_nat_nat @ v @ u) @ (set_Pr2131844118at_nat @ p3)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[934,491])).
% 99.43/42.65 thf(6472,plain,((member701585322at_nat @ (product_Pair_nat_nat @ v @ u) @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (set_Pr2131844118at_nat @ p3)))))),inference(pre_uni,[status(thm)],[6232:[bind(A, $thf(product_Pair_nat_nat @ v @ u)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p3))))]])).
% 99.43/42.65 thf(180,axiom,((isPath_capacity @ c @ s @ p3 @ t)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_assms_I3_J)).
% 99.43/42.65 thf(872,plain,((isPath_capacity @ (c) @ s @ p3 @ t)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 99.43/42.65 thf(130,axiom,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ c @ A @ B @ C) => ((! [D:nat]: ((dist_capacity @ c @ A @ D @ C) => (ord_less_eq_nat @ B @ D))) => ((min_dist_capacity @ c @ A @ C) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_min__distI__eq)).
% 99.43/42.65 thf(707,plain,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ (c) @ A @ B @ C) => ((! [D:nat]: ((dist_capacity @ (c) @ A @ D @ C) => (ord_less_eq_nat @ B @ D))) => ((min_dist_capacity @ (c) @ A @ C) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 99.43/42.65 thf(214,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_trans__less__add2)).
% 99.43/42.65 thf(971,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 99.43/42.65 thf(4448,plain,(! [B:nat,A:nat] : (~ (($true)) | ((ord_less_nat @ (plus_plus_nat @ A @ B) @ A) != (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat)))))),inference(paramod_ordered,[status(thm)],[4380,676])).
% 99.43/42.65 thf(4449,plain,(! [B:nat,A:nat] : (((ord_less_nat @ (plus_plus_nat @ A @ B) @ A) != (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat)))))),inference(simp,[status(thm)],[4448])).
% 99.43/42.65 thf(4460,plain,(! [B:nat,A:nat] : (((plus_plus_nat @ A @ B) != (sk2 @ ((=) @ nat))) | (A != (sk3 @ ((=) @ nat))))),inference(simp,[status(thm)],[4449])).
% 99.43/42.65 thf(4469,plain,(! [A:nat] : (((plus_plus_nat @ (sk3 @ ((=) @ nat)) @ A) != (sk2 @ ((=) @ nat))))),inference(simp,[status(thm)],[4460])).
% 99.43/42.65 thf(76,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_order__subst1)).
% 99.43/42.65 thf(502,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 99.43/42.65 thf(63,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat,G:nat]: ((isSimp1359852763pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((F != G) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ E @ G) @ (set_Pr2131844118at_nat @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_Graph_OisSPath__sg__outgoing)).
% 99.43/42.65 thf(463,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat,G:nat]: ((isSimp1359852763pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => ((~ (F = G)) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ E @ G) @ (set_Pr2131844118at_nat @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 99.43/42.65 thf(207,axiom,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ c @ A @ B @ C) => (connected_capacity @ c @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_connected__distI)).
% 99.43/42.65 thf(951,plain,((! [A:nat,B:nat,C:nat]: ((dist_capacity @ (c) @ A @ B @ C) => (connected_capacity @ (c) @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 99.43/42.65 thf(4351,plain,((p1 != p)),inference(simp,[status(thm)],[4348])).
% 99.43/42.65 thf(24,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_order__trans)).
% 99.43/42.65 thf(338,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 99.43/42.65 thf(97,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((dist_capacity @ A @ B @ C @ D) => ((! [E:nat]: ((dist_capacity @ A @ B @ E @ D) => (ord_less_eq_nat @ C @ E))) => ((min_dist_capacity @ A @ B @ D) = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_Graph_Omin__distI__eq)).
% 99.43/42.65 thf(600,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((dist_capacity @ (A) @ B @ C @ D) => ((! [E:nat]: ((dist_capacity @ (A) @ B @ E @ D) => (ord_less_eq_nat @ C @ E))) => ((min_dist_capacity @ (A) @ B @ D) = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 99.43/42.65 thf(41,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((dist_capacity @ A @ B @ C @ D) => (connected_capacity @ A @ B @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_Graph_Oconnected__distI)).
% 99.43/42.65 thf(386,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ((dist_capacity @ (A) @ B @ C @ D) => (connected_capacity @ (A) @ B @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 99.43/42.65 thf(182,axiom,((isPath_capacity @ c @ s @ p @ t)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_P)).
% 99.43/42.65 thf(876,plain,((isPath_capacity @ (c) @ s @ p @ t)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 99.43/42.65 thf(4670,plain,(! [B:nat,A:nat] : ((ord_less_eq_nat @ A @ (size_s1990949619at_nat @ p)) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ A @ B)))),inference(paramod_ordered,[status(thm)],[3324,714])).
% 99.43/42.65 thf(4671,plain,((ord_less_eq_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p))),inference(pattern_uni,[status(thm)],[4670:[bind(A, $thf(plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat)),bind(B, $thf(size_s1990949619at_nat @ p2))]])).
% 99.43/42.65 thf(58,axiom,((dist_capacity = dist_capacity)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_Graph_Odist_Ocong)).
% 99.43/42.65 thf(450,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 99.43/42.65 thf(216,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat]: ((isSimp1359852763pacity @ c @ A @ B @ C) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ D @ D) @ (set_Pr2131844118at_nat @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_isSPath__no__selfloop)).
% 99.43/42.65 thf(976,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat]: ((isSimp1359852763pacity @ (c) @ A @ B @ C) => (~ (member701585322at_nat @ (product_Pair_nat_nat @ D @ D) @ (set_Pr2131844118at_nat @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 99.43/42.65 thf(74,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_le__trans)).
% 99.43/42.65 thf(495,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 99.43/42.65 thf(10891,plain,(! [B:(product_prod_nat_nat > $o),A:product_prod_nat_nat] : ((member701585322at_nat @ A @ (collec7649004at_nat @ (B))) | ((B @ A) != (member701585322at_nat @ sk69 @ (collec7649004at_nat @ (^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (set_Pr2131844118at_nat @ p)))))))),inference(paramod_ordered,[status(thm)],[491,10837])).
% 99.43/42.65 thf(10905,plain,((member701585322at_nat @ sk69 @ (collec7649004at_nat @ (^ [A:product_prod_nat_nat]: (member701585322at_nat @ A @ (collec7649004at_nat @ (^ [B:product_prod_nat_nat]: (member701585322at_nat @ B @ (set_Pr2131844118at_nat @ p))))))))),inference(pre_uni,[status(thm)],[10891:[bind(A, $thf(sk69)),bind(B, $thf(^ [C:product_prod_nat_nat]: (member701585322at_nat @ C @ (collec7649004at_nat @ (^ [D:product_prod_nat_nat]: (member701585322at_nat @ D @ (set_Pr2131844118at_nat @ p)))))))]])).
% 99.43/42.65 thf(230,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ C @ A) @ (plus_plus_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_add__strict__left__mono)).
% 99.43/42.65 thf(1010,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ (plus_plus_nat @ C @ A) @ (plus_plus_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 99.43/42.65 thf(151,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat,F:nat]: ((dist_capacity @ A @ B @ C @ D) => ((dist_capacity @ A @ D @ E @ F) => (((min_dist_capacity @ A @ B @ F) = (plus_plus_nat @ C @ E)) => ((min_dist_capacity @ A @ D @ F) = E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_Graph_Omin__dist__split_I2_J)).
% 99.43/42.65 thf(771,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat,F:nat]: ((dist_capacity @ (A) @ B @ C @ D) => ((dist_capacity @ (A) @ D @ E @ F) => (((min_dist_capacity @ (A) @ B @ F) = (plus_plus_nat @ C @ E)) => ((min_dist_capacity @ (A) @ D @ F) = E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 99.43/42.65 thf(731,plain,(((dist_capacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat]: ? [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) & ((size_s1990949619at_nat @ E) = C))))),inference(lifteq,[status(thm)],[730])).
% 99.43/42.65 thf(1108,plain,(! [A:(product_prod_nat_nat > capacity)] : (((dist_capacity @ A) = (^ [B:nat,C:nat,D:nat]: ? [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) & ((size_s1990949619at_nat @ E) = C)))))),inference(func_ext,[status(esa)],[731])).
% 99.43/42.65 thf(4438,plain,(! [B:nat,A:nat] : (~ (($true)) | ((ord_less_nat @ (plus_plus_nat @ A @ B) @ B) != (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat)))))),inference(paramod_ordered,[status(thm)],[4380,805])).
% 99.43/42.65 thf(4439,plain,(! [B:nat,A:nat] : (((ord_less_nat @ (plus_plus_nat @ A @ B) @ B) != (ord_less_nat @ (sk2 @ ((=) @ nat)) @ (sk3 @ ((=) @ nat)))))),inference(simp,[status(thm)],[4438])).
% 99.43/42.65 thf(4459,plain,(! [B:nat,A:nat] : (((plus_plus_nat @ A @ B) != (sk2 @ ((=) @ nat))) | (B != (sk3 @ ((=) @ nat))))),inference(simp,[status(thm)],[4439])).
% 99.43/42.65 thf(4468,plain,(! [A:nat] : (((plus_plus_nat @ A @ (sk3 @ ((=) @ nat))) != (sk2 @ ((=) @ nat))))),inference(simp,[status(thm)],[4459])).
% 99.43/42.65 thf(29,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_eq__refl)).
% 99.43/42.65 thf(351,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 99.43/42.65 thf(106,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ? [C:nat]: (B = (plus_plus_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_le__iff__add)).
% 99.43/42.65 thf(632,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ? [C:nat]: (B = (plus_plus_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 99.43/42.65 thf(223,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_add__mono__thms__linordered__field_I5_J)).
% 99.43/42.65 thf(995,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 99.43/42.65 thf(88,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_le__cases)).
% 99.43/42.65 thf(549,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 99.43/42.65 thf(161,axiom,((! [A:nat,B:nat]: ((isPath_capacity @ c @ A @ nil_Pr1308055047at_nat @ B) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_isPath_Osimps_I1_J)).
% 99.43/42.65 thf(800,plain,((! [A:nat,B:nat]: ((isPath_capacity @ (c) @ A @ nil_Pr1308055047at_nat @ B) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 99.43/42.65 thf(194,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (C = D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_add__mono__thms__linordered__field_I1_J)).
% 99.43/42.65 thf(914,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_nat @ A @ B) & (C = D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 99.43/42.65 thf(234,plain,(! [B:(product_prod_nat_nat > $o),A:(product_prod_nat_nat > $o)] : ((~ ((A @ (sk1 @ (B) @ (A))) = (B @ (sk1 @ (B) @ (A))))) | ((collec7649004at_nat @ (A)) = (collec7649004at_nat @ (B))))),inference(cnf,[status(esa)],[233])).
% 99.43/42.65 thf(235,plain,(! [B:(product_prod_nat_nat > $o),A:(product_prod_nat_nat > $o)] : (((A @ (sk1 @ (B) @ (A))) != (B @ (sk1 @ (B) @ (A)))) | ((collec7649004at_nat @ (A)) = (collec7649004at_nat @ (B))))),inference(lifteq,[status(thm)],[234])).
% 99.43/42.65 thf(246,plain,(! [C:nat,B:nat,A:(nat > (nat > $o))] : ((~ (A @ (sk2 @ (A)) @ (sk3 @ (A)))) | (~ (A @ (sk4 @ (A)) @ (sk4 @ (A)))) | (A @ (sk6 @ (A)) @ (sk5 @ (A))) | (A @ B @ C))),inference(cnfConj,[status(thm)],[243])).
% 99.43/42.65 thf(4151,plain,(! [A:nat] : (~ (($true)) | ((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2))))),inference(paramod_ordered,[status(thm)],[682,3332])).
% 99.43/42.65 thf(4152,plain,(! [A:nat] : (((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ (size_s1990949619at_nat @ p) @ (size_s1990949619at_nat @ p2))))),inference(simp,[status(thm)],[4151])).
% 99.43/42.65 thf(4196,plain,(! [A:nat] : ((A != (size_s1990949619at_nat @ p)) | ((plus_plus_nat @ A @ one_one_nat) != (size_s1990949619at_nat @ p2)))),inference(simp,[status(thm)],[4152])).
% 99.43/42.65 thf(4214,plain,(((plus_plus_nat @ (size_s1990949619at_nat @ p) @ one_one_nat) != (size_s1990949619at_nat @ p2))),inference(simp,[status(thm)],[4196])).
% 99.43/42.65 thf(78,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_less__irrefl__nat)).
% 99.43/42.65 thf(510,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 99.43/42.65 thf(1114,plain,(((plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)) != (size_s1990949619at_nat @ p)) | ((min_dist_capacity @ (c) @ u @ t) != (min_dist_capacity @ (c) @ s @ t))),inference(paramod_ordered,[status(thm)],[787,232])).
% 99.43/42.65 thf(1117,plain,(((plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)) != (size_s1990949619at_nat @ p)) | ((c) != (c)) | (u != s) | (t != t)),inference(simp,[status(thm)],[1114])).
% 99.43/42.65 thf(1120,plain,(((plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)) != (size_s1990949619at_nat @ p)) | (u != s)),inference(simp,[status(thm)],[1117])).
% 99.43/42.65 thf(3325,plain,(((size_s1990949619at_nat @ p) != (size_s1990949619at_nat @ p)) | (u != s) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))),inference(paramod_ordered,[status(thm)],[3324,1120])).
% 99.43/42.65 thf(3326,plain,((u != s) | ((plus_plus_nat @ (plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) @ (size_s1990949619at_nat @ p2)) != (plus_plus_nat @ one_one_nat @ (size_s1990949619at_nat @ p2)))),inference(simp,[status(thm)],[3325])).
% 99.43/42.65 thf(3344,plain,((u != s) | ((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != one_one_nat) | ((size_s1990949619at_nat @ p2) != (size_s1990949619at_nat @ p2))),inference(simp,[status(thm)],[3326])).
% 99.43/42.65 thf(3351,plain,((u != s) | ((plus_plus_nat @ (size_s1990949619at_nat @ p1) @ one_one_nat) != one_one_nat)),inference(simp,[status(thm)],[3344])).
% 99.43/42.65 thf(40,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((isPath_capacity @ A @ B @ nil_Pr1308055047at_nat @ C) = (B = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_Graph_OisPath_Osimps_I1_J)).
% 99.43/42.65 thf(383,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat]: ((isPath_capacity @ (A) @ B @ nil_Pr1308055047at_nat @ C) = (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 99.43/42.65 thf(57,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_antisym)).
% 99.43/42.65 thf(447,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 99.43/42.65 thf(170,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_eq_nat @ A @ B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_add__mono__thms__linordered__field_I4_J)).
% 99.43/42.65 thf(833,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_eq_nat @ A @ B) & (ord_less_nat @ C @ D)) => (ord_less_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 99.43/42.65 thf(171,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_nat__add__left__cancel__le)).
% 99.43/42.65 thf(835,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 99.43/42.65 thf(267,plain,(! [B:nat,A:nat] : ((~ (A = A)) | (A = (sk7 @ B @ ((=) @ nat @ A))) | (A = (sk8 @ ((=) @ nat @ A))))),inference(replace_leibeq,[status(thm)],[263:[bind(A, $thf((=) @ nat @ B))]])).
% 99.43/42.65 thf(272,plain,(! [B:nat,A:nat] : ((A != A) | (A = (sk7 @ B @ ((=) @ nat @ A))) | (A = (sk8 @ ((=) @ nat @ A))))),inference(lifteq,[status(thm)],[267])).
% 99.43/42.65 thf(273,plain,(! [B:nat,A:nat] : ((A = (sk7 @ B @ ((=) @ nat @ A))) | (A = (sk8 @ ((=) @ nat @ A))))),inference(simp,[status(thm)],[272])).
% 99.43/42.65 thf(140,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_trans__less__add1)).
% 99.43/42.65 thf(735,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => (ord_less_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 99.43/42.65 thf(3234,plain,(! [C:nat,B:nat,A:nat] : (~ (($true)) | ((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ (plus_plus_nat @ B @ C) @ C)))),inference(paramod_ordered,[status(thm)],[682,805])).
% 99.43/42.65 thf(3235,plain,(! [C:nat,B:nat,A:nat] : (((ord_less_nat @ A @ (plus_plus_nat @ A @ one_one_nat)) != (ord_less_nat @ (plus_plus_nat @ B @ C) @ C)))),inference(simp,[status(thm)],[3234])).
% 99.43/42.65 thf(3282,plain,(! [C:nat,B:nat,A:nat] : ((A != (plus_plus_nat @ B @ C)) | ((plus_plus_nat @ A @ one_one_nat) != C))),inference(simp,[status(thm)],[3235])).
% 99.43/42.65 thf(3309,plain,(! [B:nat,A:nat] : (((plus_plus_nat @ (plus_plus_nat @ A @ B) @ one_one_nat) != B))),inference(simp,[status(thm)],[3282])).
% 99.43/42.65 thf(304,plain,(! [A:product_prod_nat_nat] : (((product_swap_nat_nat @ (product_swap_nat_nat @ A)) = A))),inference(cnf,[status(esa)],[303])).
% 99.43/42.65 thf(305,plain,(! [A:product_prod_nat_nat] : (((product_swap_nat_nat @ (product_swap_nat_nat @ A)) = A))),inference(lifteq,[status(thm)],[304])).
% 99.43/42.65 thf(195,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_eq_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_add__le__cancel__right)).
% 99.43/42.65 thf(918,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_eq_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 99.43/42.65 thf(31,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_order_Ostrict__implies__not__eq)).
% 99.43/42.65 thf(358,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 99.43/42.65 thf(1056,plain,(! [A:(product_prod_nat_nat > capacity)] : (((^ [B:nat,C:nat]: ? [D:nat]: (dist_capacity @ A @ B @ D @ C)) = (^ [B:nat,C:nat]: ? [D:list_P559422087at_nat]: (isPath_capacity @ A @ B @ D @ C))))),inference(func_ext,[status(esa)],[1022])).
% 99.43/42.65 thf(211,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ c @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((min_dist_capacity @ c @ A @ E) = (plus_plus_nat @ (min_dist_capacity @ c @ A @ D) @ one_one_nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_isShortestPath__level__edge_I4_J)).
% 99.43/42.65 thf(960,plain,((! [A:nat,B:list_P559422087at_nat,C:nat,D:nat,E:nat]: ((isShor1936442771pacity @ (c) @ A @ B @ C) => ((member701585322at_nat @ (product_Pair_nat_nat @ D @ E) @ (set_Pr2131844118at_nat @ B)) => ((min_dist_capacity @ (c) @ A @ E) = (plus_plus_nat @ (min_dist_capacity @ (c) @ A @ D) @ one_one_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 99.43/42.65 thf(134,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_add__right__mono)).
% 99.43/42.65 thf(720,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 99.43/42.65 thf(198,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_eq_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_add__leD1)).
% 99.43/42.65 thf(928,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_eq_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 99.43/42.65 thf(188,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat,F:nat]: ((dist_capacity @ A @ B @ C @ D) => ((dist_capacity @ A @ D @ E @ F) => (dist_capacity @ A @ B @ (plus_plus_nat @ C @ E) @ F))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_Graph_Odist__trans)).
% 99.43/42.65 thf(897,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:nat,D:nat,E:nat,F:nat]: ((dist_capacity @ (A) @ B @ C @ D) => ((dist_capacity @ (A) @ D @ E @ F) => (dist_capacity @ (A) @ B @ (plus_plus_nat @ C @ E) @ F))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 99.43/42.65 thf(66,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_order__class_Oorder_Oantisym)).
% 99.43/42.65 thf(474,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 99.43/42.65 thf(137,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_add__lessD1)).
% 99.43/42.65 thf(728,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 99.43/42.65 thf(22,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => (connected_capacity @ A @ E @ F))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_Graph_OisShortestPath__level__edge_I2_J)).
% 99.43/42.65 thf(332,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat,E:nat,F:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => ((member701585322at_nat @ (product_Pair_nat_nat @ E @ F) @ (set_Pr2131844118at_nat @ C)) => (connected_capacity @ (A) @ E @ F))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 99.43/42.65 thf(176,axiom,((! [A:nat,B:nat]: ((isSimp1359852763pacity @ c @ A @ nil_Pr1308055047at_nat @ B) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_simplePath__empty__conv)).
% 99.43/42.65 thf(860,plain,((! [A:nat,B:nat]: ((isSimp1359852763pacity @ (c) @ A @ nil_Pr1308055047at_nat @ B) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 99.43/42.65 thf(110,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_9_add__left__cancel)).
% 99.43/42.65 thf(644,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)],[110])).
% 99.43/42.65 thf(135,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_eq_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_add__leD2)).
% 99.43/42.65 thf(723,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ C) => (ord_less_eq_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 99.43/42.65 thf(218,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_eq_nat @ A @ B) & (C = D)) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_add__mono__thms__linordered__semiring_I3_J)).
% 99.43/42.65 thf(982,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((ord_less_eq_nat @ A @ B) & (C = D)) => (ord_less_eq_nat @ (plus_plus_nat @ A @ C) @ (plus_plus_nat @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 99.43/42.65 thf(55,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isShor1936442771pacity @ A @ B @ C @ D) => (isSimp1359852763pacity @ A @ B @ C @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_Graph_OshortestPath__is__simple)).
% 99.43/42.65 thf(442,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isShor1936442771pacity @ (A) @ B @ C @ D) => (isSimp1359852763pacity @ (A) @ B @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 99.43/42.65 thf(95,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (ord_less_nat @ (A @ D) @ (A @ E)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ (A @ B) @ (A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_less__mono__imp__le__mono)).
% 99.43/42.65 thf(592,plain,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (ord_less_nat @ (A @ D) @ (A @ E)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ (A @ B) @ (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 99.43/42.65 thf(688,plain,(((isShor1936442771pacity) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ! [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) => (ord_less_eq_nat @ (size_s1990949619at_nat @ C) @ (size_s1990949619at_nat @ E))))))),inference(lifteq,[status(thm)],[687])).
% 99.43/42.65 thf(1653,plain,(((^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ((size_s1990949619at_nat @ C) = (min_dist_capacity @ A @ B @ D)))) = (^ [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) & ! [E:list_P559422087at_nat]: ((isPath_capacity @ A @ B @ E @ D) => (ord_less_eq_nat @ (size_s1990949619at_nat @ C) @ (size_s1990949619at_nat @ E))))))),inference(rewrite,[status(thm)],[688,631])).
% 99.43/42.65 thf(65,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_order__subst2)).
% 99.43/42.65 thf(469,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 99.43/42.65 thf(203,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) => (ord_less_eq_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_add__le__imp__le__right)).
% 99.43/42.65 thf(940,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) => (ord_less_eq_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 99.43/42.65 thf(201,axiom,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isPath_capacity @ c @ A @ B @ C) => (dist_capacity @ c @ A @ (size_s1990949619at_nat @ B) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_isPath__distD)).
% 99.43/42.65 thf(935,plain,((! [A:nat,B:list_P559422087at_nat,C:nat]: ((isPath_capacity @ (c) @ A @ B @ C) => (dist_capacity @ (c) @ A @ (size_s1990949619at_nat @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 99.43/42.65 thf(229,axiom,((isShor1936442771pacity @ c @ s @ p @ t)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_assms_I1_J)).
% 99.43/42.65 thf(1009,plain,((isShor1936442771pacity @ (c) @ s @ p @ t)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 99.43/42.65 thf(1037,plain,(! [A:nat] : (((ord_less_eq_nat @ A) = (^ [B:nat]: ((ord_less_nat @ A @ B) | (A = B)))))),inference(func_ext,[status(esa)],[344])).
% 99.43/42.65 thf(152,axiom,((ord_less_nat = (^ [A:nat]: (ord_less_eq_nat @ (plus_plus_nat @ A @ one_one_nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_discrete)).
% 99.43/42.65 thf(775,plain,(((ord_less_nat) = (^ [A:nat]: (ord_less_eq_nat @ (plus_plus_nat @ A @ one_one_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 99.43/42.65 thf(90,axiom,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ A @ B @ C @ D) => (? [E:list_P559422087at_nat]: (isSimp1359852763pacity @ A @ B @ E @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_Graph_OisSPath__pathLE)).
% 99.43/42.65 thf(560,plain,((! [A:(product_prod_nat_nat > capacity),B:nat,C:list_P559422087at_nat,D:nat]: ((isPath_capacity @ (A) @ B @ C @ D) => (? [E:list_P559422087at_nat]: (isSimp1359852763pacity @ (A) @ B @ E @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 99.43/42.65 thf(14121,plain,(($false)),inference(e,[status(thm)],[365,760,479,347,893,518,777,481,909,628,1031,762,683,12299,994,741,10837,873,247,379,677,730,276,1305,597,3332,797,715,12522,538,930,814,1327,1001,417,301,4467,885,12303,4348,3342,6878,838,934,949,421,606,1013,289,492,789,321,1334,485,238,937,7739,806,480,687,280,634,877,866,6932,428,265,507,1072,453,527,312,233,380,529,793,925,810,9588,366,714,292,6856,942,439,957,746,260,815,693,630,275,788,467,625,435,329,4553,522,757,682,551,4461,456,847,484,9658,879,324,974,697,650,1328,725,403,388,869,783,989,857,1006,8884,328,1082,669,637,489,679,547,706,4530,12410,738,1668,1002,9607,11927,371,647,997,1333,244,266,805,921,541,657,765,10819,398,674,953,586,718,343,237,906,750,618,264,689,444,375,513,4380,732,6881,12301,286,577,958,7709,819,562,904,641,391,313,787,3340,335,236,10857,713,498,6757,947,979,831,681,12297,318,880,303,271,863,900,5143,362,451,245,9570,477,631,345,799,621,700,1029,964,626,1022,462,4462,609,10219,240,912,399,768,1044,780,1015,1000,851,438,658,394,986,306,241,653,589,12368,663,374,487,516,1018,355,754,426,7896,968,823,6472,872,705,707,971,327,4469,263,993,673,502,9567,463,951,7737,4351,338,656,600,386,876,4671,991,231,450,482,671,976,495,10905,1010,771,1108,813,517,4468,351,632,995,731,786,3324,11785,2120,549,800,290,914,378,235,246,4214,510,3351,383,447,6439,833,835,7787,3337,273,735,3309,305,918,341,358,1056,960,720,928,897,474,624,728,332,860,644,459,723,982,442,1120,803,309,676,491,2191,592,232,6933,1653,469,940,935,8991,1009,1037,775,560])).
% 99.43/42.65 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 99.43/42.65 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------