%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP024-5 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 09:12:11 EDT 2022 % Result : Unsatisfiable 197.18s 197.60s % Output : CNFRefutation 197.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP024-5 : TPTP v8.1.0. Released v2.2.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.13/0.33 % Computer : n009.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon Jun 13 22:34:23 EDT 2022 % 0.13/0.34 % CPUTime : % 197.18/197.60 Theorem Proved. % 197.18/197.60 % SZS status Unsatisfiable % 197.18/197.60 % SZS output start CNFRefutation % 197.18/197.60 [1=axiom,[], % 197.18/197.60 commutator(commutator(X10,X11),X12) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [2=axiom,[], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,X11))) = commutator(X10,X11)]. % 197.18/197.60 [3=axiom,[], % 197.18/197.60 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 197.18/197.60 [4=axiom,[], % 197.18/197.60 multiply(inverse(X10),X10) = identity]. % 197.18/197.60 [5=axiom,[], % 197.18/197.60 multiply(identity,X10) = X10]. % 197.18/197.60 [6=axiom,[], % 197.18/197.60 thtop(X10,X10) = thmfalse]. % 197.18/197.60 [7=axiom,[], % 197.18/197.60 thtop(multiply(a,commutator(b,c)),multiply(commutator(b,c),a)) = thmtrue]. % 197.18/197.60 [8=param(3,4),[5], % 197.18/197.60 multiply(inverse(X11),multiply(X11,X10)) = X10]. % 197.18/197.60 [9=param(8,3),[], % 197.18/197.60 multiply(inverse(multiply(X10,X11)),multiply(X10,multiply(X11,X12))) = X12]. % 197.18/197.60 [10=param(8,4),[], % 197.18/197.60 multiply(inverse(inverse(X10)),identity) = X10]. % 197.18/197.60 [12=param(8,8),[], % 197.18/197.60 multiply(inverse(inverse(X10)),X11) = multiply(X10,X11)]. % 197.18/197.60 [13=demod(10),[12], % 197.18/197.60 multiply(X10,identity) = X10]. % 197.18/197.60 [14=param(13,4),[], % 197.18/197.60 inverse(identity) = identity]. % 197.18/197.60 [15=param(2,4),[13,4], % 197.18/197.60 commutator(inverse(X10),X10) = identity]. % 197.18/197.60 [16=param(2,5),[14,4,5], % 197.18/197.60 commutator(identity,X10) = identity]. % 197.18/197.60 [17=param(2,8),[4], % 197.18/197.60 commutator(X10,X10) = identity]. % 197.18/197.60 [18=param(2,8),[12], % 197.18/197.60 multiply(X10,multiply(inverse(multiply(X10,X11)),X11)) = commutator(inverse(X10),multiply(X10,X11))]. % 197.18/197.60 [19=param(8,2),[12], % 197.18/197.60 multiply(X10,commutator(X10,X11)) = multiply(inverse(X11),multiply(X10,X11))]. % 197.18/197.60 [20=param(2,13),[14,5,4], % 197.18/197.60 commutator(X10,identity) = identity]. % 197.18/197.60 [21=param(9,2),[], % 197.18/197.60 multiply(inverse(multiply(inverse(X10),inverse(X11))),commutator(X10,X11)) = multiply(X10,X11)]. % 197.18/197.60 [22=param(2,9),[4], % 197.18/197.60 commutator(X10,multiply(X10,X10)) = identity]. % 197.18/197.60 [27=param(1,17),[16], % 197.18/197.60 commutator(X10,commutator(X10,X11)) = identity]. % 197.18/197.60 [28=param(12,2),[], % 197.18/197.60 multiply(X10,multiply(inverse(X11),multiply(inverse(X10),X11))) = commutator(inverse(X10),X11)]. % 197.18/197.60 [29=param(2,12),[], % 197.18/197.60 multiply(inverse(X10),multiply(X11,multiply(X10,inverse(X11)))) = commutator(X10,inverse(X11))]. % 197.18/197.60 [31=param(12,4),[], % 197.18/197.60 multiply(X10,inverse(X10)) = identity]. % 197.18/197.60 [32=param(12,8),[], % 197.18/197.60 multiply(X10,multiply(inverse(X10),X11)) = X11]. % 197.18/197.60 [33=param(12,13),[13], % 197.18/197.60 inverse(inverse(X10)) = X10]. % 197.18/197.60 [35=param(31,3),[], % 197.18/197.60 multiply(X10,multiply(X11,inverse(multiply(X10,X11)))) = identity]. % 197.18/197.60 [36=param(9,31),[13], % 197.18/197.60 multiply(inverse(multiply(X10,X11)),X10) = inverse(X11)]. % 197.18/197.60 [37=param(1,15),[16], % 197.18/197.60 commutator(inverse(X10),commutator(X10,X11)) = identity]. % 197.18/197.60 [42=param(1,22),[16], % 197.18/197.60 commutator(X10,commutator(multiply(X10,X10),X11)) = identity]. % 197.18/197.60 [44=param(8,19),[33], % 197.18/197.60 multiply(X10,multiply(X11,commutator(X11,X10))) = multiply(X11,X10)]. % 197.18/197.60 [48=param(9,32),[], % 197.18/197.60 multiply(inverse(multiply(X10,X11)),multiply(X10,X12)) = multiply(inverse(X11),X12)]. % 197.18/197.60 [51=param(21,27),[13], % 197.18/197.60 inverse(multiply(inverse(X10),inverse(commutator(X10,X11)))) = multiply(X10,commutator(X10,X11))]. % 197.18/197.60 [52=param(21,37),[33,13], % 197.18/197.60 multiply(inverse(X10),commutator(X10,X11)) = inverse(multiply(X10,inverse(commutator(X10,X11))))]. % 197.18/197.60 [53=param(36,2),[], % 197.18/197.60 multiply(inverse(commutator(X10,X11)),inverse(X10)) = inverse(multiply(inverse(X11),multiply(X10,X11)))]. % 197.18/197.60 [54=param(36,8),[], % 197.18/197.60 multiply(inverse(X10),inverse(X11)) = inverse(multiply(X11,X10))]. % 197.18/197.60 [55=demod(53),[54], % 197.18/197.60 inverse(multiply(X10,commutator(X10,X11))) = inverse(multiply(inverse(X11),multiply(X10,X11)))]. % 197.18/197.60 [58=param(36,32),[], % 197.18/197.60 multiply(inverse(X10),X11) = inverse(multiply(inverse(X11),X10))]. % 197.18/197.60 [59=demod(18),[58], % 197.18/197.60 multiply(X10,inverse(multiply(inverse(X11),multiply(X10,X11)))) = commutator(inverse(X10),multiply(X10,X11))]. % 197.18/197.60 [64=param(3,44),[3,3], % 197.18/197.60 multiply(X11,multiply(X10,multiply(commutator(X10,X11),X12))) = multiply(X10,multiply(X11,X12))]. % 197.18/197.60 [66=param(44,27),[13], % 197.18/197.60 multiply(commutator(X10,X11),X10) = multiply(X10,commutator(X10,X11))]. % 197.18/197.60 [69=param(44,42),[13], % 197.18/197.60 multiply(commutator(multiply(X10,X10),X11),X10) = multiply(X10,commutator(multiply(X10,X10),X11))]. % 197.18/197.60 [70=param(2,66),[8,4,1], % 197.18/197.60 commutator(X10,commutator(X11,X10)) = identity]. % 197.18/197.60 [71=param(3,66),[3], % 197.18/197.60 multiply(commutator(X10,X11),multiply(X10,X12)) = multiply(X10,multiply(commutator(X10,X11),X12))]. % 197.18/197.60 [72=param(8,29),[33], % 197.18/197.60 multiply(X10,commutator(X10,inverse(X11))) = multiply(X11,multiply(X10,inverse(X11)))]. % 197.18/197.60 [73=param(29,33),[], % 197.18/197.60 multiply(X10,multiply(X11,multiply(inverse(X10),inverse(X11)))) = commutator(inverse(X10),inverse(X11))]. % 197.18/197.60 [75=param(70,1),[], % 197.18/197.60 commutator(X10,commutator(X11,commutator(X12,X10))) = identity]. % 197.18/197.60 [77=param(44,70),[13], % 197.18/197.60 multiply(commutator(X10,X11),X11) = multiply(X11,commutator(X10,X11))]. % 197.18/197.60 [78=param(3,77),[3], % 197.18/197.60 multiply(commutator(X11,X10),multiply(X10,X12)) = multiply(X10,multiply(commutator(X11,X10),X12))]. % 197.18/197.60 [80=param(8,35),[13], % 197.18/197.60 multiply(X11,inverse(multiply(X10,X11))) = inverse(X10)]. % 197.18/197.60 [82=param(2,80),[33,3,29], % 197.18/197.60 commutator(X10,inverse(multiply(X11,X10))) = commutator(X10,inverse(X11))]. % 197.18/197.60 [84=param(80,3),[], % 197.18/197.60 multiply(X10,inverse(multiply(X11,multiply(X12,X10)))) = inverse(multiply(X11,X12))]. % 197.18/197.60 [87=param(80,19),[3,33], % 197.18/197.60 multiply(X10,multiply(X11,inverse(multiply(X10,commutator(X10,X11))))) = X11]. % 197.18/197.60 [90=param(80,66),[], % 197.18/197.60 multiply(X10,inverse(multiply(X10,commutator(X10,X11)))) = inverse(commutator(X10,X11))]. % 197.18/197.60 [91=param(80,77),[], % 197.18/197.60 multiply(X10,inverse(multiply(X10,commutator(X11,X10)))) = inverse(commutator(X11,X10))]. % 197.18/197.60 [99=param(1,82),[1], % 197.18/197.60 commutator(X10,commutator(inverse(multiply(X11,X10)),X12)) = commutator(X10,commutator(inverse(X11),X12))]. % 197.18/197.60 [105=param(58,33),[], % 197.18/197.60 multiply(X10,X11) = inverse(multiply(inverse(X11),inverse(X10)))]. % 197.18/197.60 [110=demod(69),[105], % 197.18/197.60 inverse(multiply(inverse(X10),inverse(commutator(multiply(X10,X10),X11)))) = multiply(X10,commutator(multiply(X10,X10),X11))]. % 197.18/197.60 [111=param(58,58),[3], % 197.18/197.60 multiply(inverse(X10),multiply(X11,X12)) = inverse(multiply(inverse(X12),multiply(inverse(X11),X10)))]. % 197.18/197.60 [113=param(58,19),[-111,58], % 197.18/197.60 multiply(inverse(X10),multiply(X11,X10)) = inverse(multiply(inverse(X11),commutator(inverse(X11),X10)))]. % 197.18/197.60 [114=param(58,58),[3], % 197.18/197.60 inverse(multiply(inverse(X10),multiply(X11,X12))) = multiply(inverse(X12),multiply(inverse(X11),X10))]. % 197.18/197.60 [115=demod(28),[-114,59], % 197.18/197.60 commutator(inverse(X10),multiply(X10,X11)) = commutator(inverse(X10),X11)]. % 197.18/197.60 [118=param(115,2),[33,27,33], % 197.18/197.60 commutator(X10,multiply(inverse(X11),multiply(X10,X11))) = identity]. % 197.18/197.60 [119=param(115,8),[33,33], % 197.18/197.60 commutator(X10,multiply(X10,X11)) = commutator(X10,X11)]. % 197.18/197.60 [122=param(115,19),[33,33], % 197.18/197.60 commutator(X10,multiply(X11,commutator(X11,X10))) = commutator(X10,multiply(X11,X10))]. % 197.18/197.60 [123=param(115,29),[33,27,33], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,inverse(X11)))) = identity]. % 197.18/197.60 [124=param(115,33),[33], % 197.18/197.60 commutator(X10,multiply(inverse(X10),X11)) = commutator(X10,X11)]. % 197.18/197.60 [129=param(119,1),[1], % 197.18/197.60 commutator(X10,commutator(X11,multiply(commutator(X10,X11),X12))) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [130=param(1,119),[1], % 197.18/197.60 commutator(X10,commutator(multiply(X10,X11),X12)) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [131=param(119,3),[], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X10,multiply(X11,X12))) = commutator(multiply(X10,X11),X12)]. % 197.18/197.60 [132=param(19,119),[113,115], % 197.18/197.60 inverse(multiply(inverse(X10),commutator(inverse(X10),X11))) = multiply(X10,commutator(X10,X11))]. % 197.18/197.60 [134=param(70,119),[], % 197.18/197.60 commutator(multiply(X10,X11),commutator(X10,X11)) = identity]. % 197.18/197.60 [150=param(48,2),[3,2], % 197.18/197.60 commutator(multiply(inverse(X11),X10),X11) = commutator(X10,X11)]. % 197.18/197.60 [151=param(48,8),[], % 197.18/197.60 multiply(inverse(multiply(X11,X10)),X12) = multiply(inverse(X10),multiply(inverse(X11),X12))]. % 197.18/197.60 [153=param(27,150),[], % 197.18/197.60 commutator(multiply(inverse(X10),X11),commutator(X11,X10)) = identity]. % 197.18/197.60 [162=param(153,119),[58,8], % 197.18/197.60 commutator(inverse(X10),commutator(X11,X10)) = identity]. % 197.18/197.60 [168=param(44,162),[13,105,33], % 197.18/197.60 multiply(inverse(X10),commutator(X11,X10)) = inverse(multiply(X10,inverse(commutator(X11,X10))))]. % 197.18/197.60 [169=param(162,82),[33], % 197.18/197.60 commutator(multiply(X10,X11),commutator(X11,inverse(X10))) = identity]. % 197.18/197.60 [171=param(162,119),[], % 197.18/197.60 commutator(inverse(multiply(X10,X11)),commutator(X10,X11)) = identity]. % 197.18/197.60 [175=param(171,82),[80,33], % 197.18/197.60 commutator(X10,commutator(X11,inverse(X10))) = identity]. % 197.18/197.60 [179=param(33,51),[], % 197.18/197.60 multiply(inverse(X10),inverse(commutator(X10,X11))) = inverse(multiply(X10,commutator(X10,X11)))]. % 197.18/197.60 [186=param(80,52),[33,-72,33], % 197.18/197.60 multiply(X10,commutator(X10,inverse(commutator(X10,X11)))) = X10]. % 197.18/197.60 [191=param(8,186),[4], % 197.18/197.60 commutator(X10,inverse(commutator(X10,X11))) = identity]. % 197.18/197.60 [195=param(2,54),[33,33], % 197.18/197.60 multiply(X10,multiply(X11,inverse(multiply(X11,X10)))) = commutator(inverse(X10),inverse(X11))]. % 197.18/197.60 [196=param(54,33),[], % 197.18/197.60 multiply(X10,inverse(X11)) = inverse(multiply(X11,inverse(X10)))]. % 197.18/197.60 [197=param(54,54),[3], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),inverse(X12))) = inverse(multiply(X12,multiply(X11,X10)))]. % 197.18/197.60 [199=param(54,3),[], % 197.18/197.60 inverse(multiply(X10,multiply(X11,X12))) = multiply(inverse(X12),inverse(multiply(X10,X11)))]. % 197.18/197.60 [206=param(55,82),[33,80,3], % 197.18/197.60 inverse(multiply(X10,commutator(X10,inverse(X11)))) = inverse(multiply(X11,multiply(X10,inverse(X11))))]. % 197.18/197.60 [222=param(64,19),[1,162,13], % 197.18/197.60 multiply(X10,commutator(inverse(X11),X10)) = multiply(inverse(X11),multiply(X10,X11))]. % 197.18/197.60 [223=param(64,31),[13], % 197.18/197.60 multiply(X11,multiply(X10,inverse(commutator(X11,X10)))) = multiply(X10,X11)]. % 197.18/197.60 [232=param(196,3),[], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,X12)))) = multiply(X11,multiply(X12,inverse(X10)))]. % 197.18/197.60 [233=param(196,54),[3], % 197.18/197.60 multiply(X10,multiply(inverse(X11),inverse(X12))) = inverse(multiply(X12,multiply(X11,inverse(X10))))]. % 197.18/197.60 [234=demod(73),[233], % 197.18/197.60 multiply(X10,inverse(multiply(X11,multiply(X10,inverse(X11))))) = commutator(inverse(X10),inverse(X11))]. % 197.18/197.60 [237=param(196,3),[], % 197.18/197.60 inverse(multiply(X10,multiply(X11,inverse(X12)))) = multiply(X12,inverse(multiply(X10,X11)))]. % 197.18/197.60 [244=param(2,72),[111,8,54,33,8], % 197.18/197.60 commutator(X11,multiply(X10,inverse(X11))) = commutator(X10,inverse(X11))]. % 197.18/197.60 [246=param(64,72),[1,175,13], % 197.18/197.60 multiply(X10,commutator(X11,X10)) = multiply(X11,multiply(X10,inverse(X11)))]. % 197.18/197.60 [248=param(244,3),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X12,inverse(X10)))) = commutator(multiply(X11,X12),inverse(X10))]. % 197.18/197.60 [249=param(244,33),[33], % 197.18/197.60 commutator(inverse(X10),multiply(X11,X10)) = commutator(X11,X10)]. % 197.18/197.60 [252=param(244,54),[], % 197.18/197.60 commutator(X10,inverse(multiply(X10,X11))) = commutator(inverse(X11),inverse(X10))]. % 197.18/197.60 [253=param(244,80),[82], % 197.18/197.60 commutator(multiply(X10,X11),inverse(X10)) = commutator(X11,inverse(X10))]. % 197.18/197.60 [258=param(191,244),[], % 197.18/197.60 commutator(X10,inverse(commutator(X11,inverse(X10)))) = identity]. % 197.18/197.60 [262=param(258,33),[], % 197.18/197.60 commutator(inverse(X10),inverse(commutator(X11,X10))) = identity]. % 197.18/197.60 [278=param(44,262),[13,54], % 197.18/197.60 multiply(inverse(X10),inverse(commutator(X11,X10))) = inverse(multiply(X10,commutator(X11,X10)))]. % 197.18/197.60 [282=param(84,19),[], % 197.18/197.60 multiply(X10,inverse(multiply(X11,commutator(X11,X10)))) = inverse(multiply(inverse(X10),X11))]. % 197.18/197.60 [285=param(1,249),[1], % 197.18/197.60 commutator(inverse(X11),commutator(multiply(X10,X11),X12)) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [287=param(249,8),[115], % 197.18/197.60 commutator(inverse(multiply(X10,X11)),X11) = commutator(inverse(X10),X11)]. % 197.18/197.60 [291=param(249,52),[82,37], % 197.18/197.60 commutator(inverse(commutator(X10,X11)),inverse(X10)) = identity]. % 197.18/197.60 [296=param(291,33),[], % 197.18/197.60 commutator(inverse(commutator(inverse(X10),X11)),X10) = identity]. % 197.18/197.60 [304=param(19,296),[58,14,5,58,132,8], % 197.18/197.60 inverse(commutator(inverse(X10),X11)) = commutator(X10,X11)]. % 197.18/197.60 [307=param(304,33),[], % 197.18/197.60 commutator(inverse(X10),X11) = inverse(commutator(X10,X11))]. % 197.18/197.60 [311=demod(99),[307,307], % 197.18/197.60 commutator(X10,inverse(commutator(multiply(X11,X10),X12))) = commutator(X10,inverse(commutator(X11,X12)))]. % 197.18/197.60 [314=demod(222),[307], % 197.18/197.60 multiply(X10,inverse(commutator(X11,X10))) = multiply(inverse(X11),multiply(X10,X11))]. % 197.18/197.60 [319=demod(234),[307], % 197.18/197.60 multiply(X10,inverse(multiply(X11,multiply(X10,inverse(X11))))) = inverse(commutator(X10,inverse(X11)))]. % 197.18/197.60 [321=demod(195),[307], % 197.18/197.60 multiply(X10,multiply(X11,inverse(multiply(X11,X10)))) = inverse(commutator(X10,inverse(X11)))]. % 197.18/197.60 [324=demod(249),[307], % 197.18/197.60 inverse(commutator(X10,multiply(X11,X10))) = commutator(X11,X10)]. % 197.18/197.60 [326=demod(285),[307], % 197.18/197.60 inverse(commutator(X10,commutator(multiply(X11,X10),X12))) = commutator(X11,commutator(X10,X12))]. % 197.18/197.60 [328=demod(252),[307], % 197.18/197.60 commutator(X10,inverse(multiply(X10,X11))) = inverse(commutator(X11,inverse(X10)))]. % 197.18/197.60 [329=demod(287),[307,307], % 197.18/197.60 inverse(commutator(multiply(X10,X11),X11)) = inverse(commutator(X10,X11))]. % 197.18/197.60 [331=param(8,87),[], % 197.18/197.60 multiply(inverse(X10),X11) = multiply(X11,inverse(multiply(X10,commutator(X10,X11))))]. % 197.18/197.60 [332=demod(4),[], % 197.18/197.60 multiply(inverse(X10),X10) = identity]. % 197.18/197.60 [336=param(87,134),[3,13,-237,223,3,321], % 197.18/197.60 inverse(commutator(X10,inverse(X11))) = commutator(X10,X11)]. % 197.18/197.60 [337=demod(321),[336], % 197.18/197.60 multiply(X10,multiply(X11,inverse(multiply(X11,X10)))) = commutator(X10,X11)]. % 197.18/197.60 [339=demod(319),[336], % 197.18/197.60 multiply(X10,inverse(multiply(X11,multiply(X10,inverse(X11))))) = commutator(X10,X11)]. % 197.18/197.60 [341=demod(328),[336], % 197.18/197.60 commutator(X10,inverse(multiply(X10,X11))) = commutator(X11,X10)]. % 197.18/197.60 [343=param(87,169),[3,13,-237,336,44,3,337], % 197.18/197.60 commutator(X10,X11) = commutator(X11,inverse(X10))]. % 197.18/197.60 [344=demod(329),[343,82,336], % 197.18/197.60 commutator(X10,X11) = inverse(commutator(X11,X10))]. % 197.18/197.60 [350=demod(253),[343,307,341], % 197.18/197.60 commutator(X10,inverse(X11)) = inverse(commutator(X10,X11))]. % 197.18/197.60 [351=demod(244),[350], % 197.18/197.60 commutator(X10,multiply(X11,inverse(X10))) = inverse(commutator(X11,X10))]. % 197.18/197.60 [353=demod(206),[350], % 197.18/197.60 inverse(multiply(X10,inverse(commutator(X10,X11)))) = inverse(multiply(X11,multiply(X10,inverse(X11))))]. % 197.18/197.60 [354=demod(72),[350], % 197.18/197.60 multiply(X10,inverse(commutator(X10,X11))) = multiply(X11,multiply(X10,inverse(X11)))]. % 197.18/197.60 [356=demod(311),[350,326,350], % 197.18/197.60 commutator(X10,commutator(X11,X12)) = inverse(commutator(X11,commutator(X10,X12)))]. % 197.18/197.60 [366=demod(248),[350], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X12,inverse(X10)))) = inverse(commutator(multiply(X11,X12),X10))]. % 197.18/197.60 [368=param(44,350),[], % 197.18/197.60 multiply(inverse(X10),multiply(X11,inverse(commutator(X11,X10)))) = multiply(X11,inverse(X10))]. % 197.18/197.60 [370=param(350,58),[], % 197.18/197.60 commutator(X10,multiply(inverse(X11),X12)) = inverse(commutator(X10,multiply(inverse(X12),X11)))]. % 197.18/197.60 [372=param(307,54),[], % 197.18/197.60 commutator(multiply(inverse(X10),inverse(X11)),X12) = inverse(commutator(multiply(X11,X10),X12))]. % 197.18/197.60 [374=param(307,196),[], % 197.18/197.60 commutator(multiply(X10,inverse(X11)),X12) = inverse(commutator(multiply(X11,inverse(X10)),X12))]. % 197.18/197.60 [375=param(344,1),[], % 197.18/197.60 inverse(commutator(X10,commutator(X11,X12))) = commutator(X11,commutator(X12,X10))]. % 197.18/197.60 [378=param(7,344),[343,350,58], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(inverse(a),commutator(c,b)))) = thmtrue]. % 197.18/197.60 [381=param(87,344),[], % 197.18/197.60 multiply(X10,multiply(X11,inverse(multiply(X10,inverse(commutator(X11,X10)))))) = X11]. % 197.18/197.60 [383=param(54,344),[], % 197.18/197.60 multiply(commutator(X10,X11),inverse(X12)) = inverse(multiply(X12,commutator(X11,X10)))]. % 197.18/197.60 [384=param(54,344),[], % 197.18/197.60 multiply(inverse(X10),commutator(X11,X12)) = inverse(multiply(commutator(X12,X11),X10))]. % 197.18/197.60 [385=param(58,344),[], % 197.18/197.60 multiply(commutator(X10,X11),X12) = inverse(multiply(inverse(X12),commutator(X11,X10)))]. % 197.18/197.60 [387=param(332,344),[], % 197.18/197.60 multiply(commutator(X10,X11),commutator(X11,X10)) = identity]. % 197.18/197.60 [391=param(3,387),[5], % 197.18/197.60 multiply(commutator(X11,X12),multiply(commutator(X12,X11),X10)) = X10]. % 197.18/197.60 [392=param(33,324),[], % 197.18/197.60 commutator(X11,multiply(X10,X11)) = inverse(commutator(X10,X11))]. % 197.18/197.60 [393=demod(122),[392], % 197.18/197.60 commutator(X10,multiply(X11,commutator(X11,X10))) = inverse(commutator(X11,X10))]. % 197.18/197.60 [394=param(1,392),[307,1], % 197.18/197.60 commutator(X11,commutator(multiply(X10,X11),X12)) = inverse(commutator(X10,commutator(X11,X12)))]. % 197.18/197.60 [395=param(392,3),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X12,X10))) = inverse(commutator(multiply(X11,X12),X10))]. % 197.18/197.60 [396=param(392,19),[307,392,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X10,commutator(X10,X11))) = inverse(commutator(X10,X11))]. % 197.18/197.60 [410=param(105,3),[], % 197.18/197.60 inverse(multiply(inverse(X10),inverse(multiply(X11,X12)))) = multiply(X11,multiply(X12,X10))]. % 197.18/197.60 [417=param(393,344),[], % 197.18/197.60 commutator(X10,multiply(X11,inverse(commutator(X10,X11)))) = inverse(commutator(X11,X10))]. % 197.18/197.60 [422=param(8,391),[], % 197.18/197.60 multiply(inverse(commutator(X10,X11)),X12) = multiply(commutator(X11,X10),X12)]. % 197.18/197.60 [424=param(119,391),[1,1], % 197.18/197.60 commutator(X10,commutator(X11,multiply(commutator(X11,X10),X12))) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [428=param(8,337),[52], % 197.18/197.60 inverse(multiply(X10,inverse(commutator(X10,X11)))) = multiply(X11,inverse(multiply(X11,X10)))]. % 197.18/197.60 [430=param(124,337),[307,350,27,14], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X11,inverse(X10))))) = identity]. % 197.18/197.60 [438=param(87,430),[13,3,54,339], % 197.18/197.60 multiply(X10,commutator(X11,X10)) = multiply(X11,inverse(multiply(X11,inverse(X10))))]. % 197.18/197.60 [439=param(223,54),[350,58,168,33], % 197.18/197.60 multiply(X10,inverse(multiply(X11,inverse(commutator(X10,X11))))) = multiply(inverse(X11),X10)]. % 197.18/197.60 [440=param(223,58),[307,33,58,33], % 197.18/197.60 multiply(inverse(X11),multiply(X10,commutator(X11,X10))) = multiply(X10,inverse(X11))]. % 197.18/197.60 [441=param(223,71),[1,70,14,385,14,5], % 197.18/197.60 multiply(X10,commutator(X10,X11)) = multiply(X10,inverse(commutator(X11,X10)))]. % 197.18/197.60 [442=param(223,78),[1,17,20,14,385,14,5], % 197.18/197.60 multiply(X10,commutator(X11,X10)) = multiply(X10,inverse(commutator(X10,X11)))]. % 197.18/197.60 [443=param(124,223),[351,307,33], % 197.18/197.60 commutator(X11,multiply(X10,commutator(X11,X10))) = inverse(commutator(X10,X11))]. % 197.18/197.60 [444=param(223,392),[33,3,3], % 197.18/197.60 multiply(X10,multiply(X11,multiply(X10,commutator(X11,X10)))) = multiply(X11,multiply(X10,X10))]. % 197.18/197.60 [449=param(129,344),[1,343,350,350,424,33], % 197.18/197.60 commutator(X10,commutator(X11,X12)) = commutator(X11,commutator(X10,X12))]. % 197.18/197.60 [462=param(130,344),[350], % 197.18/197.60 inverse(commutator(X10,commutator(X11,multiply(X10,X12)))) = commutator(X10,commutator(X12,X11))]. % 197.18/197.60 [463=param(130,392),[350,395,350,394,33], % 197.18/197.60 inverse(commutator(X10,commutator(X11,multiply(X10,X12)))) = commutator(X11,commutator(X10,X12))]. % 197.18/197.60 [464=demod(462),[463], % 197.18/197.60 commutator(X10,commutator(X11,X12)) = commutator(X11,commutator(X12,X10))]. % 197.18/197.60 [513=param(464,130),[-375,130], % 197.18/197.60 inverse(commutator(X10,commutator(X11,X12))) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [517=demod(394),[513], % 197.18/197.60 commutator(X10,commutator(multiply(X11,X10),X12)) = commutator(X11,commutator(X10,X12))]. % 197.18/197.60 [527=param(464,344),[350,513], % 197.18/197.60 commutator(X10,commutator(X11,X12)) = commutator(X12,commutator(X11,X10))]. % 197.18/197.60 [528=param(387,464),[1], % 197.18/197.60 multiply(commutator(X10,commutator(X11,X12)),commutator(X10,commutator(X11,X12))) = identity]. % 197.18/197.60 [549=param(124,197),[350,395,33], % 197.18/197.60 commutator(multiply(X10,X11),X12) = commutator(X12,multiply(inverse(X11),inverse(X10)))]. % 197.18/197.60 [569=param(199,54),[33], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,X12)))) = multiply(X11,inverse(multiply(X10,inverse(X12))))]. % 197.18/197.60 [570=demod(438),[-569], % 197.18/197.60 multiply(X10,commutator(X11,X10)) = inverse(multiply(X11,inverse(multiply(X11,X10))))]. % 197.18/197.60 [572=param(199,196),[33], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,inverse(X12))))) = multiply(X11,inverse(multiply(X10,X12)))]. % 197.18/197.60 [577=param(417,392),[33,3,343,350,392,33], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,commutator(X11,X10)))) = inverse(commutator(X11,X10))]. % 197.18/197.60 [632=param(442,129),[513,1,343,350,350,424,513], % 197.18/197.60 multiply(X10,commutator(X10,commutator(X11,X12))) = multiply(X10,commutator(X11,commutator(X10,X12)))]. % 197.18/197.60 [653=param(246,54),[350,278], % 197.18/197.60 multiply(X10,inverse(multiply(X10,X11))) = inverse(multiply(X11,commutator(X10,X11)))]. % 197.18/197.60 [655=param(84,246),[], % 197.18/197.60 multiply(inverse(X10),inverse(multiply(X11,commutator(X10,X11)))) = inverse(multiply(X10,X11))]. % 197.18/197.60 [656=param(131,246),[350,343,350,119,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X11,commutator(X10,X11))) = commutator(X10,X11)]. % 197.18/197.60 [660=param(344,656),[], % 197.18/197.60 commutator(multiply(X11,commutator(X10,X11)),multiply(X10,X11)) = inverse(commutator(X10,X11))]. % 197.18/197.60 [663=param(660,344),[], % 197.18/197.60 commutator(multiply(X10,inverse(commutator(X10,X11))),multiply(X11,X10)) = inverse(commutator(X11,X10))]. % 197.18/197.60 [667=param(577,58),[307,58,33,307,33], % 197.18/197.60 commutator(X10,multiply(inverse(X11),multiply(X10,inverse(commutator(X11,X10))))) = commutator(X11,X10)]. % 197.18/197.60 [672=param(577,392),[3,223,392,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X11,multiply(X11,X10))) = commutator(X10,X11)]. % 197.18/197.60 [677=param(344,672),[], % 197.18/197.60 commutator(multiply(X11,multiply(X11,X10)),multiply(X10,X11)) = inverse(commutator(X10,X11))]. % 197.18/197.60 [679=param(677,32),[3,343,350,124,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(inverse(X10),multiply(X11,X10))) = commutator(X10,X11)]. % 197.18/197.60 [683=param(396,307),[179,350,343,350,33,307,33], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(inverse(X10),X11)) = commutator(X10,X11)]. % 197.18/197.60 [693=param(33,282),[], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,commutator(X11,X10))))) = multiply(inverse(X10),X11)]. % 197.18/197.60 [713=param(679,19),[], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X11,commutator(X11,X10))) = commutator(X10,X11)]. % 197.18/197.60 [717=param(713,54),[350,307,33,52,350,307,33,350,307,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X10,inverse(commutator(X10,X11)))) = commutator(X11,X10)]. % 197.18/197.60 [719=param(713,105),[343,33], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(inverse(X10),inverse(X11))) = commutator(X11,X10)]. % 197.18/197.60 [724=param(344,713),[], % 197.18/197.60 commutator(multiply(X11,commutator(X11,X10)),multiply(X10,X11)) = inverse(commutator(X10,X11))]. % 197.18/197.60 [727=param(724,123),[13,3,3,343,350,123,14,14], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,multiply(inverse(X11),X10)))) = identity]. % 197.18/197.60 [731=param(727,8),[3], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X10,multiply(X10,multiply(X11,X11)))) = identity]. % 197.18/197.60 [769=param(717,105),[33,385,33,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X10,commutator(X11,X10))) = commutator(X11,X10)]. % 197.18/197.60 [770=param(717,246),[351,33,343,350,351,33], % 197.18/197.60 commutator(multiply(X10,commutator(X11,X10)),multiply(X11,commutator(X10,X11))) = commutator(X10,X11)]. % 197.18/197.60 [776=param(769,392),[3,3,223,392], % 197.18/197.60 commutator(multiply(X10,multiply(X11,X11)),multiply(X11,X10)) = inverse(commutator(X10,X11))]. % 197.18/197.60 [782=param(344,776),[33], % 197.18/197.60 commutator(multiply(X11,X10),multiply(X10,multiply(X11,X11))) = commutator(X10,X11)]. % 197.18/197.60 [785=param(782,8),[54,3,350,343,350,119,33], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,inverse(multiply(X11,X11))))) = commutator(X11,X10)]. % 197.18/197.60 [840=param(54,383),[33,33], % 197.18/197.60 multiply(X10,commutator(X11,X12)) = multiply(X10,inverse(commutator(X12,X11)))]. % 197.18/197.60 [891=param(731,528),[13], % 197.18/197.60 commutator(multiply(X10,commutator(X11,commutator(X12,X13))),multiply(X10,X10)) = identity]. % 197.18/197.60 [1024=param(549,118),[3,-549], % 197.18/197.60 commutator(multiply(X10,X11),multiply(inverse(X12),multiply(X10,multiply(X11,X12)))) = identity]. % 197.18/197.60 [1075=param(1024,80),[33,3], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X12,multiply(X11,multiply(X10,inverse(X12))))) = identity]. % 197.18/197.60 [1115=param(1075,54),[], % 197.18/197.60 commutator(multiply(inverse(X10),X11),multiply(X12,multiply(X11,inverse(multiply(X12,X10))))) = identity]. % 197.18/197.60 [1125=param(1075,381),[3,151,33,8], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,multiply(commutator(X10,X12),inverse(X11))))) = identity]. % 197.18/197.60 [1331=param(1125,785),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,multiply(commutator(X12,X10),inverse(X11))))) = identity]. % 197.18/197.60 [1332=param(1331,33),[], % 197.18/197.60 commutator(X10,multiply(inverse(X11),multiply(X10,multiply(commutator(X12,X10),X11)))) = identity]. % 197.18/197.60 [1354=param(1332,713),[3,391], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(inverse(X12),multiply(X10,X12))) = identity]. % 197.18/197.60 [1363=param(1354,428),[33,3,-569,90,33], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(X10,commutator(X12,X10))) = identity]. % 197.18/197.60 [2077=param(372,1115),[14,33], % 197.18/197.60 commutator(multiply(inverse(X10),X11),multiply(X12,multiply(X10,inverse(multiply(X12,X11))))) = identity]. % 197.18/197.60 [2080=param(2077,19),[84], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(X12,inverse(multiply(X12,X10)))) = identity]. % 197.18/197.60 [2088=param(2080,667),[], % 197.18/197.60 commutator(multiply(X10,commutator(X11,X10)),multiply(X12,inverse(multiply(X12,X10)))) = identity]. % 197.18/197.60 [2089=param(2080,719),[3,387,13], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X11,multiply(X10,commutator(X10,X12)))))) = identity]. % 197.18/197.60 [2090=param(2080,770),[3,387,13], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X11,multiply(X10,commutator(X12,X10)))))) = identity]. % 197.18/197.60 [2092=param(2090,199),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(inverse(commutator(X12,X10)),inverse(multiply(X11,X10))))) = identity]. % 197.18/197.60 [2099=param(344,2088),[14], % 197.18/197.60 commutator(multiply(X10,inverse(multiply(X10,X11))),multiply(X11,commutator(X12,X11))) = identity]. % 197.18/197.60 [2102=param(2099,392),[3,223], % 197.18/197.60 commutator(multiply(X10,inverse(multiply(X10,multiply(X11,X12)))),multiply(X12,X11)) = identity]. % 197.18/197.60 [2103=param(2102,32),[3], % 197.18/197.60 commutator(multiply(X10,inverse(multiply(X10,X11))),multiply(inverse(X12),multiply(X11,X12))) = identity]. % 197.18/197.60 [2105=param(2103,439),[80,33,151,33], % 197.18/197.60 commutator(X10,multiply(inverse(X11),multiply(commutator(X12,X10),multiply(inverse(X10),X11)))) = identity]. % 197.18/197.60 [2109=param(2105,80),[33,3], % 197.18/197.60 commutator(X10,multiply(X11,multiply(inverse(X10),multiply(commutator(X12,X10),inverse(X11))))) = identity]. % 197.18/197.60 [2120=param(2109,383),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(inverse(X10),inverse(multiply(X11,commutator(X10,X12)))))) = identity]. % 197.18/197.60 [2143=param(2092,344),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(commutator(X10,X12),inverse(multiply(X11,X10))))) = identity]. % 197.18/197.60 [2146=param(2143,58),[33], % 197.18/197.60 commutator(X10,multiply(inverse(X11),multiply(commutator(X10,X12),multiply(inverse(X10),X11)))) = identity]. % 197.18/197.60 [2190=param(2146,80),[33,3], % 197.18/197.60 commutator(X10,multiply(X11,multiply(inverse(X10),multiply(commutator(X10,X12),inverse(X11))))) = identity]. % 197.18/197.60 [2193=param(2190,383),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(inverse(X10),inverse(multiply(X11,commutator(X12,X10)))))) = identity]. % 197.18/197.60 [2318=param(3,2),[3,3], % 197.18/197.60 multiply(commutator(X10,X11),X12) = multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,X12))))]. % 197.18/197.60 [2402=demod(385),[2318], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,X12)))) = inverse(multiply(inverse(X12),commutator(X11,X10)))]. % 197.18/197.60 [2404=demod(71),[2318,2318,32], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,multiply(X10,X12))))) = multiply(inverse(X11),multiply(X10,multiply(X11,X12)))]. % 197.18/197.60 [2421=demod(422),[2318], % 197.18/197.60 multiply(inverse(commutator(X10,X11)),X12) = multiply(inverse(X11),multiply(inverse(X10),multiply(X11,multiply(X10,X12))))]. % 197.18/197.60 [2474=demod(78),[2318,2318], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,multiply(X11,X12))))) = multiply(X11,multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,X12)))))]. % 197.18/197.60 [2643=param(84,54),[], % 197.18/197.60 multiply(inverse(X10),inverse(multiply(X11,inverse(multiply(X10,X12))))) = inverse(multiply(X11,inverse(X12)))]. % 197.18/197.60 [2644=param(84,58),[], % 197.18/197.60 multiply(X10,inverse(multiply(X11,inverse(multiply(inverse(X10),X12))))) = inverse(multiply(X11,inverse(X12)))]. % 197.18/197.60 [2682=param(110,344),[], % 197.18/197.60 inverse(multiply(inverse(X10),commutator(X11,multiply(X10,X10)))) = multiply(X10,commutator(multiply(X10,X10),X11))]. % 197.18/197.60 [2713=param(124,151),[], % 197.18/197.60 commutator(multiply(X10,X11),multiply(inverse(X11),multiply(inverse(X10),X12))) = commutator(multiply(X10,X11),X12)]. % 197.18/197.60 [2715=param(131,8),[], % 197.18/197.60 commutator(multiply(X10,inverse(X11)),multiply(X10,X12)) = commutator(multiply(X10,inverse(X11)),multiply(X11,X12))]. % 197.18/197.60 [2730=param(179,449),[513], % 197.18/197.60 multiply(inverse(X10),commutator(X11,commutator(X10,X12))) = inverse(multiply(X10,commutator(X10,commutator(X11,X12))))]. % 197.18/197.60 [2731=param(179,464),[513], % 197.18/197.60 multiply(inverse(X10),commutator(X11,commutator(X12,X10))) = inverse(multiply(X10,commutator(X10,commutator(X11,X12))))]. % 197.18/197.60 [2733=param(179,517),[513,2730,517], % 197.18/197.60 inverse(multiply(X10,commutator(X10,commutator(X11,X12)))) = inverse(multiply(X10,commutator(X11,commutator(X10,X12))))]. % 197.18/197.60 [2929=param(366,54),[], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X10,X12)))) = inverse(commutator(multiply(X11,inverse(X12)),X10))]. % 197.18/197.60 [2936=param(2929,441),[2929,33,343,350,33,343,350,33], % 197.18/197.60 commutator(X10,multiply(X11,commutator(X12,X10))) = commutator(X10,multiply(X11,inverse(commutator(X10,X12))))]. % 197.18/197.60 [2937=param(2929,442),[2929,33,343,350,33,343,350,33], % 197.18/197.60 commutator(X10,multiply(X11,commutator(X10,X12))) = commutator(X10,multiply(X11,inverse(commutator(X12,X10))))]. % 197.18/197.60 [3345=param(2929,653),[33,33,343,350,33], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X12,commutator(X10,X12)))) = commutator(X10,multiply(X11,multiply(X10,X12)))]. % 197.18/197.60 [3642=param(663,119),[3,343,350,119,33], % 197.18/197.60 commutator(multiply(X10,inverse(commutator(X10,X11))),multiply(X10,multiply(X11,X10))) = commutator(X10,X11)]. % 197.18/197.60 [3687=param(569,90),[33,33], % 197.18/197.60 multiply(X11,inverse(multiply(X10,multiply(X11,commutator(X11,X12))))) = inverse(multiply(X10,commutator(X11,X12)))]. % 197.18/197.60 [3689=param(569,570),[33], % 197.18/197.60 inverse(multiply(X10,multiply(X11,commutator(X12,X11)))) = multiply(X12,inverse(multiply(X10,multiply(X12,X11))))]. % 197.18/197.60 [3691=param(33,2682),[], % 197.18/197.60 multiply(inverse(X10),commutator(X11,multiply(X10,X10))) = inverse(multiply(X10,commutator(multiply(X10,X10),X11)))]. % 197.18/197.60 [3692=param(8,3691),[33], % 197.18/197.60 multiply(X10,inverse(multiply(X10,commutator(multiply(X10,X10),X11)))) = commutator(X11,multiply(X10,X10))]. % 197.18/197.60 [3724=param(2644,3692),[54,350,33,54,307,33], % 197.18/197.60 inverse(multiply(inverse(X10),commutator(multiply(X10,X10),X11))) = multiply(X10,commutator(X11,multiply(X10,X10)))]. % 197.18/197.60 [3725=param(33,3724),[], % 197.18/197.60 multiply(inverse(X10),commutator(multiply(X10,X10),X11)) = inverse(multiply(X10,commutator(X11,multiply(X10,X10))))]. % 197.18/197.60 [4889=param(3642,443),[33,3,2318,2402,168,33,223,443], % 197.18/197.60 commutator(multiply(X10,commutator(X11,X10)),multiply(X10,multiply(X10,X11))) = inverse(commutator(X11,X10))]. % 197.18/197.60 [4894=param(4889,392),[3,223,3,3,392,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X11,multiply(X10,multiply(X11,multiply(X10,X10))))) = commutator(X11,X10)]. % 197.18/197.60 [6473=param(2402,197),[33,33,33,350,307,33], % 197.18/197.60 multiply(X10,multiply(X11,inverse(multiply(X12,multiply(X11,X10))))) = inverse(multiply(X12,commutator(X11,X10)))]. % 197.18/197.60 [6987=param(4894,8),[54,3,8,3,350,343,350,119,33], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,multiply(X10,inverse(multiply(X11,X11)))))) = commutator(X11,X10)]. % 197.18/197.60 [6990=param(6987,232),[3], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X11,multiply(X11,inverse(multiply(X10,X10))))))) = commutator(X11,X10)]. % 197.18/197.60 [6991=param(6990,428),[343,350,119,350,33,3,278,3,350,2929,343,350,2929,343,350,33,33], % 197.18/197.60 inverse(commutator(X10,multiply(X11,inverse(commutator(X11,multiply(X10,X10)))))) = commutator(X11,X10)]. % 197.18/197.60 [6993=param(33,6991),[], % 197.18/197.60 commutator(X11,multiply(X10,inverse(commutator(X10,multiply(X11,X11))))) = inverse(commutator(X10,X11))]. % 197.18/197.60 [6994=param(6993,54),[350,33,307,350,33], % 197.18/197.60 inverse(commutator(X10,multiply(X11,commutator(X11,multiply(X10,X10))))) = commutator(X11,X10)]. % 197.18/197.60 [6999=param(33,6994),[], % 197.18/197.60 commutator(X11,multiply(X10,commutator(X10,multiply(X11,X11)))) = inverse(commutator(X10,X11))]. % 197.18/197.60 [7457=param(90,2733),[513], % 197.18/197.60 multiply(X10,inverse(multiply(X10,commutator(X11,commutator(X10,X12))))) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [7458=param(7457,344),[350,513], % 197.18/197.60 multiply(X10,inverse(multiply(X10,commutator(X11,commutator(X12,X10))))) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [8049=param(151,19),[], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X12,multiply(X11,X10)))) = multiply(X12,commutator(X12,multiply(X11,X10)))]. % 197.18/197.60 [8123=param(199,197),[151,33,33], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,multiply(X12,X13))))) = multiply(X11,multiply(X12,inverse(multiply(X10,inverse(X13)))))]. % 197.18/197.60 [8182=param(232,199),[3], % 197.18/197.60 multiply(X10,inverse(multiply(X11,multiply(X12,X13)))) = inverse(multiply(X11,multiply(X12,inverse(multiply(X10,inverse(X13))))))]. % 197.18/197.60 [8195=param(199,233),[151,33,33], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,multiply(X12,inverse(X13)))))) = multiply(X11,multiply(X12,inverse(multiply(X10,X13))))]. % 197.18/197.60 [8224=param(232,237),[3], % 197.18/197.60 multiply(X10,inverse(multiply(X11,multiply(X12,inverse(X13))))) = inverse(multiply(X11,multiply(X12,inverse(multiply(X10,X13)))))]. % 197.18/197.60 [8248=param(87,6999),[3,2318,3,-569,91,33,151,32,32], % 197.18/197.60 multiply(inverse(X10),multiply(X11,multiply(X10,commutator(X11,X10)))) = multiply(X11,commutator(X11,multiply(X10,X10)))]. % 197.18/197.60 [8314=param(378,331),[356,343,350,350,513,513,2318], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(inverse(c),multiply(inverse(b),multiply(c,multiply(b,inverse(multiply(a,commutator(c,commutator(b,a)))))))))) = thmtrue]. % 197.18/197.60 [8331=param(2929,282),[33,33,343,350,33], % 197.18/197.60 commutator(X10,multiply(X11,multiply(inverse(X10),X12))) = commutator(X10,multiply(X11,multiply(X12,commutator(X12,X10))))]. % 197.18/197.60 [8512=param(19,1363),[3,2318,13,2,3,2318,2404,151,8,8049], % 197.18/197.60 multiply(X10,commutator(X10,multiply(X11,commutator(X12,X10)))) = multiply(X10,commutator(X10,X11))]. % 197.18/197.60 [8513=param(8,8512),[8], % 197.18/197.60 commutator(X10,multiply(X11,commutator(X12,X10))) = commutator(X10,X11)]. % 197.18/197.60 [8515=demod(2936),[8513], % 197.18/197.60 commutator(X10,multiply(X11,inverse(commutator(X10,X12)))) = commutator(X10,X11)]. % 197.18/197.60 [8536=param(8513,3),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X12,commutator(X13,X10)))) = commutator(X10,multiply(X11,X12))]. % 197.18/197.60 [8538=demod(8331),[8536], % 197.18/197.60 commutator(X10,multiply(X11,multiply(inverse(X10),X12))) = commutator(X10,multiply(X11,X12))]. % 197.18/197.60 [8546=demod(2120),[8538], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X11,commutator(X10,X12))))) = identity]. % 197.18/197.60 [8547=demod(2193),[8538], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X11,commutator(X12,X10))))) = identity]. % 197.18/197.60 [8562=param(8513,119),[], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X12,commutator(X10,X11))) = commutator(multiply(X10,X11),X12)]. % 197.18/197.60 [8567=param(8513,307),[], % 197.18/197.60 commutator(X10,multiply(X11,inverse(commutator(X12,X10)))) = commutator(X10,X11)]. % 197.18/197.60 [8568=demod(2937),[8567], % 197.18/197.60 commutator(X10,multiply(X11,commutator(X10,X12))) = commutator(X10,X11)]. % 197.18/197.60 [8576=param(449,8513),[], % 197.18/197.60 commutator(X11,commutator(X10,multiply(X12,commutator(X13,X11)))) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [8589=param(8568,3),[], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X12,commutator(X10,X13)))) = commutator(X10,multiply(X11,X12))]. % 197.18/197.60 [8591=demod(3345),[8589], % 197.18/197.60 commutator(X10,multiply(X11,multiply(X10,X12))) = commutator(X10,multiply(X11,X12))]. % 197.18/197.60 [8595=param(8568,449),[], % 197.18/197.60 commutator(X10,multiply(X11,commutator(X12,commutator(X10,X13)))) = commutator(X10,X11)]. % 197.18/197.60 [8608=param(8591,3),[], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X12,multiply(X10,multiply(X11,X13)))) = commutator(multiply(X10,X11),multiply(X12,X13))]. % 197.18/197.60 [8610=param(8591,80),[], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X12,X10)))) = commutator(X10,multiply(X11,inverse(X12)))]. % 197.18/197.60 [8620=param(8591,196),[], % 197.18/197.60 commutator(X10,multiply(X11,inverse(multiply(X12,inverse(X10))))) = commutator(X10,multiply(X11,inverse(X12)))]. % 197.18/197.60 [8624=param(354,8591),[3,3,6473], % 197.18/197.60 multiply(X11,multiply(X10,inverse(multiply(X11,commutator(X10,X12))))) = multiply(X10,inverse(commutator(X10,multiply(X11,X12))))]. % 197.18/197.60 [8731=param(8610,8),[33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X12,inverse(X11))) = commutator(multiply(X10,X11),multiply(X12,X10))]. % 197.18/197.60 [8815=param(370,8562),[350,33,2421,2713], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X11,multiply(X10,X12))) = commutator(multiply(X10,X11),X12)]. % 197.18/197.60 [8922=param(8515,683),[8731], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(X12,X10)) = commutator(multiply(X10,commutator(X10,X11)),X12)]. % 197.18/197.60 [8925=param(683,8568),[8568], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(inverse(X10),multiply(X11,commutator(X10,X12)))) = commutator(X10,X11)]. % 197.18/197.60 [9010=param(8314,439),[343,350,8591,8,350,8568,33,3,3,3,54,3,2421,2404,32], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(inverse(b),multiply(c,multiply(b,inverse(multiply(a,multiply(c,commutator(c,commutator(b,a)))))))))) = thmtrue]. % 197.18/197.60 [9037=param(9010,282),[343,350,8591,3687,350,8595,33,3,3,384,343,350,2421,2404,8224,32], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(c,multiply(b,inverse(multiply(a,multiply(b,multiply(c,commutator(c,commutator(b,a)))))))))) = thmtrue]. % 197.18/197.60 [9038=param(444,27),[2318,13,2,2318,44,2318,8248,8], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X10,X11)))) = multiply(X10,commutator(X10,multiply(X11,X11)))]. % 197.18/197.60 [9172=param(653,3725),[33,8,307,130,27,14,2318,13,3,151,9038,8], % 197.18/197.60 commutator(X10,multiply(X11,X11)) = inverse(commutator(X11,multiply(X10,X10)))]. % 197.18/197.60 [9199=param(344,9172),[33], % 197.18/197.60 commutator(X10,multiply(X11,X11)) = commutator(multiply(X10,X10),X11)]. % 197.18/197.60 [9232=param(9172,8815),[3,3,8608,395,33,343,350,395,33], % 197.18/197.60 commutator(multiply(X10,X10),multiply(X10,X11)) = commutator(multiply(X10,X10),X11)]. % 197.18/197.60 [9239=param(9172,131),[3,343,350,8591,33,3,3,3,3,131,8608], % 197.18/197.60 commutator(multiply(X11,X10),multiply(X11,X11)) = commutator(X10,multiply(X11,X11))]. % 197.18/197.60 [9240=demod(891),[9239,1,1], % 197.18/197.60 commutator(X10,commutator(X11,commutator(X12,multiply(X13,X13)))) = identity]. % 197.18/197.60 [9256=param(9240,464),[1], % 197.18/197.60 commutator(X10,commutator(multiply(X11,X11),commutator(X12,X13))) = identity]. % 197.18/197.60 [9294=param(374,9239),[307,33], % 197.18/197.60 commutator(multiply(X10,inverse(X11)),multiply(X11,X11)) = commutator(X10,multiply(X11,X11))]. % 197.18/197.60 [9402=param(9199,344),[], % 197.18/197.60 commutator(multiply(X10,X10),X11) = inverse(commutator(multiply(X11,X11),X10))]. % 197.18/197.60 [9458=param(370,9294),[54,350,33,33,33], % 197.18/197.60 commutator(multiply(X10,X11),multiply(X11,X11)) = commutator(X10,multiply(X11,X11))]. % 197.18/197.60 [9715=param(1,9458),[1], % 197.18/197.60 commutator(multiply(X10,X11),commutator(multiply(X11,X11),X12)) = commutator(X10,commutator(multiply(X11,X11),X12))]. % 197.18/197.60 [9942=param(9715,351),[350,513,351,350,513], % 197.18/197.60 commutator(multiply(X10,X11),commutator(X12,multiply(X11,X11))) = commutator(X10,commutator(X12,multiply(X11,X11)))]. % 197.18/197.60 [9955=param(9942,54),[54,350,350,307,513,513,54,350,350,307,513,513], % 197.18/197.60 commutator(multiply(X10,X11),commutator(X12,multiply(X10,X10))) = commutator(X11,commutator(X12,multiply(X10,X10)))]. % 197.18/197.60 [10076=param(370,8922),[350,33], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(inverse(X10),X12)) = commutator(multiply(X10,commutator(X10,X11)),X12)]. % 197.18/197.60 [10078=demod(8925),[10076], % 197.18/197.60 commutator(multiply(X10,commutator(X10,X11)),multiply(X11,commutator(X10,X12))) = commutator(X10,X11)]. % 197.18/197.60 [10155=param(569,441),[33], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,commutator(X11,X12))))) = multiply(X11,inverse(multiply(X10,commutator(X12,X11))))]. % 197.18/197.60 [10162=param(569,840),[33], % 197.18/197.60 inverse(multiply(X10,inverse(multiply(X11,commutator(X12,X13))))) = multiply(X11,inverse(multiply(X10,commutator(X13,X12))))]. % 197.18/197.60 [10273=param(9037,572),[8182,513,8624,33], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(c,inverse(multiply(a,multiply(c,inverse(commutator(c,multiply(b,commutator(b,a)))))))))) = thmtrue]. % 197.18/197.60 [10303=param(10273,354),[3,2318,-8195,-569,-569,-569,2644,2644,33], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(c,multiply(b,inverse(multiply(b,multiply(a,multiply(c,inverse(commutator(b,a)))))))))) = thmtrue]. % 197.18/197.60 [10317=param(10303,197),[54,151,33,-199,2318,-3689,343,350,8182,33,8624,-569,-569,2644,-569,33], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),multiply(c,inverse(multiply(c,multiply(inverse(a),commutator(c,multiply(b,a))))))) = thmtrue]. % 197.18/197.60 [12046=param(2,196),[3], % 197.18/197.60 multiply(inverse(X10),multiply(X11,multiply(inverse(X12),multiply(X10,multiply(X12,inverse(X11)))))) = commutator(X10,multiply(X12,inverse(X11)))]. % 197.18/197.60 [12224=param(111,441),[2421,32], % 197.18/197.60 multiply(inverse(X10),multiply(X11,inverse(commutator(X12,X11)))) = inverse(multiply(inverse(X12),multiply(inverse(X11),multiply(X12,X10))))]. % 197.18/197.60 [12652=param(54,353),[3,3], % 197.18/197.60 multiply(inverse(X10),inverse(multiply(X11,inverse(commutator(X11,X12))))) = inverse(multiply(X12,multiply(X11,multiply(inverse(X12),X10))))]. % 197.18/197.60 [12930=param(3725,449),[1], % 197.18/197.60 multiply(inverse(X10),commutator(X11,commutator(multiply(X10,X10),X12))) = inverse(multiply(X10,commutator(X11,commutator(X12,multiply(X10,X10)))))]. % 197.18/197.60 [12953=param(2731,9402),[2318,8248,8,1,513,12930], % 197.18/197.60 inverse(multiply(X10,commutator(X11,commutator(X12,multiply(X10,X10))))) = inverse(multiply(X10,commutator(X10,commutator(multiply(X12,X12),X11))))]. % 197.18/197.60 [14097=demod(655),[], % 197.18/197.60 multiply(inverse(X10),inverse(multiply(X11,commutator(X10,X11)))) = inverse(multiply(X10,X11))]. % 197.18/197.60 [14648=param(569,7458),[513,33], % 197.18/197.60 multiply(X11,inverse(multiply(X10,multiply(X11,commutator(X12,commutator(X13,X11)))))) = inverse(multiply(X10,commutator(X11,commutator(X12,X13))))]. % 197.18/197.60 [14652=param(7458,9232),[3,3,14648,9955], % 197.18/197.60 multiply(X10,inverse(multiply(X10,commutator(X11,commutator(X12,multiply(X10,X10)))))) = commutator(X11,commutator(X12,multiply(X10,X10)))]. % 197.18/197.60 [16060=param(44,449),[2318], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,multiply(X12,commutator(X10,commutator(X12,X11))))))) = multiply(X12,commutator(X10,X11))]. % 197.18/197.60 [16101=param(8567,2318),[], % 197.18/197.60 commutator(X10,multiply(inverse(X11),multiply(inverse(X12),multiply(X11,multiply(X12,inverse(commutator(X13,X10))))))) = commutator(X10,commutator(X11,X12))]. % 197.18/197.60 [16291=param(8576,9172),[], % 197.18/197.60 commutator(multiply(X10,X10),commutator(X11,multiply(X12,inverse(commutator(X10,multiply(X13,X13)))))) = commutator(X11,commutator(multiply(X10,X10),X12))]. % 197.18/197.60 [16467=param(10317,653),[8568,350,3,2318,3,151], % 197.18/197.60 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(inverse(a),multiply(inverse(c),multiply(inverse(a),multiply(inverse(b),multiply(c,multiply(b,multiply(a,inverse(commutator(c,a))))))))))) = thmtrue]. % 197.18/197.60 [16480=param(653,8546),[3,58,14,5], % 197.18/197.60 multiply(X11,inverse(multiply(X11,multiply(X10,inverse(multiply(X10,commutator(X11,X12))))))) = inverse(multiply(X10,inverse(multiply(X10,commutator(X11,X12)))))]. % 197.18/197.60 [16641=param(331,151),[350], % 197.18/197.60 multiply(inverse(X10),inverse(multiply(X11,X12))) = multiply(inverse(X12),multiply(inverse(X11),inverse(multiply(X10,inverse(commutator(X10,multiply(X11,X12)))))))]. % 197.18/197.60 [16650=param(331,8547),[13,3,54], % 197.18/197.60 multiply(X10,inverse(multiply(X11,multiply(X10,commutator(X12,X11))))) = multiply(inverse(X11),multiply(X10,inverse(multiply(X10,commutator(X12,X11)))))]. % 197.18/197.60 [17143=param(368,10078),[3,2318,223,8,-439,17,14,13,31,13,58,3,2318,32], % 197.18/197.60 inverse(multiply(inverse(X10),multiply(X11,commutator(X10,X12)))) = multiply(inverse(X11),multiply(X10,multiply(X11,inverse(multiply(X11,commutator(X10,X12))))))]. % 197.18/197.60 [17596=demod(2),[], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,X11))) = commutator(X10,X11)]. % 197.18/197.60 [19236=param(314,632),[513,2318,2318,16060,2421,1,1,75,14,13], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(inverse(X12),multiply(X11,multiply(X12,multiply(X10,multiply(X10,commutator(X12,X11)))))))) = X10]. % 197.18/197.60 [20067=param(14097,8546),[3,58,14,5], % 197.18/197.60 multiply(inverse(X10),inverse(multiply(X11,inverse(multiply(X11,commutator(X10,X12)))))) = inverse(multiply(X10,multiply(X11,inverse(multiply(X11,commutator(X10,X12))))))]. % 197.18/197.60 [20072=param(14097,9256),[2318,2318,13,17596,3,2421,151,19236,-439,17,14,13,31,14,-439,16,14,13,5], % 197.18/197.60 inverse(multiply(X10,commutator(multiply(X11,X11),commutator(X12,X13)))) = inverse(X10)]. % 197.18/197.60 [20077=param(20072,5),[513,14], % 197.18/197.60 commutator(multiply(X10,X10),commutator(X11,X12)) = identity]. % 197.18/197.60 [20078=demod(16291),[20077], % 197.18/197.60 commutator(X10,commutator(multiply(X11,X11),X12)) = identity]. % 197.18/197.60 [20079=demod(12953),[20078,13], % 197.18/197.60 inverse(multiply(X10,commutator(X11,commutator(X12,multiply(X10,X10))))) = inverse(X10)]. % 197.18/197.60 [20080=demod(14652),[20079,31], % 197.18/197.60 commutator(X10,commutator(X11,multiply(X12,X12))) = identity]. % 197.18/197.60 [20105=param(20080,3),[], % 197.18/197.60 commutator(X10,commutator(X11,multiply(X12,multiply(X13,multiply(X12,X13))))) = identity]. % 197.18/197.60 [20234=param(20105,246),[3,440], % 197.18/197.60 commutator(X10,commutator(X11,multiply(X12,multiply(X13,multiply(X13,inverse(X12)))))) = identity]. % 197.18/197.60 [20437=param(570,464),[2318], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,commutator(X11,commutator(X12,X10)))))) = inverse(multiply(X12,inverse(multiply(X12,commutator(X10,X11)))))]. % 197.18/197.60 [20439=param(570,527),[2318], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),multiply(X10,multiply(X11,commutator(X11,commutator(X10,X12)))))) = inverse(multiply(X12,inverse(multiply(X12,commutator(X10,X11)))))]. % 197.18/197.60 [20607=param(20234,8815),[], % 197.18/197.60 commutator(X10,commutator(multiply(X11,X12),multiply(X11,inverse(X12)))) = identity]. % 197.18/197.60 [20619=param(20607,449),[], % 197.18/197.60 commutator(multiply(X10,X11),commutator(X12,multiply(X10,inverse(X11)))) = identity]. % 197.18/197.60 [20637=param(20619,105),[33,350,350,513], % 197.18/197.60 commutator(multiply(X10,X11),commutator(X12,multiply(X11,inverse(X10)))) = identity]. % 197.18/197.60 [20838=param(653,20637),[2318,3,-439,16,14,13,5,151,33,12046,3,3], % 197.18/197.60 multiply(X12,multiply(X11,inverse(multiply(X12,multiply(X11,commutator(X10,multiply(X11,inverse(X12)))))))) = inverse(commutator(X10,multiply(X11,inverse(X12))))]. % 197.18/197.60 [20842=param(14097,20637),[2318,3,-439,16,14,13,5,151,33,12046,151,3], % 197.18/197.60 multiply(inverse(X10),multiply(inverse(X11),inverse(commutator(X12,multiply(X10,inverse(X11)))))) = inverse(multiply(X11,multiply(X10,commutator(X12,multiply(X10,inverse(X11))))))]. % 197.18/197.64 [21295=param(111,111),[3,3], % 197.18/197.64 multiply(inverse(X10),multiply(X11,multiply(X12,multiply(X13,X14)))) = inverse(multiply(inverse(X14),multiply(inverse(X13),multiply(inverse(X12),multiply(inverse(X11),X10)))))]. % 197.18/197.64 [21995=param(199,111),[3,3], % 197.18/197.64 multiply(inverse(X10),multiply(X11,multiply(X12,inverse(multiply(X13,X14))))) = inverse(multiply(X13,multiply(X14,multiply(inverse(X12),multiply(inverse(X11),X10)))))]. % 197.18/197.64 [24425=param(354,8620),[3,151,33], % 197.18/197.64 multiply(X11,multiply(X10,multiply(inverse(X12),multiply(X10,inverse(multiply(X11,inverse(multiply(X12,inverse(X10))))))))) = multiply(X10,inverse(commutator(X10,multiply(X11,inverse(X12)))))]. % 197.18/197.64 [24957=param(44,2089),[13,3,58], % 197.18/197.64 multiply(X10,inverse(multiply(inverse(X11),multiply(X10,multiply(X11,commutator(X11,X12)))))) = multiply(X11,multiply(X10,inverse(multiply(X10,multiply(X11,commutator(X11,X12))))))]. % 197.18/197.64 [26862=param(693,2421),[307,1,513], % 197.18/197.64 inverse(multiply(X10,inverse(multiply(inverse(X11),multiply(inverse(X12),multiply(X11,multiply(X12,commutator(X12,commutator(X11,X10))))))))) = multiply(inverse(X10),inverse(commutator(X12,X11)))]. % 197.18/197.64 [27968=param(6473,196),[350], % 197.18/197.64 multiply(inverse(X10),multiply(X11,inverse(multiply(X12,inverse(multiply(X10,inverse(X11))))))) = inverse(multiply(X12,inverse(commutator(X11,X10))))]. % 197.18/197.64 [27969=demod(24425),[27968], % 197.18/197.64 multiply(X10,multiply(X11,inverse(multiply(X10,inverse(commutator(X11,X12)))))) = multiply(X11,inverse(commutator(X11,multiply(X10,inverse(X12)))))]. % 197.18/197.64 [28167=param(8591,2318),[2318], % 197.18/197.64 commutator(X10,multiply(inverse(X11),multiply(inverse(X12),multiply(X11,multiply(X12,multiply(X10,X13)))))) = commutator(X10,multiply(inverse(X11),multiply(inverse(X12),multiply(X11,multiply(X12,X13)))))]. % 197.18/197.64 [29172=param(16467,693),[343,350,8538,28167,16101,356,343,350,350,513,513,513,3,3,3,3,3,3,2421,20437,343,350,-569,33,-8195,-569,-8123,-569,-569,33,33], % 197.18/197.64 thtop(multiply(a,inverse(commutator(c,b))),multiply(a,multiply(b,inverse(multiply(inverse(c),multiply(inverse(a),multiply(inverse(b),multiply(c,multiply(b,multiply(a,multiply(b,inverse(commutator(c,a))))))))))))) = thmtrue]. % 197.18/197.64 [29599=param(29172,410),[58,-439,343,350,33,-10155,343,350,33,54,3,21295,33,12224,113,343,33,343,350,179,33,8,-26862,20439,343,350,-569,33,-569,33,-8195,-16650,-572,33,2318,8182,33,-8195,-8123,33,8182,33,2474,-17143,8182,179,33,24957,8182,27969,196,350,33,90,33,33,33], % 197.18/197.64 thtop(multiply(a,inverse(commutator(c,b))),multiply(a,multiply(b,inverse(multiply(inverse(c),multiply(inverse(a),multiply(c,multiply(a,multiply(b,commutator(c,multiply(b,inverse(a)))))))))))) = thmtrue]. % 197.18/197.64 [29706=param(29599,410),[33,3,3,3,3,3,2318,3,-199,21995,-232,-439,343,350,33,-10155,343,350,33,-8123,33,8,3,8182,27969,196,350,33,-10162,343,350,-569,33,8], % 197.18/197.64 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(inverse(c),multiply(inverse(a),multiply(c,multiply(a,multiply(b,inverse(multiply(a,multiply(b,inverse(commutator(c,multiply(b,inverse(a)))))))))))))) = thmtrue]. % 197.18/197.64 [29816=param(29706,232),[3,3,16641,1,-2715,343,350,9232,350,343,350,33,350,20080,14,14,2318,3,-439,16,14,13,5,113,307,179,33,8,20842,20838,33], % 197.18/197.64 thtop(multiply(a,inverse(commutator(c,b))),inverse(multiply(inverse(c),multiply(inverse(a),multiply(c,commutator(c,multiply(b,inverse(a)))))))) = thmtrue]. % 197.18/197.64 [29836=param(29816,331),[8591,8568,350,3,3,2318,3,12652,-439,17,14,13,31,13,21995,-232,-439,343,350,33,-10155,343,350,33,-8123,33,8,3687,20067,16480,2643,33,6], % 197.18/197.64 thmtrue = thmfalse]. % 197.18/197.64 % SZS output end CNFRefutation % 197.18/197.64 Space: 837193 KB %------------------------------------------------------------------------------