%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP002-2 : TPTP v8.1.0. Bugfixed v1.2.1. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n016.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:05 EDT 2022 % Result : Unsatisfiable 0.86s 1.23s % Output : CNFRefutation 0.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : GRP002-2 : TPTP v8.1.0. Bugfixed v1.2.1. % 0.10/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n016.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 Jun 13 07:16:59 EDT 2022 % 0.13/0.34 % CPUTime : % 0.86/1.23 Theorem Proved. % 0.86/1.23 % SZS status Unsatisfiable % 0.86/1.23 % SZS output start CNFRefutation % 0.86/1.23 [1=axiom,[], % 0.86/1.23 multiply(j,inverse(h)) = k]. % 0.86/1.23 [2=axiom,[], % 0.86/1.23 multiply(h,b) = j]. % 0.86/1.23 [3=axiom,[], % 0.86/1.23 multiply(d,inverse(b)) = h]. % 0.86/1.23 [4=axiom,[], % 0.86/1.23 multiply(c,inverse(a)) = d]. % 0.86/1.23 [5=axiom,[], % 0.86/1.23 multiply(a,b) = c]. % 0.86/1.23 [6=axiom,[], % 0.86/1.23 multiply(X10,multiply(X10,X10)) = identity]. % 0.86/1.23 [7=axiom,[], % 0.86/1.23 multiply(X10,inverse(X10)) = identity]. % 0.86/1.23 [8=axiom,[], % 0.86/1.23 multiply(X10,identity) = X10]. % 0.86/1.23 [9=axiom,[], % 0.86/1.23 multiply(multiply(X10,X11),X12) = multiply(X10,multiply(X11,X12))]. % 0.86/1.23 [10=axiom,[], % 0.86/1.23 multiply(inverse(X10),X10) = identity]. % 0.86/1.23 [11=axiom,[], % 0.86/1.23 multiply(identity,X10) = X10]. % 0.86/1.23 [12=axiom,[], % 0.86/1.23 thtop(X10,X10) = thmfalse]. % 0.86/1.23 [13=axiom,[], % 0.86/1.23 thtop(multiply(k,inverse(b)),identity) = thmtrue]. % 0.86/1.23 [15=param(9,1),[], % 0.86/1.23 multiply(j,multiply(inverse(h),X10)) = multiply(k,X10)]. % 0.86/1.23 [16=param(9,2),[], % 0.86/1.23 multiply(h,multiply(b,X10)) = multiply(j,X10)]. % 0.86/1.23 [17=param(9,3),[], % 0.86/1.23 multiply(d,multiply(inverse(b),X10)) = multiply(h,X10)]. % 0.86/1.23 [19=param(9,5),[], % 0.86/1.23 multiply(a,multiply(b,X10)) = multiply(c,X10)]. % 0.86/1.23 [20=param(9,6),[9], % 0.86/1.23 multiply(X10,multiply(X11,multiply(X10,multiply(X11,multiply(X10,X11))))) = identity]. % 0.86/1.23 [21=param(9,6),[11,9], % 0.86/1.23 multiply(X11,multiply(X11,multiply(X11,X10))) = X10]. % 0.86/1.23 [27=param(15,10),[8], % 0.86/1.23 multiply(k,h) = j]. % 0.86/1.23 [30=param(16,6),[8], % 0.86/1.23 multiply(j,multiply(b,b)) = h]. % 0.86/1.23 [31=param(16,7),[8], % 0.86/1.23 multiply(j,inverse(b)) = h]. % 0.86/1.23 [33=param(9,30),[9], % 0.86/1.23 multiply(j,multiply(b,multiply(b,X10))) = multiply(h,X10)]. % 0.86/1.23 [36=param(17,10),[8,2], % 0.86/1.23 d = j]. % 0.86/1.23 [40=demod(4),[36], % 0.86/1.23 multiply(c,inverse(a)) = j]. % 0.86/1.23 [42=param(19,7),[8], % 0.86/1.23 multiply(c,inverse(b)) = a]. % 0.86/1.23 [46=param(9,20),[11,9,9,9,9], % 0.86/1.23 multiply(X11,multiply(X12,multiply(X11,multiply(X12,multiply(X11,multiply(X12,X10)))))) = X10]. % 0.86/1.23 [55=param(21,2),[], % 0.86/1.23 multiply(h,multiply(h,j)) = b]. % 0.86/1.23 [56=param(21,7),[8], % 0.86/1.23 multiply(X10,X10) = inverse(X10)]. % 0.86/1.23 [57=param(21,10),[8,56], % 0.86/1.23 inverse(inverse(X10)) = X10]. % 0.86/1.23 [58=param(21,15),[], % 0.86/1.23 multiply(inverse(h),X10) = multiply(j,multiply(j,multiply(k,X10)))]. % 0.86/1.23 [60=param(21,16),[], % 0.86/1.23 multiply(b,X10) = multiply(h,multiply(h,multiply(j,X10)))]. % 0.86/1.23 [63=demod(33),[60,60], % 0.86/1.23 multiply(j,multiply(h,multiply(h,multiply(j,multiply(h,multiply(h,multiply(j,X10))))))) = multiply(h,X10)]. % 0.86/1.23 [67=param(21,20),[8,56], % 0.86/1.23 multiply(X11,multiply(X10,multiply(X11,multiply(X10,X11)))) = inverse(X10)]. % 0.86/1.23 [68=param(21,27),[], % 0.86/1.23 multiply(k,multiply(k,j)) = h]. % 0.86/1.23 [69=param(21,31),[], % 0.86/1.23 multiply(j,multiply(j,h)) = inverse(b)]. % 0.86/1.23 [70=param(21,40),[], % 0.86/1.23 multiply(c,multiply(c,j)) = inverse(a)]. % 0.86/1.23 [71=param(21,42),[], % 0.86/1.23 multiply(c,multiply(c,a)) = inverse(b)]. % 0.86/1.23 [72=param(56,9),[], % 0.86/1.23 multiply(X10,multiply(X11,multiply(X10,X11))) = inverse(multiply(X10,X11))]. % 0.86/1.23 [73=demod(67),[72], % 0.86/1.23 multiply(X10,inverse(multiply(X11,X10))) = inverse(X11)]. % 0.86/1.23 [74=param(9,56),[], % 0.86/1.23 multiply(inverse(X10),X11) = multiply(X10,multiply(X10,X11))]. % 0.86/1.23 [76=demod(58),[74], % 0.86/1.23 multiply(h,multiply(h,X10)) = multiply(j,multiply(j,multiply(k,X10)))]. % 0.86/1.23 [79=demod(63),[76,21,76,21], % 0.86/1.23 multiply(h,X10) = multiply(k,multiply(k,multiply(j,X10)))]. % 0.86/1.23 [80=demod(2),[79], % 0.86/1.23 multiply(k,multiply(k,multiply(j,b))) = j]. % 0.86/1.23 [81=demod(76),[79,79], % 0.86/1.23 multiply(j,multiply(j,multiply(k,X10))) = multiply(k,multiply(k,multiply(j,multiply(k,multiply(k,multiply(j,X10))))))]. % 0.86/1.23 [86=demod(60),[79,79], % 0.86/1.23 multiply(b,X10) = multiply(k,multiply(k,multiply(j,multiply(k,multiply(k,multiply(j,multiply(j,X10)))))))]. % 0.86/1.23 [89=demod(55),[79,56,79], % 0.86/1.23 multiply(k,multiply(k,multiply(j,multiply(k,multiply(k,inverse(j)))))) = b]. % 0.86/1.23 [92=param(46,31),[], % 0.86/1.23 multiply(X10,multiply(j,multiply(X10,multiply(j,multiply(X10,h))))) = inverse(b)]. % 0.86/1.23 [94=param(46,42),[], % 0.86/1.23 multiply(X10,multiply(c,multiply(X10,multiply(c,multiply(X10,a))))) = inverse(b)]. % 0.86/1.23 [97=param(21,72),[], % 0.86/1.23 multiply(X10,multiply(X10,inverse(multiply(X10,X11)))) = multiply(X11,multiply(X10,X11))]. % 0.86/1.23 [98=param(72,68),[9,68], % 0.86/1.23 multiply(k,multiply(k,multiply(j,h))) = inverse(h)]. % 0.86/1.23 [99=param(72,69),[9,79,31,27,-97,69,57], % 0.86/1.23 multiply(j,multiply(k,multiply(k,inverse(multiply(k,j))))) = b]. % 0.86/1.23 [102=param(73,9),[], % 0.86/1.23 multiply(X10,inverse(multiply(X11,multiply(X12,X10)))) = inverse(multiply(X11,X12))]. % 0.86/1.23 [103=param(21,73),[], % 0.86/1.23 multiply(X10,multiply(X10,inverse(X11))) = inverse(multiply(X11,X10))]. % 0.86/1.23 [104=param(73,70),[57,9], % 0.86/1.23 multiply(c,multiply(j,a)) = inverse(c)]. % 0.86/1.23 [108=param(21,104),[7,8], % 0.86/1.23 multiply(j,a) = c]. % 0.86/1.23 [110=param(21,108),[], % 0.86/1.23 multiply(j,multiply(j,c)) = a]. % 0.86/1.23 [112=param(21,80),[], % 0.86/1.23 multiply(j,b) = multiply(k,j)]. % 0.86/1.23 [115=param(72,110),[9,110], % 0.86/1.23 multiply(j,multiply(j,multiply(c,a))) = inverse(a)]. % 0.86/1.23 [116=param(81,68),[69,-97,21], % 0.86/1.23 multiply(k,multiply(k,multiply(j,multiply(k,inverse(multiply(k,j)))))) = inverse(b)]. % 0.86/1.23 [117=param(21,115),[], % 0.86/1.23 multiply(c,a) = multiply(j,inverse(a))]. % 0.86/1.23 [118=demod(71),[117], % 0.86/1.23 multiply(c,multiply(j,inverse(a))) = inverse(b)]. % 0.86/1.23 [123=param(21,98),[], % 0.86/1.23 multiply(j,h) = multiply(k,inverse(h))]. % 0.86/1.23 [124=demod(69),[123], % 0.86/1.23 multiply(j,multiply(k,inverse(h))) = inverse(b)]. % 0.86/1.23 [125=param(72,123),[79,124,123], % 0.86/1.23 multiply(j,multiply(k,multiply(k,inverse(b)))) = inverse(multiply(k,inverse(h)))]. % 0.86/1.23 [127=param(46,124),[], % 0.86/1.23 multiply(j,multiply(k,multiply(j,multiply(k,inverse(b))))) = inverse(h)]. % 0.86/1.23 [132=param(103,73),[9,56], % 0.86/1.23 multiply(X10,inverse(X11)) = inverse(multiply(X11,inverse(X10)))]. % 0.86/1.23 [134=param(57,103),[], % 0.86/1.23 inverse(multiply(X10,multiply(X10,inverse(X11)))) = multiply(X11,X10)]. % 0.86/1.23 [138=param(132,9),[], % 0.86/1.23 inverse(multiply(X10,inverse(multiply(X11,X12)))) = multiply(X11,multiply(X12,inverse(X10)))]. % 0.86/1.23 [139=param(132,79),[], % 0.86/1.23 inverse(multiply(X10,inverse(h))) = multiply(k,multiply(k,multiply(j,inverse(X10))))]. % 0.86/1.23 [140=param(103,132),[], % 0.86/1.23 multiply(X10,inverse(multiply(X11,inverse(X10)))) = inverse(multiply(X11,X10))]. % 0.86/1.23 [141=param(132,9),[], % 0.86/1.23 inverse(multiply(X10,multiply(X11,inverse(X12)))) = multiply(X12,inverse(multiply(X10,X11)))]. % 0.86/1.23 [142=param(132,79),[], % 0.86/1.23 inverse(multiply(k,multiply(k,multiply(j,inverse(X10))))) = multiply(X10,inverse(h))]. % 0.86/1.23 [145=param(134,9),[], % 0.86/1.23 inverse(multiply(X10,multiply(X10,inverse(multiply(X11,X12))))) = multiply(X11,multiply(X12,X10))]. % 0.86/1.23 [150=param(21,89),[], % 0.86/1.23 multiply(j,multiply(k,multiply(k,inverse(j)))) = multiply(k,b)]. % 0.86/1.23 [152=param(102,68),[9], % 0.86/1.23 multiply(k,multiply(j,inverse(multiply(X10,h)))) = inverse(multiply(X10,k))]. % 0.86/1.23 [153=param(102,110),[9], % 0.86/1.23 multiply(j,multiply(c,inverse(multiply(X10,a)))) = inverse(multiply(X10,j))]. % 0.86/1.23 [156=param(21,153),[73], % 0.86/1.23 multiply(c,inverse(multiply(X10,a))) = multiply(j,inverse(X10))]. % 0.86/1.23 [157=param(156,9),[], % 0.86/1.23 multiply(c,inverse(multiply(X10,multiply(X11,a)))) = multiply(j,inverse(multiply(X10,X11)))]. % 0.86/1.23 [160=param(92,27),[56], % 0.86/1.23 multiply(k,multiply(j,multiply(k,inverse(j)))) = inverse(b)]. % 0.86/1.23 [161=param(21,160),[], % 0.86/1.23 multiply(j,multiply(k,inverse(j))) = multiply(k,multiply(k,inverse(b)))]. % 0.86/1.23 [162=param(21,161),[125], % 0.86/1.23 multiply(j,inverse(multiply(k,inverse(h)))) = multiply(k,inverse(j))]. % 0.86/1.23 [163=param(72,161),[9,74,125,162,150,161], % 0.86/1.23 inverse(multiply(k,multiply(k,inverse(b)))) = multiply(k,b)]. % 0.86/1.23 [164=param(94,108),[56], % 0.86/1.23 multiply(j,multiply(c,multiply(j,inverse(c)))) = inverse(b)]. % 0.86/1.23 [165=param(57,163),[], % 0.86/1.23 multiply(k,multiply(k,inverse(b))) = inverse(multiply(k,b))]. % 0.86/1.23 [177=param(21,164),[31,123], % 0.86/1.23 multiply(c,multiply(j,inverse(c))) = multiply(k,inverse(h))]. % 0.86/1.23 [183=param(21,152),[73], % 0.86/1.23 multiply(j,inverse(multiply(X10,h))) = multiply(k,inverse(X10))]. % 0.86/1.23 [185=param(183,9),[], % 0.86/1.23 multiply(j,inverse(multiply(X10,multiply(X11,h)))) = multiply(k,inverse(multiply(X10,X11)))]. % 0.86/1.23 [192=param(185,56),[], % 0.86/1.23 multiply(j,inverse(multiply(X10,inverse(h)))) = multiply(k,inverse(multiply(X10,h)))]. % 0.86/1.23 [193=param(21,116),[], % 0.86/1.23 multiply(j,multiply(k,inverse(multiply(k,j)))) = multiply(k,inverse(b))]. % 0.86/1.23 [196=param(157,56),[], % 0.86/1.23 multiply(c,inverse(multiply(X10,inverse(a)))) = multiply(j,inverse(multiply(X10,a)))]. % 0.86/1.23 [203=param(138,132),[], % 0.86/1.23 multiply(X10,inverse(multiply(X11,inverse(X12)))) = inverse(multiply(X11,inverse(multiply(X10,X12))))]. % 0.86/1.23 [207=param(21,139),[], % 0.86/1.23 multiply(k,inverse(multiply(X10,inverse(h)))) = multiply(j,inverse(X10))]. % 0.86/1.23 [214=param(141,132),[], % 0.86/1.23 inverse(multiply(X10,inverse(multiply(X11,inverse(X12))))) = multiply(X11,inverse(multiply(X10,X12)))]. % 0.86/1.23 [231=param(145,196),[-134,57,117,118,57], % 0.86/1.23 inverse(multiply(c,multiply(j,inverse(multiply(X10,a))))) = multiply(X10,b)]. % 0.86/1.23 [232=param(145,127),[-134,57,-134,-141,-141,203,-134,203,86,56,7,8,56,-207,203,27,203,203,68,57,-214,203,86,123,124,165,-214,31,203,27,203,57,57,21,57,57,68,192,27,203,-134,-214,140,57,68,-142,7,8,56,57,57,56,57,132,57], % 0.86/1.23 multiply(k,inverse(multiply(j,multiply(k,inverse(b))))) = inverse(h)]. % 0.86/1.23 [233=param(21,232),[], % 0.86/1.23 inverse(multiply(j,multiply(k,inverse(b)))) = multiply(k,multiply(k,inverse(h)))]. % 0.86/1.23 [234=param(57,233),[], % 0.86/1.23 multiply(j,multiply(k,inverse(b))) = inverse(multiply(k,multiply(k,inverse(h))))]. % 0.86/1.23 [235=demod(127),[234], % 0.86/1.23 multiply(j,multiply(k,inverse(multiply(k,multiply(k,inverse(h)))))) = inverse(h)]. % 0.86/1.23 [238=param(57,231),[], % 0.86/1.23 multiply(c,multiply(j,inverse(multiply(X10,a)))) = inverse(multiply(X10,b))]. % 0.86/1.23 [240=param(238,79),[108,-214,-214,57,-214,203,177,203,27,57,203,57,79,112,68,27], % 0.86/1.23 multiply(k,inverse(multiply(k,j))) = inverse(j)]. % 0.86/1.23 [241=demod(193),[240,7], % 0.86/1.23 multiply(k,inverse(b)) = identity]. % 0.86/1.23 [242=demod(234),[241,8], % 0.86/1.23 inverse(multiply(k,multiply(k,inverse(h)))) = j]. % 0.86/1.23 [243=demod(235),[242,-97,240], % 0.86/1.23 multiply(k,inverse(j)) = inverse(h)]. % 0.86/1.23 [253=demod(99),[240,243,-142,7,8,56,57], % 0.86/1.23 b = k]. % 0.86/1.23 [265=param(13,253),[7,12], % 0.86/1.23 thmtrue = thmfalse]. % 0.86/1.23 % SZS output end CNFRefutation % 0.86/1.23 Space: 669 KB %------------------------------------------------------------------------------