%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : TOP049-1 : TPTP v8.1.0. Released v8.1.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n027.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 : Thu Jul 21 21:25:58 EDT 2022 % Result : Unsatisfiable 0.41s 1.06s % Output : CNFRefutation 0.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : TOP049-1 : TPTP v8.1.0. Released v8.1.0. % 0.06/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sun May 29 08:06:45 EDT 2022 % 0.12/0.33 % CPUTime : % 0.41/1.06 Theorem Proved. % 0.41/1.06 % SZS status Unsatisfiable % 0.41/1.06 % SZS output start CNFRefutation % 0.41/1.06 [1=axiom,[], % 0.41/1.06 product(a4,a8) = a9]. % 0.41/1.06 [2=axiom,[], % 0.41/1.06 product(a10,a3) = a4]. % 0.41/1.06 [3=axiom,[], % 0.41/1.06 product(a8,a9) = a10]. % 0.41/1.06 [4=axiom,[], % 0.41/1.06 product(a7,a4) = a8]. % 0.41/1.06 [5=axiom,[], % 0.41/1.06 product(a6,a1) = a7]. % 0.41/1.06 [6=axiom,[], % 0.41/1.06 product(a5,a4) = a6]. % 0.41/1.06 [7=axiom,[], % 0.41/1.06 product(a2,a10) = a5]. % 0.41/1.06 [8=axiom,[], % 0.41/1.06 product(a3,a4) = a2]. % 0.41/1.06 [9=axiom,[], % 0.41/1.06 product(a1,a2) = a3]. % 0.41/1.06 [10=axiom,[], % 0.41/1.06 product(a9,a7) = a1]. % 0.41/1.06 [11=axiom,[], % 0.41/1.06 product(product(X10,X11),X12) = product(product(X10,X12),product(X11,X12))]. % 0.41/1.06 [12=axiom,[], % 0.41/1.06 product(product(X10,X11),X11) = X10]. % 0.41/1.06 [13=axiom,[], % 0.41/1.06 product(X10,X10) = X10]. % 0.41/1.06 [14=axiom,[], % 0.41/1.06 thtop(X10,X10) = thmfalse]. % 0.41/1.06 [15=axiom,[], % 0.41/1.06 thtop(tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5),tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6)) = thmtrue]. % 0.41/1.06 [16=param(12,1),[], % 0.41/1.06 product(a9,a8) = a4]. % 0.41/1.06 [17=param(12,2),[], % 0.41/1.06 product(a4,a3) = a10]. % 0.41/1.06 [18=param(12,3),[], % 0.41/1.06 product(a10,a9) = a8]. % 0.41/1.06 [19=param(12,4),[], % 0.41/1.06 product(a8,a4) = a7]. % 0.41/1.06 [21=param(12,6),[], % 0.41/1.06 product(a6,a4) = a5]. % 0.41/1.06 [23=param(12,8),[], % 0.41/1.06 product(a2,a4) = a3]. % 0.41/1.06 [24=param(12,9),[], % 0.41/1.06 product(a3,a2) = a1]. % 0.41/1.06 [25=param(12,10),[], % 0.41/1.06 product(a1,a7) = a9]. % 0.41/1.06 [26=param(11,1),[], % 0.41/1.06 product(product(a4,X10),product(a8,X10)) = product(a9,X10)]. % 0.41/1.06 [27=param(11,2),[], % 0.41/1.06 product(product(a10,X10),product(a3,X10)) = product(a4,X10)]. % 0.41/1.06 [28=param(11,3),[], % 0.41/1.06 product(product(a8,X10),product(a9,X10)) = product(a10,X10)]. % 0.41/1.06 [29=param(11,4),[], % 0.41/1.06 product(product(a7,X10),product(a4,X10)) = product(a8,X10)]. % 0.41/1.06 [30=param(11,5),[], % 0.41/1.06 product(product(a6,X10),product(a1,X10)) = product(a7,X10)]. % 0.41/1.06 [31=param(11,6),[], % 0.41/1.06 product(product(a5,X10),product(a4,X10)) = product(a6,X10)]. % 0.41/1.06 [32=param(11,7),[], % 0.41/1.06 product(product(a2,X10),product(a10,X10)) = product(a5,X10)]. % 0.41/1.06 [33=param(11,8),[], % 0.41/1.06 product(product(a3,X10),product(a4,X10)) = product(a2,X10)]. % 0.41/1.06 [34=param(11,9),[], % 0.41/1.06 product(product(a1,X10),product(a2,X10)) = product(a3,X10)]. % 0.41/1.06 [47=param(11,7),[], % 0.41/1.06 product(product(a2,X10),a10) = product(a5,product(X10,a10))]. % 0.41/1.06 [60=param(11,23),[], % 0.41/1.06 product(product(a2,X10),a4) = product(a3,product(X10,a4))]. % 0.41/1.06 [66=param(11,21),[], % 0.41/1.06 product(product(a6,X10),product(a4,X10)) = product(a5,X10)]. % 0.41/1.06 [72=param(11,18),[], % 0.41/1.06 product(product(a10,X10),product(a9,X10)) = product(a8,X10)]. % 0.41/1.06 [73=param(11,18),[], % 0.41/1.06 product(product(a10,X10),a9) = product(a8,product(X10,a9))]. % 0.41/1.06 [81=param(26,17),[], % 0.41/1.06 product(a9,a3) = product(a10,product(a8,a3))]. % 0.41/1.06 [97=param(28,81),[2], % 0.41/1.06 product(product(a8,a3),product(a10,product(a8,a3))) = a4]. % 0.41/1.06 [106=param(29,17),[11], % 0.41/1.06 product(product(a7,a10),product(a3,a10)) = product(a8,a3)]. % 0.41/1.06 [118=param(30,21),[4], % 0.41/1.06 product(a5,product(a1,a4)) = a8]. % 0.41/1.06 [126=param(31,1),[], % 0.41/1.06 product(product(a5,a8),a9) = product(a6,a8)]. % 0.41/1.06 [130=param(31,118),[], % 0.41/1.06 product(a8,product(a4,product(a1,a4))) = product(a6,product(a1,a4))]. % 0.41/1.06 [135=param(32,2),[60,8,24], % 0.41/1.06 product(a5,a3) = a1]. % 0.41/1.06 [137=param(32,18),[11,16,60,19], % 0.41/1.06 product(a3,a7) = product(a5,a9)]. % 0.41/1.06 [141=param(11,135),[], % 0.41/1.06 product(product(a5,X10),product(a3,X10)) = product(a1,X10)]. % 0.41/1.06 [144=param(12,135),[], % 0.41/1.06 product(a1,a3) = a5]. % 0.41/1.06 [145=param(31,135),[17], % 0.41/1.06 product(a1,a10) = product(a6,a3)]. % 0.41/1.06 [146=param(11,144),[], % 0.41/1.06 product(product(a1,X10),product(a3,X10)) = product(a5,X10)]. % 0.41/1.06 [148=param(30,144),[11], % 0.41/1.06 product(product(a6,a5),product(a3,a5)) = product(a7,a3)]. % 0.41/1.06 [150=param(33,13),[17], % 0.41/1.06 product(a3,a10) = product(a2,a3)]. % 0.41/1.06 [152=demod(106),[150], % 0.41/1.06 product(product(a7,a10),product(a2,a3)) = product(a8,a3)]. % 0.41/1.06 [158=param(12,150),[47,150], % 0.41/1.06 product(a5,product(a2,a3)) = a3]. % 0.41/1.06 [162=param(12,145),[11,150], % 0.41/1.06 product(product(a6,a10),product(a2,a3)) = a1]. % 0.41/1.06 [163=param(30,145),[], % 0.41/1.06 product(product(a6,a10),product(a6,a3)) = product(a7,a10)]. % 0.41/1.06 [164=param(34,7),[145,11,148,150], % 0.41/1.06 product(a7,a3) = product(a2,a3)]. % 0.41/1.06 [165=demod(148),[164], % 0.41/1.06 product(product(a6,a5),product(a3,a5)) = product(a2,a3)]. % 0.41/1.06 [166=param(34,13),[], % 0.41/1.06 product(a1,product(a2,a1)) = product(a3,a1)]. % 0.41/1.06 [167=param(34,25),[137], % 0.41/1.06 product(a9,product(a2,a7)) = product(a5,a9)]. % 0.41/1.06 [170=param(12,164),[12], % 0.41/1.06 a7 = a2]. % 0.41/1.06 [171=demod(167),[170,13], % 0.41/1.06 product(a9,a2) = product(a5,a9)]. % 0.41/1.06 [172=demod(163),[170,7], % 0.41/1.06 product(product(a6,a10),product(a6,a3)) = a5]. % 0.41/1.06 [173=demod(152),[170,7,158], % 0.41/1.06 product(a8,a3) = a3]. % 0.41/1.06 [174=demod(97),[173,173,2,8], % 0.41/1.06 a2 = a4]. % 0.41/1.06 [175=demod(171),[174], % 0.41/1.06 product(a9,a4) = product(a5,a9)]. % 0.41/1.06 [176=demod(170),[174], % 0.41/1.06 a7 = a4]. % 0.41/1.06 [177=demod(166),[174], % 0.41/1.06 product(a1,product(a4,a1)) = product(a3,a1)]. % 0.41/1.06 [178=demod(165),[174,17], % 0.41/1.06 product(product(a6,a5),product(a3,a5)) = a10]. % 0.41/1.06 [179=demod(162),[174,17,12], % 0.41/1.06 a1 = a6]. % 0.41/1.06 [180=demod(177),[179,179,179], % 0.41/1.06 product(a3,a6) = product(a6,product(a4,a6))]. % 0.41/1.06 [184=demod(146),[179], % 0.41/1.06 product(product(a6,X10),product(a3,X10)) = product(a5,X10)]. % 0.41/1.06 [185=demod(178),[184,13], % 0.41/1.06 a5 = a10]. % 0.41/1.06 [188=demod(175),[185,18], % 0.41/1.06 product(a9,a4) = a8]. % 0.41/1.06 [189=demod(172),[185], % 0.41/1.06 product(product(a6,a10),product(a6,a3)) = a10]. % 0.41/1.06 [192=demod(126),[185,73,3], % 0.41/1.06 product(a6,a8) = product(a8,a10)]. % 0.41/1.06 [195=demod(66),[185], % 0.41/1.06 product(product(a6,X10),product(a4,X10)) = product(a10,X10)]. % 0.41/1.06 [200=demod(6),[185], % 0.41/1.06 product(a10,a4) = a6]. % 0.41/1.06 [201=demod(145),[179], % 0.41/1.06 product(a6,a3) = product(a6,a10)]. % 0.41/1.06 [202=demod(189),[201,-11,13], % 0.41/1.06 product(a6,a10) = a10]. % 0.41/1.06 [203=demod(201),[202], % 0.41/1.06 product(a6,a3) = a10]. % 0.41/1.06 [210=demod(141),[185,27,179], % 0.41/1.06 product(a4,X10) = product(a6,X10)]. % 0.41/1.06 [211=demod(1),[210,192], % 0.41/1.06 product(a8,a10) = a9]. % 0.41/1.06 [216=demod(195),[210,13], % 0.41/1.06 product(a10,X10) = product(a6,X10)]. % 0.41/1.06 [217=demod(2),[216,203], % 0.41/1.06 a4 = a10]. % 0.41/1.06 [219=demod(188),[217], % 0.41/1.06 product(a9,a10) = a8]. % 0.41/1.06 [220=demod(176),[217], % 0.41/1.06 a7 = a10]. % 0.41/1.06 [221=demod(174),[217], % 0.41/1.06 a2 = a10]. % 0.41/1.06 [226=demod(200),[217,13], % 0.41/1.06 a10 = a6]. % 0.41/1.06 [229=demod(221),[226], % 0.41/1.06 a2 = a6]. % 0.41/1.06 [230=demod(220),[226], % 0.41/1.06 a7 = a6]. % 0.41/1.06 [231=demod(219),[226], % 0.41/1.06 product(a9,a6) = a8]. % 0.41/1.06 [232=demod(217),[226], % 0.41/1.06 a4 = a6]. % 0.41/1.06 [233=demod(211),[226], % 0.41/1.06 product(a8,a6) = a9]. % 0.41/1.06 [234=demod(203),[226], % 0.41/1.06 product(a6,a3) = a6]. % 0.41/1.06 [235=demod(185),[226], % 0.41/1.06 a5 = a6]. % 0.41/1.06 [240=demod(72),[226], % 0.41/1.06 product(product(a6,X10),product(a9,X10)) = product(a8,X10)]. % 0.41/1.06 [249=demod(180),[232,13,13], % 0.41/1.06 product(a3,a6) = a6]. % 0.41/1.06 [250=demod(130),[232,179,232,13,13,233,179,232,13,13], % 0.41/1.06 a9 = a6]. % 0.41/1.06 [256=demod(240),[250,13], % 0.41/1.06 product(a6,X10) = product(a8,X10)]. % 0.41/1.06 [261=demod(234),[256,173], % 0.41/1.06 a3 = a6]. % 0.41/1.06 [262=demod(249),[261,256], % 0.41/1.06 product(a8,a6) = a6]. % 0.41/1.06 [263=demod(231),[250,256,262], % 0.41/1.06 a6 = a8]. % 0.41/1.06 [264=demod(261),[263], % 0.41/1.06 a3 = a8]. % 0.41/1.06 [265=demod(250),[263], % 0.41/1.06 a9 = a8]. % 0.41/1.06 [266=demod(235),[263], % 0.41/1.06 a5 = a8]. % 0.41/1.06 [267=demod(232),[263], % 0.41/1.06 a4 = a8]. % 0.41/1.06 [268=demod(230),[263], % 0.41/1.06 a7 = a8]. % 0.41/1.06 [269=demod(229),[263], % 0.41/1.06 a2 = a8]. % 0.41/1.06 [270=demod(226),[263], % 0.41/1.06 a10 = a8]. % 0.41/1.06 [271=demod(179),[263], % 0.41/1.06 a1 = a8]. % 0.41/1.06 [272=param(15,271),[265,263,268,269,264,267,266,269,270,265,268,264,267,266,263,14], % 0.41/1.06 thmtrue = thmfalse]. % 0.41/1.06 % SZS output end CNFRefutation % 0.41/1.06 Space: 93 KB %------------------------------------------------------------------------------