%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP688-1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n014.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:15:25 EDT 2022 % Result : Unsatisfiable 16.95s 17.31s % Output : CNFRefutation 16.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : GRP688-1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : fiesta-wrapper %s % 0.13/0.34 % Computer : n014.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 21:33:07 EDT 2022 % 0.13/0.35 % CPUTime : % 16.95/17.31 Theorem Proved. % 16.95/17.31 % SZS status Unsatisfiable % 16.95/17.31 % SZS output start CNFRefutation % 16.95/17.31 [1=axiom,[], % 16.95/17.31 mult(op_d,mult(op_d,op_d)) = unit]. % 16.95/17.31 [2=axiom,[], % 16.95/17.31 mult(op_c,mult(op_c,mult(op_c,op_c))) = unit]. % 16.95/17.31 [3=axiom,[], % 16.95/17.31 mult(i(X10),i(X11)) = i(mult(X10,X11))]. % 16.95/17.31 [4=axiom,[], % 16.95/17.31 mult(i(X10),mult(X10,X11)) = X11]. % 16.95/17.31 [5=axiom,[], % 16.95/17.31 mult(mult(X10,mult(X11,X10)),X12) = mult(X10,mult(X11,mult(X10,X12)))]. % 16.95/17.31 [6=axiom,[], % 16.95/17.31 mult(unit,X10) = X10]. % 16.95/17.31 [7=axiom,[], % 16.95/17.31 mult(X10,unit) = X10]. % 16.95/17.31 [8=axiom,[], % 16.95/17.31 rd(mult(X10,X11),X11) = X10]. % 16.95/17.31 [9=axiom,[], % 16.95/17.31 mult(rd(X10,X11),X11) = X10]. % 16.95/17.31 [10=axiom,[], % 16.95/17.31 ld(X10,mult(X10,X11)) = X11]. % 16.95/17.31 [12=axiom,[], % 16.95/17.31 thtop(X10,X10) = thmfalse]. % 16.95/17.31 [13=axiom,[], % 16.95/17.31 thtop(mult(op_c,op_d),mult(op_d,op_c)) = thmtrue]. % 16.95/17.31 [18=param(10,3),[], % 16.95/17.31 ld(i(X10),i(mult(X10,X11))) = i(X11)]. % 16.95/17.31 [21=param(4,1),[7], % 16.95/17.31 mult(op_d,op_d) = i(op_d)]. % 16.95/17.31 [24=param(4,2),[7], % 16.95/17.31 mult(op_c,mult(op_c,op_c)) = i(op_c)]. % 16.95/17.31 [29=param(4,7),[], % 16.95/17.31 mult(i(X10),X10) = unit]. % 16.95/17.31 [31=param(10,4),[], % 16.95/17.31 ld(i(X10),X11) = mult(X10,X11)]. % 16.95/17.31 [32=demod(18),[31], % 16.95/17.31 mult(X10,i(mult(X10,X11))) = i(X11)]. % 16.95/17.31 [37=param(5,9),[], % 16.95/17.31 mult(mult(X10,X11),X12) = mult(X10,mult(rd(X11,X10),mult(X10,X12)))]. % 16.95/17.31 [41=param(29,3),[29], % 16.95/17.31 i(unit) = unit]. % 16.95/17.31 [42=param(4,29),[7], % 16.95/17.31 i(i(X10)) = X10]. % 16.95/17.31 [43=param(8,3),[], % 16.95/17.31 rd(i(mult(X10,X11)),i(X11)) = i(X10)]. % 16.95/17.31 [44=param(8,4),[], % 16.95/17.31 rd(X10,mult(X11,X10)) = i(X11)]. % 16.95/17.31 [45=param(8,6),[], % 16.95/17.31 rd(X10,X10) = unit]. % 16.95/17.31 [46=param(8,21),[], % 16.95/17.31 rd(i(op_d),op_d) = op_d]. % 16.95/17.31 [49=param(3,42),[], % 16.95/17.31 mult(i(X10),X11) = i(mult(X10,i(X11)))]. % 16.95/17.31 [54=param(32,7),[41], % 16.95/17.31 mult(X10,i(X10)) = unit]. % 16.95/17.31 [56=param(32,9),[], % 16.95/17.31 mult(rd(X10,X11),i(X10)) = i(X11)]. % 16.95/17.31 [57=param(32,24),[42], % 16.95/17.31 i(mult(op_c,op_c)) = mult(op_c,op_c)]. % 16.95/17.31 [58=param(8,37),[], % 16.95/17.31 rd(mult(X10,mult(rd(X11,X10),mult(X10,X12))),X12) = mult(X10,X11)]. % 16.95/17.31 [59=param(37,21),[49,45,6], % 16.95/17.31 mult(op_d,mult(op_d,X10)) = i(mult(op_d,i(X10)))]. % 16.95/17.31 [60=param(37,24),[49,8], % 16.95/17.31 mult(op_c,mult(op_c,mult(op_c,X10))) = i(mult(op_c,i(X10)))]. % 16.95/17.31 [62=param(43,9),[], % 16.95/17.31 rd(i(X10),i(X11)) = i(rd(X10,X11))]. % 16.95/17.31 [63=param(8,49),[], % 16.95/17.31 rd(i(mult(X10,i(X11))),X11) = i(X10)]. % 16.95/17.31 [65=param(8,56),[62], % 16.95/17.31 i(rd(X10,X11)) = rd(X11,X10)]. % 16.95/17.31 [67=demod(63),[-65], % 16.95/17.31 i(rd(X10,i(mult(X11,i(X10))))) = i(X11)]. % 16.95/17.31 [68=demod(46),[-65], % 16.95/17.31 i(rd(op_d,i(op_d))) = op_d]. % 16.95/17.31 [69=demod(58),[-65], % 16.95/17.31 i(rd(X10,mult(X11,mult(rd(X12,X11),mult(X11,X10))))) = mult(X11,X12)]. % 16.95/17.31 [72=param(42,68),[], % 16.95/17.31 rd(op_d,i(op_d)) = i(op_d)]. % 16.95/17.31 [73=param(49,65),[], % 16.95/17.31 mult(rd(X10,X11),X12) = i(mult(rd(X11,X10),i(X12)))]. % 16.95/17.31 [75=param(56,65),[], % 16.95/17.31 mult(rd(rd(X10,X11),X12),rd(X11,X10)) = i(X12)]. % 16.95/17.31 [76=param(60,32),[42], % 16.95/17.31 mult(op_c,mult(op_c,i(X10))) = i(mult(op_c,mult(op_c,X10)))]. % 16.95/17.31 [78=param(62,42),[], % 16.95/17.31 rd(i(X10),X11) = i(rd(X10,i(X11)))]. % 16.95/17.31 [81=param(65,78),[42], % 16.95/17.31 rd(X10,i(X11)) = rd(X11,i(X10))]. % 16.95/17.31 [87=param(81,65),[], % 16.95/17.31 rd(X10,rd(X11,X12)) = rd(rd(X12,X11),i(X10))]. % 16.95/17.31 [88=param(42,67),[42], % 16.95/17.31 rd(X11,i(mult(X10,i(X11)))) = X10]. % 16.95/17.31 [91=param(69,21),[], % 16.95/17.31 i(rd(op_d,mult(op_d,mult(rd(X10,op_d),i(op_d))))) = mult(op_d,X10)]. % 16.95/17.31 [93=param(69,54),[7,78,42], % 16.95/17.31 rd(X10,i(mult(X10,rd(X11,X10)))) = mult(X10,X11)]. % 16.95/17.31 [94=param(93,45),[7], % 16.95/17.31 mult(X10,X10) = rd(X10,i(X10))]. % 16.95/17.31 [99=demod(57),[94,94], % 16.95/17.31 i(rd(op_c,i(op_c))) = rd(op_c,i(op_c))]. % 16.95/17.31 [102=param(93,65),[], % 16.95/17.31 rd(X10,i(mult(X10,i(rd(X10,X11))))) = mult(X10,X11)]. % 16.95/17.31 [104=param(32,94),[], % 16.95/17.31 mult(X10,i(rd(X10,i(X10)))) = i(X10)]. % 16.95/17.31 [105=param(37,94),[45,6], % 16.95/17.31 mult(rd(X10,i(X10)),X11) = mult(X10,mult(X10,X11))]. % 16.95/17.31 [106=param(88,94),[42,78,42], % 16.95/17.31 rd(X10,rd(X10,i(X10))) = i(X10)]. % 16.95/17.31 [110=param(73,42),[], % 16.95/17.31 i(mult(rd(X10,X11),X12)) = mult(rd(X11,X10),i(X12))]. % 16.95/17.31 [112=param(75,44),[49], % 16.95/17.31 i(mult(X10,i(rd(X11,X12)))) = i(mult(X10,rd(X12,X11)))]. % 16.95/17.31 [115=param(75,81),[42], % 16.95/17.31 mult(rd(X10,i(rd(X11,X12))),rd(X12,X11)) = X10]. % 16.95/17.31 [145=param(56,87),[42], % 16.95/17.31 mult(rd(X10,rd(X11,X12)),i(rd(X12,X11))) = X10]. % 16.95/17.31 [156=param(102,44),[42], % 16.95/17.31 mult(X10,mult(X11,X10)) = rd(X10,i(mult(X10,X11)))]. % 16.95/17.31 [157=param(102,88),[], % 16.95/17.31 mult(X10,i(mult(X11,i(X10)))) = rd(X10,i(mult(X10,i(X11))))]. % 16.95/17.31 [158=param(42,91),[], % 16.95/17.31 rd(op_d,mult(op_d,mult(rd(X10,op_d),i(op_d)))) = i(mult(op_d,X10))]. % 16.95/17.31 [159=param(32,156),[], % 16.95/17.31 mult(X10,i(rd(X10,i(mult(X10,X11))))) = i(mult(X11,X10))]. % 16.95/17.31 [160=param(32,157),[42], % 16.95/17.31 mult(X10,i(rd(X10,i(mult(X10,i(X11)))))) = mult(X11,i(X10))]. % 16.95/17.31 [161=demod(158),[-160,59,42], % 16.95/17.31 rd(op_d,i(mult(op_d,rd(op_d,i(mult(op_d,i(rd(X10,op_d)))))))) = i(mult(op_d,X10))]. % 16.95/17.31 [188=param(112,159),[42,78,81], % 16.95/17.31 mult(X10,X11) = i(mult(X11,i(rd(X11,i(mult(X11,X10))))))]. % 16.95/17.31 [191=param(32,159),[], % 16.95/17.31 mult(X10,mult(X11,i(rd(X11,i(mult(X11,X10)))))) = i(X11)]. % 16.95/17.31 [202=param(42,69),[], % 16.95/17.31 rd(X12,mult(X10,mult(rd(X11,X10),mult(X10,X12)))) = i(mult(X10,X11))]. % 16.95/17.31 [206=param(37,156),[-65,44,42], % 16.95/17.31 mult(rd(X10,i(mult(X10,X11))),X12) = mult(X10,mult(X11,mult(X10,X12)))]. % 16.95/17.31 [210=param(76,65),[], % 16.95/17.31 mult(op_c,mult(op_c,rd(X10,X11))) = i(mult(op_c,mult(op_c,rd(X11,X10))))]. % 16.95/17.31 [318=param(102,161),[42,59,42,32], % 16.95/17.31 i(rd(op_d,i(mult(op_d,i(rd(X10,op_d)))))) = rd(op_d,mult(op_d,i(X10)))]. % 16.95/17.31 [319=param(42,318),[], % 16.95/17.31 rd(op_d,i(mult(op_d,i(rd(X10,op_d))))) = i(rd(op_d,mult(op_d,i(X10))))]. % 16.95/17.31 [320=param(319,65),[], % 16.95/17.31 rd(op_d,i(mult(op_d,rd(op_d,X10)))) = i(rd(op_d,mult(op_d,i(X10))))]. % 16.95/17.31 [433=param(88,206),[], % 16.95/17.31 rd(X10,i(mult(X11,mult(X12,mult(X11,i(X10)))))) = rd(X11,i(mult(X11,X12)))]. % 16.95/17.31 [544=param(59,188),[], % 16.95/17.31 mult(op_d,i(mult(X10,i(rd(X10,i(mult(X10,op_d))))))) = i(mult(op_d,i(X10)))]. % 16.95/17.31 [545=param(73,188),[49,42,78,42,49,42], % 16.95/17.31 i(mult(X10,i(rd(X10,i(mult(X10,i(rd(X11,X12)))))))) = mult(rd(X12,X11),X10)]. % 16.95/17.31 [583=param(159,159),[], % 16.95/17.31 mult(X10,i(rd(X10,mult(X11,i(rd(X11,i(mult(X11,X10)))))))) = i(mult(X11,X10))]. % 16.95/17.31 [615=param(202,65),[49], % 16.95/17.31 rd(X10,mult(X11,i(mult(rd(X11,X12),i(mult(X11,X10)))))) = i(mult(X11,X12))]. % 16.95/17.31 [646=param(433,32),[], % 16.95/17.31 rd(mult(X10,X11),i(mult(X10,mult(X12,i(X11))))) = rd(X10,i(mult(X10,X12)))]. % 16.95/17.31 [647=param(433,42),[78,42], % 16.95/17.31 i(rd(X10,mult(X11,mult(X12,mult(X11,X10))))) = rd(X11,i(mult(X11,X12)))]. % 16.95/17.31 [650=param(42,647),[], % 16.95/17.31 rd(X12,mult(X10,mult(X11,mult(X10,X12)))) = i(rd(X10,i(mult(X10,X11))))]. % 16.95/17.31 [651=param(650,94),[], % 16.95/17.31 rd(X10,mult(X10,mult(X11,rd(X10,i(X10))))) = i(rd(X10,i(mult(X10,X11))))]. % 16.95/17.32 [652=param(651,115),[78,42], % 16.95/17.32 i(rd(X10,i(mult(X10,rd(X11,rd(X10,i(X10))))))) = rd(X10,mult(X10,X11))]. % 16.95/17.32 [653=param(646,32),[81], % 16.95/17.32 rd(mult(X10,i(X11)),i(mult(X10,mult(X12,X11)))) = rd(X10,i(mult(X10,X12)))]. % 16.95/17.32 [656=param(646,104),[81], % 16.95/17.32 rd(mult(X10,i(X11)),i(mult(X10,rd(X11,i(X11))))) = rd(X10,i(mult(X10,X11)))]. % 16.95/17.32 [670=param(42,652),[], % 16.95/17.32 rd(X10,i(mult(X10,rd(X11,rd(X10,i(X10)))))) = i(rd(X10,mult(X10,X11)))]. % 16.95/17.32 [678=param(191,670),[42], % 16.95/17.32 mult(rd(X10,rd(X11,i(X11))),mult(X11,rd(X11,mult(X11,X10)))) = i(X11)]. % 16.95/17.32 [685=param(88,544),[42], % 16.95/17.32 rd(mult(X10,i(rd(X10,i(mult(X10,op_d))))),mult(op_d,i(X10))) = op_d]. % 16.95/17.32 [686=param(685,99),[-545,78,99,99,42,583,78], % 16.95/17.32 i(rd(mult(op_d,rd(op_c,i(op_c))),i(mult(op_d,rd(op_c,i(op_c)))))) = op_d]. % 16.95/17.32 [715=param(110,678),[42], % 16.95/17.32 mult(rd(rd(X10,i(X10)),X11),i(mult(X10,rd(X10,mult(X10,X11))))) = X10]. % 16.95/17.32 [725=param(715,88),[], % 16.95/17.32 mult(X10,i(mult(X11,rd(X11,mult(X11,i(mult(X10,i(rd(X11,i(X11)))))))))) = X11]. % 16.95/17.32 [727=param(42,686),[], % 16.95/17.32 rd(mult(op_d,rd(op_c,i(op_c))),i(mult(op_d,rd(op_c,i(op_c))))) = i(op_d)]. % 16.95/17.32 [728=param(106,727),[81], % 16.95/17.32 rd(op_d,i(mult(op_d,rd(op_c,i(op_c))))) = i(mult(op_d,rd(op_c,i(op_c))))]. % 16.95/17.32 [729=param(102,728),[42,59,99,42,32,99], % 16.95/17.32 rd(op_d,mult(op_d,rd(op_c,i(op_c)))) = rd(op_c,i(op_c))]. % 16.95/17.32 [731=param(320,728),[32,99,99,42,59,99,728,42], % 16.95/17.32 mult(op_d,rd(op_c,i(op_c))) = rd(op_d,rd(op_c,i(op_c)))]. % 16.95/17.32 [733=demod(729),[731], % 16.95/17.32 rd(op_d,rd(op_d,rd(op_c,i(op_c)))) = rd(op_c,i(op_c))]. % 16.95/17.32 [737=param(59,731),[99,731], % 16.95/17.32 mult(op_d,rd(op_d,rd(op_c,i(op_c)))) = i(rd(op_d,rd(op_c,i(op_c))))]. % 16.95/17.32 [740=param(656,731),[81], % 16.95/17.32 rd(rd(op_d,rd(op_c,i(op_c))),i(mult(op_d,i(op_c)))) = rd(op_d,i(mult(op_d,op_c)))]. % 16.95/17.32 [742=param(145,733),[-65,42,105], % 16.95/17.32 mult(op_c,mult(op_c,rd(op_d,rd(op_c,i(op_c))))) = op_d]. % 16.95/17.32 [744=param(615,733),[105,76,42,737,42], % 16.95/17.32 rd(X10,mult(op_d,mult(op_c,mult(op_c,mult(op_d,X10))))) = rd(op_d,rd(op_c,i(op_c)))]. % 16.95/17.32 [747=param(653,742),[81,94,99,106], % 16.95/17.32 rd(op_d,i(mult(op_c,i(rd(op_d,rd(op_c,i(op_c))))))) = i(op_c)]. % 16.95/17.32 [754=param(102,747),[42], % 16.95/17.32 mult(op_d,i(mult(op_c,i(rd(op_d,rd(op_c,i(op_c))))))) = rd(op_d,i(mult(op_d,op_c)))]. % 16.95/17.32 [766=param(32,754),[42], % 16.95/17.32 mult(op_c,i(rd(op_d,rd(op_c,i(op_c))))) = mult(op_d,i(rd(op_d,i(mult(op_d,op_c)))))]. % 16.95/17.32 [1009=param(32,725),[42], % 16.95/17.32 mult(X11,rd(X11,mult(X11,i(mult(X10,i(rd(X11,i(X11)))))))) = mult(X10,i(X11))]. % 16.95/17.32 [1011=param(1009,99),[], % 16.95/17.32 mult(op_c,rd(op_c,mult(op_c,i(mult(X10,rd(op_c,i(op_c))))))) = mult(X10,i(op_c))]. % 16.95/17.32 [1013=param(1011,731),[766], % 16.95/17.32 mult(op_c,rd(op_c,mult(op_d,i(rd(op_d,i(mult(op_d,op_c))))))) = mult(op_d,i(op_c))]. % 16.95/17.32 [1016=param(210,1013),[-65,583], % 16.95/17.32 mult(op_c,mult(op_d,i(op_c))) = i(mult(op_c,i(mult(op_d,op_c))))]. % 16.95/17.32 [1017=param(433,1016),[], % 16.95/17.32 rd(op_c,i(mult(op_d,i(mult(op_c,i(mult(op_d,op_c))))))) = rd(op_d,i(mult(op_d,op_c)))]. % 16.95/17.32 [1018=param(744,1016),[32,42,59,78,42], % 16.95/17.32 i(rd(op_c,mult(op_d,i(op_c)))) = rd(op_d,rd(op_c,i(op_c)))]. % 16.95/17.32 [1020=param(42,1018),[], % 16.95/17.32 rd(op_c,mult(op_d,i(op_c))) = i(rd(op_d,rd(op_c,i(op_c))))]. % 16.95/17.32 [1021=param(615,1020),[49,42,42,650,670,188,42,1016,42], % 16.95/17.32 mult(op_c,i(mult(op_d,op_c))) = rd(op_c,i(mult(op_d,i(rd(op_d,i(mult(op_d,op_c)))))))]. % 16.95/17.32 [1022=demod(1017),[1021], % 16.95/17.32 rd(op_c,i(mult(op_d,i(rd(op_c,i(mult(op_d,i(rd(op_d,i(mult(op_d,op_c))))))))))) = rd(op_d,i(mult(op_d,op_c)))]. % 16.95/17.32 [1023=demod(1016),[1021], % 16.95/17.32 mult(op_c,mult(op_d,i(op_c))) = i(rd(op_c,i(mult(op_d,i(rd(op_d,i(mult(op_d,op_c))))))))]. % 16.95/17.32 [1025=param(32,1021),[42], % 16.95/17.32 mult(op_c,i(rd(op_c,i(mult(op_d,i(rd(op_d,i(mult(op_d,op_c))))))))) = mult(op_d,op_c)]. % 16.95/17.32 [1232=param(206,188),[42], % 16.95/17.32 mult(rd(X10,mult(X11,i(rd(X11,i(mult(X11,X10)))))),X12) = mult(X10,mult(X11,mult(X10,X12)))]. % 16.95/17.32 [1467=param(744,78),[], % 16.95/17.32 i(rd(X10,i(mult(op_d,mult(op_c,mult(op_c,mult(op_d,i(X10)))))))) = rd(op_d,rd(op_c,i(op_c)))]. % 16.95/17.32 [1817=param(206,1013),[88,1232], % 16.95/17.32 mult(op_c,mult(op_c,mult(op_d,mult(op_c,mult(op_c,X10))))) = mult(op_d,X10)]. % 16.95/17.32 [1824=param(1817,60),[32,42], % 16.95/17.32 mult(op_c,mult(op_c,mult(op_d,X10))) = mult(op_d,mult(op_c,mult(op_c,X10)))]. % 16.95/17.32 [1826=demod(1467),[1824,76,59,42,42], % 16.95/17.32 i(rd(X10,mult(op_d,mult(op_c,mult(op_c,X10))))) = rd(op_d,rd(op_c,i(op_c)))]. % 16.95/17.32 [1861=param(42,1826),[], % 16.95/17.32 rd(X10,mult(op_d,mult(op_c,mult(op_c,X10)))) = i(rd(op_d,rd(op_c,i(op_c))))]. % 16.95/17.32 [1880=param(1861,1023),[1025,59], % 16.95/17.32 rd(mult(op_d,i(op_c)),i(mult(op_d,i(op_c)))) = i(rd(op_d,rd(op_c,i(op_c))))]. % 16.95/17.32 [1885=param(106,1880),[81,740], % 16.95/17.32 i(mult(op_d,i(op_c))) = rd(op_d,i(mult(op_d,op_c)))]. % 16.95/17.32 [1899=param(42,1885),[], % 16.95/17.32 mult(op_d,i(op_c)) = i(rd(op_d,i(mult(op_d,op_c))))]. % 16.95/17.32 [1901=demod(1023),[1899], % 16.95/17.32 mult(op_c,i(rd(op_d,i(mult(op_d,op_c))))) = i(rd(op_c,i(mult(op_d,i(rd(op_d,i(mult(op_d,op_c))))))))]. % 16.95/17.32 [1906=param(59,1899),[42], % 16.95/17.32 mult(op_d,i(rd(op_d,i(mult(op_d,op_c))))) = i(mult(op_d,op_c))]. % 16.95/17.32 [1913=demod(1901),[1906,42,44,42], % 16.95/17.32 mult(op_c,i(rd(op_d,i(mult(op_d,op_c))))) = op_d]. % 16.95/17.32 [1918=demod(1022),[1906,42,44,42,94,72,42,-65], % 16.95/17.32 rd(op_d,i(mult(op_d,op_c))) = i(rd(op_d,op_c))]. % 16.95/17.32 [1922=demod(1913),[1918,42], % 16.95/17.32 mult(op_c,rd(op_d,op_c)) = op_d]. % 16.95/17.32 [1926=demod(1906),[1918,42], % 16.95/17.32 mult(op_d,rd(op_d,op_c)) = i(mult(op_d,op_c))]. % 16.95/17.32 [1960=param(93,1922),[81,188,1918,42,1926,42], % 16.95/17.32 mult(op_d,op_c) = rd(op_d,i(op_c))]. % 16.95/17.32 [1967=demod(1926),[1960], % 16.95/17.32 mult(op_d,rd(op_d,op_c)) = i(rd(op_d,i(op_c)))]. % 16.95/17.32 [1968=demod(1918),[1960], % 16.95/17.32 rd(op_d,i(rd(op_d,i(op_c)))) = i(rd(op_d,op_c))]. % 16.95/17.32 [1991=param(13,1960),[188,1960,1968,42,1967,42,12], % 16.95/17.32 thmtrue = thmfalse]. % 16.95/17.32 % SZS output end CNFRefutation % 16.95/17.32 Space: 72688 KB %------------------------------------------------------------------------------