%------------------------------------------------------------------------------
% File : Matita---1.0
% Problem : GRP002-3 : TPTP v8.1.0. Released v1.0.0.
% 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:28:21 EDT 2022
% Result : Unsatisfiable 9.64s 2.75s
% Output : CNFRefutation 9.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP002-3 : TPTP v8.1.0. Released v1.0.0.
% 0.06/0.12 % 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.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Tue Jun 14 00:17:38 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 1832: Facts:
% 0.12/0.34 1832: Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 0.12/0.34 1832: Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 0.12/0.34 1832: Id : 4, {_}:
% 0.12/0.34 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
% 0.12/0.34 [8, 7, 6] by associativity ?6 ?7 ?8
% 0.12/0.34 1832: Id : 5, {_}:
% 0.12/0.34 commutator ?10 ?11
% 0.12/0.34 =<=
% 0.12/0.34 multiply ?10 (multiply ?11 (multiply (inverse ?10) (inverse ?11)))
% 0.12/0.34 [11, 10] by commutator ?10 ?11
% 0.12/0.34 1832: Id : 6, {_}:
% 0.12/0.34 multiply ?13 (multiply ?13 ?13) =>= identity
% 0.12/0.34 [13] by x_cubed_is_identity ?13
% 0.12/0.34 1832: Goal:
% 0.12/0.34 1832: Id : 1, {_}:
% 0.12/0.34 commutator (commutator a b) b =>= identity
% 0.12/0.34 [] by prove_commutator
% 9.64/2.75 Statistics :
% 9.64/2.75 Max weight : 30
% 9.64/2.75 Found proof, 2.410274s
% 9.64/2.75 % SZS status Unsatisfiable for theBenchmark.p
% 9.64/2.75 % SZS output start CNFRefutation for theBenchmark.p
% 9.64/2.75 Id : 24, {_}: commutator ?51 ?52 =<= multiply ?51 (multiply ?52 (multiply (inverse ?51) (inverse ?52))) [52, 51] by commutator ?51 ?52
% 9.64/2.75 Id : 3, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
% 9.64/2.75 Id : 11, {_}: multiply (multiply ?22 ?23) ?24 =>= multiply ?22 (multiply ?23 ?24) [24, 23, 22] by associativity ?22 ?23 ?24
% 9.64/2.75 Id : 6, {_}: multiply ?13 (multiply ?13 ?13) =>= identity [13] by x_cubed_is_identity ?13
% 9.64/2.75 Id : 5, {_}: commutator ?10 ?11 =<= multiply ?10 (multiply ?11 (multiply (inverse ?10) (inverse ?11))) [11, 10] by commutator ?10 ?11
% 9.64/2.75 Id : 2, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
% 9.64/2.75 Id : 4, {_}: multiply (multiply ?6 ?7) ?8 =>= multiply ?6 (multiply ?7 ?8) [8, 7, 6] by associativity ?6 ?7 ?8
% 9.64/2.75 Id : 21, {_}: commutator identity ?41 =<= multiply ?41 (multiply (inverse identity) (inverse ?41)) [41] by Super 2 with 5 at 2
% 9.64/2.75 Id : 13, {_}: multiply identity ?29 =<= multiply (inverse ?30) (multiply ?30 ?29) [30, 29] by Super 11 with 3 at 1,2
% 9.64/2.75 Id : 87, {_}: ?128 =<= multiply (inverse ?129) (multiply ?129 ?128) [129, 128] by Demod 13 with 2 at 2
% 9.64/2.75 Id : 88, {_}: ?131 =<= multiply (inverse identity) ?131 [131] by Super 87 with 2 at 2,3
% 9.64/2.75 Id : 102, {_}: multiply (inverse identity) (inverse identity) =>= identity [] by Super 6 with 88 at 2,2
% 9.64/2.75 Id : 122, {_}: inverse identity =>= identity [] by Demod 102 with 88 at 2
% 9.64/2.75 Id : 159, {_}: commutator identity ?41 =<= multiply ?41 (multiply identity (inverse ?41)) [41] by Demod 21 with 122 at 1,2,3
% 9.64/2.75 Id : 160, {_}: commutator identity ?41 =<= multiply ?41 (inverse ?41) [41] by Demod 159 with 2 at 2,3
% 9.64/2.75 Id : 161, {_}: multiply (commutator identity ?199) ?200 =<= multiply ?199 (multiply (inverse ?199) ?200) [200, 199] by Super 4 with 160 at 1,2
% 9.64/2.75 Id : 17, {_}: ?29 =<= multiply (inverse ?30) (multiply ?30 ?29) [30, 29] by Demod 13 with 2 at 2
% 9.64/2.75 Id : 93, {_}: multiply ?144 ?145 =<= multiply (inverse (inverse ?144)) ?145 [145, 144] by Super 87 with 17 at 2,3
% 9.64/2.75 Id : 220, {_}: multiply ?272 (inverse ?272) =>= identity [272] by Super 3 with 93 at 2
% 9.64/2.75 Id : 238, {_}: commutator identity ?272 =>= identity [272] by Demod 220 with 160 at 2
% 9.64/2.75 Id : 443, {_}: multiply identity ?200 =<= multiply ?199 (multiply (inverse ?199) ?200) [199, 200] by Demod 161 with 238 at 1,2
% 9.64/2.75 Id : 444, {_}: ?200 =<= multiply ?199 (multiply (inverse ?199) ?200) [199, 200] by Demod 443 with 2 at 2
% 9.64/2.75 Id : 162, {_}: commutator identity (multiply ?202 ?203) =<= multiply ?202 (multiply ?203 (inverse (multiply ?202 ?203))) [203, 202] by Super 4 with 160 at 2
% 9.64/2.75 Id : 962, {_}: identity =<= multiply ?202 (multiply ?203 (inverse (multiply ?202 ?203))) [203, 202] by Demod 162 with 238 at 2
% 9.64/2.75 Id : 966, {_}: multiply ?968 (inverse (multiply ?969 ?968)) =>= multiply (inverse ?969) identity [969, 968] by Super 17 with 962 at 2,3
% 9.64/2.75 Id : 89, {_}: ?133 =<= multiply (inverse (inverse ?133)) identity [133] by Super 87 with 3 at 2,3
% 9.64/2.75 Id : 213, {_}: ?133 =<= multiply ?133 identity [133] by Demod 89 with 93 at 3
% 9.64/2.75 Id : 1018, {_}: multiply ?968 (inverse (multiply ?969 ?968)) =>= inverse ?969 [969, 968] by Demod 966 with 213 at 3
% 9.64/2.75 Id : 1368, {_}: inverse (multiply ?1418 (inverse ?1419)) =>= multiply ?1419 (inverse ?1418) [1419, 1418] by Super 444 with 1018 at 2,3
% 9.64/2.75 Id : 2293, {_}: inverse (multiply ?2529 (multiply ?2530 (inverse ?2531))) =>= multiply ?2531 (inverse (multiply ?2529 ?2530)) [2531, 2530, 2529] by Super 1368 with 4 at 1,2
% 9.64/2.75 Id : 1093, {_}: inverse (multiply ?1086 ?1087) =<= multiply (inverse ?1087) (inverse ?1086) [1087, 1086] by Super 17 with 1018 at 2,3
% 9.64/2.75 Id : 1425, {_}: commutator ?10 ?11 =<= multiply ?10 (multiply ?11 (inverse (multiply ?11 ?10))) [11, 10] by Demod 5 with 1093 at 2,2,3
% 9.64/2.75 Id : 2315, {_}: inverse (commutator ?2612 ?2613) =<= multiply (multiply ?2613 ?2612) (inverse (multiply ?2612 ?2613)) [2613, 2612] by Super 2293 with 1425 at 1,2
% 9.64/2.75 Id : 2431, {_}: inverse (commutator ?2612 ?2613) =<= multiply ?2613 (multiply ?2612 (inverse (multiply ?2612 ?2613))) [2613, 2612] by Demod 2315 with 4 at 3
% 9.64/2.75 Id : 2432, {_}: inverse (commutator ?2612 ?2613) =>= commutator ?2613 ?2612 [2613, 2612] by Demod 2431 with 1425 at 3
% 9.64/2.75 Id : 23, {_}: commutator (multiply ?47 ?48) ?49 =<= multiply ?47 (multiply ?48 (multiply ?49 (multiply (inverse (multiply ?47 ?48)) (inverse ?49)))) [49, 48, 47] by Super 4 with 5 at 2
% 9.64/2.75 Id : 447, {_}: commutator (multiply ?492 ?493) (inverse ?493) =<= multiply ?492 (multiply (inverse (multiply ?492 ?493)) (inverse (inverse ?493))) [493, 492] by Super 23 with 444 at 2,3
% 9.64/2.75 Id : 214, {_}: inverse (inverse ?255) =<= multiply ?255 identity [255] by Super 213 with 93 at 3
% 9.64/2.75 Id : 243, {_}: inverse (inverse ?255) =>= ?255 [255] by Demod 214 with 213 at 3
% 9.64/2.75 Id : 484, {_}: commutator (multiply ?492 ?493) (inverse ?493) =<= multiply ?492 (multiply (inverse (multiply ?492 ?493)) ?493) [493, 492] by Demod 447 with 243 at 2,2,3
% 9.64/2.75 Id : 2453, {_}: inverse (commutator ?2689 ?2690) =>= commutator ?2690 ?2689 [2690, 2689] by Demod 2431 with 1425 at 3
% 9.64/2.75 Id : 27, {_}: commutator ?58 (multiply ?59 ?60) =<= multiply ?58 (multiply ?59 (multiply ?60 (multiply (inverse ?58) (inverse (multiply ?59 ?60))))) [60, 59, 58] by Super 24 with 4 at 2,3
% 9.64/2.75 Id : 1095, {_}: commutator ?1093 (multiply ?1094 (inverse ?1093)) =<= multiply ?1093 (multiply ?1094 (multiply (inverse ?1093) (inverse ?1094))) [1094, 1093] by Super 27 with 1018 at 2,2,2,3
% 9.64/2.75 Id : 1631, {_}: commutator ?1665 (multiply ?1666 (inverse ?1665)) =>= commutator ?1665 ?1666 [1666, 1665] by Demod 1095 with 5 at 3
% 9.64/2.75 Id : 1633, {_}: commutator (inverse ?1670) (multiply ?1671 ?1670) =>= commutator (inverse ?1670) ?1671 [1671, 1670] by Super 1631 with 243 at 2,2,2
% 9.64/2.75 Id : 2460, {_}: inverse (commutator (inverse ?2705) ?2706) =<= commutator (multiply ?2706 ?2705) (inverse ?2705) [2706, 2705] by Super 2453 with 1633 at 1,2
% 9.64/2.75 Id : 2477, {_}: commutator ?2706 (inverse ?2705) =<= commutator (multiply ?2706 ?2705) (inverse ?2705) [2705, 2706] by Demod 2460 with 2432 at 2
% 9.64/2.75 Id : 11960, {_}: commutator ?492 (inverse ?493) =<= multiply ?492 (multiply (inverse (multiply ?492 ?493)) ?493) [493, 492] by Demod 484 with 2477 at 2
% 9.64/2.75 Id : 1642, {_}: commutator ?1696 (inverse (multiply ?1696 ?1697)) =>= commutator ?1696 (inverse ?1697) [1697, 1696] by Super 1631 with 1093 at 2,2
% 9.64/2.75 Id : 2461, {_}: inverse (commutator ?2708 (inverse ?2709)) =<= commutator (inverse (multiply ?2708 ?2709)) ?2708 [2709, 2708] by Super 2453 with 1642 at 1,2
% 9.64/2.75 Id : 2478, {_}: commutator (inverse ?2709) ?2708 =<= commutator (inverse (multiply ?2708 ?2709)) ?2708 [2708, 2709] by Demod 2461 with 2432 at 2
% 9.64/2.75 Id : 1097, {_}: multiply ?1099 (inverse (multiply ?1100 ?1099)) =>= inverse ?1100 [1100, 1099] by Demod 966 with 213 at 3
% 9.64/2.75 Id : 1101, {_}: multiply (inverse (multiply ?1110 ?1111)) (inverse (inverse ?1110)) =>= inverse ?1111 [1111, 1110] by Super 1097 with 1018 at 1,2,2
% 9.64/2.75 Id : 1132, {_}: multiply (inverse (multiply ?1110 ?1111)) ?1110 =>= inverse ?1111 [1111, 1110] by Demod 1101 with 243 at 2,2
% 9.64/2.75 Id : 22, {_}: multiply (commutator ?43 ?44) ?45 =<= multiply ?43 (multiply (multiply ?44 (multiply (inverse ?43) (inverse ?44))) ?45) [45, 44, 43] by Super 4 with 5 at 1,2
% 9.64/2.75 Id : 31, {_}: multiply (commutator ?43 ?44) ?45 =<= multiply ?43 (multiply ?44 (multiply (multiply (inverse ?43) (inverse ?44)) ?45)) [45, 44, 43] by Demod 22 with 4 at 2,3
% 9.64/2.75 Id : 1178, {_}: multiply (commutator ?1204 ?1205) ?1206 =<= multiply ?1204 (multiply ?1205 (multiply (inverse ?1204) (multiply (inverse ?1205) ?1206))) [1206, 1205, 1204] by Demod 31 with 4 at 2,2,3
% 9.64/2.75 Id : 1207, {_}: multiply (commutator ?1311 ?1312) (inverse (inverse ?1311)) =>= multiply ?1311 (commutator ?1312 (inverse ?1311)) [1312, 1311] by Super 1178 with 5 at 2,3
% 9.64/2.75 Id : 1313, {_}: multiply (commutator ?1311 ?1312) ?1311 =<= multiply ?1311 (commutator ?1312 (inverse ?1311)) [1312, 1311] by Demod 1207 with 243 at 2,2
% 9.64/2.75 Id : 1796, {_}: multiply (inverse (multiply (commutator ?1873 ?1874) ?1873)) ?1873 =>= inverse (commutator ?1874 (inverse ?1873)) [1874, 1873] by Super 1132 with 1313 at 1,1,2
% 9.64/2.75 Id : 22644, {_}: multiply (inverse (multiply (commutator ?1873 ?1874) ?1873)) ?1873 =>= commutator (inverse ?1873) ?1874 [1874, 1873] by Demod 1796 with 2432 at 3
% 9.64/2.75 Id : 2438, {_}: inverse (multiply (commutator ?2631 ?2632) ?2633) =<= multiply (inverse ?2633) (commutator ?2632 ?2631) [2633, 2632, 2631] by Super 1093 with 2432 at 2,3
% 9.64/2.75 Id : 2533, {_}: multiply (inverse (multiply (commutator ?2829 ?2830) ?2831)) ?2832 =>= multiply (inverse ?2831) (multiply (commutator ?2830 ?2829) ?2832) [2832, 2831, 2830, 2829] by Super 4 with 2438 at 1,2
% 9.64/2.75 Id : 27006, {_}: multiply (inverse ?1873) (multiply (commutator ?1874 ?1873) ?1873) =>= commutator (inverse ?1873) ?1874 [1874, 1873] by Demod 22644 with 2533 at 2
% 9.64/2.75 Id : 1086, {_}: inverse (multiply ?1062 (inverse ?1063)) =>= multiply ?1063 (inverse ?1062) [1063, 1062] by Super 444 with 1018 at 2,3
% 9.64/2.75 Id : 455, {_}: ?515 =<= multiply ?516 (multiply (inverse ?516) ?515) [516, 515] by Demod 443 with 2 at 2
% 9.64/2.75 Id : 459, {_}: multiply (inverse ?525) (inverse ?525) =>= multiply ?525 identity [525] by Super 455 with 6 at 2,3
% 9.64/2.75 Id : 495, {_}: multiply (inverse ?525) (inverse ?525) =>= ?525 [525] by Demod 459 with 213 at 3
% 9.64/2.75 Id : 631, {_}: inverse ?691 =<= multiply ?691 ?691 [691] by Super 444 with 495 at 2,3
% 9.64/2.75 Id : 671, {_}: multiply (inverse ?736) ?737 =<= multiply ?736 (multiply ?736 ?737) [737, 736] by Super 4 with 631 at 1,2
% 9.64/2.75 Id : 92, {_}: multiply ?141 (multiply (inverse ?142) (inverse ?141)) =?= multiply (inverse ?142) (commutator ?142 ?141) [142, 141] by Super 87 with 5 at 2,3
% 9.64/2.75 Id : 2939, {_}: multiply ?141 (inverse (multiply ?141 ?142)) =?= multiply (inverse ?142) (commutator ?142 ?141) [142, 141] by Demod 92 with 1093 at 2,2
% 9.64/2.75 Id : 2940, {_}: multiply ?141 (inverse (multiply ?141 ?142)) =?= inverse (multiply (commutator ?141 ?142) ?142) [142, 141] by Demod 2939 with 2438 at 3
% 9.64/2.75 Id : 2976, {_}: multiply (inverse ?3437) (inverse (multiply ?3437 ?3438)) =<= multiply ?3437 (inverse (multiply (commutator ?3437 ?3438) ?3438)) [3438, 3437] by Super 671 with 2940 at 2,3
% 9.64/2.75 Id : 3052, {_}: inverse (multiply (multiply ?3437 ?3438) ?3437) =<= multiply ?3437 (inverse (multiply (commutator ?3437 ?3438) ?3438)) [3438, 3437] by Demod 2976 with 1093 at 2
% 9.64/2.75 Id : 30782, {_}: inverse (multiply ?30628 (multiply ?30629 ?30628)) =<= multiply ?30628 (inverse (multiply (commutator ?30628 ?30629) ?30629)) [30629, 30628] by Demod 3052 with 4 at 1,2
% 9.64/2.75 Id : 2165, {_}: commutator ?2281 (inverse (multiply ?2281 ?2282)) =>= commutator ?2281 (inverse ?2282) [2282, 2281] by Super 1631 with 1093 at 2,2
% 9.64/2.75 Id : 2169, {_}: commutator ?2292 (inverse (inverse ?2293)) =<= commutator ?2292 (inverse (inverse (multiply ?2293 ?2292))) [2293, 2292] by Super 2165 with 1018 at 1,2,2
% 9.64/2.76 Id : 2197, {_}: commutator ?2292 ?2293 =<= commutator ?2292 (inverse (inverse (multiply ?2293 ?2292))) [2293, 2292] by Demod 2169 with 243 at 2,2
% 9.64/2.76 Id : 2198, {_}: commutator ?2292 ?2293 =<= commutator ?2292 (multiply ?2293 ?2292) [2293, 2292] by Demod 2197 with 243 at 2,3
% 9.64/2.76 Id : 2462, {_}: inverse (commutator ?2711 ?2712) =<= commutator (multiply ?2712 ?2711) ?2711 [2712, 2711] by Super 2453 with 2198 at 1,2
% 9.64/2.76 Id : 2483, {_}: commutator ?2725 ?2726 =<= commutator (multiply ?2725 ?2726) ?2726 [2726, 2725] by Demod 2462 with 2432 at 2
% 9.64/2.76 Id : 2498, {_}: commutator (inverse ?2768) (inverse ?2769) =<= commutator (inverse (multiply ?2769 ?2768)) (inverse ?2769) [2769, 2768] by Super 2483 with 1093 at 1,3
% 9.64/2.76 Id : 30813, {_}: inverse (multiply (inverse (multiply ?30721 ?30722)) (multiply (inverse ?30721) (inverse (multiply ?30721 ?30722)))) =<= multiply (inverse (multiply ?30721 ?30722)) (inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) (inverse ?30721))) [30722, 30721] by Super 30782 with 2498 at 1,1,2,3
% 9.64/2.76 Id : 1374, {_}: inverse (multiply ?1434 (multiply ?1435 (inverse ?1436))) =>= multiply ?1436 (inverse (multiply ?1434 ?1435)) [1436, 1435, 1434] by Super 1368 with 4 at 1,2
% 9.64/2.76 Id : 31444, {_}: multiply (multiply ?30721 ?30722) (inverse (multiply (inverse (multiply ?30721 ?30722)) (inverse ?30721))) =<= multiply (inverse (multiply ?30721 ?30722)) (inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) (inverse ?30721))) [30722, 30721] by Demod 30813 with 1374 at 2
% 9.64/2.76 Id : 31445, {_}: multiply (multiply ?30721 ?30722) (inverse (multiply (inverse (multiply ?30721 ?30722)) (inverse ?30721))) =<= inverse (multiply (multiply (commutator (inverse ?30722) (inverse ?30721)) (inverse ?30721)) (multiply ?30721 ?30722)) [30722, 30721] by Demod 31444 with 1093 at 3
% 9.64/2.76 Id : 31446, {_}: multiply ?30721 (multiply ?30722 (inverse (multiply (inverse (multiply ?30721 ?30722)) (inverse ?30721)))) =<= inverse (multiply (multiply (commutator (inverse ?30722) (inverse ?30721)) (inverse ?30721)) (multiply ?30721 ?30722)) [30722, 30721] by Demod 31445 with 4 at 2
% 9.64/2.76 Id : 31447, {_}: multiply ?30721 (multiply ?30722 (inverse (multiply (inverse (multiply ?30721 ?30722)) (inverse ?30721)))) =<= inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) (multiply (inverse ?30721) (multiply ?30721 ?30722))) [30722, 30721] by Demod 31446 with 4 at 1,3
% 9.64/2.76 Id : 31448, {_}: multiply ?30721 (multiply ?30722 (multiply ?30721 (inverse (inverse (multiply ?30721 ?30722))))) =<= inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) (multiply (inverse ?30721) (multiply ?30721 ?30722))) [30722, 30721] by Demod 31447 with 1086 at 2,2,2
% 9.64/2.76 Id : 31449, {_}: multiply ?30721 (multiply ?30722 (multiply ?30721 (inverse (inverse (multiply ?30721 ?30722))))) =>= inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) ?30722) [30722, 30721] by Demod 31448 with 17 at 2,1,3
% 9.64/2.76 Id : 31450, {_}: multiply ?30721 (multiply ?30722 (multiply ?30721 (multiply ?30721 ?30722))) =>= inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) ?30722) [30722, 30721] by Demod 31449 with 243 at 2,2,2,2
% 9.64/2.76 Id : 31451, {_}: multiply ?30721 (multiply ?30722 (multiply (inverse ?30721) ?30722)) =>= inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) ?30722) [30722, 30721] by Demod 31450 with 671 at 2,2,2
% 9.64/2.76 Id : 1191, {_}: multiply (commutator ?1255 ?1256) (inverse ?1256) =<= multiply ?1255 (multiply ?1256 (multiply (inverse ?1255) (inverse (inverse ?1256)))) [1256, 1255] by Super 1178 with 631 at 2,2,2,3
% 9.64/2.76 Id : 1284, {_}: multiply (commutator ?1255 ?1256) (inverse ?1256) =<= multiply ?1255 (multiply ?1256 (multiply (inverse ?1255) ?1256)) [1256, 1255] by Demod 1191 with 243 at 2,2,2,3
% 9.64/2.76 Id : 2439, {_}: inverse (multiply ?2635 (commutator ?2636 ?2637)) =<= multiply (commutator ?2637 ?2636) (inverse ?2635) [2637, 2636, 2635] by Super 1093 with 2432 at 1,3
% 9.64/2.76 Id : 15655, {_}: inverse (multiply ?1256 (commutator ?1256 ?1255)) =<= multiply ?1255 (multiply ?1256 (multiply (inverse ?1255) ?1256)) [1255, 1256] by Demod 1284 with 2439 at 2
% 9.64/2.76 Id : 31452, {_}: inverse (multiply ?30722 (commutator ?30722 ?30721)) =<= inverse (multiply (commutator (inverse ?30722) (inverse ?30721)) ?30722) [30721, 30722] by Demod 31451 with 15655 at 2
% 9.64/2.76 Id : 32268, {_}: inverse (multiply (inverse ?31556) (commutator (inverse ?31556) ?31557)) =<= multiply ?31556 (inverse (commutator (inverse (inverse ?31556)) (inverse ?31557))) [31557, 31556] by Super 1086 with 31452 at 2
% 9.64/2.76 Id : 1446, {_}: inverse (multiply ?1505 ?1506) =<= multiply (inverse ?1506) (inverse ?1505) [1506, 1505] by Super 17 with 1018 at 2,3
% 9.64/2.76 Id : 1448, {_}: inverse (multiply (inverse ?1510) ?1511) =>= multiply (inverse ?1511) ?1510 [1511, 1510] by Super 1446 with 243 at 2,3
% 9.64/2.76 Id : 32430, {_}: multiply (inverse (commutator (inverse ?31556) ?31557)) ?31556 =<= multiply ?31556 (inverse (commutator (inverse (inverse ?31556)) (inverse ?31557))) [31557, 31556] by Demod 32268 with 1448 at 2
% 9.64/2.76 Id : 32431, {_}: multiply (inverse (commutator (inverse ?31556) ?31557)) ?31556 =<= multiply ?31556 (commutator (inverse ?31557) (inverse (inverse ?31556))) [31557, 31556] by Demod 32430 with 2432 at 2,3
% 9.64/2.76 Id : 32432, {_}: multiply (commutator ?31557 (inverse ?31556)) ?31556 =<= multiply ?31556 (commutator (inverse ?31557) (inverse (inverse ?31556))) [31556, 31557] by Demod 32431 with 2432 at 1,2
% 9.64/2.76 Id : 32988, {_}: multiply (commutator ?32438 (inverse ?32439)) ?32439 =>= multiply ?32439 (commutator (inverse ?32438) ?32439) [32439, 32438] by Demod 32432 with 243 at 2,2,3
% 9.64/2.76 Id : 33010, {_}: multiply (commutator (inverse ?32511) (inverse ?32512)) ?32512 =<= multiply ?32512 (commutator (inverse (inverse (multiply (inverse ?32512) ?32511))) ?32512) [32512, 32511] by Super 32988 with 2478 at 1,2
% 9.64/2.76 Id : 32433, {_}: multiply (commutator ?31557 (inverse ?31556)) ?31556 =>= multiply ?31556 (commutator (inverse ?31557) ?31556) [31556, 31557] by Demod 32432 with 243 at 2,2,3
% 9.64/2.76 Id : 33304, {_}: multiply ?32512 (commutator (inverse (inverse ?32511)) ?32512) =<= multiply ?32512 (commutator (inverse (inverse (multiply (inverse ?32512) ?32511))) ?32512) [32511, 32512] by Demod 33010 with 32433 at 2
% 9.64/2.76 Id : 33305, {_}: multiply ?32512 (commutator (inverse (inverse ?32511)) ?32512) =<= multiply ?32512 (commutator (multiply (inverse ?32512) ?32511) ?32512) [32511, 32512] by Demod 33304 with 243 at 1,2,3
% 9.64/2.76 Id : 33306, {_}: multiply ?32512 (commutator ?32511 ?32512) =<= multiply ?32512 (commutator (multiply (inverse ?32512) ?32511) ?32512) [32511, 32512] by Demod 33305 with 243 at 1,2,2
% 9.64/2.76 Id : 2489, {_}: commutator (inverse ?2742) (multiply ?2742 ?2743) =?= commutator ?2743 (multiply ?2742 ?2743) [2743, 2742] by Super 2483 with 17 at 1,3
% 9.64/2.76 Id : 3291, {_}: commutator (inverse ?3719) (multiply ?3719 ?3720) =>= commutator ?3720 ?3719 [3720, 3719] by Demod 2489 with 2198 at 3
% 9.64/2.76 Id : 3303, {_}: commutator (inverse ?3754) ?3755 =<= commutator (multiply (inverse ?3754) ?3755) ?3754 [3755, 3754] by Super 3291 with 444 at 2,2
% 9.64/2.76 Id : 33307, {_}: multiply ?32512 (commutator ?32511 ?32512) =<= multiply ?32512 (commutator (inverse ?32512) ?32511) [32511, 32512] by Demod 33306 with 3303 at 2,3
% 9.64/2.76 Id : 1196, {_}: multiply (commutator (multiply (inverse ?1273) ?1274) ?1273) ?1274 =>= multiply (multiply (inverse ?1273) ?1274) (multiply ?1273 identity) [1274, 1273] by Super 1178 with 3 at 2,2,3
% 9.64/2.76 Id : 1291, {_}: multiply (commutator (multiply (inverse ?1273) ?1274) ?1273) ?1274 =>= multiply (inverse ?1273) (multiply ?1274 (multiply ?1273 identity)) [1274, 1273] by Demod 1196 with 4 at 3
% 9.64/2.76 Id : 1292, {_}: multiply (commutator (multiply (inverse ?1273) ?1274) ?1273) ?1274 =>= multiply (inverse ?1273) (multiply ?1274 ?1273) [1274, 1273] by Demod 1291 with 213 at 2,2,3
% 9.64/2.76 Id : 17186, {_}: multiply (commutator (inverse ?16716) ?16717) ?16717 =?= multiply (inverse ?16716) (multiply ?16717 ?16716) [16717, 16716] by Demod 1292 with 3303 at 1,2
% 9.64/2.76 Id : 17192, {_}: multiply (commutator (inverse (inverse (multiply ?16735 ?16736))) ?16735) ?16735 =?= multiply (inverse (inverse (multiply ?16735 ?16736))) (inverse (multiply (commutator ?16735 ?16736) ?16736)) [16736, 16735] by Super 17186 with 2940 at 2,3
% 9.64/2.76 Id : 17592, {_}: multiply (commutator (multiply ?16735 ?16736) ?16735) ?16735 =?= multiply (inverse (inverse (multiply ?16735 ?16736))) (inverse (multiply (commutator ?16735 ?16736) ?16736)) [16736, 16735] by Demod 17192 with 243 at 1,1,2
% 9.64/2.76 Id : 17593, {_}: multiply (commutator (multiply ?16735 ?16736) ?16735) ?16735 =?= inverse (multiply (multiply (commutator ?16735 ?16736) ?16736) (inverse (multiply ?16735 ?16736))) [16736, 16735] by Demod 17592 with 1093 at 3
% 9.64/2.76 Id : 17594, {_}: multiply (commutator (multiply ?16735 ?16736) ?16735) ?16735 =?= multiply (multiply ?16735 ?16736) (inverse (multiply (commutator ?16735 ?16736) ?16736)) [16736, 16735] by Demod 17593 with 1086 at 3
% 9.64/2.76 Id : 17595, {_}: multiply (commutator (multiply ?16735 ?16736) ?16735) ?16735 =?= multiply ?16735 (multiply ?16736 (inverse (multiply (commutator ?16735 ?16736) ?16736))) [16736, 16735] by Demod 17594 with 4 at 3
% 9.64/2.76 Id : 17596, {_}: multiply (commutator (multiply ?16735 ?16736) ?16735) ?16735 =>= multiply ?16735 (inverse (commutator ?16735 ?16736)) [16736, 16735] by Demod 17595 with 1018 at 2,3
% 9.64/2.76 Id : 17890, {_}: multiply (commutator (multiply ?17207 ?17208) ?17207) ?17207 =>= multiply ?17207 (commutator ?17208 ?17207) [17208, 17207] by Demod 17596 with 2432 at 2,3
% 9.64/2.76 Id : 17911, {_}: multiply (commutator ?17270 ?17271) ?17271 =<= multiply ?17271 (commutator (multiply (inverse ?17271) ?17270) ?17271) [17271, 17270] by Super 17890 with 444 at 1,1,2
% 9.64/2.76 Id : 18166, {_}: multiply (commutator ?17270 ?17271) ?17271 =<= multiply ?17271 (commutator (inverse ?17271) ?17270) [17271, 17270] by Demod 17911 with 3303 at 2,3
% 9.64/2.76 Id : 33308, {_}: multiply ?32512 (commutator ?32511 ?32512) =<= multiply (commutator ?32511 ?32512) ?32512 [32511, 32512] by Demod 33307 with 18166 at 3
% 9.64/2.76 Id : 33398, {_}: multiply (inverse ?1873) (multiply ?1873 (commutator ?1874 ?1873)) =>= commutator (inverse ?1873) ?1874 [1874, 1873] by Demod 27006 with 33308 at 2,2
% 9.64/2.76 Id : 33399, {_}: commutator ?1874 ?1873 =<= commutator (inverse ?1873) ?1874 [1873, 1874] by Demod 33398 with 17 at 2
% 9.64/2.76 Id : 33421, {_}: commutator ?2708 ?2709 =<= commutator (inverse (multiply ?2708 ?2709)) ?2708 [2709, 2708] by Demod 2478 with 33399 at 2
% 9.64/2.76 Id : 33422, {_}: commutator ?2708 ?2709 =<= commutator ?2708 (multiply ?2708 ?2709) [2709, 2708] by Demod 33421 with 33399 at 3
% 9.64/2.76 Id : 2494, {_}: commutator ?2757 (multiply (inverse ?2757) ?2758) =?= commutator ?2758 (multiply (inverse ?2757) ?2758) [2758, 2757] by Super 2483 with 444 at 1,3
% 9.64/2.76 Id : 3379, {_}: commutator ?3847 (multiply (inverse ?3847) ?3848) =>= commutator ?3848 (inverse ?3847) [3848, 3847] by Demod 2494 with 2198 at 3
% 9.64/2.76 Id : 3398, {_}: commutator ?3907 (multiply (inverse (inverse ?3907)) ?3908) =<= commutator (multiply (inverse ?3907) ?3908) (inverse ?3907) [3908, 3907] by Super 3379 with 671 at 2,2
% 9.64/2.76 Id : 3450, {_}: commutator ?3907 (multiply ?3907 ?3908) =<= commutator (multiply (inverse ?3907) ?3908) (inverse ?3907) [3908, 3907] by Demod 3398 with 243 at 1,2,2
% 9.64/2.76 Id : 33433, {_}: commutator (inverse ?2769) ?2768 =<= commutator (inverse (multiply ?2769 ?2768)) (inverse ?2769) [2768, 2769] by Demod 2498 with 33399 at 2
% 9.64/2.76 Id : 33434, {_}: commutator (inverse ?2769) ?2768 =<= commutator (inverse ?2769) (multiply ?2769 ?2768) [2768, 2769] by Demod 33433 with 33399 at 3
% 9.64/2.76 Id : 33435, {_}: commutator ?2768 ?2769 =<= commutator (inverse ?2769) (multiply ?2769 ?2768) [2769, 2768] by Demod 33434 with 33399 at 2
% 9.64/2.76 Id : 33436, {_}: commutator ?2768 ?2769 =<= commutator (multiply ?2769 ?2768) ?2769 [2769, 2768] by Demod 33435 with 33399 at 3
% 9.64/2.76 Id : 33453, {_}: commutator ?3907 (multiply ?3907 ?3908) =>= commutator ?3908 (inverse ?3907) [3908, 3907] by Demod 3450 with 33436 at 3
% 9.64/2.76 Id : 33475, {_}: commutator ?2708 ?2709 =<= commutator ?2709 (inverse ?2708) [2709, 2708] by Demod 33422 with 33453 at 3
% 9.64/2.76 Id : 33480, {_}: commutator ?493 ?492 =<= multiply ?492 (multiply (inverse (multiply ?492 ?493)) ?493) [492, 493] by Demod 11960 with 33475 at 2
% 9.64/2.76 Id : 33600, {_}: commutator ?32825 (commutator ?32826 ?32825) =<= multiply (commutator ?32826 ?32825) (multiply (inverse (multiply ?32825 (commutator ?32826 ?32825))) ?32825) [32826, 32825] by Super 33480 with 33308 at 1,1,2,3
% 9.64/2.76 Id : 1089, {_}: multiply (inverse ?1073) ?1074 =<= multiply ?1075 (multiply (inverse (multiply ?1073 ?1075)) ?1074) [1075, 1074, 1073] by Super 4 with 1018 at 1,2
% 9.64/2.76 Id : 33643, {_}: commutator ?32825 (commutator ?32826 ?32825) =>= multiply (inverse ?32825) ?32825 [32826, 32825] by Demod 33600 with 1089 at 3
% 9.64/2.76 Id : 33644, {_}: commutator ?32825 (commutator ?32826 ?32825) =>= identity [32826, 32825] by Demod 33643 with 3 at 3
% 9.64/2.76 Id : 33926, {_}: inverse identity =<= commutator (commutator ?32975 ?32976) ?32976 [32976, 32975] by Super 2432 with 33644 at 1,2
% 9.64/2.76 Id : 33996, {_}: identity =<= commutator (commutator ?32975 ?32976) ?32976 [32976, 32975] by Demod 33926 with 122 at 2
% 9.64/2.76 Id : 34502, {_}: identity =?= identity [] by Demod 1 with 33996 at 2
% 9.64/2.76 Id : 1, {_}: commutator (commutator a b) b =>= identity [] by prove_commutator
% 9.64/2.76 % SZS output end CNFRefutation for theBenchmark.p
% 9.64/2.76 1833: solved /export/starexec/sandbox2/benchmark/theBenchmark.p in 2.420263 using kbo
%------------------------------------------------------------------------------