%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP709-1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n013.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:31 EDT 2022 % Result : Unsatisfiable 160.12s 160.61s % Output : CNFRefutation 160.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : GRP709-1 : TPTP v8.1.0. Released v4.0.0. % 0.08/0.13 % Command : fiesta-wrapper %s % 0.13/0.35 % Computer : n013.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon Jun 13 23:09:14 EDT 2022 % 0.13/0.35 % CPUTime : % 160.12/160.61 Theorem Proved. % 160.12/160.61 % SZS status Unsatisfiable % 160.12/160.61 % SZS output start CNFRefutation % 160.12/160.61 [1=axiom,[], % 160.12/160.61 mult(mult(X10,X11),op_c) = mult(X10,mult(X11,op_c))]. % 160.12/160.61 [2=axiom,[], % 160.12/160.61 mult(op_c,X10) = mult(X10,op_c)]. % 160.12/160.61 [3=demod(1),[-2], % 160.12/160.61 mult(op_c,mult(X10,X11)) = mult(X10,mult(X11,op_c))]. % 160.12/160.61 [4=axiom,[], % 160.12/160.61 mult(mult(X10,mult(X11,X10)),X12) = mult(X10,mult(X11,mult(X10,X12)))]. % 160.12/160.61 [5=axiom,[], % 160.12/160.61 mult(unit,X10) = X10]. % 160.12/160.61 [6=axiom,[], % 160.12/160.61 mult(X10,unit) = X10]. % 160.12/160.61 [7=axiom,[], % 160.12/160.61 rd(mult(X10,X11),X11) = X10]. % 160.12/160.61 [8=axiom,[], % 160.12/160.61 mult(rd(X10,X11),X11) = X10]. % 160.12/160.61 [9=axiom,[], % 160.12/160.61 ld(X10,mult(X10,X11)) = X11]. % 160.12/160.61 [10=axiom,[], % 160.12/160.61 mult(X10,ld(X10,X11)) = X11]. % 160.12/160.61 [11=axiom,[], % 160.12/160.61 thtop(X10,X10) = thmfalse]. % 160.12/160.61 [12=axiom,[], % 160.12/160.61 thtop(mult(mult(op_c,op_c),mult(a,b)),mult(mult(mult(op_c,op_c),a),b)) = thmtrue]. % 160.12/160.61 [14=param(9,2),[], % 160.12/160.61 ld(op_c,mult(X10,op_c)) = X10]. % 160.12/160.61 [16=param(9,6),[], % 160.12/160.61 ld(X10,X10) = unit]. % 160.12/160.61 [21=param(3,10),[-2], % 160.12/160.61 mult(X11,mult(op_c,ld(X11,X10))) = mult(op_c,X10)]. % 160.12/160.61 [22=param(3,2),[], % 160.12/160.61 mult(X10,mult(op_c,X11)) = mult(op_c,mult(X10,X11))]. % 160.12/160.61 [32=param(9,4),[], % 160.12/160.61 ld(mult(X10,mult(X11,X10)),mult(X10,mult(X11,mult(X10,X12)))) = X12]. % 160.12/160.61 [39=param(7,4),[], % 160.12/160.61 rd(mult(X10,mult(X11,mult(X10,X12))),X12) = mult(X10,mult(X11,X10))]. % 160.12/160.61 [40=param(7,5),[], % 160.12/160.61 rd(X10,X10) = unit]. % 160.12/160.61 [41=param(7,6),[], % 160.12/160.61 rd(X10,unit) = X10]. % 160.12/160.61 [42=param(7,10),[], % 160.12/160.61 rd(X10,ld(X11,X10)) = X11]. % 160.12/160.61 [43=param(8,2),[], % 160.12/160.61 mult(op_c,rd(X10,op_c)) = X10]. % 160.12/160.61 [45=param(3,8),[], % 160.12/160.61 mult(op_c,mult(X10,rd(X11,op_c))) = mult(X10,X11)]. % 160.12/160.61 [46=param(4,8),[], % 160.12/160.61 mult(mult(X10,X11),X12) = mult(X10,mult(rd(X11,X10),mult(X10,X12)))]. % 160.12/160.61 [48=param(9,8),[], % 160.12/160.61 ld(rd(X10,X11),X10) = X11]. % 160.12/160.61 [49=param(14,8),[], % 160.12/160.61 ld(op_c,X10) = rd(X10,op_c)]. % 160.12/160.61 [58=param(7,43),[], % 160.12/160.61 rd(X10,rd(X10,op_c)) = op_c]. % 160.12/160.61 [79=param(9,21),[], % 160.12/160.61 ld(X10,mult(op_c,X11)) = mult(op_c,ld(X10,X11))]. % 160.12/160.61 [87=param(79,6),[], % 160.12/160.61 mult(op_c,ld(X10,unit)) = ld(X10,op_c)]. % 160.12/160.61 [88=param(79,10),[49], % 160.12/160.61 mult(op_c,ld(X10,rd(X11,op_c))) = ld(X10,X11)]. % 160.12/160.61 [89=param(79,16),[], % 160.12/160.61 mult(op_c,ld(mult(op_c,X10),X10)) = unit]. % 160.12/160.61 [92=param(9,87),[49], % 160.12/160.61 ld(X10,unit) = rd(ld(X10,op_c),op_c)]. % 160.12/160.61 [104=param(10,92),[], % 160.12/160.61 mult(X10,rd(ld(X10,op_c),op_c)) = unit]. % 160.12/160.61 [112=param(104,48),[], % 160.12/160.61 mult(rd(op_c,X10),rd(X10,op_c)) = unit]. % 160.12/160.61 [118=param(32,10),[], % 160.12/160.61 ld(mult(X10,mult(X11,X10)),mult(X10,mult(X11,X12))) = ld(X10,X12)]. % 160.12/160.61 [120=param(7,112),[], % 160.12/160.61 rd(unit,rd(X10,op_c)) = rd(op_c,X10)]. % 160.12/160.61 [123=param(120,7),[], % 160.12/160.61 rd(op_c,mult(X10,op_c)) = rd(unit,X10)]. % 160.12/160.61 [140=param(9,89),[49], % 160.12/160.61 ld(mult(op_c,X10),X10) = rd(unit,op_c)]. % 160.12/160.61 [144=param(140,10),[49], % 160.12/160.61 ld(X10,rd(X10,op_c)) = rd(unit,op_c)]. % 160.12/160.61 [149=param(10,144),[], % 160.12/160.61 mult(X10,rd(unit,op_c)) = rd(X10,op_c)]. % 160.12/160.61 [151=param(149,8),[], % 160.12/160.61 rd(rd(X10,rd(unit,op_c)),op_c) = X10]. % 160.12/160.61 [156=param(39,5),[5], % 160.12/160.61 rd(mult(X10,mult(X10,X11)),X11) = mult(X10,X10)]. % 160.12/160.61 [157=param(39,8),[], % 160.12/160.61 mult(X10,mult(rd(X11,mult(X10,X12)),X10)) = rd(mult(X10,X11),X12)]. % 160.12/160.61 [166=param(39,104),[6], % 160.12/160.61 rd(mult(X10,X11),rd(ld(X10,op_c),op_c)) = mult(X10,mult(X11,X10))]. % 160.12/160.61 [167=param(8,151),[], % 160.12/160.61 mult(X10,op_c) = rd(X10,rd(unit,op_c))]. % 160.12/160.61 [182=demod(123),[167], % 160.12/160.61 rd(op_c,rd(X10,rd(unit,op_c))) = rd(unit,X10)]. % 160.12/160.61 [190=demod(2),[167], % 160.12/160.61 mult(op_c,X10) = rd(X10,rd(unit,op_c))]. % 160.12/160.61 [196=demod(45),[190], % 160.12/160.61 rd(mult(X10,rd(X11,op_c)),rd(unit,op_c)) = mult(X10,X11)]. % 160.12/160.61 [204=demod(88),[190], % 160.12/160.61 rd(ld(X10,rd(X11,op_c)),rd(unit,op_c)) = ld(X10,X11)]. % 160.12/160.61 [217=demod(22),[190,190], % 160.12/160.61 mult(X10,rd(X11,rd(unit,op_c))) = rd(mult(X10,X11),rd(unit,op_c))]. % 160.12/160.61 [241=param(118,8),[], % 160.12/160.61 ld(mult(X10,X11),mult(X10,mult(rd(X11,X10),X12))) = ld(X10,X12)]. % 160.12/160.61 [259=param(7,157),[], % 160.12/160.61 rd(rd(mult(X10,X11),X12),mult(rd(X11,mult(X10,X12)),X10)) = X10]. % 160.12/160.61 [260=param(9,157),[], % 160.12/160.61 ld(X10,rd(mult(X10,X11),X12)) = mult(rd(X11,mult(X10,X12)),X10)]. % 160.12/160.61 [262=param(157,10),[], % 160.12/160.61 mult(X10,mult(rd(X11,X12),X10)) = rd(mult(X10,X11),ld(X10,X12))]. % 160.12/160.61 [277=param(8,196),[149], % 160.12/160.61 mult(X10,rd(X11,op_c)) = rd(mult(X10,X11),op_c)]. % 160.12/160.61 [278=param(7,277),[], % 160.12/160.61 rd(rd(mult(X10,X11),op_c),rd(X11,op_c)) = X10]. % 160.12/160.61 [279=param(9,277),[260,167], % 160.12/160.61 mult(rd(X10,rd(X11,rd(unit,op_c))),X11) = rd(X10,op_c)]. % 160.12/160.61 [281=param(278,8),[], % 160.12/160.61 rd(rd(X10,op_c),rd(X11,op_c)) = rd(X10,X11)]. % 160.12/160.61 [282=param(281,7),[167], % 160.12/160.61 rd(X10,rd(X11,op_c)) = rd(rd(X10,rd(unit,op_c)),X11)]. % 160.12/160.61 [294=param(281,7),[167], % 160.12/160.61 rd(rd(X10,op_c),X11) = rd(X10,rd(X11,rd(unit,op_c)))]. % 160.12/160.61 [307=param(8,204),[277,6], % 160.12/160.61 ld(X10,rd(X11,op_c)) = rd(ld(X10,X11),op_c)]. % 160.12/160.61 [309=param(307,48),[], % 160.12/160.61 rd(ld(rd(rd(X10,op_c),X11),X10),op_c) = X11]. % 160.12/160.61 [310=param(8,309),[167], % 160.12/160.61 ld(rd(rd(X11,op_c),X10),X11) = rd(X10,rd(unit,op_c))]. % 160.12/160.61 [311=param(310,58),[49,294], % 160.12/160.61 rd(rd(X10,rd(op_c,rd(unit,op_c))),rd(unit,op_c)) = rd(X10,op_c)]. % 160.12/160.61 [315=param(260,7),[16], % 160.12/160.61 mult(rd(X10,mult(X11,X10)),X11) = unit]. % 160.12/160.61 [316=param(260,10),[], % 160.12/160.61 ld(X10,rd(X11,X12)) = mult(rd(ld(X10,X11),mult(X10,X12)),X10)]. % 160.12/160.61 [317=param(7,315),[], % 160.12/160.61 rd(X11,mult(X10,X11)) = rd(unit,X10)]. % 160.12/160.61 [318=param(317,8),[], % 160.12/160.61 rd(X10,X11) = rd(unit,rd(X11,X10))]. % 160.12/160.61 [319=demod(7),[318,317], % 160.12/160.61 rd(unit,rd(unit,X10)) = X10]. % 160.12/160.61 [320=demod(156),[318], % 160.12/160.61 rd(unit,rd(X10,mult(X11,mult(X11,X10)))) = mult(X11,X11)]. % 160.12/160.61 [322=demod(217),[318], % 160.12/160.61 mult(X10,rd(X11,rd(unit,op_c))) = rd(unit,rd(rd(unit,op_c),mult(X10,X11)))]. % 160.12/160.61 [326=demod(277),[318], % 160.12/160.61 mult(X10,rd(X11,op_c)) = rd(unit,rd(op_c,mult(X10,X11)))]. % 160.12/160.61 [333=demod(166),[318,42,318], % 160.12/160.61 mult(X10,mult(X11,X10)) = rd(unit,rd(rd(unit,X10),mult(X10,X11)))]. % 160.12/160.61 [337=demod(262),[333], % 160.12/160.61 rd(unit,rd(rd(unit,X10),mult(X10,rd(X11,X12)))) = rd(mult(X10,X11),ld(X10,X12))]. % 160.12/160.61 [344=demod(311),[318], % 160.12/160.61 rd(unit,rd(rd(unit,op_c),rd(X10,rd(op_c,rd(unit,op_c))))) = rd(X10,op_c)]. % 160.12/160.61 [349=param(8,317),[], % 160.12/160.61 mult(rd(unit,X10),mult(X10,X11)) = X11]. % 160.12/160.61 [350=param(317,190),[], % 160.12/160.61 rd(X10,rd(X10,rd(unit,op_c))) = rd(unit,op_c)]. % 160.12/160.61 [352=param(317,279),[], % 160.12/160.61 rd(X10,rd(X11,op_c)) = rd(unit,rd(X11,rd(X10,rd(unit,op_c))))]. % 160.12/160.61 [353=param(241,6),[9], % 160.12/160.61 ld(X10,X11) = mult(rd(unit,X10),X11)]. % 160.12/160.61 [357=demod(337),[353], % 160.12/160.61 rd(unit,rd(rd(unit,X10),mult(X10,rd(X11,X12)))) = rd(mult(X10,X11),mult(rd(unit,X10),X12))]. % 160.12/160.61 [359=demod(316),[353,353], % 160.12/160.61 mult(rd(mult(rd(unit,X10),X11),mult(X10,X12)),X10) = mult(rd(unit,X10),rd(X11,X12))]. % 160.12/160.61 [364=demod(49),[353], % 160.12/160.61 mult(rd(unit,op_c),X10) = rd(X10,op_c)]. % 160.12/160.61 [377=param(259,6),[], % 160.12/160.61 rd(rd(X10,X11),mult(rd(unit,mult(X10,X11)),X10)) = X10]. % 160.12/160.61 [393=param(282,318),[], % 160.12/160.61 rd(rd(X10,rd(unit,op_c)),X11) = rd(X10,rd(unit,rd(op_c,X11)))]. % 160.12/160.61 [401=param(294,318),[], % 160.12/160.61 rd(X10,rd(unit,rd(rd(unit,op_c),X11))) = rd(rd(X10,op_c),X11)]. % 160.12/160.61 [408=param(326,318),[], % 160.12/160.61 mult(X10,rd(unit,rd(op_c,X11))) = rd(unit,rd(op_c,mult(X10,X11)))]. % 160.12/160.61 [411=param(8,320),[46,40,5], % 160.12/160.61 mult(X10,mult(X10,rd(X11,mult(X10,mult(X10,X11))))) = unit]. % 160.12/160.61 [412=param(318,320),[41], % 160.12/160.61 rd(X11,mult(X10,mult(X10,X11))) = rd(unit,mult(X10,X10))]. % 160.12/160.61 [413=demod(411),[412], % 160.12/160.61 mult(X10,mult(X10,rd(unit,mult(X10,X10)))) = unit]. % 160.12/160.61 [414=param(317,413),[41], % 160.12/160.61 mult(X10,rd(unit,mult(X10,X10))) = rd(unit,X10)]. % 160.12/160.61 [417=param(349,414),[], % 160.12/160.61 mult(rd(unit,X10),rd(unit,X10)) = rd(unit,mult(X10,X10))]. % 160.12/160.61 [421=param(412,349),[-357,40,6,318,319,417,319], % 160.12/160.61 mult(X10,X10) = rd(X10,rd(unit,X10))]. % 160.12/160.61 [430=param(46,421),[40,5], % 160.12/160.61 mult(rd(X10,rd(unit,X10)),X11) = mult(X10,mult(X10,X11))]. % 160.12/160.61 [443=param(8,393),[], % 160.12/160.61 mult(rd(X10,rd(unit,rd(op_c,X11))),X11) = rd(X10,rd(unit,op_c))]. % 160.12/160.61 [445=param(318,344),[-318,41], % 160.12/160.61 rd(rd(unit,op_c),rd(X10,rd(op_c,rd(unit,op_c)))) = rd(op_c,X10)]. % 160.12/160.61 [451=param(377,182),[5,6], % 160.12/160.61 rd(rd(op_c,rd(X10,rd(unit,op_c))),rd(unit,X10)) = unit]. % 160.12/160.61 [459=param(359,8),[], % 160.12/160.61 mult(rd(unit,mult(X10,X11)),X10) = mult(rd(unit,X10),rd(X10,X11))]. % 160.12/160.61 [461=param(317,459),[319], % 160.12/160.61 rd(X10,mult(rd(unit,X10),rd(X10,X11))) = mult(X10,X11)]. % 160.12/160.61 [463=param(461,364),[318,190], % 160.12/160.61 rd(op_c,rd(unit,rd(op_c,rd(op_c,X10)))) = rd(X10,rd(unit,op_c))]. % 160.12/160.61 [465=param(294,451),[41,350,-463], % 160.12/160.61 rd(op_c,rd(unit,rd(op_c,rd(op_c,rd(X10,op_c))))) = X10]. % 160.12/160.61 [469=param(443,465),[], % 160.12/160.61 mult(X10,rd(op_c,rd(X10,op_c))) = rd(op_c,rd(unit,op_c))]. % 160.12/160.61 [470=param(317,469),[], % 160.12/160.61 rd(rd(op_c,rd(X10,op_c)),rd(op_c,rd(unit,op_c))) = rd(unit,X10)]. % 160.12/160.61 [501=param(445,470),[], % 160.12/160.61 rd(rd(unit,op_c),rd(unit,X10)) = rd(op_c,rd(op_c,rd(X10,op_c)))]. % 160.12/160.61 [516=param(182,463),[], % 160.12/160.61 rd(op_c,rd(op_c,rd(unit,rd(op_c,rd(op_c,X10))))) = rd(unit,X10)]. % 160.12/160.61 [520=param(501,294),[318,-352,40,41], % 160.14/160.62 rd(rd(unit,op_c),rd(rd(unit,op_c),X10)) = rd(op_c,rd(op_c,X10))]. % 160.14/160.62 [523=param(12,421),[430,190,-463,190,-463,516,167,430,190,322,190,-352,318], % 160.14/160.62 thtop(rd(op_c,rd(unit,rd(op_c,rd(unit,mult(a,b))))),mult(rd(a,rd(unit,rd(op_c,rd(unit,op_c)))),b)) = thmtrue]. % 160.14/160.62 [644=param(520,317),[326,6], % 160.14/160.62 rd(rd(unit,op_c),rd(unit,X10)) = rd(op_c,rd(op_c,rd(unit,rd(op_c,X10))))]. % 160.14/160.62 [647=param(644,319),[], % 160.14/160.62 rd(rd(unit,op_c),X10) = rd(op_c,rd(op_c,rd(unit,rd(op_c,rd(unit,X10)))))]. % 160.14/160.62 [650=demod(401),[647], % 160.14/160.62 rd(rd(X10,op_c),X11) = rd(X10,rd(unit,rd(op_c,rd(op_c,rd(unit,rd(op_c,rd(unit,X11)))))))]. % 160.14/160.62 [697=demod(322),[650,319], % 160.14/160.62 mult(X10,rd(X11,rd(unit,op_c))) = rd(unit,rd(op_c,rd(op_c,rd(unit,rd(op_c,rd(unit,mult(X10,X11)))))))]. % 160.14/160.62 [1202=param(46,190),[190,697,408,190,-463,516,319], % 160.14/160.62 mult(rd(X10,rd(unit,op_c)),X11) = rd(op_c,rd(unit,rd(op_c,rd(unit,mult(rd(X10,op_c),X11)))))]. % 160.14/160.62 [2501=param(1202,393),[318,-352,40,41], % 160.14/160.62 mult(rd(X10,rd(unit,rd(op_c,rd(unit,op_c)))),X11) = rd(op_c,rd(unit,rd(op_c,rd(unit,mult(X10,X11)))))]. % 160.14/160.62 [3262=param(523,2501),[11], % 160.14/160.62 thmtrue = thmfalse]. % 160.14/160.62 % SZS output end CNFRefutation % 160.14/160.62 Space: 407574 KB %------------------------------------------------------------------------------