%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP180-2 : TPTP v8.1.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n014.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 : 600s
% DateTime : Sat Jul 16 10:29:25 EDT 2022
% Result : Unsatisfiable 148.62s 37.51s
% Output : CNFRefutation 148.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP180-2 : TPTP v8.1.0. Bugfixed v1.2.1.
% 0.03/0.12 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n014.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 : 600
% 0.12/0.33 % DateTime : Tue Jun 14 04:41:06 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 20521: Facts:
% 0.12/0.33 20521: Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 0.12/0.33 20521: Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 0.12/0.33 20521: Id : 4, {_}:
% 0.12/0.33 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
% 0.12/0.33 [8, 7, 6] by associativity ?6 ?7 ?8
% 0.12/0.33 20521: Id : 5, {_}:
% 0.12/0.33 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
% 0.12/0.33 [11, 10] by symmetry_of_glb ?10 ?11
% 0.12/0.33 20521: Id : 6, {_}:
% 0.12/0.33 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
% 0.12/0.33 [14, 13] by symmetry_of_lub ?13 ?14
% 0.12/0.33 20521: Id : 7, {_}:
% 0.12/0.33 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
% 0.12/0.33 =?=
% 0.12/0.33 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
% 0.12/0.33 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
% 0.12/0.33 20521: Id : 8, {_}:
% 0.12/0.33 least_upper_bound ?20 (least_upper_bound ?21 ?22)
% 0.12/0.33 =?=
% 0.12/0.33 least_upper_bound (least_upper_bound ?20 ?21) ?22
% 0.12/0.33 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
% 0.12/0.33 20521: Id : 9, {_}: least_upper_bound ?24 ?24 =>= ?24 [24] by idempotence_of_lub ?24
% 0.12/0.33 20521: Id : 10, {_}:
% 0.12/0.33 greatest_lower_bound ?26 ?26 =>= ?26
% 0.12/0.33 [26] by idempotence_of_gld ?26
% 0.12/0.33 20521: Id : 11, {_}:
% 0.12/0.33 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
% 0.12/0.33 [29, 28] by lub_absorbtion ?28 ?29
% 0.12/0.33 20521: Id : 12, {_}:
% 0.12/0.33 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
% 0.12/0.33 [32, 31] by glb_absorbtion ?31 ?32
% 0.12/0.33 20521: Id : 13, {_}:
% 0.12/0.33 multiply ?34 (least_upper_bound ?35 ?36)
% 0.12/0.33 =<=
% 0.12/0.33 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
% 0.12/0.33 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
% 0.12/0.33 20521: Id : 14, {_}:
% 0.12/0.33 multiply ?38 (greatest_lower_bound ?39 ?40)
% 0.12/0.33 =<=
% 0.12/0.33 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
% 0.12/0.33 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
% 0.12/0.33 20521: Id : 15, {_}:
% 0.12/0.33 multiply (least_upper_bound ?42 ?43) ?44
% 0.12/0.33 =<=
% 0.12/0.33 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
% 0.12/0.33 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
% 0.12/0.33 20521: Id : 16, {_}:
% 0.12/0.33 multiply (greatest_lower_bound ?46 ?47) ?48
% 0.12/0.33 =<=
% 0.12/0.33 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
% 0.12/0.33 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
% 0.12/0.33 20521: Id : 17, {_}: inverse identity =>= identity [] by p11_1
% 0.12/0.33 20521: Id : 18, {_}: inverse (inverse ?51) =>= ?51 [51] by p11_2 ?51
% 0.12/0.33 20521: Id : 19, {_}:
% 0.12/0.33 inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
% 0.12/0.33 [54, 53] by p11_3 ?53 ?54
% 0.12/0.33 20521: Goal:
% 0.12/0.33 20521: Id : 1, {_}:
% 0.12/0.33 multiply a (multiply (inverse (greatest_lower_bound a b)) b)
% 0.12/0.33 =>=
% 0.12/0.33 least_upper_bound a b
% 0.12/0.33 [] by prove_p11
% 148.62/37.51 Statistics :
% 148.62/37.51 Max weight : 22
% 148.62/37.51 Found proof, 37.176191s
% 148.62/37.51 % SZS status Unsatisfiable for theBenchmark.p
% 148.62/37.51 % SZS output start CNFRefutation for theBenchmark.p
% 148.62/37.51 Id : 184, {_}: multiply ?578 (greatest_lower_bound ?579 ?580) =<= greatest_lower_bound (multiply ?578 ?579) (multiply ?578 ?580) [580, 579, 578] by monotony_glb1 ?578 ?579 ?580
% 148.62/37.51 Id : 249, {_}: multiply (greatest_lower_bound ?729 ?730) ?731 =<= greatest_lower_bound (multiply ?729 ?731) (multiply ?730 ?731) [731, 730, 729] by monotony_glb2 ?729 ?730 ?731
% 148.62/37.51 Id : 9, {_}: least_upper_bound ?24 ?24 =>= ?24 [24] by idempotence_of_lub ?24
% 148.62/37.51 Id : 117, {_}: least_upper_bound ?399 (greatest_lower_bound ?399 ?400) =>= ?399 [400, 399] by lub_absorbtion ?399 ?400
% 148.62/37.51 Id : 13, {_}: multiply ?34 (least_upper_bound ?35 ?36) =<= least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36) [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
% 148.62/37.51 Id : 10, {_}: greatest_lower_bound ?26 ?26 =>= ?26 [26] by idempotence_of_gld ?26
% 148.62/37.51 Id : 7, {_}: greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18) =?= greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
% 148.62/37.51 Id : 16, {_}: multiply (greatest_lower_bound ?46 ?47) ?48 =<= greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48) [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
% 148.62/37.51 Id : 14, {_}: multiply ?38 (greatest_lower_bound ?39 ?40) =<= greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40) [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
% 148.62/37.51 Id : 8, {_}: least_upper_bound ?20 (least_upper_bound ?21 ?22) =?= least_upper_bound (least_upper_bound ?20 ?21) ?22 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
% 148.62/37.51 Id : 12, {_}: greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31 [32, 31] by glb_absorbtion ?31 ?32
% 148.62/37.51 Id : 19, {_}: inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53) [54, 53] by p11_3 ?53 ?54
% 148.62/37.51 Id : 24, {_}: multiply (multiply ?63 ?64) ?65 =?= multiply ?63 (multiply ?64 ?65) [65, 64, 63] by associativity ?63 ?64 ?65
% 148.62/37.51 Id : 217, {_}: multiply (least_upper_bound ?652 ?653) ?654 =<= least_upper_bound (multiply ?652 ?654) (multiply ?653 ?654) [654, 653, 652] by monotony_lub2 ?652 ?653 ?654
% 148.62/37.51 Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 148.62/37.51 Id : 17, {_}: inverse identity =>= identity [] by p11_1
% 148.62/37.51 Id : 298, {_}: inverse (multiply ?837 ?838) =<= multiply (inverse ?838) (inverse ?837) [838, 837] by p11_3 ?837 ?838
% 148.62/37.51 Id : 4, {_}: multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8) [8, 7, 6] by associativity ?6 ?7 ?8
% 148.62/37.51 Id : 135, {_}: greatest_lower_bound ?454 (least_upper_bound ?454 ?455) =>= ?454 [455, 454] by glb_absorbtion ?454 ?455
% 148.62/37.51 Id : 18, {_}: inverse (inverse ?51) =>= ?51 [51] by p11_2 ?51
% 148.62/37.51 Id : 15, {_}: multiply (least_upper_bound ?42 ?43) ?44 =<= least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44) [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
% 148.62/37.51 Id : 5, {_}: greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10 [11, 10] by symmetry_of_glb ?10 ?11
% 148.62/37.51 Id : 11, {_}: least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28 [29, 28] by lub_absorbtion ?28 ?29
% 148.62/37.51 Id : 6, {_}: least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13 [14, 13] by symmetry_of_lub ?13 ?14
% 148.62/37.51 Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 148.62/37.51 Id : 154, {_}: multiply ?507 (least_upper_bound ?508 ?509) =<= least_upper_bound (multiply ?507 ?508) (multiply ?507 ?509) [509, 508, 507] by monotony_lub1 ?507 ?508 ?509
% 148.62/37.51 Id : 1244, {_}: multiply (inverse ?2437) (least_upper_bound ?2437 ?2438) =>= least_upper_bound identity (multiply (inverse ?2437) ?2438) [2438, 2437] by Super 154 with 3 at 1,3
% 148.62/37.51 Id : 111, {_}: least_upper_bound (greatest_lower_bound ?377 ?378) ?377 =>= ?377 [378, 377] by Super 6 with 11 at 3
% 148.62/37.51 Id : 9556, {_}: multiply (inverse (greatest_lower_bound ?18643 ?18644)) ?18643 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?18643 ?18644)) ?18643) [18644, 18643] by Super 1244 with 111 at 2,2
% 148.62/37.51 Id : 9557, {_}: multiply (inverse (greatest_lower_bound ?18646 ?18647)) ?18646 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?18647 ?18646)) ?18646) [18647, 18646] by Super 9556 with 5 at 1,1,2,3
% 148.62/37.51 Id : 551, {_}: least_upper_bound (greatest_lower_bound ?1244 ?1245) ?1244 =>= ?1244 [1245, 1244] by Super 6 with 11 at 3
% 148.62/37.51 Id : 552, {_}: least_upper_bound (greatest_lower_bound ?1247 ?1248) ?1248 =>= ?1248 [1248, 1247] by Super 551 with 5 at 1,2
% 148.62/37.51 Id : 1254, {_}: multiply (inverse (greatest_lower_bound ?2467 ?2468)) ?2468 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?2467 ?2468)) ?2468) [2468, 2467] by Super 1244 with 552 at 2,2
% 148.62/37.51 Id : 161973, {_}: multiply (inverse (greatest_lower_bound ?18646 ?18647)) ?18646 =?= multiply (inverse (greatest_lower_bound ?18647 ?18646)) ?18646 [18647, 18646] by Demod 9557 with 1254 at 3
% 148.62/37.51 Id : 281, {_}: multiply ?786 (inverse ?786) =>= identity [786] by Super 3 with 18 at 1,2
% 148.62/37.51 Id : 1972, {_}: multiply (least_upper_bound ?3583 ?3584) (inverse ?3583) =>= least_upper_bound identity (multiply ?3584 (inverse ?3583)) [3584, 3583] by Super 15 with 281 at 1,3
% 148.62/37.51 Id : 113947, {_}: multiply ?123909 (inverse (greatest_lower_bound ?123909 ?123910)) =<= least_upper_bound identity (multiply ?123909 (inverse (greatest_lower_bound ?123909 ?123910))) [123910, 123909] by Super 1972 with 111 at 1,2
% 148.62/37.51 Id : 113948, {_}: multiply ?123912 (inverse (greatest_lower_bound ?123912 ?123913)) =<= least_upper_bound identity (multiply ?123912 (inverse (greatest_lower_bound ?123913 ?123912))) [123913, 123912] by Super 113947 with 5 at 1,2,2,3
% 148.62/37.51 Id : 1986, {_}: multiply ?3626 (inverse (greatest_lower_bound ?3627 ?3626)) =<= least_upper_bound identity (multiply ?3626 (inverse (greatest_lower_bound ?3627 ?3626))) [3627, 3626] by Super 1972 with 552 at 1,2
% 148.62/37.51 Id : 259770, {_}: multiply ?123912 (inverse (greatest_lower_bound ?123912 ?123913)) =?= multiply ?123912 (inverse (greatest_lower_bound ?123913 ?123912)) [123913, 123912] by Demod 113948 with 1986 at 3
% 148.62/37.51 Id : 136, {_}: greatest_lower_bound ?457 (least_upper_bound ?458 ?457) =>= ?457 [458, 457] by Super 135 with 6 at 2,2
% 148.62/37.51 Id : 372, {_}: multiply (multiply ?947 ?948) (inverse ?948) =>= multiply ?947 identity [948, 947] by Super 4 with 281 at 2,3
% 148.62/37.51 Id : 299, {_}: inverse (multiply identity ?840) =<= multiply (inverse ?840) identity [840] by Super 298 with 17 at 2,3
% 148.62/37.51 Id : 322, {_}: inverse ?886 =<= multiply (inverse ?886) identity [886] by Demod 299 with 2 at 1,2
% 148.62/37.51 Id : 324, {_}: inverse (inverse ?889) =<= multiply ?889 identity [889] by Super 322 with 18 at 1,3
% 148.62/37.51 Id : 334, {_}: ?889 =<= multiply ?889 identity [889] by Demod 324 with 18 at 2
% 148.62/37.51 Id : 2199, {_}: multiply (multiply ?3921 ?3922) (inverse ?3922) =>= ?3921 [3922, 3921] by Demod 372 with 334 at 3
% 148.62/37.51 Id : 223, {_}: multiply (least_upper_bound (inverse ?675) ?676) ?675 =>= least_upper_bound identity (multiply ?676 ?675) [676, 675] by Super 217 with 3 at 1,3
% 148.62/37.51 Id : 2211, {_}: multiply (least_upper_bound identity (multiply ?3957 ?3958)) (inverse ?3958) =>= least_upper_bound (inverse ?3958) ?3957 [3958, 3957] by Super 2199 with 223 at 1,2
% 148.62/37.51 Id : 300, {_}: inverse (multiply (inverse ?842) ?843) =>= multiply (inverse ?843) ?842 [843, 842] by Super 298 with 18 at 2,3
% 148.62/37.51 Id : 26, {_}: multiply (multiply ?70 (inverse ?71)) ?71 =>= multiply ?70 identity [71, 70] by Super 24 with 3 at 2,3
% 148.62/37.51 Id : 1201, {_}: multiply (multiply ?2351 (inverse ?2352)) ?2352 =>= ?2351 [2352, 2351] by Demod 26 with 334 at 3
% 148.62/37.51 Id : 1211, {_}: multiply (inverse (multiply ?2380 ?2381)) ?2380 =>= inverse ?2381 [2381, 2380] by Super 1201 with 19 at 1,2
% 148.62/37.51 Id : 2424, {_}: inverse (inverse ?4293) =<= multiply (inverse ?4294) (multiply ?4294 ?4293) [4294, 4293] by Super 300 with 1211 at 1,2
% 148.62/37.51 Id : 2635, {_}: ?4605 =<= multiply (inverse ?4606) (multiply ?4606 ?4605) [4606, 4605] by Demod 2424 with 18 at 2
% 148.62/37.51 Id : 160, {_}: multiply (inverse ?530) (least_upper_bound ?530 ?531) =>= least_upper_bound identity (multiply (inverse ?530) ?531) [531, 530] by Super 154 with 3 at 1,3
% 148.62/37.51 Id : 2639, {_}: least_upper_bound ?4616 ?4617 =<= multiply (inverse (inverse ?4616)) (least_upper_bound identity (multiply (inverse ?4616) ?4617)) [4617, 4616] by Super 2635 with 160 at 2,3
% 148.62/37.51 Id : 2680, {_}: least_upper_bound ?4616 ?4617 =<= multiply ?4616 (least_upper_bound identity (multiply (inverse ?4616) ?4617)) [4617, 4616] by Demod 2639 with 18 at 1,3
% 148.62/37.51 Id : 1186, {_}: multiply (multiply ?70 (inverse ?71)) ?71 =>= ?70 [71, 70] by Demod 26 with 334 at 3
% 148.62/37.51 Id : 1250, {_}: multiply (inverse (greatest_lower_bound ?2455 ?2456)) ?2455 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?2455 ?2456)) ?2455) [2456, 2455] by Super 1244 with 111 at 2,2
% 148.62/37.51 Id : 621, {_}: greatest_lower_bound (least_upper_bound ?1381 ?1382) ?1381 =>= ?1381 [1382, 1381] by Super 5 with 12 at 3
% 148.62/37.51 Id : 622, {_}: greatest_lower_bound (least_upper_bound ?1384 ?1385) ?1385 =>= ?1385 [1385, 1384] by Super 621 with 6 at 1,2
% 148.62/37.51 Id : 9589, {_}: multiply (inverse (greatest_lower_bound identity ?18760)) identity =>= least_upper_bound identity (inverse (greatest_lower_bound identity ?18760)) [18760] by Super 9556 with 334 at 2,3
% 148.62/37.51 Id : 9780, {_}: inverse (greatest_lower_bound identity ?18867) =<= least_upper_bound identity (inverse (greatest_lower_bound identity ?18867)) [18867] by Demod 9589 with 334 at 2
% 148.62/37.51 Id : 9781, {_}: inverse (greatest_lower_bound identity ?18869) =<= least_upper_bound identity (inverse (greatest_lower_bound ?18869 identity)) [18869] by Super 9780 with 5 at 1,2,3
% 148.62/37.51 Id : 12505, {_}: least_upper_bound identity (least_upper_bound (inverse (greatest_lower_bound ?21757 identity)) ?21758) =>= least_upper_bound (inverse (greatest_lower_bound identity ?21757)) ?21758 [21758, 21757] by Super 8 with 9781 at 1,3
% 148.62/37.51 Id : 12518, {_}: least_upper_bound identity (least_upper_bound ?21800 (inverse (greatest_lower_bound ?21801 identity))) =>= least_upper_bound (inverse (greatest_lower_bound identity ?21801)) ?21800 [21801, 21800] by Super 12505 with 6 at 2,2
% 148.62/37.51 Id : 1508, {_}: multiply (least_upper_bound identity (multiply ?2891 (inverse ?2892))) ?2892 =>= least_upper_bound (inverse (inverse ?2892)) ?2891 [2892, 2891] by Super 1186 with 223 at 1,2
% 148.62/37.51 Id : 68551, {_}: multiply (least_upper_bound identity (multiply ?82597 (inverse ?82598))) ?82598 =>= least_upper_bound ?82598 ?82597 [82598, 82597] by Demod 1508 with 18 at 1,3
% 148.62/37.51 Id : 68594, {_}: multiply (multiply (inverse (greatest_lower_bound (inverse ?82732) ?82733)) (inverse ?82732)) ?82732 =>= least_upper_bound ?82732 (inverse (greatest_lower_bound (inverse ?82732) ?82733)) [82733, 82732] by Super 68551 with 1250 at 1,2
% 148.62/37.51 Id : 68693, {_}: multiply (inverse (greatest_lower_bound (inverse ?82732) ?82733)) (multiply (inverse ?82732) ?82732) =>= least_upper_bound ?82732 (inverse (greatest_lower_bound (inverse ?82732) ?82733)) [82733, 82732] by Demod 68594 with 4 at 2
% 148.62/37.51 Id : 405, {_}: inverse (multiply (multiply (inverse ?980) ?981) ?982) =<= multiply (inverse ?982) (multiply (inverse ?981) ?980) [982, 981, 980] by Super 19 with 300 at 2,3
% 148.62/37.51 Id : 422, {_}: inverse (multiply (inverse ?980) (multiply ?981 ?982)) =<= multiply (inverse ?982) (multiply (inverse ?981) ?980) [982, 981, 980] by Demod 405 with 4 at 1,2
% 148.62/37.51 Id : 423, {_}: multiply (inverse (multiply ?981 ?982)) ?980 =<= multiply (inverse ?982) (multiply (inverse ?981) ?980) [980, 982, 981] by Demod 422 with 300 at 2
% 148.62/37.51 Id : 68694, {_}: multiply (inverse (multiply ?82732 (greatest_lower_bound (inverse ?82732) ?82733))) ?82732 =>= least_upper_bound ?82732 (inverse (greatest_lower_bound (inverse ?82732) ?82733)) [82733, 82732] by Demod 68693 with 423 at 2
% 148.62/37.51 Id : 68695, {_}: inverse (greatest_lower_bound (inverse ?82732) ?82733) =<= least_upper_bound ?82732 (inverse (greatest_lower_bound (inverse ?82732) ?82733)) [82733, 82732] by Demod 68694 with 1211 at 2
% 148.62/37.51 Id : 68734, {_}: least_upper_bound identity (inverse (greatest_lower_bound (inverse ?82821) identity)) =<= least_upper_bound (inverse (greatest_lower_bound identity (inverse ?82821))) ?82821 [82821] by Super 12518 with 68695 at 2,2
% 148.62/37.51 Id : 69070, {_}: inverse (greatest_lower_bound identity (inverse ?82821)) =<= least_upper_bound (inverse (greatest_lower_bound identity (inverse ?82821))) ?82821 [82821] by Demod 68734 with 9781 at 2
% 148.62/37.51 Id : 70927, {_}: greatest_lower_bound (inverse (greatest_lower_bound identity (inverse ?84296))) ?84296 =>= ?84296 [84296] by Super 622 with 69070 at 1,2
% 148.62/37.51 Id : 70929, {_}: greatest_lower_bound (inverse (greatest_lower_bound identity ?84299)) (inverse ?84299) =>= inverse ?84299 [84299] by Super 70927 with 18 at 2,1,1,2
% 148.62/37.51 Id : 72860, {_}: multiply (inverse (greatest_lower_bound (inverse (greatest_lower_bound identity ?85521)) (inverse ?85521))) (inverse (greatest_lower_bound identity ?85521)) =>= least_upper_bound identity (multiply (inverse (inverse ?85521)) (inverse (greatest_lower_bound identity ?85521))) [85521] by Super 1250 with 70929 at 1,1,2,3
% 148.62/37.51 Id : 72968, {_}: inverse (multiply (greatest_lower_bound identity ?85521) (greatest_lower_bound (inverse (greatest_lower_bound identity ?85521)) (inverse ?85521))) =>= least_upper_bound identity (multiply (inverse (inverse ?85521)) (inverse (greatest_lower_bound identity ?85521))) [85521] by Demod 72860 with 19 at 2
% 148.62/37.51 Id : 72969, {_}: inverse (multiply (greatest_lower_bound identity ?85521) (greatest_lower_bound (inverse (greatest_lower_bound identity ?85521)) (inverse ?85521))) =>= least_upper_bound identity (inverse (multiply (greatest_lower_bound identity ?85521) (inverse ?85521))) [85521] by Demod 72968 with 19 at 2,3
% 148.62/37.51 Id : 371, {_}: multiply ?944 (greatest_lower_bound (inverse ?944) ?945) =>= greatest_lower_bound identity (multiply ?944 ?945) [945, 944] by Super 14 with 281 at 1,3
% 148.62/37.51 Id : 72970, {_}: inverse (greatest_lower_bound identity (multiply (greatest_lower_bound identity ?85521) (inverse ?85521))) =<= least_upper_bound identity (inverse (multiply (greatest_lower_bound identity ?85521) (inverse ?85521))) [85521] by Demod 72969 with 371 at 1,2
% 148.62/37.51 Id : 302, {_}: inverse (multiply ?847 (inverse ?848)) =>= multiply ?848 (inverse ?847) [848, 847] by Super 298 with 18 at 1,3
% 148.62/37.51 Id : 72971, {_}: inverse (greatest_lower_bound identity (multiply (greatest_lower_bound identity ?85521) (inverse ?85521))) =>= least_upper_bound identity (multiply ?85521 (inverse (greatest_lower_bound identity ?85521))) [85521] by Demod 72970 with 302 at 2,3
% 148.62/37.51 Id : 368, {_}: multiply (greatest_lower_bound ?935 ?936) (inverse ?936) =>= greatest_lower_bound (multiply ?935 (inverse ?936)) identity [936, 935] by Super 16 with 281 at 2,3
% 148.62/37.51 Id : 395, {_}: multiply (greatest_lower_bound ?935 ?936) (inverse ?936) =>= greatest_lower_bound identity (multiply ?935 (inverse ?936)) [936, 935] by Demod 368 with 5 at 3
% 148.62/37.51 Id : 72972, {_}: inverse (greatest_lower_bound identity (greatest_lower_bound identity (multiply identity (inverse ?85521)))) =?= least_upper_bound identity (multiply ?85521 (inverse (greatest_lower_bound identity ?85521))) [85521] by Demod 72971 with 395 at 2,1,2
% 148.62/37.51 Id : 103, {_}: greatest_lower_bound ?355 (greatest_lower_bound ?355 ?356) =>= greatest_lower_bound ?355 ?356 [356, 355] by Super 7 with 10 at 1,3
% 148.62/37.51 Id : 72973, {_}: inverse (greatest_lower_bound identity (multiply identity (inverse ?85521))) =<= least_upper_bound identity (multiply ?85521 (inverse (greatest_lower_bound identity ?85521))) [85521] by Demod 72972 with 103 at 1,2
% 148.62/37.51 Id : 72974, {_}: inverse (greatest_lower_bound identity (inverse ?85521)) =<= least_upper_bound identity (multiply ?85521 (inverse (greatest_lower_bound identity ?85521))) [85521] by Demod 72973 with 2 at 2,1,2
% 148.62/37.51 Id : 375, {_}: multiply ?954 (least_upper_bound ?955 (inverse ?954)) =>= least_upper_bound (multiply ?954 ?955) identity [955, 954] by Super 13 with 281 at 2,3
% 148.62/37.51 Id : 390, {_}: multiply ?954 (least_upper_bound ?955 (inverse ?954)) =>= least_upper_bound identity (multiply ?954 ?955) [955, 954] by Demod 375 with 6 at 3
% 148.62/37.51 Id : 69374, {_}: multiply ?83445 (inverse (greatest_lower_bound identity (inverse (inverse ?83445)))) =<= least_upper_bound identity (multiply ?83445 (inverse (greatest_lower_bound identity (inverse (inverse ?83445))))) [83445] by Super 390 with 69070 at 2,2
% 148.62/37.51 Id : 69768, {_}: multiply ?83445 (inverse (greatest_lower_bound identity ?83445)) =<= least_upper_bound identity (multiply ?83445 (inverse (greatest_lower_bound identity (inverse (inverse ?83445))))) [83445] by Demod 69374 with 18 at 2,1,2,2
% 148.62/37.51 Id : 69769, {_}: multiply ?83445 (inverse (greatest_lower_bound identity ?83445)) =<= least_upper_bound identity (multiply ?83445 (inverse (greatest_lower_bound identity ?83445))) [83445] by Demod 69768 with 18 at 2,1,2,2,3
% 148.62/37.51 Id : 89952, {_}: inverse (greatest_lower_bound identity (inverse ?85521)) =<= multiply ?85521 (inverse (greatest_lower_bound identity ?85521)) [85521] by Demod 72974 with 69769 at 3
% 148.62/37.51 Id : 89976, {_}: multiply (inverse (greatest_lower_bound identity (inverse ?99534))) (greatest_lower_bound identity ?99534) =>= ?99534 [99534] by Super 1186 with 89952 at 1,2
% 148.62/37.51 Id : 221504, {_}: least_upper_bound (greatest_lower_bound identity (inverse ?272954)) (greatest_lower_bound identity ?272954) =<= multiply (greatest_lower_bound identity (inverse ?272954)) (least_upper_bound identity ?272954) [272954] by Super 2680 with 89976 at 2,2,3
% 148.62/37.51 Id : 222046, {_}: multiply (least_upper_bound identity (least_upper_bound (greatest_lower_bound identity (inverse ?273420)) (greatest_lower_bound identity ?273420))) (inverse (least_upper_bound identity ?273420)) =>= least_upper_bound (inverse (least_upper_bound identity ?273420)) (greatest_lower_bound identity (inverse ?273420)) [273420] by Super 2211 with 221504 at 2,1,2
% 148.62/37.51 Id : 113, {_}: least_upper_bound ?383 (least_upper_bound (greatest_lower_bound ?383 ?384) ?385) =>= least_upper_bound ?383 ?385 [385, 384, 383] by Super 8 with 11 at 1,3
% 148.62/37.51 Id : 222180, {_}: multiply (least_upper_bound identity (greatest_lower_bound identity ?273420)) (inverse (least_upper_bound identity ?273420)) =>= least_upper_bound (inverse (least_upper_bound identity ?273420)) (greatest_lower_bound identity (inverse ?273420)) [273420] by Demod 222046 with 113 at 1,2
% 148.62/37.51 Id : 222181, {_}: multiply identity (inverse (least_upper_bound identity ?273420)) =<= least_upper_bound (inverse (least_upper_bound identity ?273420)) (greatest_lower_bound identity (inverse ?273420)) [273420] by Demod 222180 with 11 at 1,2
% 148.62/37.51 Id : 222182, {_}: inverse (least_upper_bound identity ?273420) =<= least_upper_bound (inverse (least_upper_bound identity ?273420)) (greatest_lower_bound identity (inverse ?273420)) [273420] by Demod 222181 with 2 at 2
% 148.62/37.51 Id : 403455, {_}: greatest_lower_bound (greatest_lower_bound identity (inverse ?438811)) (inverse (least_upper_bound identity ?438811)) =>= greatest_lower_bound identity (inverse ?438811) [438811] by Super 136 with 222182 at 2,2
% 148.62/37.51 Id : 403852, {_}: greatest_lower_bound (inverse (least_upper_bound identity ?438811)) (greatest_lower_bound identity (inverse ?438811)) =>= greatest_lower_bound identity (inverse ?438811) [438811] by Demod 403455 with 5 at 2
% 148.62/37.51 Id : 585, {_}: least_upper_bound ?1313 (greatest_lower_bound ?1314 ?1313) =>= ?1313 [1314, 1313] by Super 117 with 5 at 2,2
% 148.62/37.51 Id : 592, {_}: least_upper_bound ?1334 (greatest_lower_bound ?1335 (greatest_lower_bound ?1336 ?1334)) =>= ?1334 [1336, 1335, 1334] by Super 585 with 7 at 2,2
% 148.62/37.51 Id : 4681, {_}: greatest_lower_bound ?8735 (greatest_lower_bound ?8736 (greatest_lower_bound ?8737 ?8735)) =>= greatest_lower_bound ?8736 (greatest_lower_bound ?8737 ?8735) [8737, 8736, 8735] by Super 622 with 592 at 1,2
% 148.62/37.51 Id : 520, {_}: greatest_lower_bound ?1179 (greatest_lower_bound ?1179 ?1180) =>= greatest_lower_bound ?1179 ?1180 [1180, 1179] by Super 7 with 10 at 1,3
% 148.62/37.51 Id : 872, {_}: greatest_lower_bound ?1837 (greatest_lower_bound ?1838 ?1837) =>= greatest_lower_bound ?1837 ?1838 [1838, 1837] by Super 520 with 5 at 2,2
% 148.62/37.51 Id : 883, {_}: greatest_lower_bound ?1870 (greatest_lower_bound ?1871 (greatest_lower_bound ?1872 ?1870)) =>= greatest_lower_bound ?1870 (greatest_lower_bound ?1871 ?1872) [1872, 1871, 1870] by Super 872 with 7 at 2,2
% 148.62/37.51 Id : 135600, {_}: greatest_lower_bound ?8735 (greatest_lower_bound ?8736 ?8737) =?= greatest_lower_bound ?8736 (greatest_lower_bound ?8737 ?8735) [8737, 8736, 8735] by Demod 4681 with 883 at 2
% 148.62/37.51 Id : 403853, {_}: greatest_lower_bound identity (greatest_lower_bound (inverse ?438811) (inverse (least_upper_bound identity ?438811))) =>= greatest_lower_bound identity (inverse ?438811) [438811] by Demod 403852 with 135600 at 2
% 148.62/37.51 Id : 665, {_}: greatest_lower_bound ?1464 (least_upper_bound ?1465 ?1464) =>= ?1464 [1465, 1464] by Super 135 with 6 at 2,2
% 148.62/37.51 Id : 118, {_}: least_upper_bound ?402 (greatest_lower_bound ?403 ?402) =>= ?402 [403, 402] by Super 117 with 5 at 2,2
% 148.62/37.51 Id : 672, {_}: greatest_lower_bound (greatest_lower_bound ?1484 ?1485) ?1485 =>= greatest_lower_bound ?1484 ?1485 [1485, 1484] by Super 665 with 118 at 2,2
% 148.62/37.51 Id : 659, {_}: greatest_lower_bound ?1444 (greatest_lower_bound (least_upper_bound ?1445 ?1444) ?1446) =>= greatest_lower_bound ?1444 ?1446 [1446, 1445, 1444] by Super 7 with 136 at 1,3
% 148.62/37.51 Id : 156, {_}: multiply (inverse ?514) (least_upper_bound ?515 ?514) =>= least_upper_bound (multiply (inverse ?514) ?515) identity [515, 514] by Super 154 with 3 at 2,3
% 148.62/37.51 Id : 173, {_}: multiply (inverse ?514) (least_upper_bound ?515 ?514) =>= least_upper_bound identity (multiply (inverse ?514) ?515) [515, 514] by Demod 156 with 6 at 3
% 148.62/37.51 Id : 9740, {_}: inverse (greatest_lower_bound identity ?18760) =<= least_upper_bound identity (inverse (greatest_lower_bound identity ?18760)) [18760] by Demod 9589 with 334 at 2
% 148.62/37.51 Id : 9939, {_}: greatest_lower_bound identity (inverse (greatest_lower_bound identity ?18997)) =>= identity [18997] by Super 12 with 9740 at 2,2
% 148.62/37.51 Id : 9940, {_}: greatest_lower_bound identity (inverse (greatest_lower_bound ?18999 identity)) =>= identity [18999] by Super 9939 with 5 at 1,2,2
% 148.62/37.51 Id : 10225, {_}: least_upper_bound (inverse (greatest_lower_bound ?19200 identity)) identity =>= inverse (greatest_lower_bound ?19200 identity) [19200] by Super 118 with 9940 at 2,2
% 148.62/37.51 Id : 10296, {_}: least_upper_bound identity (inverse (greatest_lower_bound ?19200 identity)) =>= inverse (greatest_lower_bound ?19200 identity) [19200] by Demod 10225 with 6 at 2
% 148.62/37.51 Id : 10297, {_}: inverse (greatest_lower_bound identity ?19200) =?= inverse (greatest_lower_bound ?19200 identity) [19200] by Demod 10296 with 9781 at 2
% 148.62/37.51 Id : 14762, {_}: multiply (inverse (greatest_lower_bound ?24329 identity)) ?24329 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound identity ?24329)) ?24329) [24329] by Super 1250 with 10297 at 1,2,3
% 148.62/37.51 Id : 10090, {_}: inverse (greatest_lower_bound identity ?19122) =<= least_upper_bound identity (inverse (greatest_lower_bound ?19122 identity)) [19122] by Super 9780 with 5 at 1,2,3
% 148.62/37.51 Id : 12751, {_}: inverse (greatest_lower_bound identity (greatest_lower_bound ?22003 ?22004)) =<= least_upper_bound identity (inverse (greatest_lower_bound ?22003 (greatest_lower_bound ?22004 identity))) [22004, 22003] by Super 10090 with 7 at 1,2,3
% 148.62/37.51 Id : 128, {_}: greatest_lower_bound (least_upper_bound ?430 ?431) ?430 =>= ?430 [431, 430] by Super 5 with 12 at 3
% 148.62/37.51 Id : 12754, {_}: inverse (greatest_lower_bound identity (greatest_lower_bound ?22011 (least_upper_bound identity ?22012))) =>= least_upper_bound identity (inverse (greatest_lower_bound ?22011 identity)) [22012, 22011] by Super 12751 with 128 at 2,1,2,3
% 148.62/37.51 Id : 18252, {_}: inverse (greatest_lower_bound identity (greatest_lower_bound ?28575 (least_upper_bound identity ?28576))) =>= inverse (greatest_lower_bound identity ?28575) [28576, 28575] by Demod 12754 with 9781 at 3
% 148.62/37.51 Id : 18283, {_}: inverse (greatest_lower_bound identity (least_upper_bound identity ?28670)) =<= inverse (greatest_lower_bound identity (least_upper_bound ?28671 (least_upper_bound identity ?28670))) [28671, 28670] by Super 18252 with 622 at 2,1,2
% 148.62/37.51 Id : 18385, {_}: inverse identity =<= inverse (greatest_lower_bound identity (least_upper_bound ?28671 (least_upper_bound identity ?28670))) [28670, 28671] by Demod 18283 with 12 at 1,2
% 148.62/37.51 Id : 18386, {_}: identity =<= inverse (greatest_lower_bound identity (least_upper_bound ?28671 (least_upper_bound identity ?28670))) [28670, 28671] by Demod 18385 with 17 at 2
% 148.62/37.51 Id : 22981, {_}: multiply (inverse (greatest_lower_bound (least_upper_bound ?33937 (least_upper_bound identity ?33938)) identity)) (least_upper_bound ?33937 (least_upper_bound identity ?33938)) =>= least_upper_bound identity (multiply identity (least_upper_bound ?33937 (least_upper_bound identity ?33938))) [33938, 33937] by Super 14762 with 18386 at 1,2,3
% 148.62/37.51 Id : 23048, {_}: multiply (inverse (greatest_lower_bound identity (least_upper_bound ?33937 (least_upper_bound identity ?33938)))) (least_upper_bound ?33937 (least_upper_bound identity ?33938)) =>= least_upper_bound identity (multiply identity (least_upper_bound ?33937 (least_upper_bound identity ?33938))) [33938, 33937] by Demod 22981 with 10297 at 1,2
% 148.62/37.51 Id : 23049, {_}: multiply (inverse (greatest_lower_bound identity (least_upper_bound ?33937 (least_upper_bound identity ?33938)))) (least_upper_bound ?33937 (least_upper_bound identity ?33938)) =>= least_upper_bound identity (least_upper_bound ?33937 (least_upper_bound identity ?33938)) [33938, 33937] by Demod 23048 with 2 at 2,3
% 148.62/37.51 Id : 23050, {_}: multiply identity (least_upper_bound ?33937 (least_upper_bound identity ?33938)) =>= least_upper_bound identity (least_upper_bound ?33937 (least_upper_bound identity ?33938)) [33938, 33937] by Demod 23049 with 18386 at 1,2
% 148.62/37.51 Id : 23051, {_}: least_upper_bound ?33937 (least_upper_bound identity ?33938) =<= least_upper_bound identity (least_upper_bound ?33937 (least_upper_bound identity ?33938)) [33938, 33937] by Demod 23050 with 2 at 2
% 148.62/37.51 Id : 23258, {_}: multiply (inverse (least_upper_bound ?34225 (least_upper_bound identity ?34226))) (least_upper_bound ?34225 (least_upper_bound identity ?34226)) =>= least_upper_bound identity (multiply (inverse (least_upper_bound ?34225 (least_upper_bound identity ?34226))) identity) [34226, 34225] by Super 173 with 23051 at 2,2
% 148.62/37.51 Id : 23370, {_}: identity =<= least_upper_bound identity (multiply (inverse (least_upper_bound ?34225 (least_upper_bound identity ?34226))) identity) [34226, 34225] by Demod 23258 with 3 at 2
% 148.62/37.51 Id : 26300, {_}: identity =<= least_upper_bound identity (inverse (least_upper_bound ?37790 (least_upper_bound identity ?37791))) [37791, 37790] by Demod 23370 with 334 at 2,3
% 148.62/37.51 Id : 26333, {_}: identity =<= least_upper_bound identity (inverse (least_upper_bound identity ?37892)) [37892] by Super 26300 with 9 at 1,2,3
% 148.62/37.51 Id : 26672, {_}: greatest_lower_bound (inverse (least_upper_bound identity ?38140)) (greatest_lower_bound identity ?38141) =>= greatest_lower_bound (inverse (least_upper_bound identity ?38140)) ?38141 [38141, 38140] by Super 659 with 26333 at 1,2,2
% 148.62/37.51 Id : 33748, {_}: greatest_lower_bound (greatest_lower_bound (inverse (least_upper_bound identity ?46128)) ?46129) (greatest_lower_bound identity ?46129) =>= greatest_lower_bound (inverse (least_upper_bound identity ?46128)) (greatest_lower_bound identity ?46129) [46129, 46128] by Super 672 with 26672 at 1,2
% 148.62/37.51 Id : 33919, {_}: greatest_lower_bound (greatest_lower_bound identity ?46129) (greatest_lower_bound (inverse (least_upper_bound identity ?46128)) ?46129) =>= greatest_lower_bound (inverse (least_upper_bound identity ?46128)) (greatest_lower_bound identity ?46129) [46128, 46129] by Demod 33748 with 5 at 2
% 148.62/37.51 Id : 33920, {_}: greatest_lower_bound (greatest_lower_bound identity ?46129) (greatest_lower_bound (inverse (least_upper_bound identity ?46128)) ?46129) =>= greatest_lower_bound (inverse (least_upper_bound identity ?46128)) ?46129 [46128, 46129] by Demod 33919 with 26672 at 3
% 148.62/37.51 Id : 33921, {_}: greatest_lower_bound identity (greatest_lower_bound ?46129 (greatest_lower_bound (inverse (least_upper_bound identity ?46128)) ?46129)) =>= greatest_lower_bound (inverse (least_upper_bound identity ?46128)) ?46129 [46128, 46129] by Demod 33920 with 7 at 2
% 148.62/37.51 Id : 521, {_}: greatest_lower_bound ?1182 (greatest_lower_bound ?1183 ?1182) =>= greatest_lower_bound ?1182 ?1183 [1183, 1182] by Super 520 with 5 at 2,2
% 148.62/37.51 Id : 33922, {_}: greatest_lower_bound identity (greatest_lower_bound ?46129 (inverse (least_upper_bound identity ?46128))) =>= greatest_lower_bound (inverse (least_upper_bound identity ?46128)) ?46129 [46128, 46129] by Demod 33921 with 521 at 2,2
% 148.62/37.51 Id : 403854, {_}: greatest_lower_bound (inverse (least_upper_bound identity ?438811)) (inverse ?438811) =>= greatest_lower_bound identity (inverse ?438811) [438811] by Demod 403853 with 33922 at 2
% 148.62/37.51 Id : 654, {_}: least_upper_bound (least_upper_bound ?1430 ?1431) ?1431 =>= least_upper_bound ?1430 ?1431 [1431, 1430] by Super 118 with 136 at 2,2
% 148.62/37.51 Id : 1255, {_}: multiply (inverse (least_upper_bound ?2470 ?2471)) (least_upper_bound ?2470 ?2471) =>= least_upper_bound identity (multiply (inverse (least_upper_bound ?2470 ?2471)) ?2471) [2471, 2470] by Super 1244 with 654 at 2,2
% 148.62/37.51 Id : 1285, {_}: identity =<= least_upper_bound identity (multiply (inverse (least_upper_bound ?2470 ?2471)) ?2471) [2471, 2470] by Demod 1255 with 3 at 2
% 148.62/37.51 Id : 68597, {_}: multiply identity ?82741 =<= least_upper_bound ?82741 (inverse (least_upper_bound ?82742 (inverse ?82741))) [82742, 82741] by Super 68551 with 1285 at 1,2
% 148.62/37.51 Id : 68700, {_}: ?82741 =<= least_upper_bound ?82741 (inverse (least_upper_bound ?82742 (inverse ?82741))) [82742, 82741] by Demod 68597 with 2 at 2
% 148.62/37.51 Id : 98582, {_}: greatest_lower_bound (inverse (least_upper_bound ?107136 (inverse ?107137))) ?107137 =>= inverse (least_upper_bound ?107136 (inverse ?107137)) [107137, 107136] by Super 136 with 68700 at 2,2
% 148.62/37.51 Id : 98584, {_}: greatest_lower_bound (inverse (least_upper_bound ?107141 ?107142)) (inverse ?107142) =>= inverse (least_upper_bound ?107141 (inverse (inverse ?107142))) [107142, 107141] by Super 98582 with 18 at 2,1,1,2
% 148.62/37.51 Id : 98988, {_}: greatest_lower_bound (inverse (least_upper_bound ?107141 ?107142)) (inverse ?107142) =>= inverse (least_upper_bound ?107141 ?107142) [107142, 107141] by Demod 98584 with 18 at 2,1,3
% 148.62/37.51 Id : 403855, {_}: inverse (least_upper_bound identity ?438811) =<= greatest_lower_bound identity (inverse ?438811) [438811] by Demod 403854 with 98988 at 2
% 148.62/37.51 Id : 404924, {_}: multiply (inverse ?439860) (inverse (greatest_lower_bound (inverse ?439860) identity)) =>= multiply (inverse ?439860) (inverse (inverse (least_upper_bound identity ?439860))) [439860] by Super 259770 with 403855 at 1,2,2
% 148.62/37.51 Id : 405034, {_}: multiply (inverse ?439860) (inverse (greatest_lower_bound identity (inverse ?439860))) =>= multiply (inverse ?439860) (inverse (inverse (least_upper_bound identity ?439860))) [439860] by Demod 404924 with 259770 at 2
% 148.62/37.51 Id : 405035, {_}: multiply (inverse ?439860) (inverse (greatest_lower_bound identity (inverse ?439860))) =>= inverse (multiply (inverse (least_upper_bound identity ?439860)) ?439860) [439860] by Demod 405034 with 19 at 3
% 148.62/37.51 Id : 405036, {_}: inverse (multiply (greatest_lower_bound identity (inverse ?439860)) ?439860) =>= inverse (multiply (inverse (least_upper_bound identity ?439860)) ?439860) [439860] by Demod 405035 with 19 at 2
% 148.62/37.51 Id : 405037, {_}: inverse (multiply (greatest_lower_bound identity (inverse ?439860)) ?439860) =>= multiply (inverse ?439860) (least_upper_bound identity ?439860) [439860] by Demod 405036 with 300 at 3
% 148.62/37.51 Id : 251, {_}: multiply (greatest_lower_bound ?736 (inverse ?737)) ?737 =>= greatest_lower_bound (multiply ?736 ?737) identity [737, 736] by Super 249 with 3 at 2,3
% 148.62/37.51 Id : 271, {_}: multiply (greatest_lower_bound ?736 (inverse ?737)) ?737 =>= greatest_lower_bound identity (multiply ?736 ?737) [737, 736] by Demod 251 with 5 at 3
% 148.62/37.51 Id : 405038, {_}: inverse (greatest_lower_bound identity (multiply identity ?439860)) =<= multiply (inverse ?439860) (least_upper_bound identity ?439860) [439860] by Demod 405037 with 271 at 1,2
% 148.62/37.51 Id : 405039, {_}: inverse (greatest_lower_bound identity (multiply identity ?439860)) =<= least_upper_bound identity (multiply (inverse ?439860) identity) [439860] by Demod 405038 with 173 at 3
% 148.62/37.51 Id : 405040, {_}: inverse (greatest_lower_bound identity ?439860) =<= least_upper_bound identity (multiply (inverse ?439860) identity) [439860] by Demod 405039 with 2 at 2,1,2
% 148.62/37.51 Id : 405991, {_}: inverse (greatest_lower_bound identity ?440575) =<= least_upper_bound identity (inverse ?440575) [440575] by Demod 405040 with 334 at 2,3
% 148.62/37.51 Id : 437964, {_}: inverse (greatest_lower_bound identity (multiply (inverse ?459575) ?459576)) =>= least_upper_bound identity (multiply (inverse ?459576) ?459575) [459576, 459575] by Super 405991 with 300 at 2,3
% 148.62/37.51 Id : 190, {_}: multiply (inverse ?601) (greatest_lower_bound ?601 ?602) =>= greatest_lower_bound identity (multiply (inverse ?601) ?602) [602, 601] by Super 184 with 3 at 1,3
% 148.62/37.51 Id : 438010, {_}: inverse (greatest_lower_bound identity (greatest_lower_bound identity (multiply (inverse ?459740) ?459741))) =?= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?459740 ?459741)) ?459740) [459741, 459740] by Super 437964 with 190 at 2,1,2
% 148.62/37.51 Id : 438487, {_}: inverse (greatest_lower_bound identity (multiply (inverse ?459740) ?459741)) =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?459740 ?459741)) ?459740) [459741, 459740] by Demod 438010 with 103 at 1,2
% 148.62/37.51 Id : 438488, {_}: inverse (greatest_lower_bound identity (multiply (inverse ?459740) ?459741)) =?= multiply (inverse (greatest_lower_bound ?459740 ?459741)) ?459740 [459741, 459740] by Demod 438487 with 1250 at 3
% 148.62/37.51 Id : 405994, {_}: inverse (greatest_lower_bound identity (multiply (inverse ?440580) ?440581)) =>= least_upper_bound identity (multiply (inverse ?440581) ?440580) [440581, 440580] by Super 405991 with 300 at 2,3
% 148.62/37.51 Id : 438489, {_}: least_upper_bound identity (multiply (inverse ?459741) ?459740) =<= multiply (inverse (greatest_lower_bound ?459740 ?459741)) ?459740 [459740, 459741] by Demod 438488 with 405994 at 2
% 148.62/37.52 Id : 459725, {_}: least_upper_bound identity (multiply (inverse ?18647) ?18646) =<= multiply (inverse (greatest_lower_bound ?18647 ?18646)) ?18646 [18646, 18647] by Demod 161973 with 438489 at 2
% 148.62/37.52 Id : 460841, {_}: least_upper_bound a b === least_upper_bound a b [] by Demod 460840 with 2680 at 2
% 148.62/37.52 Id : 460840, {_}: multiply a (least_upper_bound identity (multiply (inverse a) b)) =>= least_upper_bound a b [] by Demod 1 with 459725 at 2,2
% 148.62/37.52 Id : 1, {_}: multiply a (multiply (inverse (greatest_lower_bound a b)) b) =>= least_upper_bound a b [] by prove_p11
% 148.62/37.52 % SZS output end CNFRefutation for theBenchmark.p
% 148.62/37.52 20524: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 37.183798 using nrkbo
%------------------------------------------------------------------------------