%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ANA019-2 : TPTP v9.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 04:59:11 AM UTC 2025
% Result : Unsatisfiable 0.19s 0.39s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ANA019-2 : TPTP v9.0.0. Released v3.2.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 11:20:33 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.39 % SZS status Unsatisfiable
% 0.19/0.39 % SZS output start Proof
% 0.19/0.39 tff(c_lessequals_type, type, (
% 0.19/0.39 c_lessequals: ( $i * $i * $i ) > $o)).
% 0.19/0.39 tff(t_a_type, type, (
% 0.19/0.39 t_a: $i)).
% 0.19/0.39 tff(c_times_type, type, (
% 0.19/0.39 c_times: ( $i * $i * $i ) > $i)).
% 0.19/0.39 tff(c_HOL_Oabs_type, type, (
% 0.19/0.39 c_HOL_Oabs: ( $i * $i ) > $i)).
% 0.19/0.39 tff(v_h_type, type, (
% 0.19/0.39 v_h: $i > $i)).
% 0.19/0.39 tff(c_Suc_type, type, (
% 0.19/0.39 c_Suc: $i > $i)).
% 0.19/0.39 tff(c_minus_type, type, (
% 0.19/0.39 c_minus: ( $i * $i * $i ) > $i)).
% 0.19/0.39 tff(tc_nat_type, type, (
% 0.19/0.39 tc_nat: $i)).
% 0.19/0.39 tff(c_1_type, type, (
% 0.19/0.39 c_1: $i)).
% 0.19/0.39 tff(v_xa_type, type, (
% 0.19/0.39 v_xa: $i > $i)).
% 0.19/0.39 tff(v_x_type, type, (
% 0.19/0.39 v_x: $i)).
% 0.19/0.39 tff(v_f_type, type, (
% 0.19/0.39 v_f: $i > $i)).
% 0.19/0.39 tff(c_less_type, type, (
% 0.19/0.39 c_less: ( $i * $i * $i ) > $o)).
% 0.19/0.39 tff(c_0_type, type, (
% 0.19/0.39 c_0: $i)).
% 0.19/0.39 tff(class_OrderedGroup_Olordered__ab__group__abs_type, type, (
% 0.19/0.39 class_OrderedGroup_Olordered__ab__group__abs: $i > $o)).
% 0.19/0.39 tff(class_Ring__and__Field_Oordered__idom_type, type, (
% 0.19/0.39 class_Ring__and__Field_Oordered__idom: $i > $o)).
% 0.19/0.39 tff(class_Orderings_Oorder_type, type, (
% 0.19/0.39 class_Orderings_Oorder: $i > $o)).
% 0.19/0.39 tff(class_LOrder_Ojoin__semilorder_type, type, (
% 0.19/0.39 class_LOrder_Ojoin__semilorder: $i > $o)).
% 0.19/0.39 tff(class_Ring__and__Field_Opordered__cancel__semiring_type, type, (
% 0.19/0.39 class_Ring__and__Field_Opordered__cancel__semiring: $i > $o)).
% 0.19/0.39 tff(1,plain,
% 0.19/0.39 (^[T: $i] : refl((class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T))) <=> (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T))))),
% 0.19/0.39 inference(bind,[status(th)],[])).
% 0.19/0.39 tff(2,plain,
% 0.19/0.39 (![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T))) <=> ![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.39 inference(quant_intro,[status(thm)],[1])).
% 0.19/0.39 tff(3,plain,
% 0.19/0.39 (![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T))) <=> ![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(4,plain,
% 0.19/0.39 (^[T: $i] : rewrite(((~class_Ring__and__Field_Oordered__idom(T)) | class_OrderedGroup_Olordered__ab__group__abs(T)) <=> (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T))))),
% 0.19/0.39 inference(bind,[status(th)],[])).
% 0.19/0.39 tff(5,plain,
% 0.19/0.39 (![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_OrderedGroup_Olordered__ab__group__abs(T)) <=> ![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.39 inference(quant_intro,[status(thm)],[4])).
% 0.19/0.39 tff(6,axiom,(![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_OrderedGroup_Olordered__ab__group__abs(T))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','clsrel_Ring__and__Field_Oordered__idom_50')).
% 0.19/0.39 tff(7,plain,
% 0.19/0.39 (![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.19/0.39 tff(8,plain,
% 0.19/0.39 (![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.19/0.39 tff(9,plain,(
% 0.19/0.39 ![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.39 inference(skolemize,[status(sab)],[8])).
% 0.19/0.39 tff(10,plain,
% 0.19/0.39 (![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.19/0.39 tff(11,plain,
% 0.19/0.39 (class_Ring__and__Field_Oordered__idom(t_a) <=> class_Ring__and__Field_Oordered__idom(t_a)),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(12,axiom,(class_Ring__and__Field_Oordered__idom(t_a)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','tfree_tcs')).
% 0.19/0.39 tff(13,plain,
% 0.19/0.39 (class_Ring__and__Field_Oordered__idom(t_a)),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.19/0.39 tff(14,plain,
% 0.19/0.39 (((~![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | (class_OrderedGroup_Olordered__ab__group__abs(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a)))) <=> ((~![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | class_OrderedGroup_Olordered__ab__group__abs(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(15,plain,
% 0.19/0.40 ((~![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | (class_OrderedGroup_Olordered__ab__group__abs(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a)))),
% 0.19/0.40 inference(quant_inst,[status(thm)],[])).
% 0.19/0.40 tff(16,plain,
% 0.19/0.40 ((~![T: $i] : (class_OrderedGroup_Olordered__ab__group__abs(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | class_OrderedGroup_Olordered__ab__group__abs(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.19/0.40 tff(17,plain,
% 0.19/0.40 (class_OrderedGroup_Olordered__ab__group__abs(t_a)),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[16, 13, 10])).
% 0.19/0.40 tff(18,plain,
% 0.19/0.40 (^[T_a: $i] : refl(((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0)) <=> ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0)))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(19,plain,
% 0.19/0.40 (![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0)) <=> ![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[18])).
% 0.19/0.40 tff(20,plain,
% 0.19/0.40 (![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0)) <=> ![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(21,axiom,(![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_OrderedGroup_Oabs__eq__0_1')).
% 0.19/0.40 tff(22,plain,
% 0.19/0.40 (![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.19/0.40 tff(23,plain,(
% 0.19/0.40 ![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))),
% 0.19/0.40 inference(skolemize,[status(sab)],[22])).
% 0.19/0.40 tff(24,plain,
% 0.19/0.40 (![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[23, 19])).
% 0.19/0.40 tff(25,plain,
% 0.19/0.40 (((~![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))) | ((~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | (c_HOL_Oabs(c_0, t_a) = c_0))) <=> ((~![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))) | (~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | (c_HOL_Oabs(c_0, t_a) = c_0))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(26,plain,
% 0.19/0.40 ((~![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))) | ((~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | (c_HOL_Oabs(c_0, t_a) = c_0))),
% 0.19/0.40 inference(quant_inst,[status(thm)],[])).
% 0.19/0.40 tff(27,plain,
% 0.19/0.40 ((~![T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | (c_HOL_Oabs(c_0, T_a) = c_0))) | (~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | (c_HOL_Oabs(c_0, t_a) = c_0)),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.19/0.40 tff(28,plain,
% 0.19/0.40 (c_HOL_Oabs(c_0, t_a) = c_0),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[27, 24, 17])).
% 0.19/0.40 tff(29,plain,
% 0.19/0.40 ((v_f(c_0) = c_0) <=> (v_f(c_0) = c_0)),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(30,axiom,(v_f(c_0) = c_0), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_conjecture_0')).
% 0.19/0.40 tff(31,plain,
% 0.19/0.40 (v_f(c_0) = c_0),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[30, 29])).
% 0.19/0.40 tff(32,assumption,(v_xa(v_x) = c_0), introduced(assumption)).
% 0.19/0.40 tff(33,plain,
% 0.19/0.40 (v_f(v_xa(v_x)) = v_f(c_0)),
% 0.19/0.40 inference(monotonicity,[status(thm)],[32])).
% 0.19/0.40 tff(34,plain,
% 0.19/0.40 (v_f(v_xa(v_x)) = c_0),
% 0.19/0.40 inference(transitivity,[status(thm)],[33, 31])).
% 0.19/0.40 tff(35,plain,
% 0.19/0.40 (c_HOL_Oabs(v_f(v_xa(v_x)), t_a) = c_HOL_Oabs(c_0, t_a)),
% 0.19/0.40 inference(monotonicity,[status(thm)],[34])).
% 0.19/0.40 tff(36,plain,
% 0.19/0.40 (c_HOL_Oabs(v_f(v_xa(v_x)), t_a) = c_0),
% 0.19/0.40 inference(transitivity,[status(thm)],[35, 28])).
% 0.19/0.40 tff(37,assumption,(c_HOL_Oabs(v_f(v_xa(v_x)), t_a) = c_0), introduced(assumption)).
% 0.19/0.40 tff(38,plain,
% 0.19/0.40 (c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) <=> c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)),
% 0.19/0.40 inference(monotonicity,[status(thm)],[37])).
% 0.19/0.40 tff(39,plain,
% 0.19/0.40 (c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) <=> c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)),
% 0.19/0.40 inference(symmetry,[status(thm)],[38])).
% 0.19/0.40 tff(40,plain,
% 0.19/0.40 (^[V_a: $i, T_a: $i] : refl(((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a)) <=> ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a)))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(41,plain,
% 0.19/0.40 (![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a)) <=> ![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[40])).
% 0.19/0.40 tff(42,plain,
% 0.19/0.40 (![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a)) <=> ![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(43,axiom,(![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_OrderedGroup_Oabs__ge__zero_0')).
% 0.19/0.40 tff(44,plain,
% 0.19/0.40 (![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.19/0.40 tff(45,plain,(
% 0.19/0.40 ![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))),
% 0.19/0.40 inference(skolemize,[status(sab)],[44])).
% 0.19/0.40 tff(46,plain,
% 0.19/0.40 (![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[45, 41])).
% 0.19/0.40 tff(47,plain,
% 0.19/0.40 (((~![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))) | ((~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a))) <=> ((~![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))) | (~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(48,plain,
% 0.19/0.40 ((~![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))) | ((~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a))),
% 0.19/0.40 inference(quant_inst,[status(thm)],[])).
% 0.19/0.40 tff(49,plain,
% 0.19/0.40 ((~![V_a: $i, T_a: $i] : ((~class_OrderedGroup_Olordered__ab__group__abs(T_a)) | c_lessequals(c_0, c_HOL_Oabs(V_a, T_a), T_a))) | (~class_OrderedGroup_Olordered__ab__group__abs(t_a)) | c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a)),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.19/0.40 tff(50,plain,
% 0.19/0.40 (c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a)),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[49, 46, 17])).
% 0.19/0.40 tff(51,plain,
% 0.19/0.40 (^[T: $i] : refl((class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T))) <=> (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T))))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(52,plain,
% 0.19/0.40 (![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T))) <=> ![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[51])).
% 0.19/0.40 tff(53,plain,
% 0.19/0.40 (![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T))) <=> ![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(54,plain,
% 0.19/0.40 (^[T: $i] : rewrite(((~class_Ring__and__Field_Oordered__idom(T)) | class_LOrder_Ojoin__semilorder(T)) <=> (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T))))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(55,plain,
% 0.19/0.40 (![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_LOrder_Ojoin__semilorder(T)) <=> ![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[54])).
% 0.19/0.40 tff(56,axiom,(![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_LOrder_Ojoin__semilorder(T))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','clsrel_Ring__and__Field_Oordered__idom_35')).
% 0.19/0.40 tff(57,plain,
% 0.19/0.40 (![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[56, 55])).
% 0.19/0.40 tff(58,plain,
% 0.19/0.40 (![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[57, 53])).
% 0.19/0.40 tff(59,plain,(
% 0.19/0.40 ![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.40 inference(skolemize,[status(sab)],[58])).
% 0.19/0.40 tff(60,plain,
% 0.19/0.40 (![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[59, 52])).
% 0.19/0.40 tff(61,plain,
% 0.19/0.40 (((~![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | (class_LOrder_Ojoin__semilorder(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a)))) <=> ((~![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | class_LOrder_Ojoin__semilorder(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(62,plain,
% 0.19/0.40 ((~![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | (class_LOrder_Ojoin__semilorder(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a)))),
% 0.19/0.40 inference(quant_inst,[status(thm)],[])).
% 0.19/0.40 tff(63,plain,
% 0.19/0.40 ((~![T: $i] : (class_LOrder_Ojoin__semilorder(T) | (~class_Ring__and__Field_Oordered__idom(T)))) | class_LOrder_Ojoin__semilorder(t_a) | (~class_Ring__and__Field_Oordered__idom(t_a))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[62, 61])).
% 0.19/0.40 tff(64,plain,
% 0.19/0.40 (class_LOrder_Ojoin__semilorder(t_a)),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[63, 13, 60])).
% 0.19/0.40 tff(65,plain,
% 0.19/0.40 (^[T: $i] : refl((class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T))) <=> (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T))))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(66,plain,
% 0.19/0.40 (![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T))) <=> ![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[65])).
% 0.19/0.40 tff(67,plain,
% 0.19/0.40 (![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T))) <=> ![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(68,plain,
% 0.19/0.40 (^[T: $i] : rewrite(((~class_LOrder_Ojoin__semilorder(T)) | class_Orderings_Oorder(T)) <=> (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T))))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(69,plain,
% 0.19/0.40 (![T: $i] : ((~class_LOrder_Ojoin__semilorder(T)) | class_Orderings_Oorder(T)) <=> ![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[68])).
% 0.19/0.40 tff(70,axiom,(![T: $i] : ((~class_LOrder_Ojoin__semilorder(T)) | class_Orderings_Oorder(T))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','clsrel_LOrder_Ojoin__semilorder_1')).
% 0.19/0.40 tff(71,plain,
% 0.19/0.40 (![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[70, 69])).
% 0.19/0.40 tff(72,plain,
% 0.19/0.40 (![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[71, 67])).
% 0.19/0.40 tff(73,plain,(
% 0.19/0.40 ![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))),
% 0.19/0.40 inference(skolemize,[status(sab)],[72])).
% 0.19/0.40 tff(74,plain,
% 0.19/0.40 (![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[73, 66])).
% 0.19/0.40 tff(75,plain,
% 0.19/0.40 (((~![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))) | (class_Orderings_Oorder(t_a) | (~class_LOrder_Ojoin__semilorder(t_a)))) <=> ((~![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))) | class_Orderings_Oorder(t_a) | (~class_LOrder_Ojoin__semilorder(t_a)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(76,plain,
% 0.19/0.40 ((~![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))) | (class_Orderings_Oorder(t_a) | (~class_LOrder_Ojoin__semilorder(t_a)))),
% 0.19/0.40 inference(quant_inst,[status(thm)],[])).
% 0.19/0.40 tff(77,plain,
% 0.19/0.40 ((~![T: $i] : (class_Orderings_Oorder(T) | (~class_LOrder_Ojoin__semilorder(T)))) | class_Orderings_Oorder(t_a) | (~class_LOrder_Ojoin__semilorder(t_a))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[76, 75])).
% 0.19/0.40 tff(78,plain,
% 0.19/0.40 (class_Orderings_Oorder(t_a)),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[77, 74, 64])).
% 0.19/0.40 tff(79,plain,
% 0.19/0.40 (^[V_x: $i, T_a: $i, V_y: $i] : refl((c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a))) <=> (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a))))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(80,plain,
% 0.19/0.40 (![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a))) <=> ![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[79])).
% 0.19/0.40 tff(81,plain,
% 0.19/0.40 (![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a))) <=> ![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(82,plain,
% 0.19/0.40 (^[V_x: $i, T_a: $i, V_y: $i] : rewrite((((~class_Orderings_Oorder(T_a)) | (~c_less(V_x, V_y, T_a))) | c_lessequals(V_x, V_y, T_a)) <=> (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a))))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(83,plain,
% 0.19/0.40 (![V_x: $i, T_a: $i, V_y: $i] : (((~class_Orderings_Oorder(T_a)) | (~c_less(V_x, V_y, T_a))) | c_lessequals(V_x, V_y, T_a)) <=> ![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[82])).
% 0.19/0.40 tff(84,axiom,(![V_x: $i, T_a: $i, V_y: $i] : (((~class_Orderings_Oorder(T_a)) | (~c_less(V_x, V_y, T_a))) | c_lessequals(V_x, V_y, T_a))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_Orderings_Oorder__less__imp__le_0')).
% 0.19/0.40 tff(85,plain,
% 0.19/0.40 (![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.19/0.40 tff(86,plain,
% 0.19/0.40 (![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[85, 81])).
% 0.19/0.40 tff(87,plain,(
% 0.19/0.40 ![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))),
% 0.19/0.40 inference(skolemize,[status(sab)],[86])).
% 0.19/0.40 tff(88,plain,
% 0.19/0.40 (![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[87, 80])).
% 0.19/0.40 tff(89,plain,
% 0.19/0.40 (c_less(c_0, v_x, t_a) <=> c_less(c_0, v_x, t_a)),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(90,axiom,(c_less(c_0, v_x, t_a)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_conjecture_1')).
% 0.19/0.40 tff(91,plain,
% 0.19/0.40 (c_less(c_0, v_x, t_a)),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[90, 89])).
% 0.19/0.40 tff(92,plain,
% 0.19/0.40 (((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | ((~c_less(c_0, v_x, t_a)) | c_lessequals(c_0, v_x, t_a) | (~class_Orderings_Oorder(t_a)))) <=> ((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | (~c_less(c_0, v_x, t_a)) | c_lessequals(c_0, v_x, t_a) | (~class_Orderings_Oorder(t_a)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(93,plain,
% 0.19/0.40 ((c_lessequals(c_0, v_x, t_a) | (~c_less(c_0, v_x, t_a)) | (~class_Orderings_Oorder(t_a))) <=> ((~c_less(c_0, v_x, t_a)) | c_lessequals(c_0, v_x, t_a) | (~class_Orderings_Oorder(t_a)))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(94,plain,
% 0.19/0.40 (((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | (c_lessequals(c_0, v_x, t_a) | (~c_less(c_0, v_x, t_a)) | (~class_Orderings_Oorder(t_a)))) <=> ((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | ((~c_less(c_0, v_x, t_a)) | c_lessequals(c_0, v_x, t_a) | (~class_Orderings_Oorder(t_a))))),
% 0.19/0.40 inference(monotonicity,[status(thm)],[93])).
% 0.19/0.40 tff(95,plain,
% 0.19/0.40 (((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | (c_lessequals(c_0, v_x, t_a) | (~c_less(c_0, v_x, t_a)) | (~class_Orderings_Oorder(t_a)))) <=> ((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | (~c_less(c_0, v_x, t_a)) | c_lessequals(c_0, v_x, t_a) | (~class_Orderings_Oorder(t_a)))),
% 0.19/0.40 inference(transitivity,[status(thm)],[94, 92])).
% 0.19/0.40 tff(96,plain,
% 0.19/0.40 ((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | (c_lessequals(c_0, v_x, t_a) | (~c_less(c_0, v_x, t_a)) | (~class_Orderings_Oorder(t_a)))),
% 0.19/0.40 inference(quant_inst,[status(thm)],[])).
% 0.19/0.40 tff(97,plain,
% 0.19/0.40 ((~![V_x: $i, T_a: $i, V_y: $i] : (c_lessequals(V_x, V_y, T_a) | (~c_less(V_x, V_y, T_a)) | (~class_Orderings_Oorder(T_a)))) | (~c_less(c_0, v_x, t_a)) | c_lessequals(c_0, v_x, t_a) | (~class_Orderings_Oorder(t_a))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.19/0.40 tff(98,plain,
% 0.19/0.40 (c_lessequals(c_0, v_x, t_a) | (~class_Orderings_Oorder(t_a))),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[97, 91, 88])).
% 0.19/0.40 tff(99,plain,
% 0.19/0.40 (c_lessequals(c_0, v_x, t_a)),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[98, 78])).
% 0.19/0.40 tff(100,plain,
% 0.19/0.40 (^[T: $i] : refl(((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T)) <=> ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T)))),
% 0.19/0.40 inference(bind,[status(th)],[])).
% 0.19/0.40 tff(101,plain,
% 0.19/0.40 (![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T)) <=> ![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))),
% 0.19/0.40 inference(quant_intro,[status(thm)],[100])).
% 0.19/0.40 tff(102,plain,
% 0.19/0.40 (![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T)) <=> ![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(103,axiom,(![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','clsrel_Ring__and__Field_Oordered__idom_40')).
% 0.19/0.41 tff(104,plain,
% 0.19/0.41 (![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.19/0.41 tff(105,plain,(
% 0.19/0.41 ![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))),
% 0.19/0.41 inference(skolemize,[status(sab)],[104])).
% 0.19/0.41 tff(106,plain,
% 0.19/0.41 (![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[105, 101])).
% 0.19/0.41 tff(107,plain,
% 0.19/0.41 (((~![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))) | ((~class_Ring__and__Field_Oordered__idom(t_a)) | class_Ring__and__Field_Opordered__cancel__semiring(t_a))) <=> ((~![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))) | (~class_Ring__and__Field_Oordered__idom(t_a)) | class_Ring__and__Field_Opordered__cancel__semiring(t_a))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(108,plain,
% 0.19/0.41 ((~![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))) | ((~class_Ring__and__Field_Oordered__idom(t_a)) | class_Ring__and__Field_Opordered__cancel__semiring(t_a))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(109,plain,
% 0.19/0.41 ((~![T: $i] : ((~class_Ring__and__Field_Oordered__idom(T)) | class_Ring__and__Field_Opordered__cancel__semiring(T))) | (~class_Ring__and__Field_Oordered__idom(t_a)) | class_Ring__and__Field_Opordered__cancel__semiring(t_a)),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[108, 107])).
% 0.19/0.41 tff(110,plain,
% 0.19/0.41 (class_Ring__and__Field_Opordered__cancel__semiring(t_a)),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[109, 13, 106])).
% 0.19/0.41 tff(111,plain,
% 0.19/0.41 (^[V_b: $i, V_a: $i, T_a: $i] : refl((c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a))) <=> (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a))))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(112,plain,
% 0.19/0.41 (![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a))) <=> ![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[111])).
% 0.19/0.41 tff(113,plain,
% 0.19/0.41 (![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a))) <=> ![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(114,plain,
% 0.19/0.41 (^[V_b: $i, V_a: $i, T_a: $i] : trans(monotonicity(rewrite((((~class_Ring__and__Field_Opordered__cancel__semiring(T_a)) | (~c_lessequals(c_0, V_b, T_a))) | (~c_lessequals(c_0, V_a, T_a))) <=> ((~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))), (((((~class_Ring__and__Field_Opordered__cancel__semiring(T_a)) | (~c_lessequals(c_0, V_b, T_a))) | (~c_lessequals(c_0, V_a, T_a))) | c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a)) <=> (((~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a))) | c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a)))), rewrite((((~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a))) | c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a)) <=> (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))), (((((~class_Ring__and__Field_Opordered__cancel__semiring(T_a)) | (~c_lessequals(c_0, V_b, T_a))) | (~c_lessequals(c_0, V_a, T_a))) | c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a)) <=> (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(115,plain,
% 0.19/0.41 (![V_b: $i, V_a: $i, T_a: $i] : ((((~class_Ring__and__Field_Opordered__cancel__semiring(T_a)) | (~c_lessequals(c_0, V_b, T_a))) | (~c_lessequals(c_0, V_a, T_a))) | c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a)) <=> ![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[114])).
% 0.19/0.41 tff(116,axiom,(![V_b: $i, V_a: $i, T_a: $i] : ((((~class_Ring__and__Field_Opordered__cancel__semiring(T_a)) | (~c_lessequals(c_0, V_b, T_a))) | (~c_lessequals(c_0, V_a, T_a))) | c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_Ring__and__Field_Omult__nonneg__nonneg_0')).
% 0.19/0.41 tff(117,plain,
% 0.19/0.41 (![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[116, 115])).
% 0.19/0.41 tff(118,plain,
% 0.19/0.41 (![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[117, 113])).
% 0.19/0.41 tff(119,plain,(
% 0.19/0.41 ![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))),
% 0.19/0.41 inference(skolemize,[status(sab)],[118])).
% 0.19/0.41 tff(120,plain,
% 0.19/0.41 (![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[119, 112])).
% 0.19/0.41 tff(121,plain,
% 0.19/0.41 (((~![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))) | (c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) | (~c_lessequals(c_0, v_x, t_a)) | (~c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(t_a)))) <=> ((~![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))) | c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) | (~c_lessequals(c_0, v_x, t_a)) | (~c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(t_a)))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(122,plain,
% 0.19/0.41 ((~![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))) | (c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) | (~c_lessequals(c_0, v_x, t_a)) | (~c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(t_a)))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(123,plain,
% 0.19/0.41 ((~![V_b: $i, V_a: $i, T_a: $i] : (c_lessequals(c_0, c_times(V_a, V_b, T_a), T_a) | (~c_lessequals(c_0, V_a, T_a)) | (~c_lessequals(c_0, V_b, T_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(T_a)))) | c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) | (~c_lessequals(c_0, v_x, t_a)) | (~c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a)) | (~class_Ring__and__Field_Opordered__cancel__semiring(t_a))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.19/0.41 tff(124,plain,
% 0.19/0.41 (c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) | (~c_lessequals(c_0, v_x, t_a)) | (~c_lessequals(c_0, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[123, 120, 110])).
% 0.19/0.41 tff(125,plain,
% 0.19/0.41 (c_lessequals(c_0, c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[124, 99, 50])).
% 0.19/0.41 tff(126,plain,
% 0.19/0.41 (c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[125, 39])).
% 0.19/0.41 tff(127,plain,
% 0.19/0.41 (^[V_U: $i] : refl(((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a))) <=> ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a))))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(128,plain,
% 0.19/0.41 (![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a))) <=> ![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[127])).
% 0.19/0.41 tff(129,plain,
% 0.19/0.41 (![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a))) <=> ![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(130,plain,
% 0.19/0.41 (^[V_U: $i] : rewrite(((~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)) | (~c_less(c_0, V_U, t_a))) <=> ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a))))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(131,plain,
% 0.19/0.41 (![V_U: $i] : ((~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)) | (~c_less(c_0, V_U, t_a))) <=> ![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[130])).
% 0.19/0.41 tff(132,axiom,(![V_U: $i] : ((~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)) | (~c_less(c_0, V_U, t_a)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_conjecture_3')).
% 0.19/0.41 tff(133,plain,
% 0.19/0.41 (![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.19/0.41 tff(134,plain,
% 0.19/0.41 (![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[133, 129])).
% 0.19/0.41 tff(135,plain,(
% 0.19/0.41 ![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(skolemize,[status(sab)],[134])).
% 0.19/0.41 tff(136,plain,
% 0.19/0.41 (![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[135, 128])).
% 0.19/0.41 tff(137,plain,
% 0.19/0.41 (((~![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))) | ((~c_less(c_0, v_x, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)))) <=> ((~![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))) | (~c_less(c_0, v_x, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(138,plain,
% 0.19/0.41 ((~![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))) | ((~c_less(c_0, v_x, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.41 tff(139,plain,
% 0.19/0.41 ((~![V_U: $i] : ((~c_less(c_0, V_U, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(V_U)), t_a), c_times(V_U, c_HOL_Oabs(v_h(v_xa(V_U)), t_a), t_a), t_a)))) | (~c_less(c_0, v_x, t_a)) | (~c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[138, 137])).
% 0.19/0.41 tff(140,plain,
% 0.19/0.41 (~c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[139, 91, 136])).
% 0.19/0.41 tff(141,plain,
% 0.19/0.41 ($false),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[140, 126])).
% 0.19/0.41 tff(142,plain,(~(c_HOL_Oabs(v_f(v_xa(v_x)), t_a) = c_0)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.41 tff(143,plain,
% 0.19/0.41 ($false),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[142, 36])).
% 0.19/0.41 tff(144,plain,(~(v_xa(v_x) = c_0)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.41 tff(145,assumption,(~c_less(c_0, v_xa(v_x), tc_nat)), introduced(assumption)).
% 0.19/0.41 tff(146,plain,
% 0.19/0.41 (^[V_n: $i] : refl(((V_n = c_0) | c_less(c_0, V_n, tc_nat)) <=> ((V_n = c_0) | c_less(c_0, V_n, tc_nat)))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(147,plain,
% 0.19/0.41 (![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat)) <=> ![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[146])).
% 0.19/0.41 tff(148,plain,
% 0.19/0.41 (![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat)) <=> ![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(149,plain,
% 0.19/0.41 (^[V_n: $i] : rewrite((c_less(c_0, V_n, tc_nat) | (V_n = c_0)) <=> ((V_n = c_0) | c_less(c_0, V_n, tc_nat)))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(150,plain,
% 0.19/0.41 (![V_n: $i] : (c_less(c_0, V_n, tc_nat) | (V_n = c_0)) <=> ![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[149])).
% 0.19/0.41 tff(151,axiom,(![V_n: $i] : (c_less(c_0, V_n, tc_nat) | (V_n = c_0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_Nat_Onot__gr0_0')).
% 0.19/0.41 tff(152,plain,
% 0.19/0.41 (![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.19/0.41 tff(153,plain,
% 0.19/0.41 (![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[152, 148])).
% 0.19/0.41 tff(154,plain,(
% 0.19/0.41 ![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))),
% 0.19/0.41 inference(skolemize,[status(sab)],[153])).
% 0.19/0.41 tff(155,plain,
% 0.19/0.41 (![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[154, 147])).
% 0.19/0.41 tff(156,plain,
% 0.19/0.41 (((~![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))) | ((v_xa(v_x) = c_0) | c_less(c_0, v_xa(v_x), tc_nat))) <=> ((~![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))) | (v_xa(v_x) = c_0) | c_less(c_0, v_xa(v_x), tc_nat))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(157,plain,
% 0.19/0.41 ((~![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))) | ((v_xa(v_x) = c_0) | c_less(c_0, v_xa(v_x), tc_nat))),
% 0.19/0.41 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(158,plain,
% 0.19/0.42 ((~![V_n: $i] : ((V_n = c_0) | c_less(c_0, V_n, tc_nat))) | (v_xa(v_x) = c_0) | c_less(c_0, v_xa(v_x), tc_nat)),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[157, 156])).
% 0.19/0.42 tff(159,plain,
% 0.19/0.42 ($false),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[158, 155, 145, 144])).
% 0.19/0.42 tff(160,plain,(c_less(c_0, v_xa(v_x), tc_nat)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.42 tff(161,plain,
% 0.19/0.42 (^[V_x: $i] : refl(((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat)))) <=> ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat)))))),
% 0.19/0.42 inference(bind,[status(th)],[])).
% 0.19/0.42 tff(162,plain,
% 0.19/0.42 (![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat)))) <=> ![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))),
% 0.19/0.42 inference(quant_intro,[status(thm)],[161])).
% 0.19/0.42 tff(163,plain,
% 0.19/0.42 (![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat)))) <=> ![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(164,axiom,(![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_NatBin_OSuc__pred_H_0')).
% 0.19/0.42 tff(165,plain,
% 0.19/0.42 (![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[164, 163])).
% 0.19/0.42 tff(166,plain,(
% 0.19/0.42 ![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))),
% 0.19/0.42 inference(skolemize,[status(sab)],[165])).
% 0.19/0.42 tff(167,plain,
% 0.19/0.42 (![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[166, 162])).
% 0.19/0.42 tff(168,plain,
% 0.19/0.42 (((~![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))) | ((~c_less(c_0, v_xa(v_x), tc_nat)) | (v_xa(v_x) = c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))))) <=> ((~![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))) | (~c_less(c_0, v_xa(v_x), tc_nat)) | (v_xa(v_x) = c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(169,plain,
% 0.19/0.42 ((~![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))) | ((~c_less(c_0, v_xa(v_x), tc_nat)) | (v_xa(v_x) = c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(170,plain,
% 0.19/0.42 ((~![V_x: $i] : ((~c_less(c_0, V_x, tc_nat)) | (V_x = c_Suc(c_minus(V_x, c_1, tc_nat))))) | (~c_less(c_0, v_xa(v_x), tc_nat)) | (v_xa(v_x) = c_Suc(c_minus(v_xa(v_x), c_1, tc_nat)))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[169, 168])).
% 0.19/0.42 tff(171,plain,
% 0.19/0.42 ((~c_less(c_0, v_xa(v_x), tc_nat)) | (v_xa(v_x) = c_Suc(c_minus(v_xa(v_x), c_1, tc_nat)))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[170, 167])).
% 0.19/0.42 tff(172,plain,
% 0.19/0.42 (v_xa(v_x) = c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[171, 160])).
% 0.19/0.42 tff(173,plain,
% 0.19/0.42 (c_Suc(c_minus(v_xa(v_x), c_1, tc_nat)) = v_xa(v_x)),
% 0.19/0.42 inference(symmetry,[status(thm)],[172])).
% 0.19/0.42 tff(174,plain,
% 0.19/0.42 (v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))) = v_h(v_xa(v_x))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[173])).
% 0.19/0.42 tff(175,plain,
% 0.19/0.42 (c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a) = c_HOL_Oabs(v_h(v_xa(v_x)), t_a)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[174])).
% 0.19/0.42 tff(176,plain,
% 0.19/0.42 (c_times(v_x, c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), t_a) = c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[175])).
% 0.19/0.42 tff(177,plain,
% 0.19/0.42 (v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))) = v_f(v_xa(v_x))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[173])).
% 0.19/0.42 tff(178,plain,
% 0.19/0.42 (c_HOL_Oabs(v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a) = c_HOL_Oabs(v_f(v_xa(v_x)), t_a)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[177])).
% 0.19/0.42 tff(179,plain,
% 0.19/0.42 (c_lessequals(c_HOL_Oabs(v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), t_a), t_a) <=> c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)),
% 0.19/0.42 inference(monotonicity,[status(thm)],[178, 176])).
% 0.19/0.42 tff(180,plain,
% 0.19/0.42 (c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a) <=> c_lessequals(c_HOL_Oabs(v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), t_a), t_a)),
% 0.19/0.42 inference(symmetry,[status(thm)],[179])).
% 0.19/0.42 tff(181,plain,
% 0.19/0.42 ((~c_lessequals(c_HOL_Oabs(v_f(v_xa(v_x)), t_a), c_times(v_x, c_HOL_Oabs(v_h(v_xa(v_x)), t_a), t_a), t_a)) <=> (~c_lessequals(c_HOL_Oabs(v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), t_a), t_a))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[180])).
% 0.19/0.42 tff(182,plain,
% 0.19/0.42 (~c_lessequals(c_HOL_Oabs(v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), t_a), t_a)),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[140, 181])).
% 0.19/0.42 tff(183,plain,
% 0.19/0.42 (^[V_U: $i] : refl(c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a) <=> c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a))),
% 0.19/0.42 inference(bind,[status(th)],[])).
% 0.19/0.42 tff(184,plain,
% 0.19/0.42 (![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a) <=> ![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a)),
% 0.19/0.42 inference(quant_intro,[status(thm)],[183])).
% 0.19/0.42 tff(185,plain,
% 0.19/0.42 (![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a) <=> ![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a)),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(186,axiom,(![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cls_conjecture_2')).
% 0.19/0.42 tff(187,plain,
% 0.19/0.42 (![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a)),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[186, 185])).
% 0.19/0.42 tff(188,plain,(
% 0.19/0.42 ![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a)),
% 0.19/0.42 inference(skolemize,[status(sab)],[187])).
% 0.19/0.42 tff(189,plain,
% 0.19/0.42 (![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a)),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[188, 184])).
% 0.19/0.42 tff(190,plain,
% 0.19/0.42 ((~![V_U: $i] : c_lessequals(c_HOL_Oabs(v_f(c_Suc(V_U)), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(V_U)), t_a), t_a), t_a)) | c_lessequals(c_HOL_Oabs(v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), t_a), t_a)),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(191,plain,
% 0.19/0.42 (c_lessequals(c_HOL_Oabs(v_f(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), c_times(v_x, c_HOL_Oabs(v_h(c_Suc(c_minus(v_xa(v_x), c_1, tc_nat))), t_a), t_a), t_a)),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[190, 189])).
% 0.19/0.42 tff(192,plain,
% 0.19/0.42 ($false),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[191, 182])).
% 0.19/0.42 % SZS output end Proof
% 0.19/0.42 % E exiting
%------------------------------------------------------------------------------