%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : RNG020-7 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n018.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 : Mon Jul 18 20:27:48 EDT 2022 % Result : Unsatisfiable 132.47s 132.93s % Output : CNFRefutation 132.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : RNG020-7 : TPTP v8.1.0. Released v1.0.0. % 0.11/0.13 % Command : fiesta-wrapper %s % 0.13/0.35 % Computer : n018.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon May 30 07:38:56 EDT 2022 % 0.13/0.35 % CPUTime : % 132.47/132.93 Theorem Proved. % 132.47/132.93 % SZS status Unsatisfiable % 132.47/132.93 % SZS output start CNFRefutation % 132.47/132.93 [1=axiom,[], % 132.47/132.93 add(additive_inverse(multiply(X10,X12)),additive_inverse(multiply(X11,X12))) = multiply(add(X10,X11),additive_inverse(X12))]. % 132.47/132.93 [3=axiom,[], % 132.47/132.93 add(multiply(X10,X12),additive_inverse(multiply(X11,X12))) = multiply(add(X10,additive_inverse(X11)),X12)]. % 132.47/132.93 [5=axiom,[], % 132.47/132.93 multiply(X10,additive_inverse(X11)) = additive_inverse(multiply(X10,X11))]. % 132.47/132.93 [6=demod(1),[5], % 132.47/132.93 add(additive_inverse(multiply(X10,X11)),additive_inverse(multiply(X12,X11))) = additive_inverse(multiply(add(X10,X12),X11))]. % 132.47/132.93 [7=axiom,[], % 132.47/132.93 multiply(additive_inverse(X10),X11) = additive_inverse(multiply(X10,X11))]. % 132.47/132.93 [10=axiom,[], % 132.47/132.93 add(multiply(X11,X10),additive_inverse(multiply(X10,X11))) = commutator(X10,X11)]. % 132.47/132.93 [11=axiom,[], % 132.47/132.93 associator(X10,X11,X12) = add(multiply(multiply(X10,X11),X12),additive_inverse(multiply(X10,multiply(X11,X12))))]. % 132.47/132.93 [14=axiom,[], % 132.47/132.93 add(add(X10,X11),X12) = add(X10,add(X11,X12))]. % 132.47/132.93 [15=axiom,[], % 132.47/132.93 add(X10,X11) = add(X11,X10)]. % 132.47/132.93 [16=demod(11),[15], % 132.47/132.93 associator(X10,X11,X12) = add(additive_inverse(multiply(X10,multiply(X11,X12))),multiply(multiply(X10,X11),X12))]. % 132.47/132.93 [17=axiom,[], % 132.47/132.93 add(multiply(X10,X12),multiply(X11,X12)) = multiply(add(X10,X11),X12)]. % 132.47/132.93 [18=axiom,[], % 132.47/132.93 add(multiply(X10,X11),multiply(X10,X12)) = multiply(X10,add(X11,X12))]. % 132.47/132.93 [19=axiom,[], % 132.47/132.93 additive_inverse(additive_inverse(X10)) = X10]. % 132.47/132.93 [20=axiom,[], % 132.47/132.93 add(X10,additive_inverse(X10)) = additive_identity]. % 132.47/132.93 [23=axiom,[], % 132.47/132.93 add(X10,additive_identity) = X10]. % 132.47/132.93 [24=axiom,[], % 132.47/132.93 add(additive_identity,X10) = X10]. % 132.47/132.93 [25=axiom,[], % 132.47/132.93 thtop(X10,X10) = thmfalse]. % 132.47/132.93 [26=axiom,[15,16,16,16,14], % 132.47/132.93 thtop(add(additive_inverse(multiply(x,multiply(add(v,u),y))),multiply(multiply(x,add(v,u)),y)),add(additive_inverse(multiply(x,multiply(u,y))),add(multiply(multiply(x,u),y),add(additive_inverse(multiply(x,multiply(v,y))),multiply(multiply(x,v),y))))) = thmtrue]. % 132.47/132.93 [35=param(6,15),[6], % 132.47/132.93 additive_inverse(multiply(add(X10,X11),X12)) = additive_inverse(multiply(add(X11,X10),X12))]. % 132.47/132.93 [36=param(14,15),[], % 132.47/132.93 add(X10,add(X11,X12)) = add(X12,add(X10,X11))]. % 132.47/132.93 [37=param(14,15),[14], % 132.47/132.93 add(X10,add(X11,X12)) = add(X11,add(X10,X12))]. % 132.47/132.93 [38=param(14,20),[], % 132.47/132.93 add(X10,add(X11,additive_inverse(add(X10,X11)))) = additive_identity]. % 132.47/132.93 [39=param(14,20),[24], % 132.47/132.93 add(X11,add(additive_inverse(X11),X10)) = X10]. % 132.47/132.93 [42=param(39,15),[], % 132.47/132.93 add(X10,add(X11,additive_inverse(X10))) = X11]. % 132.47/132.93 [50=param(42,14),[], % 132.47/132.93 add(X10,add(X11,add(X12,additive_inverse(X10)))) = add(X11,X12)]. % 132.47/132.93 [54=param(10,5),[7,19], % 132.47/132.93 add(additive_inverse(multiply(X10,X11)),multiply(X11,X10)) = commutator(additive_inverse(X11),X10)]. % 132.47/132.93 [55=param(10,5),[7,19,54], % 132.47/132.93 commutator(additive_inverse(X10),X11) = commutator(X10,additive_inverse(X11))]. % 132.47/132.93 [56=demod(54),[55], % 132.47/132.93 add(additive_inverse(multiply(X10,X11)),multiply(X11,X10)) = commutator(X11,additive_inverse(X10))]. % 132.47/132.93 [57=param(10,15),[56], % 132.47/132.93 commutator(X10,X11) = commutator(X11,additive_inverse(X10))]. % 132.47/132.93 [60=param(42,10),[15], % 132.47/132.93 add(commutator(X10,X11),multiply(X10,X11)) = multiply(X11,X10)]. % 132.47/132.93 [62=param(14,60),[], % 132.47/132.93 add(multiply(X10,X11),X12) = add(commutator(X11,X10),add(multiply(X11,X10),X12))]. % 132.47/132.93 [65=param(60,57),[5,7], % 132.47/132.93 add(commutator(X10,X11),additive_inverse(multiply(X11,X10))) = additive_inverse(multiply(X10,X11))]. % 132.47/132.93 [70=param(38,15),[14,15], % 132.47/132.93 add(X10,add(X11,additive_inverse(add(X11,X10)))) = additive_identity]. % 132.47/132.93 [82=param(39,70),[23], % 132.47/132.93 add(X11,additive_inverse(add(X11,additive_inverse(X10)))) = X10]. % 132.47/132.93 [85=param(39,82),[], % 132.47/132.93 additive_inverse(add(additive_inverse(X10),additive_inverse(X11))) = add(X10,X11)]. % 132.47/132.93 [89=param(85,19),[], % 132.47/132.93 add(additive_inverse(X10),X11) = additive_inverse(add(X10,additive_inverse(X11)))]. % 132.47/132.93 [92=demod(56),[89,10], % 132.47/132.93 commutator(X10,additive_inverse(X11)) = additive_inverse(commutator(X10,X11))]. % 132.47/132.93 [93=demod(55),[92], % 132.47/132.93 commutator(additive_inverse(X10),X11) = additive_inverse(commutator(X10,X11))]. % 132.47/132.93 [94=demod(57),[92], % 132.47/132.93 commutator(X10,X11) = additive_inverse(commutator(X11,X10))]. % 132.47/132.93 [98=param(89,15),[], % 132.47/132.93 additive_inverse(add(X10,additive_inverse(X11))) = add(X11,additive_inverse(X10))]. % 132.47/132.93 [100=param(42,89),[19], % 132.47/132.93 add(X10,additive_inverse(add(X11,X10))) = additive_inverse(X11)]. % 132.47/132.93 [102=param(36,14),[14], % 132.47/132.93 add(X10,add(X11,add(X12,X13))) = add(X11,add(X12,add(X13,X10)))]. % 132.47/132.93 [103=param(14,36),[14,14,14], % 132.47/132.93 add(X10,add(X11,add(X12,X13))) = add(X11,add(X12,add(X10,X13)))]. % 132.47/132.93 [105=param(36,60),[36], % 132.47/132.93 add(X10,multiply(X11,X12)) = add(commutator(X12,X11),add(multiply(X12,X11),X10))]. % 132.47/132.93 [107=param(36,89),[], % 132.47/132.93 add(X10,additive_inverse(add(X11,additive_inverse(X12)))) = add(X12,add(X10,additive_inverse(X11)))]. % 132.47/132.93 [111=param(20,94),[], % 132.47/132.93 add(commutator(X10,X11),commutator(X11,X10)) = additive_identity]. % 132.47/132.93 [112=param(89,94),[], % 132.47/132.93 add(commutator(X10,X11),X12) = additive_inverse(add(commutator(X11,X10),additive_inverse(X12)))]. % 132.47/132.93 [114=param(93,94),[], % 132.47/132.93 commutator(commutator(X10,X11),X12) = additive_inverse(commutator(commutator(X11,X10),X12))]. % 132.47/132.93 [118=param(100,15),[], % 132.47/132.93 add(X10,additive_inverse(add(X10,X11))) = additive_inverse(X11)]. % 132.47/132.93 [120=param(37,15),[14], % 132.47/132.93 add(X10,add(X11,X12)) = add(X10,add(X12,X11))]. % 132.47/132.93 [121=param(37,36),[], % 132.47/132.93 add(X10,add(X11,X12)) = add(X12,add(X11,X10))]. % 132.47/132.93 [123=param(37,60),[], % 132.47/132.93 add(X10,multiply(X11,X12)) = add(commutator(X12,X11),add(X10,multiply(X12,X11)))]. % 132.47/132.93 [124=param(37,89),[89], % 132.47/132.93 add(X10,additive_inverse(add(X11,additive_inverse(X12)))) = additive_inverse(add(X11,additive_inverse(add(X10,X12))))]. % 132.47/132.93 [125=param(37,100),[], % 132.47/132.93 add(X12,add(X10,additive_inverse(add(X11,X12)))) = add(X10,additive_inverse(X11))]. % 132.47/132.93 [126=param(118,36),[], % 132.47/132.93 add(X10,additive_inverse(add(X11,add(X10,X12)))) = additive_inverse(add(X12,X11))]. % 132.47/132.93 [127=param(118,37),[], % 132.47/132.93 add(X10,additive_inverse(add(X11,add(X10,X12)))) = additive_inverse(add(X11,X12))]. % 132.47/132.93 [128=demod(126),[127], % 132.47/132.93 additive_inverse(add(X10,X11)) = additive_inverse(add(X11,X10))]. % 132.47/132.93 [129=param(37,118),[], % 132.47/132.93 add(X12,add(X10,additive_inverse(add(X12,X11)))) = add(X10,additive_inverse(X11))]. % 132.47/132.93 [130=param(14,111),[24], % 132.47/132.93 add(commutator(X11,X12),add(commutator(X12,X11),X10)) = X10]. % 132.47/132.93 [131=param(36,111),[23], % 132.47/132.93 add(commutator(X11,X12),add(X10,commutator(X12,X11))) = X10]. % 132.47/132.93 [134=param(128,14),[], % 132.47/132.93 additive_inverse(add(X10,add(X11,X12))) = additive_inverse(add(X12,add(X10,X11)))]. % 132.47/132.93 [136=param(89,128),[89,14,14], % 132.47/132.93 additive_inverse(add(X10,add(X11,additive_inverse(X12)))) = additive_inverse(add(X11,add(X10,additive_inverse(X12))))]. % 132.47/132.93 [143=param(98,98),[14,89,19], % 132.47/132.93 additive_inverse(add(X10,add(X11,additive_inverse(X12)))) = add(X12,additive_inverse(add(X11,X10)))]. % 132.47/132.93 [145=param(14,131),[14], % 132.47/132.93 add(commutator(X12,X13),add(X10,add(commutator(X13,X12),X11))) = add(X10,X11)]. % 132.47/132.93 [146=param(37,131),[], % 132.47/132.93 add(commutator(X12,X13),add(X10,add(X11,commutator(X13,X12)))) = add(X10,X11)]. % 132.47/132.93 [148=param(130,118),[], % 132.47/132.93 add(commutator(X10,X11),additive_inverse(X12)) = additive_inverse(add(commutator(X11,X10),X12))]. % 132.47/132.93 [152=param(14,121),[14,14,14], % 132.47/132.93 add(X10,add(X11,add(X12,X13))) = add(X12,add(X11,add(X10,X13)))]. % 132.47/132.93 [155=param(121,89),[89], % 132.47/132.93 add(X10,additive_inverse(add(X11,additive_inverse(X12)))) = add(X12,additive_inverse(add(X11,additive_inverse(X10))))]. % 132.47/132.93 [161=param(120,18),[18], % 132.47/132.93 add(X10,multiply(X11,add(X12,X13))) = add(X10,multiply(X11,add(X13,X12)))]. % 132.47/132.93 [164=param(120,89),[], % 132.47/132.93 add(X10,additive_inverse(add(X11,additive_inverse(X12)))) = add(X10,add(X12,additive_inverse(X11)))]. % 132.47/132.93 [166=param(121,120),[14], % 132.47/132.93 add(X10,add(X11,add(X12,X13))) = add(X13,add(X12,add(X11,X10)))]. % 132.47/132.93 [167=param(128,120),[14], % 132.47/132.93 additive_inverse(add(X10,add(X11,X12))) = additive_inverse(add(X12,add(X11,X10)))]. % 132.47/132.93 [190=param(62,15),[], % 132.47/132.93 add(commutator(X10,X11),add(X12,multiply(X10,X11))) = add(multiply(X11,X10),X12)]. % 132.47/132.93 [191=param(62,37),[], % 132.47/132.93 add(multiply(X10,X11),X12) = add(multiply(X11,X10),add(commutator(X11,X10),X12))]. % 132.47/132.93 [198=param(94,114),[19], % 132.47/132.93 commutator(commutator(X10,X11),X12) = commutator(X12,commutator(X11,X10))]. % 132.47/132.93 [206=param(111,198),[], % 132.47/132.93 add(commutator(X10,commutator(X11,X12)),commutator(X10,commutator(X12,X11))) = additive_identity]. % 132.47/132.93 [214=param(14,206),[24], % 132.47/132.93 add(commutator(X11,commutator(X12,X13)),add(commutator(X11,commutator(X13,X12)),X10)) = X10]. % 132.47/132.93 [219=param(167,107),[89,19], % 132.47/132.93 additive_inverse(add(X10,additive_inverse(add(X11,additive_inverse(X12))))) = add(X11,additive_inverse(add(X10,X12)))]. % 132.47/132.93 [322=param(161,15),[], % 132.47/132.93 add(X10,multiply(X11,add(X12,X13))) = add(multiply(X11,add(X13,X12)),X10)]. % 132.47/132.93 [352=param(14,18),[], % 132.47/132.93 add(multiply(X10,add(X11,X12)),X13) = add(multiply(X10,X11),add(multiply(X10,X12),X13))]. % 132.47/132.93 [353=demod(322),[352], % 132.47/132.93 add(X10,multiply(X11,add(X12,X13))) = add(multiply(X11,X13),add(multiply(X11,X12),X10))]. % 132.47/132.93 [427=param(129,60),[], % 132.47/132.93 add(commutator(X10,X11),add(X12,additive_inverse(multiply(X11,X10)))) = add(X12,additive_inverse(multiply(X10,X11)))]. % 132.47/132.93 [437=param(62,17),[], % 132.47/132.93 add(multiply(X11,X10),multiply(X12,X11)) = add(commutator(X10,X11),multiply(add(X10,X12),X11))]. % 132.47/132.93 [438=param(62,18),[], % 132.47/132.93 add(multiply(X11,X10),multiply(X10,X12)) = add(commutator(X10,X11),multiply(X10,add(X11,X12)))]. % 132.47/132.93 [446=param(127,14),[14], % 132.47/132.93 add(X10,additive_inverse(add(X11,add(X12,add(X10,X13))))) = additive_inverse(add(X11,add(X12,X13)))]. % 132.47/132.93 [449=param(127,130),[], % 132.47/132.93 add(commutator(X10,X11),additive_inverse(add(X12,X13))) = additive_inverse(add(X12,add(commutator(X11,X10),X13)))]. % 132.47/132.93 [506=demod(191),[], % 132.47/132.93 add(multiply(X10,X11),X12) = add(multiply(X11,X10),add(commutator(X11,X10),X12))]. % 132.47/132.93 [1282=param(506,118),[], % 132.47/132.93 add(multiply(X10,X11),add(commutator(X10,X11),additive_inverse(add(multiply(X11,X10),X12)))) = additive_inverse(X12)]. % 132.47/132.93 [1537=param(1282,164),[19], % 132.47/132.93 add(multiply(X10,X11),add(commutator(X10,X11),add(X12,additive_inverse(multiply(X11,X10))))) = X12]. % 132.47/132.93 [1642=param(62,37),[], % 132.47/132.93 add(commutator(X10,X11),add(multiply(X10,X11),add(X12,X13))) = add(X12,add(multiply(X11,X10),X13))]. % 132.47/132.93 [1652=param(62,3),[], % 132.47/132.93 add(multiply(X11,X10),additive_inverse(multiply(X12,X11))) = add(commutator(X10,X11),multiply(add(X10,additive_inverse(X12)),X11))]. % 132.47/132.93 [1671=param(36,65),[36,89], % 132.47/132.93 add(X10,additive_inverse(multiply(X11,X12))) = add(commutator(X11,X12),additive_inverse(add(multiply(X12,X11),additive_inverse(X10))))]. % 132.47/132.93 [1708=param(129,129),[], % 132.47/132.93 add(X10,add(X11,additive_inverse(add(X12,additive_inverse(X13))))) = add(X11,additive_inverse(add(X12,additive_inverse(add(X10,X13)))))]. % 132.47/132.93 [1717=param(127,127),[], % 132.47/132.93 add(X10,additive_inverse(add(X11,additive_inverse(add(X12,X13))))) = additive_inverse(add(X11,additive_inverse(add(X12,add(X10,X13)))))]. % 132.47/132.93 [1718=param(127,129),[], % 132.47/132.93 add(X10,additive_inverse(add(X11,add(X12,additive_inverse(X13))))) = additive_inverse(add(X11,add(X12,additive_inverse(add(X10,X13)))))]. % 132.47/132.93 [1721=param(125,18),[], % 132.47/132.93 add(multiply(X10,X11),add(X12,additive_inverse(multiply(X10,add(X13,X11))))) = add(X12,additive_inverse(multiply(X10,X13)))]. % 132.47/132.93 [1786=param(103,60),[], % 132.47/132.93 add(X10,add(X11,multiply(X12,X13))) = add(X11,add(commutator(X13,X12),add(X10,multiply(X13,X12))))]. % 132.47/132.93 [1887=demod(50),[], % 132.47/132.93 add(X10,add(X11,add(X12,additive_inverse(X10)))) = add(X11,X12)]. % 132.47/132.93 [2008=param(123,17),[438], % 132.47/132.93 add(commutator(X10,X11),add(commutator(X10,X12),multiply(X10,add(X12,X11)))) = multiply(add(X12,X11),X10)]. % 132.47/132.93 [2203=param(134,143),[89,14,19], % 132.47/132.93 additive_inverse(add(X10,additive_inverse(add(X11,add(X12,additive_inverse(X13)))))) = add(X12,add(X11,additive_inverse(add(X10,X13))))]. % 132.47/132.93 [2395=param(134,155),[89,14,89,19,19], % 132.47/132.93 additive_inverse(add(X10,add(X11,additive_inverse(add(X12,additive_inverse(X13)))))) = add(X12,additive_inverse(add(X11,add(X10,X13))))]. % 132.47/132.93 [2712=param(145,214),[], % 132.47/132.93 add(commutator(commutator(X10,X11),X12),add(X13,X14)) = add(X13,add(commutator(X12,commutator(X11,X10)),X14))]. % 132.47/132.93 [9986=param(1721,65),[1652,100,7], % 132.47/132.93 add(commutator(add(X12,X10),X11),additive_inverse(multiply(X11,X12))) = add(commutator(X10,X11),additive_inverse(multiply(X12,X11)))]. % 132.47/132.93 [9999=param(1537,9986),[1887], % 132.47/132.93 add(commutator(X10,X11),commutator(X12,X11)) = commutator(add(X10,X12),X11)]. % 132.47/132.93 [10237=param(9999,94),[], % 132.47/132.93 add(commutator(X10,X11),additive_inverse(commutator(X11,X12))) = commutator(add(X10,X12),X11)]. % 132.47/132.93 [10463=param(1887,10237),[], % 132.47/132.93 add(commutator(X10,X11),add(X12,commutator(add(X13,X11),X10))) = add(X12,commutator(X13,X10))]. % 132.47/132.93 [10797=param(146,10463),[], % 132.47/132.93 add(commutator(X10,add(X11,X12)),add(X13,commutator(X11,X10))) = add(commutator(X10,X12),X13)]. % 132.47/132.93 [10813=param(146,10797),[], % 132.47/132.93 add(commutator(X10,add(X11,X12)),X13) = add(commutator(X10,X11),add(commutator(X10,X12),X13))]. % 132.47/132.93 [12117=param(103,65),[], % 132.47/132.93 add(X10,add(X11,additive_inverse(multiply(X12,X13)))) = add(X11,add(commutator(X12,X13),add(X10,additive_inverse(multiply(X13,X12)))))]. % 132.47/132.93 [12235=param(103,112),[], % 132.47/132.93 add(X10,add(X11,additive_inverse(add(commutator(X12,X13),additive_inverse(X14))))) = add(X11,add(commutator(X13,X12),add(X10,X14)))]. % 132.47/132.93 [12237=param(103,112),[], % 132.47/132.93 add(X10,additive_inverse(add(commutator(X11,X12),additive_inverse(add(X13,X14))))) = add(X13,add(X10,add(commutator(X12,X11),X14)))]. % 132.47/132.93 [12365=param(10813,60),[], % 132.47/132.93 add(commutator(X10,multiply(X11,X12)),X13) = add(commutator(X10,commutator(X12,X11)),add(commutator(X10,multiply(X12,X11)),X13))]. % 132.47/132.93 [12382=param(134,102),[14,14], % 132.47/132.93 additive_inverse(add(X10,add(X11,add(X12,add(X13,X14))))) = additive_inverse(add(X11,add(X12,add(X13,add(X10,X14)))))]. % 132.47/132.93 [12630=param(103,148),[], % 132.47/132.93 add(X10,add(X11,additive_inverse(add(commutator(X12,X13),X14)))) = add(X11,add(commutator(X13,X12),add(X10,additive_inverse(X14))))]. % 132.47/132.93 [12718=param(152,112),[], % 132.47/132.93 add(X10,additive_inverse(add(commutator(X11,X12),additive_inverse(add(X13,X14))))) = add(X13,add(commutator(X12,X11),add(X10,X14)))]. % 132.47/132.93 [12777=param(352,60),[], % 132.47/132.93 add(multiply(X10,multiply(X11,X12)),X13) = add(multiply(X10,commutator(X12,X11)),add(multiply(X10,multiply(X12,X11)),X13))]. % 132.47/132.93 [15054=param(353,60),[], % 132.47/132.93 add(X10,multiply(X11,multiply(X12,X13))) = add(multiply(X11,multiply(X13,X12)),add(multiply(X11,commutator(X13,X12)),X10))]. % 132.47/132.93 [16148=param(103,62),[], % 132.47/132.93 add(X10,add(X11,add(multiply(X12,X13),X14))) = add(commutator(X13,X12),add(multiply(X13,X12),add(X10,add(X11,X14))))]. % 132.47/132.93 [16394=param(124,35),[], % 132.47/132.93 add(X10,additive_inverse(add(X11,additive_inverse(multiply(add(X12,X13),X14))))) = additive_inverse(add(X11,additive_inverse(add(X10,multiply(add(X13,X12),X14)))))]. % 132.47/132.93 [16443=param(10813,18),[], % 132.47/132.93 add(commutator(X10,multiply(X11,add(X12,X13))),X14) = add(commutator(X10,multiply(X11,X12)),add(commutator(X10,multiply(X11,X13)),X14))]. % 132.47/132.93 [16458=param(10813,123),[], % 132.47/132.93 add(commutator(X10,X11),add(commutator(X10,X12),add(X13,multiply(X10,add(X11,X12))))) = add(X13,multiply(add(X11,X12),X10))]. % 132.47/132.93 [17119=param(352,18),[], % 132.47/132.93 add(multiply(X10,multiply(X11,add(X12,X13))),X14) = add(multiply(X10,multiply(X11,X12)),add(multiply(X10,multiply(X11,X13)),X14))]. % 132.47/132.93 [17830=param(26,166),[105,17119,12777,12777,16148,57,92,16148,57,92,16148,57,92,-1642,57,92,16443,12365,-12235,57,92,19,89,19,-2712,57,92,57,19,12365,-12718,57,92,136,89,19,19,62,-12718,57,92,89,19,19,89,446,19,62,-12718,57,92,-12237,57,92,136,89,19,19,89,19,19,-12718,57,92,-12237,57,92,89,19,19,89,19,19,-12718,57,92,-12237,57,92,89,127,19,89,19,19,89,19,19,62,-12718,57,92,-2395,89,19,19,-2712,57,92,57,19,-2712,57,92,57,19,19,89,446,19,62,-12718,57,92,12382,89,19,19,-12718,57,92,12382,89,19,19,-12718,57,92,89,446,19,89,19,19,1671,-427,57,92,-98,-427,57,92,12777,89,-219,12365,1718,19,19,-12235,57,92,19,89,19,-2203,-219,19,89,12365,19,-12235,57,92,19,89,19,12117,-427,57,92,89,12365,1718,12365,127,118,19,-2712,57,92,57,19,-219,19,1708,1717,19,12630,57,92,1717,12365,-12235,57,92,89,19,19,-2712,57,92,57,19,-2712,57,92,57,19,127,19,89,118,19,-12235,57,92,89,19,19,-12235,57,92,89,19,19,-12235,57,92,19,89,19,12117,-427,57,92,89,19,15054,18,18,1786,-190,57,92,437,57,92,89,16394,15,-16458,89,118,19,118,19,2008,89,19,12365,-2395,12365,118,118,19,-2712,57,92,57,19,-2712,57,92,57,19,-2712,57,92,57,19,62,-12235,57,92,89,19,19,-12235,57,92,89,19,19,-12235,57,92,19,89,19,-2712,57,92,57,19,12777,-12235,57,92,89,19,19,-12235,57,92,19,89,19,-2712,57,92,57,19,-2712,57,92,57,19,-2712,57,92,57,19,-12235,57,92,89,19,19,-12235,57,92,89,19,19,-2712,57,92,57,19,-2712,57,92,57,19,-2712,57,92,57,19,-12235,57,92,89,19,19,-2712,57,92,57,19,-2712,57,92,57,19,-12235,57,92,89,19,19,-12235,57,92,89,19,19,-12235,57,92,89,19,19,-12235,57,92,89,19,19,-12235,57,92,19,89,19,-2712,57,92,57,19,12365,-12718,57,92,136,89,19,19,-12718,57,92,-449,57,92,89,19,89,19,19,-12718,57,92,-449,57,92,89,19,89,19,19,-12718,57,92,89,19,19,-12718,57,92,89,19,19,25], % 132.55/132.95 thmtrue = thmfalse]. % 132.55/132.95 % SZS output end CNFRefutation % 132.55/132.95 Space: 463291 KB %------------------------------------------------------------------------------