%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : GRP751-1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n025.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:40 EDT 2022 % Result : Unsatisfiable 9.76s 10.16s % Output : CNFRefutation 9.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP751-1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : fiesta-wrapper %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 13 11:50:24 EDT 2022 % 0.12/0.34 % CPUTime : % 9.76/10.16 Theorem Proved. % 9.76/10.16 % SZS status Unsatisfiable % 9.76/10.16 % SZS output start CNFRefutation % 9.76/10.16 [1=axiom,[], % 9.76/10.16 mult(mult(X10,X11),mult(X12,X12)) = mult(mult(X10,X12),mult(X11,X12))]. % 9.76/10.16 [2=axiom,[], % 9.76/10.16 mult(mult(X10,X10),mult(X11,X12)) = mult(mult(X10,X11),mult(X10,X12))]. % 9.76/10.16 [3=axiom,[], % 9.76/10.16 mult(mult(X10,mult(X10,X10)),mult(X11,X12)) = mult(mult(X10,X11),mult(mult(X10,X10),X12))]. % 9.76/10.16 [4=axiom,[], % 9.76/10.16 rd(mult(X10,X11),X11) = X10]. % 9.76/10.16 [5=axiom,[], % 9.76/10.16 mult(rd(X10,X11),X11) = X10]. % 9.76/10.16 [6=axiom,[], % 9.76/10.16 ld(X10,mult(X10,X11)) = X11]. % 9.76/10.16 [7=axiom,[], % 9.76/10.16 mult(X10,ld(X10,X11)) = X11]. % 9.76/10.16 [8=axiom,[], % 9.76/10.16 thtop(X10,X10) = thmfalse]. % 9.76/10.16 [9=axiom,[], % 9.76/10.16 thtop(mult(a,mult(b,c)),mult(mult(rd(a,a),b),mult(a,c))) = thmtrue]. % 9.76/10.16 [11=param(1,5),[], % 9.76/10.16 mult(mult(rd(X10,X12),X11),mult(X12,X11)) = mult(X10,mult(X11,X11))]. % 9.76/10.16 [12=param(6,1),[], % 9.76/10.16 ld(mult(X10,X11),mult(mult(X10,X12),mult(X11,X12))) = mult(X12,X12)]. % 9.76/10.16 [13=param(1,7),[], % 9.76/10.16 mult(X10,mult(X11,X11)) = mult(mult(X12,X11),mult(ld(X12,X10),X11))]. % 9.76/10.16 [14=param(1,5),[], % 9.76/10.16 mult(mult(rd(X10,X12),X11),mult(X12,X12)) = mult(X10,mult(X11,X12))]. % 9.76/10.16 [16=param(4,1),[], % 9.76/10.16 rd(mult(mult(X10,X11),mult(X12,X11)),mult(X11,X11)) = mult(X10,X12)]. % 9.76/10.16 [18=param(4,7),[], % 9.76/10.16 rd(X10,ld(X11,X10)) = X11]. % 9.76/10.16 [19=param(4,2),[], % 9.76/10.16 rd(mult(mult(X10,X11),mult(X10,X12)),mult(X11,X12)) = mult(X10,X10)]. % 9.76/10.16 [20=param(2,5),[], % 9.76/10.16 mult(mult(X10,X10),X11) = mult(mult(X10,rd(X11,X12)),mult(X10,X12))]. % 9.76/10.16 [22=param(2,7),[], % 9.76/10.16 mult(mult(X10,X10),X11) = mult(mult(X10,X12),mult(X10,ld(X12,X11)))]. % 9.76/10.16 [25=param(2,7),[], % 9.76/10.16 mult(mult(X11,X11),mult(ld(X11,X10),X12)) = mult(X10,mult(X11,X12))]. % 9.76/10.16 [26=param(2,7),[], % 9.76/10.16 mult(mult(X10,X11),X12) = mult(mult(X10,X10),mult(X11,ld(X10,X12)))]. % 9.76/10.16 [28=param(6,25),[], % 9.76/10.16 ld(mult(X10,X10),mult(X11,mult(X10,X12))) = mult(ld(X10,X11),X12)]. % 9.76/10.16 [29=param(25,7),[], % 9.76/10.16 mult(X12,mult(X10,ld(ld(X10,X12),X11))) = mult(mult(X10,X10),X11)]. % 9.76/10.16 [31=param(6,29),[], % 9.76/10.16 mult(X11,ld(ld(X11,X10),X12)) = ld(X10,mult(mult(X11,X11),X12))]. % 9.76/10.16 [33=param(31,6),[], % 9.76/10.16 ld(mult(X10,X11),mult(mult(X10,X10),X12)) = mult(X10,ld(X11,X12))]. % 9.76/10.16 [35=param(4,11),[], % 9.76/10.16 rd(mult(X10,mult(X11,X11)),mult(X12,X11)) = mult(rd(X10,X12),X11)]. % 9.76/10.16 [38=param(33,7),[], % 9.76/10.16 ld(mult(X10,X11),X12) = mult(X10,ld(X11,ld(mult(X10,X10),X12)))]. % 9.76/10.16 [39=param(28,7),[], % 9.76/10.16 ld(mult(X10,X10),mult(X11,X12)) = mult(ld(X10,X11),ld(X10,X12))]. % 9.76/10.16 [40=param(39,7),[], % 9.76/10.16 ld(mult(X10,X10),X11) = mult(ld(X10,X12),ld(X10,ld(X12,X11)))]. % 9.76/10.16 [41=param(6,13),[], % 9.76/10.16 ld(X10,mult(mult(X11,X12),mult(ld(X11,X10),X12))) = mult(X12,X12)]. % 9.76/10.16 [44=param(4,14),[], % 9.76/10.16 rd(mult(X10,mult(X11,X12)),mult(X12,X12)) = mult(rd(X10,X12),X11)]. % 9.76/10.16 [46=param(14,7),[], % 9.76/10.16 mult(X12,mult(ld(rd(X12,X11),X10),X11)) = mult(X10,mult(X11,X11))]. % 9.76/10.16 [47=param(6,46),[], % 9.76/10.16 mult(ld(rd(X10,X12),X11),X12) = ld(X10,mult(X11,mult(X12,X12)))]. % 9.76/10.16 [48=param(4,47),[], % 9.76/10.16 ld(rd(X10,X12),X11) = rd(ld(X10,mult(X11,mult(X12,X12))),X12)]. % 9.76/10.16 [49=param(7,48),[], % 9.76/10.16 mult(rd(X10,X11),rd(ld(X10,mult(X12,mult(X11,X11))),X11)) = X12]. % 9.76/10.16 [50=param(19,7),[], % 9.76/10.16 rd(mult(mult(X10,X11),X12),mult(X11,ld(X10,X12))) = mult(X10,X10)]. % 9.76/10.16 [52=param(50,7),[], % 9.76/10.16 rd(mult(X10,X11),mult(ld(X12,X10),ld(X12,X11))) = mult(X12,X12)]. % 9.76/10.16 [55=param(4,20),[], % 9.76/10.16 rd(mult(mult(X10,X10),X11),mult(X10,X12)) = mult(X10,rd(X11,X12))]. % 9.76/10.16 [57=param(4,22),[], % 9.76/10.16 rd(mult(mult(X10,X10),X11),mult(X10,ld(X12,X11))) = mult(X10,X12)]. % 9.76/10.16 [60=param(4,35),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X11)),mult(X12,X11)),X11) = rd(X10,X12)]. % 9.76/10.16 [62=param(4,49),[], % 9.76/10.16 rd(X10,rd(ld(X11,mult(X10,mult(X12,X12))),X12)) = rd(X11,X12)]. % 9.76/10.16 [63=param(38,12),[39,6], % 9.76/10.16 mult(X10,ld(X11,mult(X12,ld(X10,mult(X11,X12))))) = mult(X12,X12)]. % 9.76/10.16 [67=param(6,63),[], % 9.76/10.16 ld(X10,mult(X11,X11)) = ld(X12,mult(X11,ld(X10,mult(X12,X11))))]. % 9.76/10.16 [69=param(40,6),[], % 9.76/10.16 mult(X10,ld(X11,ld(mult(X11,X10),X12))) = ld(mult(X11,X11),X12)]. % 9.76/10.16 [70=param(4,44),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X12)),mult(X12,X12)),X11) = rd(X10,X12)]. % 9.76/10.16 [71=param(55,7),[], % 9.76/10.16 mult(X11,rd(ld(mult(X11,X11),X10),X12)) = rd(X10,mult(X11,X12))]. % 9.76/10.16 [72=param(55,7),[], % 9.76/10.16 rd(mult(mult(X10,X10),X11),X12) = mult(X10,rd(X11,ld(X10,X12)))]. % 9.76/10.16 [74=param(6,55),[], % 9.76/10.16 ld(X10,rd(mult(mult(X10,X10),X11),mult(X10,X12))) = rd(X11,X12)]. % 9.76/10.16 [75=param(4,71),[], % 9.76/10.16 rd(rd(X10,mult(X11,X12)),rd(ld(mult(X11,X11),X10),X12)) = X11]. % 9.76/10.16 [76=param(6,71),[], % 9.76/10.16 ld(X10,rd(X11,mult(X10,X12))) = rd(ld(mult(X10,X10),X11),X12)]. % 9.76/10.16 [77=param(74,7),[], % 9.76/10.16 ld(X10,rd(mult(mult(X10,X10),X11),X12)) = rd(X11,ld(X10,X12))]. % 9.76/10.16 [80=param(7,67),[], % 9.76/10.16 mult(X10,ld(X11,mult(X12,X12))) = mult(X12,ld(X11,mult(X10,X12)))]. % 9.76/10.16 [93=param(4,3),[], % 9.76/10.16 rd(mult(mult(X10,X11),mult(mult(X10,X10),X12)),mult(X11,X12)) = mult(X10,mult(X10,X10))]. % 9.76/10.16 [94=param(6,3),[38,39,6,39], % 9.76/10.16 mult(X10,mult(ld(X10,X11),ld(X10,ld(X10,mult(mult(X10,X10),X12))))) = mult(X11,X12)]. % 9.76/10.16 [96=param(4,3),[], % 9.76/10.16 rd(mult(mult(X10,mult(X10,X10)),mult(X11,X12)),mult(mult(X10,X10),X12)) = mult(X10,X11)]. % 9.76/10.16 [113=param(13,7),[], % 9.76/10.16 mult(X10,mult(ld(X11,X12),ld(X11,X10))) = mult(X12,mult(ld(X11,X10),ld(X11,X10)))]. % 9.76/10.16 [116=param(70,2),[], % 9.76/10.16 rd(rd(mult(mult(X10,X11),mult(X10,X12)),mult(X12,X12)),X11) = rd(mult(X10,X10),X12)]. % 9.76/10.16 [120=param(70,25),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X12)),mult(X12,X12)),ld(X11,X10)) = rd(mult(X11,X11),X12)]. % 9.76/10.16 [121=param(16,7),[], % 9.76/10.16 rd(mult(X10,mult(X11,ld(X12,X10))),mult(ld(X12,X10),ld(X12,X10))) = mult(X12,X11)]. % 9.76/10.16 [128=param(60,14),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X12)),mult(X13,X12)),X12) = rd(mult(rd(X10,X12),X11),X13)]. % 9.76/10.16 [133=param(60,20),[], % 9.76/10.16 rd(rd(mult(mult(X10,X10),X11),mult(X12,X10)),X10) = rd(mult(X10,rd(X11,X10)),X12)]. % 9.76/10.16 [134=param(70,20),[], % 9.76/10.16 rd(rd(mult(mult(X10,X10),X11),mult(X12,X12)),X10) = rd(mult(X10,rd(X11,X12)),X12)]. % 9.76/10.16 [140=param(57,20),[], % 9.76/10.16 rd(mult(mult(X10,rd(X11,X12)),mult(X10,X12)),mult(X10,ld(X13,X11))) = mult(X10,X13)]. % 9.76/10.16 [146=param(22,14),[-35,4], % 9.76/10.16 mult(mult(rd(X10,X11),X12),mult(rd(X10,X11),ld(X12,mult(X11,X11)))) = mult(X10,X10)]. % 9.76/10.16 [152=param(33,26),[], % 9.76/10.16 ld(mult(X10,X11),mult(mult(X10,X12),X13)) = mult(X10,ld(X11,mult(X12,ld(X10,X13))))]. % 9.76/10.16 [156=param(77,26),[], % 9.76/10.16 ld(X10,rd(mult(mult(X10,X11),X12),X13)) = rd(mult(X11,ld(X10,X12)),ld(X10,X13))]. % 9.76/10.16 [169=param(35,7),[], % 9.76/10.16 rd(mult(X10,mult(ld(X11,X12),ld(X11,X12))),X12) = mult(rd(X10,X11),ld(X11,X12))]. % 9.76/10.16 [171=param(35,25),[7], % 9.76/10.16 mult(rd(mult(X12,X12),X11),ld(X12,X10)) = rd(mult(X10,X10),mult(X11,ld(X12,X10)))]. % 9.76/10.16 [174=param(14,35),[], % 9.76/10.16 mult(rd(mult(X10,mult(X11,X11)),mult(X12,X11)),mult(X12,X12)) = mult(X10,mult(X11,X12))]. % 9.76/10.16 [180=param(41,7),[], % 9.76/10.16 ld(X10,mult(X11,mult(ld(X12,X10),ld(X12,X11)))) = mult(ld(X12,X11),ld(X12,X11))]. % 9.76/10.16 [190=param(156,7),[], % 9.76/10.16 ld(X10,rd(mult(X11,X12),X13)) = rd(mult(ld(X10,X11),ld(X10,X12)),ld(X10,X13))]. % 9.76/10.16 [197=param(152,7),[], % 9.76/10.16 ld(mult(X10,X11),mult(X12,X13)) = mult(X10,ld(X11,mult(ld(X10,X12),ld(X10,X13))))]. % 9.76/10.16 [208=param(44,35),[], % 9.76/10.16 rd(mult(X10,mult(X11,X12)),mult(X12,X12)) = rd(mult(X10,mult(X11,X11)),mult(X12,X11))]. % 9.76/10.16 [227=param(55,1),[], % 9.76/10.16 rd(mult(mult(X10,X11),mult(X10,X11)),mult(X10,X12)) = mult(X10,rd(mult(X11,X11),X12))]. % 9.76/10.16 [232=param(55,20),[], % 9.76/10.16 rd(mult(mult(X10,rd(X11,X12)),mult(X10,X12)),mult(X10,X13)) = mult(X10,rd(X11,X13))]. % 9.76/10.16 [242=param(75,16),[197,7], % 9.76/10.16 rd(mult(X10,X11),rd(mult(ld(X12,mult(X10,X12)),ld(X12,mult(X11,X12))),X12)) = X12]. % 9.76/10.16 [274=param(69,67),[197,80,7,197,7,180], % 9.76/10.16 mult(X10,ld(X11,mult(ld(X11,X12),ld(X10,X12)))) = mult(ld(X11,X12),ld(X11,X12))]. % 9.76/10.16 [277=param(72,1),[], % 9.76/10.16 rd(mult(mult(X10,X11),mult(X10,X10)),X12) = mult(X10,rd(mult(X11,X10),ld(X10,X12)))]. % 9.76/10.16 [279=param(72,20),[], % 9.76/10.16 rd(mult(mult(X10,rd(X11,X12)),mult(X10,X12)),X13) = mult(X10,rd(X11,ld(X10,X13)))]. % 9.76/10.16 [281=param(72,26),[], % 9.76/10.16 rd(mult(mult(X10,X11),X12),X13) = mult(X10,rd(mult(X11,ld(X10,X12)),ld(X10,X13)))]. % 9.76/10.16 [290=param(26,274),[25,7], % 9.76/10.16 mult(mult(X11,X12),mult(ld(X11,X10),ld(X12,X10))) = mult(X10,X10)]. % 9.76/10.16 [294=param(70,290),[52], % 9.76/10.16 rd(mult(X10,X10),ld(X11,X12)) = rd(mult(X11,X10),ld(X10,X12))]. % 9.76/10.16 [298=param(72,294),[], % 9.76/10.16 mult(X10,rd(mult(X10,X11),ld(X11,X12))) = rd(mult(mult(X10,X10),mult(X11,X11)),X12)]. % 9.76/10.16 [309=param(94,41),[6], % 9.76/10.16 mult(X10,mult(ld(X10,X11),X10)) = mult(X11,mult(ld(X10,X10),X10))]. % 9.76/10.16 [318=param(44,309),[44], % 9.76/10.16 mult(rd(X10,X10),ld(X10,X11)) = mult(rd(X11,X10),ld(X10,X10))]. % 9.76/10.16 [385=param(120,1),[4], % 9.76/10.16 rd(mult(X10,X11),ld(X11,mult(X10,X12))) = rd(mult(X11,X11),X12)]. % 9.76/10.16 [388=param(120,44),[], % 9.76/10.16 rd(mult(rd(X10,X11),X12),ld(X12,X10)) = rd(mult(X12,X12),X11)]. % 9.76/10.16 [394=param(385,67),[], % 9.76/10.16 rd(mult(X10,X11),ld(X12,mult(X10,X10))) = rd(mult(X11,X11),ld(X12,mult(X11,X10)))]. % 9.76/10.16 [400=param(116,121),[], % 9.76/10.16 rd(mult(X11,X11),ld(X10,mult(X11,X12))) = rd(mult(X10,X11),X12)]. % 9.76/10.16 [401=demod(394),[400], % 9.76/10.16 rd(mult(X10,X11),ld(X12,mult(X10,X10))) = rd(mult(X12,X11),X10)]. % 9.76/10.16 [408=param(401,7),[], % 9.76/10.16 rd(X10,ld(X11,mult(X12,X12))) = rd(mult(X11,ld(X12,X10)),X12)]. % 9.76/10.16 [413=param(401,55),[197,6,6,7], % 9.76/10.16 rd(mult(mult(X10,X11),X12),mult(X11,X11)) = mult(X10,rd(X12,X11))]. % 9.76/10.16 [453=param(408,171),[48,6,4], % 9.76/10.16 rd(rd(mult(X10,X10),mult(X11,ld(X12,X10))),X12) = rd(X10,X11)]. % 9.76/10.16 [456=param(453,318),[], % 9.76/10.16 rd(rd(mult(X10,X10),mult(rd(X10,X11),ld(X11,X11))),X11) = rd(X10,rd(X11,X11))]. % 9.76/10.16 [457=param(453,318),[], % 9.76/10.16 rd(rd(mult(X10,X10),mult(rd(X10,X10),ld(X10,X11))),X10) = rd(X10,rd(X11,X10))]. % 9.76/10.16 [458=param(128,55),[4], % 9.76/10.16 rd(mult(rd(mult(X10,X10),X12),X11),X10) = rd(mult(X10,X11),X12)]. % 9.76/10.16 [459=param(128,93),[], % 9.76/10.16 rd(mult(rd(mult(X10,X12),X11),mult(X10,X10)),X12) = rd(mult(X10,mult(X10,X10)),X11)]. % 9.76/10.16 [460=param(128,96),[], % 9.76/10.16 rd(mult(rd(mult(X10,mult(X10,X10)),X12),X11),mult(X10,X10)) = rd(mult(X10,X11),X12)]. % 9.76/10.16 [472=param(133,7),[-76,7], % 9.76/10.16 rd(rd(X10,mult(X11,X12)),X12) = rd(rd(X10,mult(X12,X12)),X11)]. % 9.76/10.16 [483=param(72,388),[], % 9.76/10.16 rd(mult(mult(X10,X10),mult(rd(X12,X11),X10)),X12) = mult(X10,rd(mult(X10,X10),X11))]. % 9.76/10.16 [488=param(134,72),[], % 9.76/10.16 rd(mult(X10,rd(X11,ld(X10,mult(X12,X12)))),X10) = rd(mult(X10,rd(X11,X12)),X12)]. % 9.76/10.16 [491=param(488,120),[134,4], % 9.76/10.16 rd(mult(X10,rd(mult(X10,X10),X11)),X10) = rd(mult(X10,rd(mult(X12,X10),X11)),X12)]. % 9.76/10.16 [499=param(483,1),[], % 9.76/10.16 rd(mult(mult(X10,rd(X11,X12)),mult(X10,X10)),X11) = mult(X10,rd(mult(X10,X10),X12))]. % 9.76/10.16 [510=param(60,459),[], % 9.76/10.16 rd(rd(mult(X10,mult(X10,X10)),X11),X10) = rd(rd(mult(X10,mult(X12,X10)),X11),X12)]. % 9.76/10.16 [525=param(146,80),[-35,4], % 9.76/10.16 mult(mult(rd(X10,X11),X12),mult(X11,ld(X12,X10))) = mult(X10,X10)]. % 9.76/10.16 [526=param(4,525),[], % 9.76/10.16 rd(mult(X10,X10),mult(X11,ld(X12,X10))) = mult(rd(X10,X11),X12)]. % 9.76/10.16 [527=param(6,525),[197,48,6,4,48,6,4], % 9.76/10.16 mult(rd(X10,X11),ld(X12,mult(X11,X11))) = mult(X11,ld(X12,X10))]. % 9.76/10.16 [529=demod(38),[-527,-76], % 9.76/10.16 ld(mult(X10,X11),X12) = mult(ld(X10,rd(X12,mult(X10,X10))),ld(X11,mult(X10,X10)))]. % 9.76/10.16 [587=param(529,6),[190,6,6], % 9.76/10.16 mult(rd(mult(X10,ld(X11,X12)),X11),ld(X10,mult(X11,X11))) = X12]. % 9.76/10.16 [588=param(587,6),[], % 9.76/10.16 mult(rd(mult(X10,X11),X12),ld(X10,mult(X12,X12))) = mult(X12,X11)]. % 9.76/10.16 [600=param(4,527),[], % 9.76/10.16 rd(mult(rd(X10,X11),ld(X12,mult(X11,X11))),ld(X12,X10)) = X11]. % 9.76/10.16 [616=param(526,35),[], % 9.76/10.16 rd(mult(X10,X10),mult(X11,ld(X12,X10))) = rd(mult(X10,mult(X12,X12)),mult(X11,X12))]. % 9.76/10.16 [625=param(616,318),[-35,4], % 9.76/10.16 rd(mult(X10,X10),mult(rd(X10,X11),ld(X11,X11))) = rd(mult(X10,mult(X11,X11)),X11)]. % 9.76/10.16 [626=demod(456),[625], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X11)),X11),X11) = rd(X10,rd(X11,X11))]. % 9.76/10.16 [627=param(616,318),[-35,4], % 9.76/10.16 rd(mult(X10,X10),mult(rd(X10,X10),ld(X10,X11))) = rd(mult(X10,mult(X10,X10)),X11)]. % 9.76/10.16 [628=demod(457),[627], % 9.76/10.16 rd(rd(mult(X10,mult(X10,X10)),X11),X10) = rd(X10,rd(X11,X10))]. % 9.76/10.16 [629=demod(510),[628], % 9.76/10.16 rd(rd(mult(X10,mult(X12,X10)),X11),X12) = rd(X10,rd(X11,X10))]. % 9.76/10.16 [635=param(629,401),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X12)),X12),X11) = rd(X12,rd(ld(X10,mult(X12,X12)),X12))]. % 9.76/10.16 [644=param(626,401),[629], % 9.76/10.16 rd(X10,rd(ld(X11,mult(X10,X10)),X10)) = rd(X11,rd(X10,X10))]. % 9.76/10.16 [645=demod(635),[644], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X12)),X12),X11) = rd(X10,rd(X12,X12))]. % 9.76/10.16 [649=param(645,7),[], % 9.76/10.16 rd(rd(mult(X10,X11),ld(X12,X11)),X12) = rd(X10,rd(ld(X12,X11),ld(X12,X11)))]. % 9.76/10.16 [659=param(645,499),[], % 9.76/10.16 rd(mult(X10,rd(mult(X10,X10),X11)),X10) = rd(mult(X10,rd(X10,X11)),rd(X10,X10))]. % 9.76/10.16 [660=demod(491),[659], % 9.76/10.16 rd(mult(X10,rd(mult(X12,X10),X11)),X12) = rd(mult(X10,rd(X10,X11)),rd(X10,X10))]. % 9.76/10.16 [662=param(644,67),[], % 9.76/10.16 rd(X10,rd(ld(X11,mult(X10,ld(X12,mult(X11,X10)))),X10)) = rd(X12,rd(X10,X10))]. % 9.76/10.16 [672=param(169,113),[], % 9.76/10.16 rd(mult(X10,mult(ld(X11,X12),ld(X11,X10))),X10) = mult(rd(X12,X11),ld(X11,X10))]. % 9.76/10.16 [727=param(134,208),[4], % 9.76/10.16 rd(rd(mult(mult(X10,X10),mult(X11,X11)),mult(X12,X11)),X10) = rd(mult(X10,X11),X12)]. % 9.76/10.16 [767=param(727,14),[-35,4,-35,4], % 9.76/10.16 rd(rd(mult(X10,X10),mult(X11,X12)),rd(X10,X12)) = rd(X10,X11)]. % 9.76/10.16 [770=param(767,7),[], % 9.76/10.16 rd(rd(mult(X10,X10),X11),rd(X10,ld(X12,X11))) = rd(X10,X12)]. % 9.76/10.16 [780=param(770,19),[], % 9.76/10.16 rd(mult(X10,X10),rd(mult(X10,X11),ld(X12,mult(X11,X11)))) = rd(mult(X10,X11),X12)]. % 9.76/10.16 [790=param(780,408),[], % 9.76/10.16 rd(mult(X10,X10),rd(mult(X11,ld(X12,mult(X10,X12))),X12)) = rd(mult(X10,X12),X11)]. % 9.76/10.16 [797=param(767,227),[], % 9.76/10.16 rd(mult(X10,rd(mult(X11,X11),X12)),rd(mult(X10,X11),X12)) = rd(mult(X10,X11),X10)]. % 9.76/10.16 [837=param(797,242),[790], % 9.76/10.16 rd(mult(X10,rd(mult(X11,X12),ld(X12,mult(X10,X12)))),X12) = rd(mult(X10,X11),X10)]. % 9.76/10.16 [934=param(116,279),[], % 9.76/10.16 rd(mult(X10,rd(X11,ld(X10,mult(X12,X12)))),rd(X11,X12)) = rd(mult(X10,X10),X12)]. % 9.76/10.16 [942=param(934,600),[458], % 9.76/10.16 rd(mult(X10,X11),rd(mult(X12,ld(X10,mult(X11,X11))),X11)) = rd(mult(X10,X10),X12)]. % 9.76/10.16 [948=param(942,527),[], % 9.76/10.16 rd(mult(X10,X11),rd(mult(X11,ld(X10,X12)),X11)) = rd(mult(X10,X10),rd(X12,X11))]. % 9.76/10.16 [953=param(948,388),[7,-35,-35,4], % 9.76/10.16 rd(rd(mult(X12,mult(X10,X10)),X11),ld(X10,X12)) = rd(mult(X10,X10),rd(X11,X10))]. % 9.76/10.16 [963=param(953,140),[6], % 9.76/10.16 rd(mult(X10,X10),rd(mult(X10,ld(X11,X12)),X10)) = rd(mult(X10,X11),rd(X12,X10))]. % 9.76/10.16 [966=param(953,232),[6], % 9.76/10.16 rd(mult(X10,rd(X11,X12)),rd(X11,X10)) = rd(mult(X10,X10),rd(mult(X10,X12),X10))]. % 9.76/10.16 [969=demod(660),[966], % 9.76/10.16 rd(mult(X10,rd(mult(X11,X10),X12)),X11) = rd(mult(X10,X10),rd(mult(X10,X12),X10))]. % 9.76/10.16 [977=param(969,400),[963], % 9.76/10.16 rd(mult(X10,rd(mult(X11,X10),X12)),X10) = rd(mult(X10,X11),rd(mult(X10,X12),X10))]. % 9.76/10.16 [993=param(977,277),[7], % 9.76/10.16 rd(rd(mult(mult(X10,X11),mult(X10,X10)),X12),X10) = rd(mult(X10,X11),rd(X12,X10))]. % 9.76/10.16 [996=param(993,7),[7], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X11)),X12),X11) = rd(X10,rd(X12,X11))]. % 9.76/10.16 [1000=param(996,20),[], % 9.76/10.16 rd(rd(mult(mult(X10,X10),X11),X12),X10) = rd(mult(X10,rd(X11,X10)),rd(X12,X10))]. % 9.76/10.16 [1017=param(996,458),[996], % 9.76/10.16 rd(rd(mult(X10,X10),X11),rd(X10,X12)) = rd(X10,rd(X11,X12))]. % 9.76/10.16 [1018=param(996,459),[629], % 9.76/10.16 rd(rd(mult(X10,X12),X11),rd(X12,X10)) = rd(X10,rd(X11,X10))]. % 9.76/10.16 [1027=param(1018,18),[], % 9.76/10.16 rd(X12,rd(ld(X10,mult(X12,X11)),X12)) = rd(X10,rd(X11,X12))]. % 9.76/10.16 [1028=demod(662),[1027], % 9.76/10.16 rd(X10,rd(ld(X11,mult(X10,X12)),X12)) = rd(X11,rd(X12,X12))]. % 9.76/10.16 [1040=param(1018,401),[1028], % 9.76/10.16 rd(rd(mult(X10,X11),X12),rd(X11,X12)) = rd(X10,rd(X12,X12))]. % 9.76/10.16 [1072=param(1017,400),[], % 9.76/10.16 rd(X11,rd(ld(X10,mult(X11,X12)),X13)) = rd(rd(mult(X10,X11),X12),rd(X11,X13))]. % 9.76/10.16 [1073=demod(62),[1072], % 9.76/10.16 rd(rd(mult(X10,X11),mult(X12,X12)),rd(X11,X12)) = rd(X10,X12)]. % 9.76/10.16 [1079=param(298,14),[-35,4,-35,4], % 9.76/10.16 mult(rd(X10,X12),rd(X10,ld(X12,X11))) = rd(mult(X10,X10),X11)]. % 9.76/10.16 [1085=param(1079,6),[], % 9.76/10.16 mult(rd(X10,X11),rd(X10,X12)) = rd(mult(X10,X10),mult(X11,X12))]. % 9.76/10.16 [1091=param(1073,7),[], % 9.76/10.16 rd(rd(X10,mult(X11,X11)),rd(ld(X12,X10),X11)) = rd(X12,X11)]. % 9.76/10.16 [1095=param(1073,837),[529,4,6,472,4], % 9.76/10.16 rd(rd(mult(X10,X11),X10),rd(X11,ld(X12,X10))) = rd(X10,X12)]. % 9.76/10.16 [1096=param(1095,4),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,ld(X12,X10))),X10),X11) = rd(X10,X12)]. % 9.76/10.16 [1116=param(1096,672),[], % 9.76/10.16 rd(mult(rd(X10,X11),ld(X11,X12)),ld(X11,X10)) = rd(X12,X11)]. % 9.76/10.16 [1120=param(1116,6),[], % 9.76/10.16 rd(mult(rd(X10,X11),X12),ld(X11,X10)) = rd(mult(X11,X12),X11)]. % 9.76/10.16 [1122=param(1120,6),[], % 9.76/10.16 rd(mult(rd(mult(X10,X11),X10),X12),X11) = rd(mult(X10,X12),X10)]. % 9.76/10.16 [1137=param(996,1120),[996], % 9.76/10.16 rd(rd(X12,X10),rd(ld(X10,X12),X11)) = rd(X10,rd(X10,X11))]. % 9.76/10.16 [1148=param(1137,4),[1072], % 9.76/10.16 rd(rd(mult(X10,X11),X10),rd(X11,X12)) = rd(X10,rd(X10,X12))]. % 9.76/10.16 [1149=param(1137,18),[], % 9.76/10.16 rd(X11,rd(X11,ld(X12,ld(X11,X10)))) = rd(rd(X10,X11),X12)]. % 9.76/10.16 [1155=param(1149,6),[], % 9.76/10.16 rd(X10,rd(X10,ld(X11,X12))) = rd(rd(mult(X10,X12),X10),X11)]. % 9.76/10.16 [1156=param(1148,4),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X12)),X10),X11) = rd(X10,rd(X10,X12))]. % 9.76/10.16 [1194=param(1122,44),[1156], % 9.76/10.16 rd(mult(X10,mult(X11,X12)),X10) = mult(rd(X10,rd(X10,X12)),X11)]. % 9.76/10.16 [1198=param(1122,169),[413], % 9.76/10.16 mult(rd(X10,X11),rd(X12,ld(X11,X10))) = rd(mult(X10,X12),X10)]. % 9.76/10.16 [1220=param(1198,1120),[], % 9.76/10.16 mult(rd(X10,X11),rd(mult(X11,X12),X11)) = rd(mult(X10,mult(rd(X10,X11),X12)),X10)]. % 9.76/10.16 [1251=param(1220,44),[-35,4], % 9.76/10.16 rd(mult(X10,mult(rd(X10,X11),X12)),X10) = rd(mult(X10,mult(X11,X12)),mult(X11,X11))]. % 9.76/10.16 [1296=param(1000,7),[529,6,4,7], % 9.76/10.16 rd(rd(X10,X11),X12) = rd(rd(X10,mult(X12,X12)),rd(X11,X12))]. % 9.76/10.16 [1300=demod(649),[1296], % 9.76/10.16 rd(rd(mult(X10,X11),mult(X12,X12)),rd(ld(X12,X11),X12)) = rd(X10,rd(ld(X12,X11),ld(X12,X11)))]. % 9.76/10.16 [1398=param(588,1194),[6], % 9.76/10.16 mult(mult(rd(X10,rd(X10,X11)),X12),X10) = mult(X10,mult(X12,X11))]. % 9.76/10.16 [1408=param(1398,18),[], % 9.76/10.16 mult(mult(rd(X10,X11),X12),X10) = mult(X10,mult(X12,ld(X11,X10)))]. % 9.76/10.16 [1765=param(1408,1155),[48,6,4], % 9.76/10.16 mult(mult(rd(rd(mult(X10,X11),X10),X12),X13),X10) = mult(X10,mult(X13,ld(X12,X11)))]. % 9.76/10.16 [1853=param(460,44),[629], % 9.76/10.16 rd(mult(X10,mult(X11,X10)),X12) = mult(rd(X10,rd(X12,X10)),X11)]. % 9.76/10.16 [1888=param(128,1853),[4], % 9.76/10.16 rd(mult(rd(X10,X11),X12),X10) = rd(mult(rd(X10,X10),X12),X11)]. % 9.76/10.16 [1891=param(1853,401),[1072,4], % 9.76/10.16 mult(rd(X10,rd(X11,X11)),X12) = rd(mult(X10,mult(X12,X11)),X11)]. % 9.76/10.16 [1900=param(1853,4),[], % 9.76/10.16 mult(rd(X10,X11),X12) = rd(mult(X10,mult(X12,X10)),mult(X11,X10))]. % 9.76/10.16 [1913=param(1900,18),[], % 9.76/10.16 mult(X10,X11) = rd(mult(X12,mult(X11,X12)),mult(ld(X10,X12),X12))]. % 9.76/10.16 [2222=param(128,1913),[], % 9.76/10.16 rd(mult(X10,X11),X12) = rd(mult(rd(X12,X12),X11),ld(X10,X12))]. % 9.76/10.16 [2247=param(281,2222),[7], % 9.76/10.16 rd(mult(mult(X10,rd(X12,X12)),X11),X12) = mult(X10,rd(X11,X12))]. % 9.76/10.16 [2276=param(2247,1085),[458], % 9.76/10.16 mult(rd(X10,X12),rd(X11,X10)) = rd(mult(X10,X11),mult(X12,X10))]. % 9.76/10.16 [2284=param(14,2276),[], % 9.76/10.16 mult(rd(mult(X10,X11),mult(X12,X10)),mult(X12,X12)) = mult(X10,mult(rd(X11,X10),X12))]. % 9.76/10.16 [2431=param(1891,2222),[-1300,-35,4,1091], % 9.76/10.16 mult(rd(X10,X10),X11) = rd(mult(X10,mult(X11,ld(X10,X12))),X12)]. % 9.76/10.16 [2447=param(2431,44),[], % 9.76/10.16 rd(mult(X10,mult(X11,ld(X10,X12))),X12) = rd(mult(X10,mult(X11,X10)),mult(X10,X10))]. % 9.76/10.16 [2475=param(996,1888),[996], % 9.76/10.16 rd(rd(X10,X10),rd(X11,X12)) = rd(rd(X10,X11),rd(X10,X12))]. % 9.76/10.16 [2499=param(1040,1888),[], % 9.76/10.16 rd(rd(mult(rd(X10,X11),X12),X10),rd(X12,X11)) = rd(rd(X10,X10),rd(X11,X11))]. % 9.76/10.16 [2512=param(2475,4),[], % 9.76/10.16 rd(rd(mult(X10,X11),X12),X10) = rd(rd(mult(X10,X11),mult(X10,X11)),rd(X12,X11))]. % 9.76/10.16 [2568=param(2499,4),[-2512,4], % 9.76/10.16 rd(rd(mult(X10,X11),mult(X10,X12)),rd(X11,X12)) = rd(X10,X10)]. % 9.76/10.16 [2569=param(2568,4),[], % 9.76/10.16 rd(rd(mult(X10,mult(X11,X12)),mult(X10,X12)),X11) = rd(X10,X10)]. % 9.76/10.16 [2572=param(1891,2568),[-1888,4], % 9.76/10.16 mult(rd(X10,X10),X11) = rd(mult(X10,mult(X11,X12)),mult(X10,X12))]. % 9.76/10.16 [2615=param(2572,309),[-1900], % 9.76/10.16 mult(rd(X10,X11),ld(X10,X11)) = mult(rd(X11,X11),ld(X10,X10))]. % 9.76/10.16 [2628=param(1251,2615),[2447,-1765,-35,-35,14,2569], % 9.76/10.16 rd(mult(X10,mult(rd(X11,X11),X10)),mult(X10,X10)) = rd(mult(X10,X11),mult(X10,X11))]. % 9.76/10.16 [2702=param(2628,44),[], % 9.76/10.16 mult(rd(X10,X10),rd(X11,X11)) = rd(mult(X10,X11),mult(X10,X11))]. % 9.76/10.16 [2707=param(2247,2702),[-1888,4], % 9.76/10.16 mult(rd(X10,X10),rd(X11,X12)) = rd(mult(X10,X11),mult(X10,X12))]. % 9.76/10.16 [2709=param(14,2707),[], % 9.76/10.16 mult(rd(mult(X10,X11),mult(X10,X12)),mult(X10,X10)) = mult(X10,mult(rd(X11,X12),X10))]. % 9.76/10.16 [2791=param(174,2709),[2284,4], % 9.76/10.16 mult(rd(mult(X10,X11),mult(X10,X12)),mult(X10,X13)) = mult(X10,mult(rd(X11,X12),X13))]. % 9.76/10.16 [2795=param(2791,35),[4], % 9.76/10.16 mult(mult(rd(X10,X10),X11),mult(X10,X12)) = mult(X10,mult(X11,X12))]. % 9.76/10.16 [2797=param(9,2795),[8], % 9.76/10.16 thmtrue = thmfalse]. % 9.76/10.16 % SZS output end CNFRefutation % 9.76/10.16 Space: 13569 KB %------------------------------------------------------------------------------