%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : TOP053-1 : TPTP v8.1.0. Released v8.1.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n029.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.42s 1.06s % Output : CNFRefutation 0.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : TOP053-1 : TPTP v8.1.0. Released v8.1.0. % 0.12/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n029.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 14:30:58 EDT 2022 % 0.12/0.33 % CPUTime : % 0.42/1.06 Theorem Proved. % 0.42/1.06 % SZS status Unsatisfiable % 0.42/1.06 % SZS output start CNFRefutation % 0.42/1.06 [1=axiom,[], % 0.42/1.06 product(a11,a10) = a1]. % 0.42/1.06 [2=axiom,[], % 0.42/1.06 product(a4,a7) = a11]. % 0.42/1.06 [3=axiom,[], % 0.42/1.06 product(a15,a8) = a4]. % 0.42/1.06 [4=axiom,[], % 0.42/1.06 product(a14,a3) = a15]. % 0.42/1.06 [5=axiom,[], % 0.42/1.06 product(a2,a12) = a14]. % 0.42/1.06 [6=axiom,[], % 0.42/1.06 product(a6,a7) = a2]. % 0.42/1.06 [7=axiom,[], % 0.42/1.06 product(a13,a8) = a6]. % 0.42/1.06 [8=axiom,[], % 0.42/1.06 product(a12,a3) = a13]. % 0.42/1.06 [9=axiom,[], % 0.42/1.06 product(a10,a11) = a12]. % 0.42/1.06 [10=axiom,[], % 0.42/1.06 product(a9,a1) = a10]. % 0.42/1.06 [11=axiom,[], % 0.42/1.06 product(a8,a2) = a9]. % 0.42/1.06 [12=axiom,[], % 0.42/1.06 product(a7,a3) = a8]. % 0.42/1.06 [13=axiom,[], % 0.42/1.06 product(a5,a6) = a7]. % 0.42/1.06 [14=axiom,[], % 0.42/1.06 product(a3,a4) = a5]. % 0.42/1.06 [15=axiom,[], % 0.42/1.06 product(a1,a2) = a3]. % 0.42/1.06 [16=axiom,[], % 0.42/1.06 product(product(X10,X11),X12) = product(product(X10,X12),product(X11,X12))]. % 0.42/1.06 [17=axiom,[], % 0.42/1.06 product(product(X10,X11),X11) = X10]. % 0.42/1.06 [18=axiom,[], % 0.42/1.06 product(X10,X10) = X10]. % 0.42/1.06 [19=axiom,[], % 0.42/1.06 thtop(X10,X10) = thmfalse]. % 0.42/1.06 [20=axiom,[], % 0.42/1.06 thtop(tuple(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14),tuple(a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15)) = thmtrue]. % 0.42/1.06 [21=param(17,1),[], % 0.42/1.06 product(a1,a10) = a11]. % 0.42/1.06 [22=param(17,2),[], % 0.42/1.06 product(a11,a7) = a4]. % 0.42/1.06 [23=param(17,3),[], % 0.42/1.06 product(a4,a8) = a15]. % 0.42/1.06 [24=param(17,4),[], % 0.42/1.06 product(a15,a3) = a14]. % 0.42/1.06 [25=param(17,5),[], % 0.42/1.06 product(a14,a12) = a2]. % 0.42/1.06 [26=param(17,6),[], % 0.42/1.06 product(a2,a7) = a6]. % 0.42/1.06 [27=param(17,7),[], % 0.42/1.06 product(a6,a8) = a13]. % 0.42/1.06 [28=param(17,8),[], % 0.42/1.06 product(a13,a3) = a12]. % 0.42/1.06 [29=param(17,9),[], % 0.42/1.06 product(a12,a11) = a10]. % 0.42/1.06 [30=param(17,10),[], % 0.42/1.06 product(a10,a1) = a9]. % 0.42/1.06 [31=param(17,11),[], % 0.42/1.06 product(a9,a2) = a8]. % 0.42/1.06 [32=param(17,12),[], % 0.42/1.06 product(a8,a3) = a7]. % 0.42/1.06 [33=param(17,13),[], % 0.42/1.06 product(a7,a6) = a5]. % 0.42/1.06 [34=param(17,14),[], % 0.42/1.06 product(a5,a4) = a3]. % 0.42/1.06 [35=param(17,15),[], % 0.42/1.06 product(a3,a2) = a1]. % 0.42/1.06 [36=param(16,1),[], % 0.42/1.06 product(product(a11,X10),product(a10,X10)) = product(a1,X10)]. % 0.42/1.06 [37=param(16,2),[], % 0.42/1.06 product(product(a4,X10),product(a7,X10)) = product(a11,X10)]. % 0.42/1.06 [38=param(16,3),[], % 0.42/1.06 product(product(a15,X10),product(a8,X10)) = product(a4,X10)]. % 0.42/1.06 [39=param(16,4),[], % 0.42/1.06 product(product(a14,X10),product(a3,X10)) = product(a15,X10)]. % 0.42/1.06 [40=param(16,5),[], % 0.42/1.06 product(product(a2,X10),product(a12,X10)) = product(a14,X10)]. % 0.42/1.06 [41=param(16,6),[], % 0.42/1.06 product(product(a6,X10),product(a7,X10)) = product(a2,X10)]. % 0.42/1.06 [42=param(16,7),[], % 0.42/1.06 product(product(a13,X10),product(a8,X10)) = product(a6,X10)]. % 0.42/1.06 [43=param(16,8),[], % 0.42/1.06 product(product(a12,X10),product(a3,X10)) = product(a13,X10)]. % 0.42/1.06 [44=param(16,9),[], % 0.42/1.06 product(product(a10,X10),product(a11,X10)) = product(a12,X10)]. % 0.42/1.06 [45=param(16,10),[], % 0.42/1.06 product(product(a9,X10),product(a1,X10)) = product(a10,X10)]. % 0.42/1.06 [46=param(16,11),[], % 0.42/1.06 product(product(a8,X10),product(a2,X10)) = product(a9,X10)]. % 0.42/1.06 [47=param(16,12),[], % 0.42/1.06 product(product(a7,X10),product(a3,X10)) = product(a8,X10)]. % 0.42/1.06 [50=param(16,15),[], % 0.42/1.06 product(product(a1,X10),product(a2,X10)) = product(a3,X10)]. % 0.42/1.06 [63=param(16,7),[], % 0.42/1.06 product(product(X10,a8),a6) = product(product(X10,a13),a8)]. % 0.42/1.06 [70=param(16,11),[16], % 0.42/1.06 product(product(X10,a8),a2) = product(product(X10,a9),product(a2,a9))]. % 0.42/1.06 [79=param(16,35),[], % 0.42/1.06 product(product(X10,a2),a1) = product(product(X10,a3),a2)]. % 0.42/1.06 [86=param(16,21),[], % 0.42/1.06 product(product(a1,X10),product(a10,X10)) = product(a11,X10)]. % 0.42/1.06 [93=param(16,31),[16], % 0.42/1.06 product(product(X10,a8),product(a2,a8)) = product(product(X10,a9),a2)]. % 0.42/1.06 [95=param(16,22),[], % 0.42/1.06 product(product(a11,X10),a7) = product(a4,product(X10,a7))]. % 0.42/1.06 [100=param(16,29),[], % 0.42/1.06 product(product(a12,X10),product(a11,X10)) = product(a10,X10)]. % 0.42/1.06 [105=param(16,23),[], % 0.42/1.06 product(product(a4,X10),product(a8,X10)) = product(a15,X10)]. % 0.42/1.06 [106=param(16,23),[], % 0.42/1.06 product(product(a4,X10),a8) = product(a15,product(X10,a8))]. % 0.42/1.06 [114=param(16,24),[16], % 0.42/1.06 product(product(X10,a14),product(a3,a14)) = product(product(X10,a15),a3)]. % 0.42/1.06 [126=param(37,12),[106], % 0.42/1.06 product(a15,product(a3,a8)) = product(a11,a3)]. % 0.42/1.06 [132=param(38,11),[16], % 0.42/1.06 product(product(a15,a9),product(a2,a9)) = product(a4,a2)]. % 0.42/1.06 [134=param(38,24),[32], % 0.42/1.06 product(a4,a3) = product(a14,a7)]. % 0.42/1.06 [143=param(39,14),[16], % 0.42/1.06 product(product(a14,a5),product(a4,a5)) = product(a15,a4)]. % 0.42/1.06 [145=param(39,25),[], % 0.42/1.06 product(a2,product(a3,a12)) = product(a15,a12)]. % 0.42/1.06 [150=param(40,18),[], % 0.42/1.06 product(a2,product(a12,a2)) = product(a14,a2)]. % 0.42/1.06 [151=param(40,26),[], % 0.42/1.06 product(a6,product(a12,a7)) = product(a14,a7)]. % 0.42/1.06 [152=param(40,145),[], % 0.42/1.06 product(product(a15,a12),product(a12,product(a3,a12))) = product(a14,product(a3,a12))]. % 0.42/1.06 [154=param(16,150),[], % 0.42/1.06 product(product(a2,X10),product(product(a12,a2),X10)) = product(product(a14,a2),X10)]. % 0.42/1.06 [155=param(40,150),[], % 0.42/1.06 product(product(a14,a2),product(a12,product(a12,a2))) = product(a14,product(a12,a2))]. % 0.42/1.06 [158=param(41,27),[], % 0.42/1.06 product(a2,a8) = product(a13,product(a7,a8))]. % 0.42/1.06 [159=demod(93),[158], % 0.42/1.06 product(product(X10,a8),product(a13,product(a7,a8))) = product(product(X10,a9),a2)]. % 0.42/1.06 [166=param(40,158),[16,-16], % 0.42/1.06 product(product(a13,product(a12,a8)),product(product(a7,a12),a8)) = product(a14,a8)]. % 0.42/1.06 [169=param(42,28),[32], % 0.42/1.06 product(a6,a3) = product(a12,a7)]. % 0.42/1.06 [172=param(16,169),[], % 0.42/1.06 product(product(X10,a3),product(a12,a7)) = product(product(X10,a6),a3)]. % 0.42/1.06 [178=param(43,18),[], % 0.42/1.06 product(a12,product(a3,a12)) = product(a13,a12)]. % 0.42/1.06 [179=demod(152),[178,-16], % 0.42/1.06 product(product(a15,a13),a12) = product(a14,product(a3,a12))]. % 0.42/1.06 [190=param(44,1),[18,30], % 0.42/1.06 product(a12,a10) = a9]. % 0.42/1.06 [195=param(17,190),[], % 0.42/1.06 product(a9,a10) = a12]. % 0.42/1.06 [196=param(43,190),[], % 0.42/1.06 product(a9,product(a3,a10)) = product(a13,a10)]. % 0.42/1.06 [199=param(45,15),[31,32], % 0.42/1.06 product(a10,a2) = a7]. % 0.42/1.06 [207=param(17,199),[], % 0.42/1.06 product(a7,a2) = a10]. % 0.42/1.06 [208=param(36,199),[95,26,15], % 0.42/1.06 product(a4,a6) = a3]. % 0.42/1.06 [209=param(44,199),[], % 0.42/1.06 product(a7,product(a11,a2)) = product(a12,a2)]. % 0.42/1.06 [212=param(17,208),[], % 0.42/1.06 product(a3,a6) = a4]. % 0.42/1.06 [222=param(16,207),[], % 0.42/1.06 product(product(a7,X10),product(a2,X10)) = product(a10,X10)]. % 0.42/1.06 [225=param(37,207),[16], % 0.42/1.06 product(product(a4,a10),product(a2,a10)) = product(a11,a2)]. % 0.42/1.06 [226=param(41,207),[16,18], % 0.42/1.06 product(product(a6,a10),product(a2,a10)) = a2]. % 0.42/1.06 [227=param(47,14),[16], % 0.42/1.06 product(product(a7,a5),product(a4,a5)) = product(a8,a4)]. % 0.42/1.06 [229=param(47,33),[212,34], % 0.42/1.06 product(a8,a6) = a3]. % 0.42/1.06 [233=param(16,229),[63], % 0.42/1.06 product(product(X10,a6),a3) = product(product(X10,a13),a8)]. % 0.42/1.06 [234=demod(172),[233], % 0.42/1.06 product(product(X10,a3),product(a12,a7)) = product(product(X10,a13),a8)]. % 0.42/1.06 [235=param(17,229),[212], % 0.42/1.06 a4 = a8]. % 0.42/1.06 [236=demod(227),[235,-16,235,18], % 0.42/1.06 product(product(a7,a8),a5) = a8]. % 0.42/1.06 [237=demod(225),[235,46,195], % 0.42/1.06 product(a11,a2) = a12]. % 0.42/1.06 [238=demod(209),[237], % 0.42/1.06 product(a7,a12) = product(a12,a2)]. % 0.42/1.06 [239=demod(166),[238,16,158,159], % 0.42/1.06 product(product(a13,product(a12,a8)),product(product(a12,a9),a2)) = product(a14,a8)]. % 0.42/1.06 [247=demod(143),[235,-16,235], % 0.42/1.06 product(product(a14,a8),a5) = product(a15,a8)]. % 0.42/1.06 [256=demod(134),[235,32], % 0.42/1.06 product(a14,a7) = a7]. % 0.42/1.06 [258=demod(151),[256], % 0.42/1.06 product(a6,product(a12,a7)) = a7]. % 0.42/1.06 [261=demod(132),[235,11], % 0.42/1.06 product(product(a15,a9),product(a2,a9)) = a9]. % 0.42/1.06 [269=demod(105),[235,18], % 0.42/1.06 product(a8,X10) = product(a15,X10)]. % 0.42/1.06 [271=demod(32),[269,24], % 0.42/1.06 a7 = a14]. % 0.42/1.06 [273=demod(258),[271,271], % 0.42/1.06 product(a6,product(a12,a14)) = a14]. % 0.42/1.06 [276=demod(238),[271,25], % 0.42/1.06 product(a12,a2) = a2]. % 0.42/1.06 [277=demod(155),[276,276,17,276], % 0.42/1.06 product(a14,a2) = a14]. % 0.42/1.06 [278=demod(154),[276,18,277], % 0.42/1.06 product(a2,X10) = product(a14,X10)]. % 0.42/1.06 [279=demod(226),[278,-16], % 0.42/1.06 product(product(a6,a14),a10) = a2]. % 0.42/1.06 [281=demod(5),[278,25], % 0.42/1.06 a2 = a14]. % 0.42/1.06 [282=demod(279),[281], % 0.42/1.06 product(product(a6,a14),a10) = a14]. % 0.42/1.06 [283=demod(276),[281,281], % 0.42/1.06 product(a12,a14) = a14]. % 0.42/1.06 [285=demod(273),[283], % 0.42/1.06 product(a6,a14) = a14]. % 0.42/1.06 [286=demod(282),[285], % 0.42/1.06 product(a14,a10) = a14]. % 0.42/1.06 [287=demod(239),[281,16,283], % 0.42/1.06 product(product(a13,product(a12,a8)),product(a14,product(a9,a14))) = product(a14,a8)]. % 0.42/1.06 [288=demod(237),[281], % 0.42/1.06 product(a11,a14) = a12]. % 0.42/1.06 [291=demod(79),[281,281,16,114], % 0.42/1.06 product(product(X10,a14),a1) = product(product(X10,a15),a3)]. % 0.42/1.06 [294=demod(35),[281], % 0.42/1.06 product(a3,a14) = a1]. % 0.42/1.06 [298=demod(31),[281], % 0.42/1.06 product(a9,a14) = a8]. % 0.42/1.06 [299=demod(287),[298,16,-16,283,17], % 0.42/1.06 product(a14,a8) = a13]. % 0.42/1.06 [301=demod(247),[299], % 0.42/1.06 product(a13,a5) = product(a15,a8)]. % 0.42/1.06 [303=demod(15),[281], % 0.42/1.06 product(a1,a14) = a3]. % 0.42/1.06 [310=demod(50),[281], % 0.42/1.06 product(product(a1,X10),product(a14,X10)) = product(a3,X10)]. % 0.42/1.06 [311=demod(145),[281], % 0.42/1.06 product(a14,product(a3,a12)) = product(a15,a12)]. % 0.42/1.06 [312=demod(179),[311], % 0.42/1.06 product(product(a15,a13),a12) = product(a15,a12)]. % 0.42/1.06 [313=demod(261),[281,-16], % 0.42/1.06 product(product(a15,a14),a9) = a9]. % 0.42/1.06 [315=demod(70),[281,16,269,-16,281,-16], % 0.42/1.06 product(product(X10,a14),a9) = product(product(X10,a15),a14)]. % 0.42/1.06 [316=demod(313),[315,18], % 0.42/1.06 product(a15,a14) = a9]. % 0.42/1.06 [321=demod(236),[271,299,301], % 0.42/1.06 product(a15,a8) = a8]. % 0.42/1.06 [323=demod(234),[271,283,16,294,291], % 0.42/1.06 product(product(X10,a13),a8) = product(product(X10,a15),a3)]. % 0.42/1.06 [329=demod(222),[271,281,18], % 0.42/1.06 product(a10,X10) = product(a14,X10)]. % 0.42/1.06 [333=demod(100),[329], % 0.42/1.06 product(product(a12,X10),product(a11,X10)) = product(a14,X10)]. % 0.42/1.06 [335=demod(86),[329,310], % 0.42/1.06 product(a3,X10) = product(a11,X10)]. % 0.42/1.06 [336=demod(196),[335,1,10], % 0.42/1.06 product(a13,a10) = a10]. % 0.42/1.06 [338=demod(126),[335], % 0.42/1.06 product(a11,a3) = product(a15,product(a11,a8))]. % 0.42/1.06 [352=demod(43),[335,333], % 0.42/1.06 product(a13,X10) = product(a14,X10)]. % 0.42/1.06 [353=demod(336),[352,286], % 0.42/1.06 a10 = a14]. % 0.42/1.06 [355=demod(195),[353,298], % 0.42/1.06 a8 = a12]. % 0.42/1.06 [357=demod(338),[355], % 0.42/1.06 product(a11,a3) = product(a15,product(a11,a12))]. % 0.42/1.06 [359=demod(323),[355], % 0.42/1.06 product(product(X10,a13),a12) = product(product(X10,a15),a3)]. % 0.42/1.06 [360=demod(312),[359,18,24], % 0.42/1.06 product(a15,a12) = a14]. % 0.42/1.06 [363=demod(321),[355,360,355], % 0.42/1.06 a12 = a14]. % 0.42/1.06 [366=demod(360),[363,316], % 0.42/1.06 a9 = a14]. % 0.42/1.06 [372=demod(316),[366], % 0.42/1.06 product(a15,a14) = a14]. % 0.42/1.06 [379=demod(357),[363], % 0.42/1.06 product(a11,a3) = product(a15,product(a11,a14))]. % 0.42/1.06 [381=demod(355),[363], % 0.42/1.06 a8 = a14]. % 0.42/1.06 [387=demod(288),[363], % 0.42/1.06 product(a11,a14) = a14]. % 0.42/1.06 [388=demod(379),[387,372], % 0.42/1.06 product(a11,a3) = a14]. % 0.42/1.06 [393=demod(8),[363,4], % 0.42/1.06 a13 = a15]. % 0.42/1.06 [394=demod(352),[393], % 0.42/1.06 product(a14,X10) = product(a15,X10)]. % 0.42/1.06 [395=demod(4),[394,24], % 0.42/1.06 a14 = a15]. % 0.42/1.06 [398=demod(388),[395], % 0.42/1.06 product(a11,a3) = a15]. % 0.42/1.06 [401=demod(381),[395], % 0.42/1.06 a8 = a15]. % 0.42/1.06 [405=demod(366),[395], % 0.42/1.06 a9 = a15]. % 0.42/1.06 [406=demod(363),[395], % 0.42/1.06 a12 = a15]. % 0.42/1.06 [407=demod(353),[395], % 0.42/1.06 a10 = a15]. % 0.42/1.06 [409=demod(303),[395], % 0.42/1.06 product(a1,a15) = a3]. % 0.42/1.06 [411=demod(281),[395], % 0.42/1.06 a2 = a15]. % 0.42/1.06 [412=demod(271),[395], % 0.42/1.06 a7 = a15]. % 0.42/1.06 [428=demod(235),[401], % 0.42/1.06 a4 = a15]. % 0.42/1.06 [430=demod(21),[407,409], % 0.42/1.06 a3 = a11]. % 0.42/1.06 [433=demod(398),[430,18], % 0.42/1.06 a11 = a15]. % 0.42/1.06 [435=demod(430),[433], % 0.42/1.06 a3 = a15]. % 0.42/1.06 [441=demod(1),[433,407,18], % 0.42/1.06 a1 = a15]. % 0.42/1.06 [442=demod(7),[393,401,18], % 0.42/1.06 a6 = a15]. % 0.42/1.06 [447=demod(33),[412,442,18], % 0.42/1.06 a5 = a15]. % 0.42/1.06 [448=param(20,447),[441,411,435,428,442,412,401,405,407,433,406,393,395,411,435,428,447,442,412,401,405,407,433,406,393,395,19], % 0.42/1.06 thmtrue = thmfalse]. % 0.42/1.06 % SZS output end CNFRefutation % 0.42/1.06 Space: 151 KB %------------------------------------------------------------------------------