%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : TOP051-1 : TPTP v8.1.0. Released v8.1.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n024.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.05s % Output : CNFRefutation 0.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : TOP051-1 : TPTP v8.1.0. Released v8.1.0. % 0.11/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n024.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:22:36 EDT 2022 % 0.12/0.33 % CPUTime : % 0.42/1.05 Theorem Proved. % 0.42/1.05 % SZS status Unsatisfiable % 0.42/1.05 % SZS output start CNFRefutation % 0.42/1.05 [1=axiom,[], % 0.42/1.05 product(a10,a5) = a11]. % 0.42/1.05 [2=axiom,[], % 0.42/1.05 product(a9,a4) = a10]. % 0.42/1.05 [3=axiom,[], % 0.42/1.05 product(a8,a6) = a9]. % 0.42/1.05 [4=axiom,[], % 0.42/1.05 product(a7,a3) = a8]. % 0.42/1.05 [5=axiom,[], % 0.42/1.05 product(a6,a2) = a7]. % 0.42/1.05 [6=axiom,[], % 0.42/1.05 product(a5,a9) = a6]. % 0.42/1.05 [7=axiom,[], % 0.42/1.05 product(a4,a10) = a5]. % 0.42/1.05 [8=axiom,[], % 0.42/1.05 product(a3,a1) = a4]. % 0.42/1.05 [9=axiom,[], % 0.42/1.05 product(a2,a7) = a3]. % 0.42/1.05 [10=axiom,[], % 0.42/1.05 product(a1,a6) = a2]. % 0.42/1.05 [11=axiom,[], % 0.42/1.05 product(product(X10,X11),X12) = product(product(X10,X12),product(X11,X12))]. % 0.42/1.05 [12=axiom,[], % 0.42/1.05 product(product(X10,X11),X11) = X10]. % 0.42/1.05 [13=axiom,[], % 0.42/1.05 product(X10,X10) = X10]. % 0.42/1.05 [14=axiom,[], % 0.42/1.05 thtop(X10,X10) = thmfalse]. % 0.42/1.05 [15=axiom,[], % 0.42/1.05 thtop(tuple(a1,a6,a5,a2,a7,a3,a4,a9,a10,a8),tuple(a2,a7,a6,a3,a8,a4,a5,a10,a11,a9)) = thmtrue]. % 0.42/1.05 [16=param(12,1),[], % 0.42/1.05 product(a11,a5) = a10]. % 0.42/1.05 [17=param(12,2),[], % 0.42/1.05 product(a10,a4) = a9]. % 0.42/1.05 [18=param(12,3),[], % 0.42/1.05 product(a9,a6) = a8]. % 0.42/1.05 [19=param(12,4),[], % 0.42/1.05 product(a8,a3) = a7]. % 0.42/1.05 [20=param(12,5),[], % 0.42/1.05 product(a7,a2) = a6]. % 0.42/1.05 [22=param(12,7),[], % 0.42/1.05 product(a5,a10) = a4]. % 0.42/1.05 [23=param(12,8),[], % 0.42/1.05 product(a4,a1) = a3]. % 0.42/1.05 [24=param(12,9),[], % 0.42/1.05 product(a3,a7) = a2]. % 0.42/1.05 [25=param(12,10),[], % 0.42/1.05 product(a2,a6) = a1]. % 0.42/1.05 [26=param(11,1),[], % 0.42/1.05 product(product(a10,X10),product(a5,X10)) = product(a11,X10)]. % 0.42/1.05 [27=param(11,2),[], % 0.42/1.05 product(product(a9,X10),product(a4,X10)) = product(a10,X10)]. % 0.42/1.05 [28=param(11,3),[], % 0.42/1.05 product(product(a8,X10),product(a6,X10)) = product(a9,X10)]. % 0.42/1.05 [29=param(11,4),[], % 0.42/1.05 product(product(a7,X10),product(a3,X10)) = product(a8,X10)]. % 0.42/1.05 [30=param(11,5),[], % 0.42/1.05 product(product(a6,X10),product(a2,X10)) = product(a7,X10)]. % 0.42/1.05 [32=param(11,7),[], % 0.42/1.05 product(product(a4,X10),product(a10,X10)) = product(a5,X10)]. % 0.42/1.05 [33=param(11,8),[], % 0.42/1.05 product(product(a3,X10),product(a1,X10)) = product(a4,X10)]. % 0.42/1.05 [34=param(11,9),[], % 0.42/1.05 product(product(a2,X10),product(a7,X10)) = product(a3,X10)]. % 0.42/1.05 [35=param(11,10),[], % 0.42/1.05 product(product(a1,X10),product(a6,X10)) = product(a2,X10)]. % 0.42/1.05 [36=param(11,12),[], % 0.42/1.05 product(product(product(X10,X12),X11),product(X12,X11)) = product(X10,X11)]. % 0.42/1.05 [42=param(11,4),[], % 0.42/1.05 product(product(a7,X10),a3) = product(a8,product(X10,a3))]. % 0.42/1.05 [46=param(11,8),[], % 0.42/1.05 product(product(a3,X10),a1) = product(a4,product(X10,a1))]. % 0.42/1.05 [51=param(11,13),[], % 0.42/1.05 product(product(X10,X11),X10) = product(X10,product(X11,X10))]. % 0.42/1.05 [54=param(11,25),[], % 0.42/1.05 product(product(X10,a6),a1) = product(product(X10,a2),a6)]. % 0.42/1.05 [56=param(11,24),[], % 0.42/1.05 product(product(a3,X10),a7) = product(a2,product(X10,a7))]. % 0.42/1.05 [57=param(11,24),[], % 0.42/1.05 product(product(X10,a7),a2) = product(product(X10,a3),a7)]. % 0.42/1.05 [58=param(11,16),[], % 0.42/1.05 product(product(a11,X10),product(a5,X10)) = product(a10,X10)]. % 0.42/1.05 [74=param(11,20),[57], % 0.42/1.05 product(product(X10,a2),a6) = product(product(X10,a3),a7)]. % 0.42/1.05 [75=demod(54),[74], % 0.42/1.05 product(product(X10,a6),a1) = product(product(X10,a3),a7)]. % 0.42/1.05 [76=param(11,18),[], % 0.42/1.05 product(product(a9,X10),product(a6,X10)) = product(a8,X10)]. % 0.42/1.05 [81=param(11,19),[], % 0.42/1.05 product(product(X10,a3),a7) = product(product(X10,a8),a3)]. % 0.42/1.05 [82=demod(75),[81], % 0.42/1.05 product(product(X10,a6),a1) = product(product(X10,a8),a3)]. % 0.42/1.05 [84=demod(57),[81], % 0.42/1.05 product(product(X10,a7),a2) = product(product(X10,a8),a3)]. % 0.42/1.05 [88=param(84,13),[20,42,19], % 0.42/1.05 product(a8,a7) = a6]. % 0.42/1.05 [92=param(26,17),[], % 0.42/1.05 product(a9,product(a5,a4)) = product(a11,a4)]. % 0.42/1.05 [100=param(27,13),[], % 0.42/1.05 product(a9,product(a4,a9)) = product(a10,a9)]. % 0.42/1.05 [103=param(11,88),[], % 0.42/1.05 product(product(a8,X10),a7) = product(a6,product(X10,a7))]. % 0.42/1.05 [104=param(11,88),[], % 0.42/1.05 product(product(X10,a7),a6) = product(product(X10,a8),a7)]. % 0.42/1.05 [105=param(12,88),[], % 0.42/1.05 product(a6,a7) = a8]. % 0.42/1.05 [109=param(28,5),[103,9], % 0.42/1.05 product(a6,a3) = product(a9,a2)]. % 0.42/1.05 [124=param(29,20),[], % 0.42/1.05 product(a6,product(a3,a2)) = product(a8,a2)]. % 0.42/1.05 [129=param(30,13),[25], % 0.42/1.05 product(a6,a1) = product(a7,a6)]. % 0.42/1.05 [136=param(11,129),[82], % 0.42/1.05 product(product(X10,a1),product(a7,a6)) = product(product(X10,a8),a3)]. % 0.42/1.05 [137=param(28,129),[136,13,19], % 0.42/1.05 product(a9,a1) = a7]. % 0.42/1.05 [141=param(11,137),[11], % 0.42/1.05 product(product(X10,a7),product(a1,a7)) = product(product(X10,a9),a1)]. % 0.42/1.05 [144=param(27,137),[23,4], % 0.42/1.05 product(a10,a1) = a8]. % 0.42/1.05 [152=param(12,144),[], % 0.42/1.05 product(a8,a1) = a10]. % 0.42/1.05 [158=param(28,152),[129,137], % 0.42/1.05 product(a10,product(a7,a6)) = a7]. % 0.42/1.05 [159=param(32,1),[11,13], % 0.42/1.05 product(product(a4,a11),product(a5,a11)) = a5]. % 0.42/1.05 [160=param(32,13),[17], % 0.42/1.05 product(a4,a9) = product(a5,a4)]. % 0.42/1.05 [161=demod(100),[160,92], % 0.42/1.05 product(a10,a9) = product(a11,a4)]. % 0.42/1.05 [164=param(32,23),[144], % 0.42/1.05 product(a3,a8) = product(a5,a1)]. % 0.42/1.05 [173=param(33,10),[11,5,56,9], % 0.42/1.05 product(a2,a3) = product(a4,a6)]. % 0.42/1.05 [182=param(12,173),[11,109], % 0.42/1.05 product(product(a4,a3),product(a9,a2)) = a2]. % 0.42/1.05 [188=param(34,13),[20,25], % 0.42/1.05 product(a3,a2) = a1]. % 0.42/1.05 [194=demod(124),[188,129], % 0.42/1.05 product(a7,a6) = product(a8,a2)]. % 0.42/1.05 [195=demod(158),[194], % 0.42/1.05 product(a10,product(a8,a2)) = a7]. % 0.42/1.05 [197=demod(129),[194], % 0.42/1.05 product(a6,a1) = product(a8,a2)]. % 0.42/1.05 [198=param(34,25),[194], % 0.42/1.05 product(a1,product(a8,a2)) = product(a3,a6)]. % 0.42/1.05 [203=param(12,188),[], % 0.42/1.05 product(a1,a2) = a3]. % 0.42/1.05 [209=param(35,13),[197,198], % 0.42/1.05 product(a2,a1) = product(a3,a6)]. % 0.42/1.05 [211=param(35,105),[11,9], % 0.42/1.05 product(product(a1,a8),product(a7,a8)) = a3]. % 0.42/1.05 [218=param(12,209),[46,197], % 0.42/1.05 product(a4,product(a8,a2)) = a2]. % 0.42/1.05 [223=param(36,5),[11,5,11,9,11,4,11,164,11,11,141,6,197], % 0.42/1.05 product(product(product(X10,a8),a7),product(a8,a2)) = product(X10,a2)]. % 0.42/1.05 [225=param(36,7),[11,7,11,1,11,11,51,16,22], % 0.42/1.05 product(product(product(X10,a11),a5),a4) = product(X10,a10)]. % 0.42/1.05 [245=param(36,197),[82], % 0.42/1.05 product(product(product(X10,a8),a3),product(a8,a2)) = product(X10,a1)]. % 0.42/1.05 [249=param(36,194),[104,223], % 0.42/1.05 product(X10,a6) = product(X10,a2)]. % 0.42/1.05 [250=demod(3),[249], % 0.42/1.05 product(a8,a2) = a9]. % 0.42/1.05 [252=demod(245),[250,11], % 0.42/1.05 product(product(product(X10,a8),a9),product(a3,a9)) = product(X10,a1)]. % 0.42/1.05 [253=demod(223),[250,11], % 0.42/1.05 product(product(product(X10,a8),a9),product(a7,a9)) = product(X10,a2)]. % 0.42/1.05 [254=demod(218),[250,160], % 0.42/1.05 product(a5,a4) = a2]. % 0.42/1.05 [259=demod(92),[254], % 0.42/1.05 product(a9,a2) = product(a11,a4)]. % 0.42/1.05 [260=demod(182),[259], % 0.42/1.05 product(product(a4,a3),product(a11,a4)) = a2]. % 0.42/1.05 [265=demod(197),[250], % 0.42/1.05 product(a6,a1) = a9]. % 0.42/1.05 [268=demod(195),[250,161], % 0.42/1.05 product(a11,a4) = a7]. % 0.42/1.05 [273=demod(260),[268,81], % 0.42/1.05 product(product(a4,a8),a3) = a2]. % 0.42/1.05 [283=demod(10),[249,203], % 0.42/1.05 a2 = a3]. % 0.42/1.05 [284=demod(273),[283], % 0.42/1.05 product(product(a4,a8),a3) = a3]. % 0.42/1.05 [289=demod(254),[283], % 0.42/1.05 product(a5,a4) = a3]. % 0.42/1.05 [290=demod(253),[283], % 0.42/1.05 product(product(product(X10,a8),a9),product(a7,a9)) = product(X10,a3)]. % 0.42/1.05 [291=demod(250),[283,19], % 0.42/1.05 a7 = a9]. % 0.42/1.05 [292=demod(290),[291,13,12], % 0.42/1.05 product(X10,a3) = product(X10,a8)]. % 0.42/1.05 [294=demod(284),[292,12], % 0.42/1.05 a3 = a4]. % 0.42/1.05 [295=demod(292),[294], % 0.42/1.05 product(X10,a4) = product(X10,a8)]. % 0.42/1.05 [296=demod(2),[295], % 0.42/1.05 product(a9,a8) = a10]. % 0.42/1.05 [298=demod(17),[295], % 0.42/1.05 product(a10,a8) = a9]. % 0.42/1.05 [302=demod(225),[295,11], % 0.42/1.05 product(product(product(X10,a11),a8),product(a5,a8)) = product(X10,a10)]. % 0.42/1.05 [306=demod(289),[295,294], % 0.42/1.05 product(a5,a8) = a4]. % 0.42/1.05 [307=demod(302),[306,295,12], % 0.42/1.05 product(X10,a10) = product(X10,a11)]. % 0.42/1.05 [308=demod(7),[307], % 0.42/1.05 product(a4,a11) = a5]. % 0.42/1.05 [309=demod(159),[308], % 0.42/1.05 product(a5,product(a5,a11)) = a5]. % 0.42/1.05 [310=demod(22),[307], % 0.42/1.05 product(a5,a11) = a4]. % 0.42/1.05 [311=demod(309),[310,295,306], % 0.42/1.05 a4 = a5]. % 0.42/1.05 [312=demod(310),[311], % 0.42/1.05 product(a5,a11) = a5]. % 0.42/1.05 [315=demod(295),[311], % 0.42/1.05 product(X10,a5) = product(X10,a8)]. % 0.42/1.05 [316=demod(1),[315,298], % 0.42/1.05 a9 = a11]. % 0.42/1.05 [321=demod(296),[316], % 0.42/1.05 product(a11,a8) = a10]. % 0.42/1.05 [323=demod(291),[316], % 0.42/1.05 a7 = a11]. % 0.42/1.05 [326=demod(265),[316], % 0.42/1.05 product(a6,a1) = a11]. % 0.42/1.05 [330=demod(76),[316], % 0.42/1.05 product(product(a11,X10),product(a6,X10)) = product(a8,X10)]. % 0.42/1.05 [337=demod(6),[316,312], % 0.42/1.05 a6 = a5]. % 0.42/1.05 [341=demod(330),[337,58], % 0.42/1.05 product(a10,X10) = product(a8,X10)]. % 0.42/1.05 [342=demod(144),[341,152], % 0.42/1.05 a10 = a8]. % 0.42/1.05 [343=demod(321),[342], % 0.42/1.05 product(a11,a8) = a8]. % 0.42/1.05 [344=demod(307),[342], % 0.42/1.05 product(X10,a8) = product(X10,a11)]. % 0.42/1.05 [345=demod(315),[344], % 0.42/1.05 product(X10,a5) = product(X10,a11)]. % 0.42/1.05 [346=demod(343),[344,13], % 0.42/1.05 a8 = a11]. % 0.42/1.05 [347=demod(342),[346], % 0.42/1.05 a10 = a11]. % 0.42/1.05 [356=demod(326),[337], % 0.42/1.05 product(a5,a1) = a11]. % 0.42/1.05 [359=demod(294),[311], % 0.42/1.05 a3 = a5]. % 0.42/1.05 [362=demod(283),[359], % 0.42/1.05 a2 = a5]. % 0.42/1.05 [363=demod(252),[346,316,12,359,316,312,345], % 0.42/1.05 product(X10,a1) = product(X10,a11)]. % 0.42/1.05 [366=demod(356),[363,312], % 0.42/1.05 a5 = a11]. % 0.42/1.05 [367=demod(362),[366], % 0.42/1.05 a2 = a11]. % 0.42/1.05 [369=demod(359),[366], % 0.42/1.05 a3 = a11]. % 0.42/1.05 [370=demod(337),[366], % 0.42/1.05 a6 = a11]. % 0.42/1.05 [371=demod(311),[366], % 0.42/1.05 a4 = a11]. % 0.42/1.05 [373=demod(211),[346,323,346,13,12,369], % 0.42/1.05 a1 = a11]. % 0.42/1.05 [374=param(15,373),[370,366,367,323,369,371,316,347,346,367,323,370,369,346,371,366,347,316,14], % 0.42/1.05 thmtrue = thmfalse]. % 0.42/1.05 % SZS output end CNFRefutation % 0.42/1.05 Space: 140 KB %------------------------------------------------------------------------------