%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP167-4 : TPTP v8.1.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% Computer : n017.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:18 EDT 2022
% Result : Unsatisfiable 215.49s 54.23s
% Output : CNFRefutation 215.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : GRP167-4 : TPTP v8.1.0. Bugfixed v1.2.1.
% 0.08/0.13 % Command : matitaprover --timeout %d --tptppath /export/starexec/sandbox2/benchmark %s
% 0.12/0.33 % Computer : n017.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 : Mon Jun 13 18:53:23 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 21775: Facts:
% 0.12/0.33 21775: Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 0.12/0.33 21775: Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 0.12/0.33 21775: 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 21775: 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 21775: 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 21775: 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 21775: 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 21775: Id : 9, {_}: least_upper_bound ?24 ?24 =>= ?24 [24] by idempotence_of_lub ?24
% 0.12/0.33 21775: 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 21775: 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 21775: 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 21775: 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 21775: 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 21775: 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 21775: 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 21775: Id : 17, {_}: inverse identity =>= identity [] by p19_1
% 0.12/0.33 21775: Id : 18, {_}: inverse (inverse ?51) =>= ?51 [51] by p19_2 ?51
% 0.12/0.33 21775: Id : 19, {_}:
% 0.12/0.33 inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
% 0.12/0.33 [54, 53] by p19_3 ?53 ?54
% 0.12/0.33 21775: Goal:
% 0.12/0.33 21775: Id : 1, {_}:
% 0.12/0.33 a
% 0.12/0.33 =<=
% 0.12/0.33 multiply (least_upper_bound a identity)
% 0.12/0.33 (greatest_lower_bound a identity)
% 0.12/0.33 [] by prove_p19
% 215.49/54.23 Statistics :
% 215.49/54.23 Max weight : 21
% 215.49/54.23 Found proof, 53.902434s
% 215.49/54.23 % SZS status Unsatisfiable for theBenchmark.p
% 215.49/54.23 % SZS output start CNFRefutation for theBenchmark.p
% 215.49/54.23 Id : 9, {_}: least_upper_bound ?24 ?24 =>= ?24 [24] by idempotence_of_lub ?24
% 215.49/54.23 Id : 190, {_}: multiply (least_upper_bound ?425 ?426) ?427 =<= least_upper_bound (multiply ?425 ?427) (multiply ?426 ?427) [427, 426, 425] by monotony_lub2 ?425 ?426 ?427
% 215.49/54.23 Id : 99, {_}: greatest_lower_bound ?257 (least_upper_bound ?257 ?258) =>= ?257 [258, 257] by glb_absorbtion ?257 ?258
% 215.49/54.23 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
% 215.49/54.23 Id : 10, {_}: greatest_lower_bound ?26 ?26 =>= ?26 [26] by idempotence_of_gld ?26
% 215.49/54.23 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
% 215.49/54.23 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
% 215.49/54.23 Id : 85, {_}: least_upper_bound ?223 (greatest_lower_bound ?223 ?224) =>= ?223 [224, 223] by lub_absorbtion ?223 ?224
% 215.49/54.23 Id : 152, {_}: multiply ?361 (greatest_lower_bound ?362 ?363) =<= greatest_lower_bound (multiply ?361 ?362) (multiply ?361 ?363) [363, 362, 361] by monotony_glb1 ?361 ?362 ?363
% 215.49/54.23 Id : 19, {_}: inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53) [54, 53] by p19_3 ?53 ?54
% 215.49/54.23 Id : 220, {_}: multiply (greatest_lower_bound ?492 ?493) ?494 =<= greatest_lower_bound (multiply ?492 ?494) (multiply ?493 ?494) [494, 493, 492] by monotony_glb2 ?492 ?493 ?494
% 215.49/54.24 Id : 24, {_}: multiply (multiply ?63 ?64) ?65 =>= multiply ?63 (multiply ?64 ?65) [65, 64, 63] by associativity ?63 ?64 ?65
% 215.49/54.24 Id : 12, {_}: greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31 [32, 31] by glb_absorbtion ?31 ?32
% 215.49/54.24 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
% 215.49/54.24 Id : 5, {_}: greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10 [11, 10] by symmetry_of_glb ?10 ?11
% 215.49/54.24 Id : 46, {_}: greatest_lower_bound ?120 (greatest_lower_bound ?121 ?122) =<= greatest_lower_bound (greatest_lower_bound ?120 ?121) ?122 [122, 121, 120] by associativity_of_glb ?120 ?121 ?122
% 215.49/54.24 Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 215.49/54.24 Id : 17, {_}: inverse identity =>= identity [] by p19_1
% 215.49/54.24 Id : 266, {_}: inverse (multiply ?586 ?587) =<= multiply (inverse ?587) (inverse ?586) [587, 586] by p19_3 ?586 ?587
% 215.49/54.24 Id : 11, {_}: least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28 [29, 28] by lub_absorbtion ?28 ?29
% 215.49/54.24 Id : 117, {_}: multiply ?300 (least_upper_bound ?301 ?302) =<= least_upper_bound (multiply ?300 ?301) (multiply ?300 ?302) [302, 301, 300] by monotony_lub1 ?300 ?301 ?302
% 215.49/54.24 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
% 215.49/54.24 Id : 6, {_}: least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13 [14, 13] by symmetry_of_lub ?13 ?14
% 215.49/54.24 Id : 60, {_}: least_upper_bound ?157 (least_upper_bound ?158 ?159) =<= least_upper_bound (least_upper_bound ?157 ?158) ?159 [159, 158, 157] by associativity_of_lub ?157 ?158 ?159
% 215.49/54.24 Id : 18, {_}: inverse (inverse ?51) =>= ?51 [51] by p19_2 ?51
% 215.49/54.24 Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 215.49/54.24 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
% 215.49/54.24 Id : 4, {_}: multiply (multiply ?6 ?7) ?8 =>= multiply ?6 (multiply ?7 ?8) [8, 7, 6] by associativity ?6 ?7 ?8
% 215.49/54.24 Id : 250, {_}: multiply ?539 (inverse ?539) =>= identity [539] by Super 3 with 18 at 1,2
% 215.49/54.24 Id : 357, {_}: multiply ?711 (least_upper_bound (inverse ?711) ?712) =>= least_upper_bound identity (multiply ?711 ?712) [712, 711] by Super 13 with 250 at 1,3
% 215.49/54.24 Id : 61, {_}: least_upper_bound ?161 (least_upper_bound ?162 ?163) =<= least_upper_bound (least_upper_bound ?162 ?161) ?163 [163, 162, 161] by Super 60 with 6 at 1,3
% 215.49/54.24 Id : 67, {_}: least_upper_bound ?161 (least_upper_bound ?162 ?163) =?= least_upper_bound ?162 (least_upper_bound ?161 ?163) [163, 162, 161] by Demod 61 with 8 at 3
% 215.49/54.24 Id : 119, {_}: multiply (inverse ?307) (least_upper_bound ?308 ?307) =>= least_upper_bound (multiply (inverse ?307) ?308) identity [308, 307] by Super 117 with 3 at 2,3
% 215.49/54.24 Id : 1110, {_}: multiply (inverse ?1836) (least_upper_bound ?1837 ?1836) =>= least_upper_bound identity (multiply (inverse ?1836) ?1837) [1837, 1836] by Demod 119 with 6 at 3
% 215.49/54.24 Id : 6543, {_}: multiply (inverse (greatest_lower_bound ?10896 ?10897)) ?10896 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?10896 ?10897)) ?10896) [10897, 10896] by Super 1110 with 11 at 2,2
% 215.49/54.24 Id : 267, {_}: inverse (multiply identity ?589) =<= multiply (inverse ?589) identity [589] by Super 266 with 17 at 2,3
% 215.49/54.24 Id : 298, {_}: inverse ?643 =<= multiply (inverse ?643) identity [643] by Demod 267 with 2 at 1,2
% 215.49/54.24 Id : 302, {_}: inverse (inverse ?650) =<= multiply ?650 identity [650] by Super 298 with 18 at 1,3
% 215.49/54.24 Id : 313, {_}: ?650 =<= multiply ?650 identity [650] by Demod 302 with 18 at 2
% 215.49/54.24 Id : 6572, {_}: multiply (inverse (greatest_lower_bound identity ?10993)) identity =>= least_upper_bound identity (inverse (greatest_lower_bound identity ?10993)) [10993] by Super 6543 with 313 at 2,3
% 215.49/54.24 Id : 6685, {_}: inverse (greatest_lower_bound identity ?10993) =<= least_upper_bound identity (inverse (greatest_lower_bound identity ?10993)) [10993] by Demod 6572 with 313 at 2
% 215.49/54.24 Id : 6711, {_}: least_upper_bound identity (least_upper_bound ?11059 (inverse (greatest_lower_bound identity ?11060))) =>= least_upper_bound ?11059 (inverse (greatest_lower_bound identity ?11060)) [11060, 11059] by Super 67 with 6685 at 2,3
% 215.49/54.24 Id : 47, {_}: greatest_lower_bound ?124 (greatest_lower_bound ?125 ?126) =<= greatest_lower_bound (greatest_lower_bound ?125 ?124) ?126 [126, 125, 124] by Super 46 with 5 at 1,3
% 215.49/54.24 Id : 53, {_}: greatest_lower_bound ?124 (greatest_lower_bound ?125 ?126) =?= greatest_lower_bound ?125 (greatest_lower_bound ?124 ?126) [126, 125, 124] by Demod 47 with 7 at 3
% 215.49/54.24 Id : 6704, {_}: greatest_lower_bound identity (inverse (greatest_lower_bound identity ?11043)) =>= identity [11043] by Super 12 with 6685 at 2,2
% 215.49/54.24 Id : 6852, {_}: greatest_lower_bound identity (greatest_lower_bound ?11164 (inverse (greatest_lower_bound identity ?11165))) =>= greatest_lower_bound ?11164 identity [11165, 11164] by Super 53 with 6704 at 2,3
% 215.49/54.24 Id : 10223, {_}: least_upper_bound identity (least_upper_bound ?15717 (inverse (greatest_lower_bound ?15718 identity))) =<= least_upper_bound ?15717 (inverse (greatest_lower_bound identity (greatest_lower_bound ?15718 (inverse (greatest_lower_bound identity ?15719))))) [15719, 15718, 15717] by Super 6711 with 6852 at 1,2,2,2
% 215.49/54.24 Id : 10444, {_}: least_upper_bound identity (least_upper_bound ?15717 (inverse (greatest_lower_bound ?15718 identity))) =>= least_upper_bound ?15717 (inverse (greatest_lower_bound ?15718 identity)) [15718, 15717] by Demod 10223 with 6852 at 1,2,3
% 215.49/54.24 Id : 6717, {_}: inverse (greatest_lower_bound identity ?11077) =<= least_upper_bound identity (inverse (greatest_lower_bound identity ?11077)) [11077] by Demod 6572 with 313 at 2
% 215.49/54.24 Id : 6720, {_}: inverse (greatest_lower_bound identity ?11083) =<= least_upper_bound identity (inverse (greatest_lower_bound ?11083 identity)) [11083] by Super 6717 with 5 at 1,2,3
% 215.49/54.24 Id : 7016, {_}: least_upper_bound identity (least_upper_bound ?11320 (inverse (greatest_lower_bound ?11321 identity))) =>= least_upper_bound ?11320 (inverse (greatest_lower_bound identity ?11321)) [11321, 11320] by Super 67 with 6720 at 2,3
% 215.49/54.24 Id : 17363, {_}: least_upper_bound ?15717 (inverse (greatest_lower_bound identity ?15718)) =?= least_upper_bound ?15717 (inverse (greatest_lower_bound ?15718 identity)) [15718, 15717] by Demod 10444 with 7016 at 2
% 215.49/54.24 Id : 26, {_}: multiply identity ?70 =<= multiply (inverse ?71) (multiply ?71 ?70) [71, 70] by Super 24 with 3 at 1,2
% 215.49/54.24 Id : 30, {_}: ?70 =<= multiply (inverse ?71) (multiply ?71 ?70) [71, 70] by Demod 26 with 2 at 2
% 215.49/54.24 Id : 45719, {_}: least_upper_bound (inverse ?53475) ?53476 =<= multiply (inverse ?53475) (least_upper_bound identity (multiply ?53475 ?53476)) [53476, 53475] by Super 30 with 357 at 2,3
% 215.49/54.24 Id : 225, {_}: multiply (greatest_lower_bound (inverse ?510) ?511) ?510 =>= greatest_lower_bound identity (multiply ?511 ?510) [511, 510] by Super 220 with 3 at 1,3
% 215.49/54.24 Id : 45729, {_}: least_upper_bound (inverse (greatest_lower_bound (inverse ?53504) ?53505)) ?53504 =<= multiply (inverse (greatest_lower_bound (inverse ?53504) ?53505)) (least_upper_bound identity (greatest_lower_bound identity (multiply ?53505 ?53504))) [53505, 53504] by Super 45719 with 225 at 2,2,3
% 215.49/54.24 Id : 45856, {_}: least_upper_bound ?53504 (inverse (greatest_lower_bound (inverse ?53504) ?53505)) =<= multiply (inverse (greatest_lower_bound (inverse ?53504) ?53505)) (least_upper_bound identity (greatest_lower_bound identity (multiply ?53505 ?53504))) [53505, 53504] by Demod 45729 with 6 at 2
% 215.49/54.24 Id : 45857, {_}: least_upper_bound ?53504 (inverse (greatest_lower_bound (inverse ?53504) ?53505)) =?= multiply (inverse (greatest_lower_bound (inverse ?53504) ?53505)) identity [53505, 53504] by Demod 45856 with 11 at 2,3
% 215.49/54.24 Id : 45858, {_}: least_upper_bound ?53504 (inverse (greatest_lower_bound (inverse ?53504) ?53505)) =>= inverse (greatest_lower_bound (inverse ?53504) ?53505) [53505, 53504] by Demod 45857 with 313 at 3
% 215.49/54.24 Id : 46437, {_}: least_upper_bound ?54332 (inverse (greatest_lower_bound identity (inverse ?54332))) =>= inverse (greatest_lower_bound (inverse ?54332) identity) [54332] by Super 17363 with 45858 at 3
% 215.49/54.24 Id : 6736, {_}: inverse (greatest_lower_bound identity ?11121) =<= least_upper_bound identity (inverse (greatest_lower_bound ?11121 identity)) [11121] by Super 6717 with 5 at 1,2,3
% 215.49/54.24 Id : 7189, {_}: inverse (greatest_lower_bound identity ?11573) =?= inverse (greatest_lower_bound identity ?11573) [11573] by Demod 6736 with 6720 at 3
% 215.49/54.24 Id : 7192, {_}: inverse (greatest_lower_bound identity ?11579) =?= inverse (greatest_lower_bound ?11579 identity) [11579] by Super 7189 with 5 at 1,3
% 215.49/54.24 Id : 46667, {_}: least_upper_bound ?54332 (inverse (greatest_lower_bound identity (inverse ?54332))) =>= inverse (greatest_lower_bound identity (inverse ?54332)) [54332] by Demod 46437 with 7192 at 3
% 215.49/54.24 Id : 47070, {_}: multiply ?54777 (inverse (greatest_lower_bound identity (inverse (inverse ?54777)))) =<= least_upper_bound identity (multiply ?54777 (inverse (greatest_lower_bound identity (inverse (inverse ?54777))))) [54777] by Super 357 with 46667 at 2,2
% 215.49/54.24 Id : 47289, {_}: multiply ?54777 (inverse (greatest_lower_bound identity ?54777)) =<= least_upper_bound identity (multiply ?54777 (inverse (greatest_lower_bound identity (inverse (inverse ?54777))))) [54777] by Demod 47070 with 18 at 2,1,2,2
% 215.49/54.24 Id : 53216, {_}: multiply ?60462 (inverse (greatest_lower_bound identity ?60462)) =<= least_upper_bound identity (multiply ?60462 (inverse (greatest_lower_bound identity ?60462))) [60462] by Demod 47289 with 18 at 2,1,2,2,3
% 215.49/54.24 Id : 1113, {_}: multiply (inverse (greatest_lower_bound ?1844 ?1845)) ?1844 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?1844 ?1845)) ?1844) [1845, 1844] by Super 1110 with 11 at 2,2
% 215.49/54.24 Id : 11905, {_}: multiply (inverse (greatest_lower_bound ?17625 identity)) ?17625 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound identity ?17625)) ?17625) [17625] by Super 1113 with 7192 at 1,2,3
% 215.49/54.24 Id : 20053, {_}: greatest_lower_bound identity (multiply (inverse (greatest_lower_bound ?26828 identity)) ?26828) =>= identity [26828] by Super 12 with 11905 at 2,2
% 215.49/54.24 Id : 20056, {_}: greatest_lower_bound identity (multiply (inverse (greatest_lower_bound identity ?26834)) ?26834) =>= identity [26834] by Super 20053 with 5 at 1,1,2,2
% 215.49/54.24 Id : 53248, {_}: multiply (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543) (inverse (greatest_lower_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543))) =>= least_upper_bound identity (multiply (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543) (inverse identity)) [60543] by Super 53216 with 20056 at 1,2,2,3
% 215.49/54.24 Id : 53686, {_}: multiply (inverse (greatest_lower_bound identity ?60543)) (multiply ?60543 (inverse (greatest_lower_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543)))) =>= least_upper_bound identity (multiply (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543) (inverse identity)) [60543] by Demod 53248 with 4 at 2
% 215.49/54.24 Id : 53687, {_}: multiply (inverse (greatest_lower_bound identity ?60543)) (multiply ?60543 (inverse (greatest_lower_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543)))) =>= least_upper_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) (multiply ?60543 (inverse identity))) [60543] by Demod 53686 with 4 at 2,3
% 215.49/54.24 Id : 268, {_}: inverse (multiply (inverse ?591) ?592) =>= multiply (inverse ?592) ?591 [592, 591] by Super 266 with 18 at 2,3
% 215.49/54.24 Id : 390, {_}: inverse (multiply ?755 (multiply (inverse ?756) ?757)) =<= multiply (multiply (inverse ?757) ?756) (inverse ?755) [757, 756, 755] by Super 19 with 268 at 1,3
% 215.49/54.24 Id : 404, {_}: inverse (multiply ?755 (multiply (inverse ?756) ?757)) =<= multiply (inverse ?757) (multiply ?756 (inverse ?755)) [757, 756, 755] by Demod 390 with 4 at 3
% 215.49/54.24 Id : 53688, {_}: inverse (multiply (greatest_lower_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543)) (multiply (inverse ?60543) (greatest_lower_bound identity ?60543))) =>= least_upper_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) (multiply ?60543 (inverse identity))) [60543] by Demod 53687 with 404 at 2
% 215.49/54.24 Id : 53689, {_}: inverse (multiply (greatest_lower_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543)) (multiply (inverse ?60543) (greatest_lower_bound identity ?60543))) =>= least_upper_bound identity (inverse (multiply identity (multiply (inverse ?60543) (greatest_lower_bound identity ?60543)))) [60543] by Demod 53688 with 404 at 2,3
% 215.49/54.24 Id : 53690, {_}: inverse (multiply identity (multiply (inverse ?60543) (greatest_lower_bound identity ?60543))) =<= least_upper_bound identity (inverse (multiply identity (multiply (inverse ?60543) (greatest_lower_bound identity ?60543)))) [60543] by Demod 53689 with 20056 at 1,1,2
% 215.49/54.24 Id : 154, {_}: multiply (inverse ?368) (greatest_lower_bound ?369 ?368) =>= greatest_lower_bound (multiply (inverse ?368) ?369) identity [369, 368] by Super 152 with 3 at 2,3
% 215.49/54.24 Id : 170, {_}: multiply (inverse ?368) (greatest_lower_bound ?369 ?368) =>= greatest_lower_bound identity (multiply (inverse ?368) ?369) [369, 368] by Demod 154 with 5 at 3
% 215.49/54.24 Id : 53691, {_}: inverse (multiply identity (greatest_lower_bound identity (multiply (inverse ?60543) identity))) =<= least_upper_bound identity (inverse (multiply identity (multiply (inverse ?60543) (greatest_lower_bound identity ?60543)))) [60543] by Demod 53690 with 170 at 2,1,2
% 215.49/54.24 Id : 53692, {_}: inverse (multiply identity (greatest_lower_bound identity (multiply (inverse ?60543) identity))) =<= least_upper_bound identity (inverse (multiply (inverse ?60543) (greatest_lower_bound identity ?60543))) [60543] by Demod 53691 with 2 at 1,2,3
% 215.49/54.24 Id : 53693, {_}: inverse (greatest_lower_bound identity (multiply (inverse ?60543) identity)) =<= least_upper_bound identity (inverse (multiply (inverse ?60543) (greatest_lower_bound identity ?60543))) [60543] by Demod 53692 with 2 at 1,2
% 215.49/54.24 Id : 53694, {_}: inverse (greatest_lower_bound identity (multiply (inverse ?60543) identity)) =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543) [60543] by Demod 53693 with 268 at 2,3
% 215.49/54.24 Id : 53695, {_}: inverse (greatest_lower_bound identity (inverse ?60543)) =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound identity ?60543)) ?60543) [60543] by Demod 53694 with 313 at 2,1,2
% 215.49/54.24 Id : 86, {_}: least_upper_bound ?226 (greatest_lower_bound ?227 ?226) =>= ?226 [227, 226] by Super 85 with 5 at 2,2
% 215.49/54.24 Id : 1115, {_}: multiply (inverse (greatest_lower_bound ?1850 ?1851)) ?1851 =<= least_upper_bound identity (multiply (inverse (greatest_lower_bound ?1850 ?1851)) ?1851) [1851, 1850] by Super 1110 with 86 at 2,2
% 215.49/54.24 Id : 53696, {_}: inverse (greatest_lower_bound identity (inverse ?60543)) =<= multiply (inverse (greatest_lower_bound identity ?60543)) ?60543 [60543] by Demod 53695 with 1115 at 3
% 215.49/54.24 Id : 362, {_}: multiply ?724 (greatest_lower_bound (inverse ?724) ?725) =>= greatest_lower_bound identity (multiply ?724 ?725) [725, 724] by Super 14 with 250 at 1,3
% 215.49/54.24 Id : 47066, {_}: greatest_lower_bound ?54769 (inverse (greatest_lower_bound identity (inverse ?54769))) =>= ?54769 [54769] by Super 12 with 46667 at 2,2
% 215.49/54.24 Id : 47836, {_}: multiply ?55074 (inverse ?55074) =<= greatest_lower_bound identity (multiply ?55074 (inverse (greatest_lower_bound identity (inverse (inverse ?55074))))) [55074] by Super 362 with 47066 at 2,2
% 215.49/54.24 Id : 48053, {_}: identity =<= greatest_lower_bound identity (multiply ?55074 (inverse (greatest_lower_bound identity (inverse (inverse ?55074))))) [55074] by Demod 47836 with 250 at 2
% 215.49/54.24 Id : 48054, {_}: identity =<= greatest_lower_bound identity (multiply ?55074 (inverse (greatest_lower_bound identity ?55074))) [55074] by Demod 48053 with 18 at 2,1,2,2,3
% 215.49/54.24 Id : 54274, {_}: inverse (greatest_lower_bound identity (inverse (multiply ?61045 (inverse (greatest_lower_bound identity ?61045))))) =>= multiply (inverse identity) (multiply ?61045 (inverse (greatest_lower_bound identity ?61045))) [61045] by Super 53696 with 48054 at 1,1,3
% 215.49/54.24 Id : 270, {_}: inverse (multiply ?596 (inverse ?597)) =>= multiply ?597 (inverse ?596) [597, 596] by Super 266 with 18 at 1,3
% 215.49/54.24 Id : 54346, {_}: inverse (greatest_lower_bound identity (multiply (greatest_lower_bound identity ?61045) (inverse ?61045))) =<= multiply (inverse identity) (multiply ?61045 (inverse (greatest_lower_bound identity ?61045))) [61045] by Demod 54274 with 270 at 2,1,2
% 215.49/54.24 Id : 54347, {_}: inverse (greatest_lower_bound identity (multiply (greatest_lower_bound identity ?61045) (inverse ?61045))) =<= inverse (multiply (greatest_lower_bound identity ?61045) (multiply (inverse ?61045) identity)) [61045] by Demod 54346 with 404 at 3
% 215.49/54.24 Id : 363, {_}: multiply (greatest_lower_bound ?727 ?728) (inverse ?728) =>= greatest_lower_bound (multiply ?727 (inverse ?728)) identity [728, 727] by Super 16 with 250 at 2,3
% 215.49/54.24 Id : 372, {_}: multiply (greatest_lower_bound ?727 ?728) (inverse ?728) =>= greatest_lower_bound identity (multiply ?727 (inverse ?728)) [728, 727] by Demod 363 with 5 at 3
% 215.49/54.24 Id : 54348, {_}: inverse (greatest_lower_bound identity (greatest_lower_bound identity (multiply identity (inverse ?61045)))) =<= inverse (multiply (greatest_lower_bound identity ?61045) (multiply (inverse ?61045) identity)) [61045] by Demod 54347 with 372 at 2,1,2
% 215.49/54.24 Id : 54349, {_}: inverse (greatest_lower_bound identity (greatest_lower_bound identity (multiply identity (inverse ?61045)))) =?= inverse (multiply (greatest_lower_bound identity ?61045) (inverse ?61045)) [61045] by Demod 54348 with 313 at 2,1,3
% 215.49/54.24 Id : 77, {_}: greatest_lower_bound ?199 (greatest_lower_bound ?199 ?200) =>= greatest_lower_bound ?199 ?200 [200, 199] by Super 7 with 10 at 1,3
% 215.49/54.24 Id : 54350, {_}: inverse (greatest_lower_bound identity (multiply identity (inverse ?61045))) =<= inverse (multiply (greatest_lower_bound identity ?61045) (inverse ?61045)) [61045] by Demod 54349 with 77 at 1,2
% 215.49/54.24 Id : 54351, {_}: inverse (greatest_lower_bound identity (multiply identity (inverse ?61045))) =?= multiply ?61045 (inverse (greatest_lower_bound identity ?61045)) [61045] by Demod 54350 with 270 at 3
% 215.49/54.24 Id : 54352, {_}: inverse (greatest_lower_bound identity (inverse ?61045)) =<= multiply ?61045 (inverse (greatest_lower_bound identity ?61045)) [61045] by Demod 54351 with 2 at 2,1,2
% 215.49/54.24 Id : 180531, {_}: multiply (inverse (greatest_lower_bound identity (inverse ?170612))) ?170613 =<= multiply ?170612 (multiply (inverse (greatest_lower_bound identity ?170612)) ?170613) [170613, 170612] by Super 4 with 54352 at 1,2
% 215.49/54.24 Id : 354, {_}: multiply (least_upper_bound ?702 ?703) (inverse ?703) =>= least_upper_bound (multiply ?702 (inverse ?703)) identity [703, 702] by Super 15 with 250 at 2,3
% 215.49/54.24 Id : 377, {_}: multiply (least_upper_bound ?702 ?703) (inverse ?703) =>= least_upper_bound identity (multiply ?702 (inverse ?703)) [703, 702] by Demod 354 with 6 at 3
% 215.49/54.24 Id : 7015, {_}: multiply (inverse (greatest_lower_bound identity ?11318)) (inverse (inverse (greatest_lower_bound ?11318 identity))) =>= least_upper_bound identity (multiply identity (inverse (inverse (greatest_lower_bound ?11318 identity)))) [11318] by Super 377 with 6720 at 1,2
% 215.49/54.24 Id : 7041, {_}: inverse (multiply (inverse (greatest_lower_bound ?11318 identity)) (greatest_lower_bound identity ?11318)) =?= least_upper_bound identity (multiply identity (inverse (inverse (greatest_lower_bound ?11318 identity)))) [11318] by Demod 7015 with 19 at 2
% 215.49/54.24 Id : 7042, {_}: inverse (multiply (inverse (greatest_lower_bound ?11318 identity)) (greatest_lower_bound identity ?11318)) =>= least_upper_bound identity (inverse (inverse (greatest_lower_bound ?11318 identity))) [11318] by Demod 7041 with 2 at 2,3
% 215.49/54.24 Id : 7043, {_}: multiply (inverse (greatest_lower_bound identity ?11318)) (greatest_lower_bound ?11318 identity) =>= least_upper_bound identity (inverse (inverse (greatest_lower_bound ?11318 identity))) [11318] by Demod 7042 with 268 at 2
% 215.49/54.24 Id : 7044, {_}: multiply (inverse (greatest_lower_bound identity ?11318)) (greatest_lower_bound ?11318 identity) =>= least_upper_bound identity (greatest_lower_bound ?11318 identity) [11318] by Demod 7043 with 18 at 2,3
% 215.49/54.24 Id : 7045, {_}: multiply (inverse (greatest_lower_bound identity ?11318)) (greatest_lower_bound ?11318 identity) =>= identity [11318] by Demod 7044 with 86 at 3
% 215.49/54.24 Id : 180635, {_}: multiply (inverse (greatest_lower_bound identity (inverse ?170971))) (greatest_lower_bound ?170971 identity) =>= multiply ?170971 identity [170971] by Super 180531 with 7045 at 2,3
% 215.49/54.24 Id : 181268, {_}: multiply (inverse (greatest_lower_bound identity (inverse ?170971))) (greatest_lower_bound ?170971 identity) =>= ?170971 [170971] by Demod 180635 with 313 at 3
% 215.49/54.24 Id : 100, {_}: greatest_lower_bound ?260 (least_upper_bound ?261 ?260) =>= ?260 [261, 260] by Super 99 with 6 at 2,2
% 215.49/54.24 Id : 359, {_}: multiply identity ?715 =<= multiply ?716 (multiply (inverse ?716) ?715) [716, 715] by Super 4 with 250 at 1,2
% 215.49/54.24 Id : 2566, {_}: ?4131 =<= multiply ?4132 (multiply (inverse ?4132) ?4131) [4132, 4131] by Demod 359 with 2 at 2
% 215.49/54.24 Id : 2935, {_}: inverse ?4609 =<= multiply ?4610 (inverse (multiply ?4609 ?4610)) [4610, 4609] by Super 2566 with 19 at 2,3
% 215.49/54.24 Id : 195, {_}: multiply (least_upper_bound (inverse ?443) ?444) ?443 =>= least_upper_bound identity (multiply ?444 ?443) [444, 443] by Super 190 with 3 at 1,3
% 215.49/54.24 Id : 2943, {_}: inverse (least_upper_bound (inverse ?4632) ?4633) =<= multiply ?4632 (inverse (least_upper_bound identity (multiply ?4633 ?4632))) [4633, 4632] by Super 2935 with 195 at 1,2,3
% 215.49/54.24 Id : 74337, {_}: inverse (inverse (least_upper_bound (inverse ?79526) ?79527)) =<= multiply (least_upper_bound identity (multiply ?79527 ?79526)) (inverse ?79526) [79527, 79526] by Super 270 with 2943 at 1,2
% 215.81/54.27 Id : 282880, {_}: least_upper_bound (inverse ?241618) ?241619 =<= multiply (least_upper_bound identity (multiply ?241619 ?241618)) (inverse ?241618) [241619, 241618] by Demod 74337 with 18 at 2
% 215.81/54.27 Id : 471, {_}: inverse (multiply ?885 (inverse ?886)) =>= multiply ?886 (inverse ?885) [886, 885] by Super 266 with 18 at 1,3
% 215.81/54.27 Id : 478, {_}: inverse (multiply ?905 (multiply ?906 (inverse ?907))) =>= multiply ?907 (inverse (multiply ?905 ?906)) [907, 906, 905] by Super 471 with 4 at 1,2
% 215.81/54.27 Id : 54682, {_}: inverse (multiply ?61270 (inverse (greatest_lower_bound identity (inverse ?61271)))) =<= multiply (greatest_lower_bound identity ?61271) (inverse (multiply ?61270 ?61271)) [61271, 61270] by Super 478 with 54352 at 2,1,2
% 215.81/54.27 Id : 181527, {_}: multiply (greatest_lower_bound identity (inverse ?171281)) (inverse ?171282) =<= multiply (greatest_lower_bound identity ?171281) (inverse (multiply ?171282 ?171281)) [171282, 171281] by Demod 54682 with 270 at 2
% 215.81/54.27 Id : 72, {_}: least_upper_bound ?186 (least_upper_bound ?186 ?187) =>= least_upper_bound ?186 ?187 [187, 186] by Super 8 with 9 at 1,3
% 215.81/54.27 Id : 1114, {_}: multiply (inverse (least_upper_bound ?1847 ?1848)) (least_upper_bound ?1847 ?1848) =>= least_upper_bound identity (multiply (inverse (least_upper_bound ?1847 ?1848)) ?1847) [1848, 1847] by Super 1110 with 72 at 2,2
% 215.81/54.27 Id : 1144, {_}: identity =<= least_upper_bound identity (multiply (inverse (least_upper_bound ?1847 ?1848)) ?1847) [1848, 1847] by Demod 1114 with 3 at 2
% 215.81/54.27 Id : 20955, {_}: identity =<= least_upper_bound identity (multiply (inverse (least_upper_bound ?27523 ?27524)) ?27523) [27524, 27523] by Demod 1114 with 3 at 2
% 215.81/54.27 Id : 21016, {_}: identity =<= least_upper_bound identity (inverse (least_upper_bound identity ?27697)) [27697] by Super 20955 with 313 at 2,3
% 215.81/54.27 Id : 21173, {_}: greatest_lower_bound (inverse (least_upper_bound identity ?27746)) identity =>= inverse (least_upper_bound identity ?27746) [27746] by Super 100 with 21016 at 2,2
% 215.81/54.27 Id : 21537, {_}: greatest_lower_bound identity (inverse (least_upper_bound identity ?28152)) =>= inverse (least_upper_bound identity ?28152) [28152] by Demod 21173 with 5 at 2
% 215.81/54.27 Id : 21540, {_}: greatest_lower_bound identity (inverse (least_upper_bound ?28158 identity)) =>= inverse (least_upper_bound identity ?28158) [28158] by Super 21537 with 6 at 1,2,2
% 215.81/54.27 Id : 21187, {_}: identity =<= least_upper_bound identity (inverse (least_upper_bound identity ?27780)) [27780] by Super 20955 with 313 at 2,3
% 215.81/54.27 Id : 21190, {_}: identity =<= least_upper_bound identity (inverse (least_upper_bound ?27786 identity)) [27786] by Super 21187 with 6 at 1,2,3
% 215.81/54.27 Id : 21355, {_}: greatest_lower_bound (inverse (least_upper_bound ?27912 identity)) identity =>= inverse (least_upper_bound ?27912 identity) [27912] by Super 100 with 21190 at 2,2
% 215.81/54.27 Id : 21428, {_}: greatest_lower_bound identity (inverse (least_upper_bound ?27912 identity)) =>= inverse (least_upper_bound ?27912 identity) [27912] by Demod 21355 with 5 at 2
% 215.81/54.27 Id : 22614, {_}: inverse (least_upper_bound ?28158 identity) =?= inverse (least_upper_bound identity ?28158) [28158] by Demod 21540 with 21428 at 2
% 215.81/54.27 Id : 22681, {_}: identity =<= least_upper_bound identity (multiply (inverse (least_upper_bound identity ?29405)) ?29405) [29405] by Super 1144 with 22614 at 1,2,3
% 215.81/54.27 Id : 34851, {_}: greatest_lower_bound (multiply (inverse (least_upper_bound identity ?42665)) ?42665) identity =>= multiply (inverse (least_upper_bound identity ?42665)) ?42665 [42665] by Super 100 with 22681 at 2,2
% 215.81/54.27 Id : 39859, {_}: greatest_lower_bound identity (multiply (inverse (least_upper_bound identity ?48184)) ?48184) =>= multiply (inverse (least_upper_bound identity ?48184)) ?48184 [48184] by Demod 34851 with 5 at 2
% 215.81/54.27 Id : 39862, {_}: greatest_lower_bound identity (multiply (inverse (least_upper_bound ?48190 identity)) ?48190) =>= multiply (inverse (least_upper_bound identity ?48190)) ?48190 [48190] by Super 39859 with 6 at 1,1,2,2
% 215.81/54.27 Id : 1578, {_}: multiply (inverse ?2637) (greatest_lower_bound ?2638 ?2637) =>= greatest_lower_bound identity (multiply (inverse ?2637) ?2638) [2638, 2637] by Demod 154 with 5 at 3
% 215.81/54.27 Id : 1581, {_}: multiply (inverse (least_upper_bound ?2645 ?2646)) ?2645 =<= greatest_lower_bound identity (multiply (inverse (least_upper_bound ?2645 ?2646)) ?2645) [2646, 2645] by Super 1578 with 12 at 2,2
% 215.81/54.27 Id : 43905, {_}: multiply (inverse (least_upper_bound ?48190 identity)) ?48190 =?= multiply (inverse (least_upper_bound identity ?48190)) ?48190 [48190] by Demod 39862 with 1581 at 2
% 215.81/54.27 Id : 39893, {_}: greatest_lower_bound identity (multiply (inverse (least_upper_bound ?48271 identity)) ?48271) =>= multiply (inverse (least_upper_bound identity ?48271)) ?48271 [48271] by Super 39859 with 6 at 1,1,2,2
% 215.81/54.27 Id : 41788, {_}: multiply (inverse (least_upper_bound identity ?48271)) ?48271 =?= multiply (inverse (least_upper_bound identity ?48271)) ?48271 [48271] by Demod 39893 with 39862 at 2
% 215.81/54.27 Id : 45736, {_}: least_upper_bound (inverse (greatest_lower_bound ?53524 ?53525)) (inverse ?53525) =<= multiply (inverse (greatest_lower_bound ?53524 ?53525)) (least_upper_bound identity (greatest_lower_bound identity (multiply ?53524 (inverse ?53525)))) [53525, 53524] by Super 45719 with 372 at 2,2,3
% 215.81/54.27 Id : 45876, {_}: least_upper_bound (inverse ?53525) (inverse (greatest_lower_bound ?53524 ?53525)) =<= multiply (inverse (greatest_lower_bound ?53524 ?53525)) (least_upper_bound identity (greatest_lower_bound identity (multiply ?53524 (inverse ?53525)))) [53524, 53525] by Demod 45736 with 6 at 2
% 215.81/54.27 Id : 45877, {_}: least_upper_bound (inverse ?53525) (inverse (greatest_lower_bound ?53524 ?53525)) =>= multiply (inverse (greatest_lower_bound ?53524 ?53525)) identity [53524, 53525] by Demod 45876 with 11 at 2,3
% 215.81/54.27 Id : 51345, {_}: least_upper_bound (inverse ?57624) (inverse (greatest_lower_bound ?57625 ?57624)) =>= inverse (greatest_lower_bound ?57625 ?57624) [57625, 57624] by Demod 45877 with 313 at 3
% 215.81/54.27 Id : 51348, {_}: least_upper_bound (inverse (least_upper_bound ?57632 ?57633)) (inverse ?57632) =>= inverse (greatest_lower_bound ?57632 (least_upper_bound ?57632 ?57633)) [57633, 57632] by Super 51345 with 12 at 1,2,2
% 215.81/54.27 Id : 51555, {_}: least_upper_bound (inverse ?57632) (inverse (least_upper_bound ?57632 ?57633)) =>= inverse (greatest_lower_bound ?57632 (least_upper_bound ?57632 ?57633)) [57633, 57632] by Demod 51348 with 6 at 2
% 215.81/54.27 Id : 57354, {_}: least_upper_bound (inverse ?64271) (inverse (least_upper_bound ?64271 ?64272)) =>= inverse ?64271 [64272, 64271] by Demod 51555 with 12 at 1,3
% 215.81/54.27 Id : 57831, {_}: least_upper_bound (inverse ?64727) (inverse (least_upper_bound identity ?64727)) =>= inverse ?64727 [64727] by Super 57354 with 22614 at 2,2
% 215.81/54.27 Id : 57901, {_}: least_upper_bound ?64896 (inverse (least_upper_bound identity (inverse ?64896))) =>= inverse (inverse ?64896) [64896] by Super 57831 with 18 at 1,2
% 215.81/54.27 Id : 58199, {_}: least_upper_bound ?64896 (inverse (least_upper_bound identity (inverse ?64896))) =>= ?64896 [64896] by Demod 57901 with 18 at 3
% 215.81/54.27 Id : 58906, {_}: multiply ?65414 (inverse ?65414) =<= least_upper_bound identity (multiply ?65414 (inverse (least_upper_bound identity (inverse (inverse ?65414))))) [65414] by Super 357 with 58199 at 2,2
% 215.81/54.27 Id : 59186, {_}: identity =<= least_upper_bound identity (multiply ?65414 (inverse (least_upper_bound identity (inverse (inverse ?65414))))) [65414] by Demod 58906 with 250 at 2
% 215.81/54.27 Id : 59187, {_}: identity =<= least_upper_bound identity (multiply ?65414 (inverse (least_upper_bound identity ?65414))) [65414] by Demod 59186 with 18 at 2,1,2,2,3
% 215.81/54.27 Id : 62951, {_}: multiply (inverse (least_upper_bound identity (multiply ?68643 (inverse (least_upper_bound identity ?68643))))) (multiply ?68643 (inverse (least_upper_bound identity ?68643))) =>= multiply (inverse identity) (multiply ?68643 (inverse (least_upper_bound identity ?68643))) [68643] by Super 41788 with 59187 at 1,1,3
% 215.81/54.27 Id : 63053, {_}: inverse (multiply (least_upper_bound identity ?68643) (multiply (inverse ?68643) (least_upper_bound identity (multiply ?68643 (inverse (least_upper_bound identity ?68643)))))) =>= multiply (inverse identity) (multiply ?68643 (inverse (least_upper_bound identity ?68643))) [68643] by Demod 62951 with 404 at 2
% 215.81/54.27 Id : 63054, {_}: inverse (multiply (least_upper_bound identity ?68643) (multiply (inverse ?68643) (least_upper_bound identity (multiply ?68643 (inverse (least_upper_bound identity ?68643)))))) =>= inverse (multiply (least_upper_bound identity ?68643) (multiply (inverse ?68643) identity)) [68643] by Demod 63053 with 404 at 3
% 215.81/54.27 Id : 1993, {_}: least_upper_bound (inverse ?3228) ?3229 =<= multiply (inverse ?3228) (least_upper_bound identity (multiply ?3228 ?3229)) [3229, 3228] by Super 30 with 357 at 2,3
% 215.81/54.27 Id : 63055, {_}: inverse (multiply (least_upper_bound identity ?68643) (least_upper_bound (inverse ?68643) (inverse (least_upper_bound identity ?68643)))) =>= inverse (multiply (least_upper_bound identity ?68643) (multiply (inverse ?68643) identity)) [68643] by Demod 63054 with 1993 at 2,1,2
% 215.81/54.27 Id : 63056, {_}: inverse (multiply (least_upper_bound identity ?68643) (least_upper_bound (inverse ?68643) (inverse (least_upper_bound identity ?68643)))) =>= inverse (multiply (least_upper_bound identity ?68643) (inverse ?68643)) [68643] by Demod 63055 with 313 at 2,1,3
% 215.81/54.27 Id : 356, {_}: multiply ?708 (least_upper_bound ?709 (inverse ?708)) =>= least_upper_bound (multiply ?708 ?709) identity [709, 708] by Super 13 with 250 at 2,3
% 215.81/54.28 Id : 376, {_}: multiply ?708 (least_upper_bound ?709 (inverse ?708)) =>= least_upper_bound identity (multiply ?708 ?709) [709, 708] by Demod 356 with 6 at 3
% 215.81/54.28 Id : 63057, {_}: inverse (least_upper_bound identity (multiply (least_upper_bound identity ?68643) (inverse ?68643))) =>= inverse (multiply (least_upper_bound identity ?68643) (inverse ?68643)) [68643] by Demod 63056 with 376 at 1,2
% 215.81/54.28 Id : 63058, {_}: inverse (least_upper_bound identity (multiply (least_upper_bound identity ?68643) (inverse ?68643))) =>= multiply ?68643 (inverse (least_upper_bound identity ?68643)) [68643] by Demod 63057 with 270 at 3
% 215.81/54.28 Id : 63059, {_}: inverse (least_upper_bound identity (least_upper_bound identity (multiply identity (inverse ?68643)))) =?= multiply ?68643 (inverse (least_upper_bound identity ?68643)) [68643] by Demod 63058 with 377 at 2,1,2
% 215.81/54.28 Id : 63060, {_}: inverse (least_upper_bound identity (multiply identity (inverse ?68643))) =?= multiply ?68643 (inverse (least_upper_bound identity ?68643)) [68643] by Demod 63059 with 72 at 1,2
% 215.81/54.28 Id : 63437, {_}: inverse (least_upper_bound identity (inverse ?68913)) =<= multiply ?68913 (inverse (least_upper_bound identity ?68913)) [68913] by Demod 63060 with 2 at 2,1,2
% 215.81/54.28 Id : 63493, {_}: inverse (least_upper_bound identity (inverse (multiply (inverse (least_upper_bound identity ?69051)) ?69051))) =>= multiply (multiply (inverse (least_upper_bound identity ?69051)) ?69051) (inverse identity) [69051] by Super 63437 with 22681 at 1,2,3
% 215.81/54.28 Id : 63733, {_}: inverse (least_upper_bound identity (multiply (inverse ?69051) (least_upper_bound identity ?69051))) =<= multiply (multiply (inverse (least_upper_bound identity ?69051)) ?69051) (inverse identity) [69051] by Demod 63493 with 268 at 2,1,2
% 215.81/54.28 Id : 63734, {_}: inverse (least_upper_bound identity (multiply (inverse ?69051) (least_upper_bound identity ?69051))) =<= multiply (inverse (least_upper_bound identity ?69051)) (multiply ?69051 (inverse identity)) [69051] by Demod 63733 with 4 at 3
% 215.81/54.28 Id : 133, {_}: multiply (inverse ?307) (least_upper_bound ?308 ?307) =>= least_upper_bound identity (multiply (inverse ?307) ?308) [308, 307] by Demod 119 with 6 at 3
% 215.81/54.28 Id : 63735, {_}: inverse (least_upper_bound identity (least_upper_bound identity (multiply (inverse ?69051) identity))) =<= multiply (inverse (least_upper_bound identity ?69051)) (multiply ?69051 (inverse identity)) [69051] by Demod 63734 with 133 at 2,1,2
% 215.81/54.28 Id : 63736, {_}: inverse (least_upper_bound identity (least_upper_bound identity (multiply (inverse ?69051) identity))) =<= inverse (multiply identity (multiply (inverse ?69051) (least_upper_bound identity ?69051))) [69051] by Demod 63735 with 404 at 3
% 215.81/54.28 Id : 63737, {_}: inverse (least_upper_bound identity (multiply (inverse ?69051) identity)) =<= inverse (multiply identity (multiply (inverse ?69051) (least_upper_bound identity ?69051))) [69051] by Demod 63736 with 72 at 1,2
% 215.81/54.28 Id : 63738, {_}: inverse (least_upper_bound identity (multiply (inverse ?69051) identity)) =<= inverse (multiply (inverse ?69051) (least_upper_bound identity ?69051)) [69051] by Demod 63737 with 2 at 1,3
% 215.81/54.28 Id : 63739, {_}: inverse (least_upper_bound identity (inverse ?69051)) =<= inverse (multiply (inverse ?69051) (least_upper_bound identity ?69051)) [69051] by Demod 63738 with 313 at 2,1,2
% 215.81/54.28 Id : 63740, {_}: inverse (least_upper_bound identity (inverse ?69051)) =<= multiply (inverse (least_upper_bound identity ?69051)) ?69051 [69051] by Demod 63739 with 268 at 3
% 215.81/54.28 Id : 63996, {_}: multiply (inverse (least_upper_bound ?48190 identity)) ?48190 =>= inverse (least_upper_bound identity (inverse ?48190)) [48190] by Demod 43905 with 63740 at 3
% 215.81/54.28 Id : 181559, {_}: multiply (greatest_lower_bound identity (inverse ?171370)) (inverse (inverse (least_upper_bound ?171370 identity))) =>= multiply (greatest_lower_bound identity ?171370) (inverse (inverse (least_upper_bound identity (inverse ?171370)))) [171370] by Super 181527 with 63996 at 1,2,3
% 215.81/54.28 Id : 181888, {_}: multiply (greatest_lower_bound identity (inverse ?171370)) (least_upper_bound ?171370 identity) =<= multiply (greatest_lower_bound identity ?171370) (inverse (inverse (least_upper_bound identity (inverse ?171370)))) [171370] by Demod 181559 with 18 at 2,2
% 215.81/54.28 Id : 181889, {_}: multiply (greatest_lower_bound identity (inverse ?171370)) (least_upper_bound ?171370 identity) =>= multiply (greatest_lower_bound identity ?171370) (least_upper_bound identity (inverse ?171370)) [171370] by Demod 181888 with 18 at 2,3
% 215.81/54.28 Id : 122, {_}: multiply (inverse ?318) (least_upper_bound ?318 ?319) =>= least_upper_bound identity (multiply (inverse ?318) ?319) [319, 318] by Super 117 with 3 at 1,3
% 215.81/54.28 Id : 882, {_}: least_upper_bound ?1558 ?1559 =<= multiply (inverse (inverse ?1558)) (least_upper_bound identity (multiply (inverse ?1558) ?1559)) [1559, 1558] by Super 30 with 122 at 2,3
% 215.81/54.28 Id : 899, {_}: least_upper_bound ?1558 ?1559 =<= multiply ?1558 (least_upper_bound identity (multiply (inverse ?1558) ?1559)) [1559, 1558] by Demod 882 with 18 at 1,3
% 215.81/54.28 Id : 2580, {_}: inverse ?4172 =<= multiply ?4173 (inverse (multiply ?4172 ?4173)) [4173, 4172] by Super 2566 with 19 at 2,3
% 215.81/54.28 Id : 54663, {_}: inverse ?61222 =<= multiply (inverse (greatest_lower_bound identity ?61222)) (inverse (inverse (greatest_lower_bound identity (inverse ?61222)))) [61222] by Super 2580 with 54352 at 1,2,3
% 215.81/54.28 Id : 54798, {_}: inverse ?61222 =<= inverse (multiply (inverse (greatest_lower_bound identity (inverse ?61222))) (greatest_lower_bound identity ?61222)) [61222] by Demod 54663 with 19 at 3
% 215.81/54.28 Id : 54799, {_}: inverse ?61222 =<= multiply (inverse (greatest_lower_bound identity ?61222)) (greatest_lower_bound identity (inverse ?61222)) [61222] by Demod 54798 with 268 at 3
% 215.81/54.28 Id : 188393, {_}: least_upper_bound (greatest_lower_bound identity ?174656) (greatest_lower_bound identity (inverse ?174656)) =<= multiply (greatest_lower_bound identity ?174656) (least_upper_bound identity (inverse ?174656)) [174656] by Super 899 with 54799 at 2,2,3
% 215.81/54.28 Id : 189198, {_}: multiply (greatest_lower_bound identity (inverse ?171370)) (least_upper_bound ?171370 identity) =>= least_upper_bound (greatest_lower_bound identity ?171370) (greatest_lower_bound identity (inverse ?171370)) [171370] by Demod 181889 with 188393 at 3
% 215.81/54.28 Id : 282978, {_}: least_upper_bound (inverse (least_upper_bound ?241934 identity)) (greatest_lower_bound identity (inverse ?241934)) =<= multiply (least_upper_bound identity (least_upper_bound (greatest_lower_bound identity ?241934) (greatest_lower_bound identity (inverse ?241934)))) (inverse (least_upper_bound ?241934 identity)) [241934] by Super 282880 with 189198 at 2,1,3
% 215.81/54.28 Id : 83, {_}: least_upper_bound ?215 (least_upper_bound (greatest_lower_bound ?215 ?216) ?217) =>= least_upper_bound ?215 ?217 [217, 216, 215] by Super 8 with 11 at 1,3
% 215.81/54.28 Id : 283476, {_}: least_upper_bound (inverse (least_upper_bound ?241934 identity)) (greatest_lower_bound identity (inverse ?241934)) =<= multiply (least_upper_bound identity (greatest_lower_bound identity (inverse ?241934))) (inverse (least_upper_bound ?241934 identity)) [241934] by Demod 282978 with 83 at 1,3
% 215.81/54.28 Id : 283477, {_}: least_upper_bound (inverse (least_upper_bound ?241934 identity)) (greatest_lower_bound identity (inverse ?241934)) =>= multiply identity (inverse (least_upper_bound ?241934 identity)) [241934] by Demod 283476 with 11 at 1,3
% 215.81/54.28 Id : 283478, {_}: least_upper_bound (inverse (least_upper_bound ?241934 identity)) (greatest_lower_bound identity (inverse ?241934)) =>= inverse (least_upper_bound ?241934 identity) [241934] by Demod 283477 with 2 at 3
% 215.81/54.28 Id : 499339, {_}: greatest_lower_bound (greatest_lower_bound identity (inverse ?393840)) (inverse (least_upper_bound ?393840 identity)) =>= greatest_lower_bound identity (inverse ?393840) [393840] by Super 100 with 283478 at 2,2
% 215.81/54.28 Id : 499616, {_}: greatest_lower_bound (inverse (least_upper_bound ?393840 identity)) (greatest_lower_bound identity (inverse ?393840)) =>= greatest_lower_bound identity (inverse ?393840) [393840] by Demod 499339 with 5 at 2
% 215.81/54.28 Id : 44, {_}: greatest_lower_bound ?112 (greatest_lower_bound ?113 ?114) =?= greatest_lower_bound ?113 (greatest_lower_bound ?114 ?112) [114, 113, 112] by Super 5 with 7 at 3
% 215.81/54.28 Id : 499617, {_}: greatest_lower_bound identity (greatest_lower_bound (inverse ?393840) (inverse (least_upper_bound ?393840 identity))) =>= greatest_lower_bound identity (inverse ?393840) [393840] by Demod 499616 with 44 at 2
% 215.81/54.28 Id : 626, {_}: greatest_lower_bound ?1083 (greatest_lower_bound (least_upper_bound ?1084 ?1083) ?1085) =>= greatest_lower_bound ?1083 ?1085 [1085, 1084, 1083] by Super 7 with 100 at 1,3
% 215.81/54.28 Id : 21366, {_}: greatest_lower_bound (inverse (least_upper_bound ?27934 identity)) (greatest_lower_bound identity ?27935) =>= greatest_lower_bound (inverse (least_upper_bound ?27934 identity)) ?27935 [27935, 27934] by Super 626 with 21190 at 1,2,2
% 215.81/54.28 Id : 21403, {_}: greatest_lower_bound identity (greatest_lower_bound ?27935 (inverse (least_upper_bound ?27934 identity))) =>= greatest_lower_bound (inverse (least_upper_bound ?27934 identity)) ?27935 [27934, 27935] by Demod 21366 with 44 at 2
% 215.81/54.28 Id : 499618, {_}: greatest_lower_bound (inverse (least_upper_bound ?393840 identity)) (inverse ?393840) =>= greatest_lower_bound identity (inverse ?393840) [393840] by Demod 499617 with 21403 at 2
% 215.81/54.28 Id : 499619, {_}: greatest_lower_bound (inverse ?393840) (inverse (least_upper_bound ?393840 identity)) =>= greatest_lower_bound identity (inverse ?393840) [393840] by Demod 499618 with 5 at 2
% 215.81/54.28 Id : 45878, {_}: least_upper_bound (inverse ?53525) (inverse (greatest_lower_bound ?53524 ?53525)) =>= inverse (greatest_lower_bound ?53524 ?53525) [53524, 53525] by Demod 45877 with 313 at 3
% 215.81/54.28 Id : 56905, {_}: greatest_lower_bound (inverse ?63759) (inverse (greatest_lower_bound ?63760 ?63759)) =>= inverse ?63759 [63760, 63759] by Super 12 with 45878 at 2,2
% 215.81/54.28 Id : 56908, {_}: greatest_lower_bound (inverse (least_upper_bound ?63767 ?63768)) (inverse ?63767) =>= inverse (least_upper_bound ?63767 ?63768) [63768, 63767] by Super 56905 with 12 at 1,2,2
% 215.81/54.28 Id : 57146, {_}: greatest_lower_bound (inverse ?63767) (inverse (least_upper_bound ?63767 ?63768)) =>= inverse (least_upper_bound ?63767 ?63768) [63768, 63767] by Demod 56908 with 5 at 2
% 215.81/54.28 Id : 499620, {_}: inverse (least_upper_bound ?393840 identity) =<= greatest_lower_bound identity (inverse ?393840) [393840] by Demod 499619 with 57146 at 2
% 215.81/54.28 Id : 500378, {_}: multiply (inverse (inverse (least_upper_bound ?170971 identity))) (greatest_lower_bound ?170971 identity) =>= ?170971 [170971] by Demod 181268 with 499620 at 1,1,2
% 215.81/54.28 Id : 500665, {_}: multiply (least_upper_bound ?170971 identity) (greatest_lower_bound ?170971 identity) =>= ?170971 [170971] by Demod 500378 with 18 at 1,2
% 215.81/54.28 Id : 501952, {_}: a =?= a [] by Demod 1 with 500665 at 3
% 215.81/54.28 Id : 1, {_}: a =<= multiply (least_upper_bound a identity) (greatest_lower_bound a identity) [] by prove_p19
% 215.81/54.28 % SZS output end CNFRefutation for theBenchmark.p
% 215.81/54.28 21776: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 53.89874 using kbo
%------------------------------------------------------------------------------