%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : RNG019-7 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n028.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 1.56s 1.92s % Output : CNFRefutation 1.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : RNG019-7 : TPTP v8.1.0. Released v1.0.0. % 0.07/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n028.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon May 30 16:36:35 EDT 2022 % 0.13/0.34 % CPUTime : % 1.56/1.92 Theorem Proved. % 1.56/1.92 % SZS status Unsatisfiable % 1.56/1.92 % SZS output start CNFRefutation % 1.56/1.92 [5=axiom,[], % 1.56/1.92 multiply(X10,additive_inverse(X11)) = additive_inverse(multiply(X10,X11))]. % 1.56/1.92 [7=axiom,[], % 1.56/1.92 multiply(additive_inverse(X10),X11) = additive_inverse(multiply(X10,X11))]. % 1.56/1.92 [10=axiom,[], % 1.56/1.92 add(multiply(X11,X10),additive_inverse(multiply(X10,X11))) = commutator(X10,X11)]. % 1.56/1.92 [11=axiom,[], % 1.56/1.92 associator(X10,X11,X12) = add(multiply(multiply(X10,X11),X12),additive_inverse(multiply(X10,multiply(X11,X12))))]. % 1.56/1.92 [14=axiom,[], % 1.56/1.92 add(add(X10,X11),X12) = add(X10,add(X11,X12))]. % 1.56/1.92 [15=axiom,[], % 1.56/1.92 add(X10,X11) = add(X11,X10)]. % 1.56/1.92 [16=demod(11),[15], % 1.56/1.92 associator(X10,X11,X12) = add(additive_inverse(multiply(X10,multiply(X11,X12))),multiply(multiply(X10,X11),X12))]. % 1.56/1.92 [18=axiom,[], % 1.56/1.92 add(multiply(X10,X11),multiply(X10,X12)) = multiply(X10,add(X11,X12))]. % 1.56/1.92 [19=axiom,[], % 1.56/1.92 additive_inverse(additive_inverse(X10)) = X10]. % 1.56/1.92 [20=axiom,[], % 1.56/1.92 add(X10,additive_inverse(X10)) = additive_identity]. % 1.56/1.92 [23=axiom,[], % 1.56/1.92 add(X10,additive_identity) = X10]. % 1.56/1.92 [24=axiom,[], % 1.56/1.92 add(additive_identity,X10) = X10]. % 1.56/1.92 [25=axiom,[], % 1.56/1.92 thtop(X10,X10) = thmfalse]. % 1.56/1.92 [26=axiom,[15,16,16,16,14], % 1.56/1.92 thtop(add(additive_inverse(multiply(x,multiply(y,add(v,u)))),multiply(multiply(x,y),add(v,u))),add(additive_inverse(multiply(x,multiply(y,u))),add(multiply(multiply(x,y),u),add(additive_inverse(multiply(x,multiply(y,v))),multiply(multiply(x,y),v))))) = thmtrue]. % 1.56/1.92 [36=param(14,15),[], % 1.56/1.92 add(X10,add(X11,X12)) = add(X12,add(X10,X11))]. % 1.56/1.92 [37=param(14,15),[14], % 1.56/1.92 add(X10,add(X11,X12)) = add(X11,add(X10,X12))]. % 1.56/1.92 [38=param(14,20),[], % 1.56/1.92 add(X10,add(X11,additive_inverse(add(X10,X11)))) = additive_identity]. % 1.56/1.92 [39=param(14,20),[24], % 1.56/1.92 add(X11,add(additive_inverse(X11),X10)) = X10]. % 1.56/1.92 [42=param(39,15),[], % 1.56/1.92 add(X10,add(X11,additive_inverse(X10))) = X11]. % 1.56/1.92 [54=param(10,5),[7,19], % 1.56/1.92 add(additive_inverse(multiply(X10,X11)),multiply(X11,X10)) = commutator(additive_inverse(X11),X10)]. % 1.56/1.92 [55=param(10,5),[7,19,54], % 1.56/1.92 commutator(additive_inverse(X10),X11) = commutator(X10,additive_inverse(X11))]. % 1.56/1.92 [56=demod(54),[55], % 1.56/1.92 add(additive_inverse(multiply(X10,X11)),multiply(X11,X10)) = commutator(X11,additive_inverse(X10))]. % 1.56/1.92 [57=param(10,15),[56], % 1.56/1.92 commutator(X10,X11) = commutator(X11,additive_inverse(X10))]. % 1.56/1.92 [60=param(42,10),[15], % 1.56/1.92 add(commutator(X10,X11),multiply(X10,X11)) = multiply(X11,X10)]. % 1.56/1.92 [62=param(14,60),[], % 1.56/1.92 add(multiply(X10,X11),X12) = add(commutator(X11,X10),add(multiply(X11,X10),X12))]. % 1.56/1.92 [70=param(38,15),[14,15], % 1.56/1.92 add(X10,add(X11,additive_inverse(add(X11,X10)))) = additive_identity]. % 1.56/1.92 [82=param(39,70),[23], % 1.56/1.92 add(X11,additive_inverse(add(X11,additive_inverse(X10)))) = X10]. % 1.56/1.92 [85=param(39,82),[], % 1.56/1.92 additive_inverse(add(additive_inverse(X10),additive_inverse(X11))) = add(X10,X11)]. % 1.56/1.92 [89=param(85,19),[], % 1.56/1.92 add(additive_inverse(X10),X11) = additive_inverse(add(X10,additive_inverse(X11)))]. % 1.56/1.92 [92=demod(56),[89,10], % 1.56/1.92 commutator(X10,additive_inverse(X11)) = additive_inverse(commutator(X10,X11))]. % 1.56/1.92 [100=param(42,89),[19], % 1.56/1.92 add(X10,additive_inverse(add(X11,X10))) = additive_inverse(X11)]. % 1.56/1.92 [105=param(36,60),[36], % 1.56/1.92 add(X10,multiply(X11,X12)) = add(commutator(X12,X11),add(multiply(X12,X11),X10))]. % 1.56/1.92 [107=param(36,89),[], % 1.56/1.92 add(X10,additive_inverse(add(X11,additive_inverse(X12)))) = add(X12,add(X10,additive_inverse(X11)))]. % 1.56/1.92 [118=param(100,15),[], % 1.56/1.92 add(X10,additive_inverse(add(X10,X11))) = additive_inverse(X11)]. % 1.56/1.92 [120=param(37,15),[14], % 1.56/1.92 add(X10,add(X11,X12)) = add(X10,add(X12,X11))]. % 1.56/1.92 [121=param(37,36),[], % 1.56/1.92 add(X10,add(X11,X12)) = add(X12,add(X11,X10))]. % 1.56/1.92 [126=param(118,36),[], % 1.56/1.92 add(X10,additive_inverse(add(X11,add(X10,X12)))) = additive_inverse(add(X12,X11))]. % 1.56/1.92 [127=param(118,37),[], % 1.56/1.92 add(X10,additive_inverse(add(X11,add(X10,X12)))) = additive_inverse(add(X11,X12))]. % 1.56/1.92 [128=demod(126),[127], % 1.56/1.92 additive_inverse(add(X10,X11)) = additive_inverse(add(X11,X10))]. % 1.56/1.92 [150=param(121,14),[], % 1.56/1.92 add(X10,add(X11,add(X12,X13))) = add(X12,add(X13,add(X11,X10)))]. % 1.56/1.92 [167=param(128,120),[14], % 1.56/1.92 additive_inverse(add(X10,add(X11,X12))) = additive_inverse(add(X12,add(X11,X10)))]. % 1.56/1.92 [219=param(167,107),[89,19], % 1.56/1.92 additive_inverse(add(X10,additive_inverse(add(X11,additive_inverse(X12))))) = add(X11,additive_inverse(add(X10,X12)))]. % 1.56/1.92 [352=param(14,18),[], % 1.56/1.92 add(multiply(X10,add(X11,X12)),X13) = add(multiply(X10,X11),add(multiply(X10,X12),X13))]. % 1.56/1.92 [438=param(62,18),[], % 1.56/1.92 add(multiply(X11,X10),multiply(X10,X12)) = add(commutator(X10,X11),multiply(X10,add(X11,X12)))]. % 1.56/1.92 [673=param(352,15),[], % 1.56/1.92 add(multiply(X10,X11),add(multiply(X10,X12),X13)) = add(X13,multiply(X10,add(X11,X12)))]. % 1.56/1.92 [804=param(26,150),[-673,62,62,105,89,-219,-219,19,18,62,438,57,92,89,118,19,19,19,62,25], % 1.56/1.92 thmtrue = thmfalse]. % 1.56/1.92 % SZS output end CNFRefutation % 1.56/1.92 Space: 5936 KB %------------------------------------------------------------------------------