%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : TOP050-1 : TPTP v8.1.0. Released v8.1.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 : Thu Jul 21 21:25:58 EDT 2022 % Result : Unsatisfiable 1.37s 1.73s % Output : CNFRefutation 1.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : TOP050-1 : TPTP v8.1.0. Released v8.1.0. % 0.07/0.12 % Command : fiesta-wrapper %s % 0.12/0.33 % Computer : n025.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 03:50:41 EDT 2022 % 0.12/0.33 % CPUTime : % 1.37/1.73 Theorem Proved. % 1.37/1.73 % SZS status Unsatisfiable % 1.37/1.73 % SZS output start CNFRefutation % 1.37/1.73 [1=axiom,[], % 1.37/1.73 product(a32,a21) = a1]. % 1.37/1.73 [2=axiom,[], % 1.37/1.73 product(a31,a3) = a32]. % 1.37/1.73 [3=axiom,[], % 1.37/1.73 product(a30,a23) = a31]. % 1.37/1.73 [4=axiom,[], % 1.37/1.73 product(a29,a1) = a30]. % 1.37/1.73 [5=axiom,[], % 1.37/1.73 product(a28,a3) = a29]. % 1.37/1.73 [6=axiom,[], % 1.37/1.73 product(a27,a21) = a28]. % 1.37/1.73 [7=axiom,[], % 1.37/1.73 product(a26,a1) = a27]. % 1.37/1.73 [8=axiom,[], % 1.37/1.73 product(a25,a23) = a26]. % 1.37/1.73 [9=axiom,[], % 1.37/1.73 product(a24,a3) = a25]. % 1.37/1.73 [10=axiom,[], % 1.37/1.73 product(a23,a21) = a24]. % 1.37/1.73 [11=axiom,[], % 1.37/1.73 product(a22,a31) = a23]. % 1.37/1.73 [12=axiom,[], % 1.37/1.73 product(a21,a25) = a22]. % 1.37/1.73 [13=axiom,[], % 1.37/1.73 product(a20,a29) = a21]. % 1.37/1.73 [14=axiom,[], % 1.37/1.73 product(a19,a11) = a20]. % 1.37/1.73 [15=axiom,[], % 1.37/1.73 product(a18,a15) = a19]. % 1.37/1.73 [16=axiom,[], % 1.37/1.73 product(a17,a9) = a18]. % 1.37/1.73 [17=axiom,[], % 1.37/1.73 product(a16,a19) = a17]. % 1.37/1.73 [18=axiom,[], % 1.37/1.73 product(a15,a5) = a16]. % 1.37/1.73 [19=axiom,[], % 1.37/1.73 product(a14,a17) = a15]. % 1.37/1.73 [20=axiom,[], % 1.37/1.73 product(a13,a7) = a14]. % 1.37/1.73 [21=axiom,[], % 1.37/1.73 product(a12,a19) = a13]. % 1.37/1.73 [22=axiom,[], % 1.37/1.73 product(a11,a5) = a12]. % 1.37/1.73 [23=axiom,[], % 1.37/1.73 product(a10,a7) = a11]. % 1.37/1.73 [24=axiom,[], % 1.37/1.73 product(a9,a17) = a10]. % 1.37/1.73 [25=axiom,[], % 1.37/1.73 product(a8,a5) = a9]. % 1.37/1.73 [26=axiom,[], % 1.37/1.73 product(a7,a19) = a8]. % 1.37/1.73 [27=axiom,[], % 1.37/1.73 product(a5,a15) = a6]. % 1.37/1.73 [28=axiom,[], % 1.37/1.73 product(a4,a11) = a5]. % 1.37/1.73 [29=axiom,[], % 1.37/1.73 product(a3,a29) = a4]. % 1.37/1.73 [30=axiom,[], % 1.37/1.73 product(a2,a25) = a3]. % 1.37/1.73 [31=axiom,[], % 1.37/1.73 product(a1,a31) = a2]. % 1.37/1.73 [32=axiom,[], % 1.37/1.73 product(product(X10,X11),X12) = product(product(X10,X12),product(X11,X12))]. % 1.37/1.73 [33=axiom,[], % 1.37/1.73 product(product(X10,X11),X11) = X10]. % 1.37/1.73 [34=axiom,[], % 1.37/1.73 product(X10,X10) = X10]. % 1.37/1.73 [35=axiom,[], % 1.37/1.73 thtop(X10,X10) = thmfalse]. % 1.37/1.73 [36=axiom,[], % 1.37/1.73 thtop(tuple(a1,a30,a31,a2,a24,a25,a3,a28,a29,a4,a10,a11,a5,a14,a15,a6,a7,a18,a19,a8,a9,a16,a17,a12,a13,a20,a21,a22,a23,a26,a27),tuple(a2,a31,a32,a3,a25,a26,a4,a29,a30,a5,a11,a12,a6,a15,a16,a7,a8,a19,a20,a9,a10,a17,a18,a13,a14,a21,a22,a23,a24,a27,a28)) = thmtrue]. % 1.37/1.73 [37=param(33,1),[], % 1.37/1.73 product(a1,a21) = a32]. % 1.37/1.73 [38=param(33,2),[], % 1.37/1.73 product(a32,a3) = a31]. % 1.37/1.73 [39=param(33,3),[], % 1.37/1.73 product(a31,a23) = a30]. % 1.37/1.73 [40=param(33,4),[], % 1.37/1.73 product(a30,a1) = a29]. % 1.37/1.73 [41=param(33,5),[], % 1.37/1.73 product(a29,a3) = a28]. % 1.37/1.73 [42=param(33,6),[], % 1.37/1.73 product(a28,a21) = a27]. % 1.37/1.73 [43=param(33,7),[], % 1.37/1.73 product(a27,a1) = a26]. % 1.37/1.73 [44=param(33,8),[], % 1.37/1.73 product(a26,a23) = a25]. % 1.37/1.73 [45=param(33,9),[], % 1.37/1.73 product(a25,a3) = a24]. % 1.37/1.73 [46=param(33,10),[], % 1.37/1.73 product(a24,a21) = a23]. % 1.37/1.73 [47=param(33,11),[], % 1.37/1.73 product(a23,a31) = a22]. % 1.37/1.73 [48=param(33,12),[], % 1.37/1.73 product(a22,a25) = a21]. % 1.37/1.73 [49=param(33,13),[], % 1.37/1.73 product(a21,a29) = a20]. % 1.37/1.73 [50=param(33,14),[], % 1.37/1.73 product(a20,a11) = a19]. % 1.37/1.73 [51=param(33,15),[], % 1.37/1.73 product(a19,a15) = a18]. % 1.37/1.73 [52=param(33,16),[], % 1.37/1.73 product(a18,a9) = a17]. % 1.37/1.73 [53=param(33,17),[], % 1.37/1.73 product(a17,a19) = a16]. % 1.37/1.73 [54=param(33,18),[], % 1.37/1.73 product(a16,a5) = a15]. % 1.37/1.73 [55=param(33,19),[], % 1.37/1.73 product(a15,a17) = a14]. % 1.37/1.73 [56=param(33,20),[], % 1.37/1.73 product(a14,a7) = a13]. % 1.37/1.73 [57=param(33,21),[], % 1.37/1.73 product(a13,a19) = a12]. % 1.37/1.73 [58=param(33,22),[], % 1.37/1.73 product(a12,a5) = a11]. % 1.37/1.73 [59=param(33,23),[], % 1.37/1.73 product(a11,a7) = a10]. % 1.37/1.73 [60=param(33,24),[], % 1.37/1.73 product(a10,a17) = a9]. % 1.37/1.73 [61=param(33,25),[], % 1.37/1.73 product(a9,a5) = a8]. % 1.37/1.73 [62=param(33,26),[], % 1.37/1.73 product(a8,a19) = a7]. % 1.37/1.73 [63=param(33,27),[], % 1.37/1.73 product(a6,a15) = a5]. % 1.37/1.73 [64=param(33,28),[], % 1.37/1.73 product(a5,a11) = a4]. % 1.37/1.73 [65=param(33,29),[], % 1.37/1.73 product(a4,a29) = a3]. % 1.37/1.73 [66=param(33,30),[], % 1.37/1.73 product(a3,a25) = a2]. % 1.37/1.73 [67=param(33,31),[], % 1.37/1.73 product(a2,a31) = a1]. % 1.37/1.73 [68=param(32,1),[], % 1.37/1.73 product(product(a32,X10),product(a21,X10)) = product(a1,X10)]. % 1.37/1.73 [69=param(32,2),[], % 1.37/1.73 product(product(a31,X10),product(a3,X10)) = product(a32,X10)]. % 1.37/1.73 [70=param(32,3),[], % 1.37/1.73 product(product(a30,X10),product(a23,X10)) = product(a31,X10)]. % 1.37/1.73 [71=param(32,4),[], % 1.37/1.73 product(product(a29,X10),product(a1,X10)) = product(a30,X10)]. % 1.37/1.73 [72=param(32,5),[], % 1.37/1.73 product(product(a28,X10),product(a3,X10)) = product(a29,X10)]. % 1.37/1.73 [73=param(32,6),[], % 1.37/1.73 product(product(a27,X10),product(a21,X10)) = product(a28,X10)]. % 1.37/1.73 [74=param(32,7),[], % 1.37/1.73 product(product(a26,X10),product(a1,X10)) = product(a27,X10)]. % 1.37/1.73 [75=param(32,8),[], % 1.37/1.73 product(product(a25,X10),product(a23,X10)) = product(a26,X10)]. % 1.37/1.73 [76=param(32,9),[], % 1.37/1.73 product(product(a24,X10),product(a3,X10)) = product(a25,X10)]. % 1.37/1.73 [77=param(32,10),[], % 1.37/1.73 product(product(a23,X10),product(a21,X10)) = product(a24,X10)]. % 1.37/1.73 [78=param(32,11),[], % 1.37/1.73 product(product(a22,X10),product(a31,X10)) = product(a23,X10)]. % 1.37/1.73 [79=param(32,12),[], % 1.37/1.73 product(product(a21,X10),product(a25,X10)) = product(a22,X10)]. % 1.37/1.73 [80=param(32,13),[], % 1.37/1.73 product(product(a20,X10),product(a29,X10)) = product(a21,X10)]. % 1.37/1.73 [81=param(32,14),[], % 1.37/1.73 product(product(a19,X10),product(a11,X10)) = product(a20,X10)]. % 1.37/1.73 [82=param(32,15),[], % 1.37/1.73 product(product(a18,X10),product(a15,X10)) = product(a19,X10)]. % 1.37/1.73 [83=param(32,16),[], % 1.37/1.73 product(product(a17,X10),product(a9,X10)) = product(a18,X10)]. % 1.37/1.73 [84=param(32,17),[], % 1.37/1.73 product(product(a16,X10),product(a19,X10)) = product(a17,X10)]. % 1.37/1.73 [85=param(32,18),[], % 1.37/1.73 product(product(a15,X10),product(a5,X10)) = product(a16,X10)]. % 1.37/1.73 [86=param(32,19),[], % 1.37/1.73 product(product(a14,X10),product(a17,X10)) = product(a15,X10)]. % 1.37/1.73 [87=param(32,20),[], % 1.37/1.73 product(product(a13,X10),product(a7,X10)) = product(a14,X10)]. % 1.37/1.73 [88=param(32,21),[], % 1.37/1.73 product(product(a12,X10),product(a19,X10)) = product(a13,X10)]. % 1.37/1.73 [89=param(32,22),[], % 1.37/1.73 product(product(a11,X10),product(a5,X10)) = product(a12,X10)]. % 1.37/1.73 [90=param(32,23),[], % 1.37/1.73 product(product(a10,X10),product(a7,X10)) = product(a11,X10)]. % 1.37/1.73 [91=param(32,24),[], % 1.37/1.73 product(product(a9,X10),product(a17,X10)) = product(a10,X10)]. % 1.37/1.73 [92=param(32,25),[], % 1.37/1.73 product(product(a8,X10),product(a5,X10)) = product(a9,X10)]. % 1.37/1.73 [93=param(32,26),[], % 1.37/1.73 product(product(a7,X10),product(a19,X10)) = product(a8,X10)]. % 1.37/1.73 [94=param(32,27),[], % 1.37/1.73 product(product(a5,X10),product(a15,X10)) = product(a6,X10)]. % 1.37/1.73 [95=param(32,28),[], % 1.37/1.73 product(product(a4,X10),product(a11,X10)) = product(a5,X10)]. % 1.37/1.73 [96=param(32,29),[], % 1.37/1.73 product(product(a3,X10),product(a29,X10)) = product(a4,X10)]. % 1.37/1.73 [97=param(32,30),[], % 1.37/1.73 product(product(a2,X10),product(a25,X10)) = product(a3,X10)]. % 1.37/1.73 [98=param(32,31),[], % 1.37/1.73 product(product(a1,X10),product(a31,X10)) = product(a2,X10)]. % 1.37/1.73 [99=param(32,33),[], % 1.37/1.73 product(product(product(X10,X12),X11),product(X12,X11)) = product(X10,X11)]. % 1.37/1.73 [100=param(32,1),[], % 1.37/1.73 product(product(a32,X10),a21) = product(a1,product(X10,a21))]. % 1.37/1.73 [101=param(32,1),[], % 1.37/1.73 product(product(X10,a21),a1) = product(product(X10,a32),a21)]. % 1.37/1.73 [102=param(32,2),[], % 1.37/1.73 product(product(a31,X10),a3) = product(a32,product(X10,a3))]. % 1.37/1.73 [103=param(32,3),[], % 1.37/1.73 product(product(a30,X10),a23) = product(a31,product(X10,a23))]. % 1.37/1.73 [104=param(32,3),[], % 1.37/1.73 product(product(X10,a23),a31) = product(product(X10,a30),a23)]. % 1.37/1.73 [106=param(32,4),[32], % 1.37/1.73 product(product(X10,a29),a1) = product(product(X10,a30),product(a1,a30))]. % 1.37/1.73 [107=param(32,5),[], % 1.37/1.73 product(product(a28,X10),a3) = product(a29,product(X10,a3))]. % 1.37/1.73 [108=param(32,5),[32,29,32], % 1.37/1.73 product(product(X10,a4),product(a29,a4)) = product(product(X10,a28),a3)]. % 1.37/1.73 [111=param(32,7),[], % 1.37/1.73 product(product(a26,X10),a1) = product(a27,product(X10,a1))]. % 1.37/1.73 [112=param(32,7),[32], % 1.37/1.73 product(product(X10,a26),a1) = product(product(X10,a27),product(a1,a27))]. % 1.37/1.73 [114=param(32,9),[], % 1.37/1.73 product(product(a24,X10),a3) = product(a25,product(X10,a3))]. % 1.37/1.73 [115=param(32,9),[], % 1.37/1.73 product(product(X10,a3),a25) = product(product(X10,a24),a3)]. % 1.37/1.73 [116=param(32,10),[], % 1.37/1.73 product(product(a23,X10),a21) = product(a24,product(X10,a21))]. % 1.37/1.73 [117=param(32,10),[32], % 1.37/1.73 product(product(X10,a23),a21) = product(product(X10,a24),product(a21,a24))]. % 1.37/1.73 [118=param(32,11),[], % 1.37/1.73 product(product(a22,X10),a31) = product(a23,product(X10,a31))]. % 1.37/1.73 [119=param(32,11),[32,39,32], % 1.37/1.73 product(product(X10,a22),a31) = product(product(X10,a30),product(a23,a30))]. % 1.37/1.73 [120=param(32,12),[], % 1.37/1.73 product(product(a21,X10),a25) = product(a22,product(X10,a25))]. % 1.37/1.73 [121=param(32,12),[32], % 1.37/1.73 product(product(X10,a21),a25) = product(product(X10,a22),product(a25,a22))]. % 1.37/1.73 [122=param(32,13),[], % 1.37/1.73 product(product(a20,X10),a29) = product(a21,product(X10,a29))]. % 1.37/1.73 [125=param(32,14),[32], % 1.37/1.73 product(product(X10,a19),a11) = product(product(X10,a20),product(a11,a20))]. % 1.37/1.73 [126=param(32,15),[], % 1.37/1.73 product(product(a18,X10),a15) = product(a19,product(X10,a15))]. % 1.37/1.73 [127=param(32,15),[32], % 1.37/1.73 product(product(X10,a19),product(a15,a19)) = product(product(X10,a18),a15)]. % 1.37/1.73 [130=param(32,17),[], % 1.37/1.73 product(product(a16,X10),a19) = product(a17,product(X10,a19))]. % 1.37/1.73 [131=param(32,17),[32], % 1.37/1.73 product(product(X10,a17),product(a19,a17)) = product(product(X10,a16),a19)]. % 1.37/1.73 [132=param(32,18),[], % 1.37/1.73 product(product(a15,X10),a5) = product(a16,product(X10,a5))]. % 1.37/1.73 [134=param(32,19),[], % 1.37/1.73 product(product(a14,X10),a17) = product(a15,product(X10,a17))]. % 1.37/1.73 [135=param(32,19),[], % 1.37/1.73 product(product(X10,a17),a15) = product(product(X10,a14),a17)]. % 1.37/1.73 [138=param(32,21),[], % 1.37/1.73 product(product(a12,X10),a19) = product(a13,product(X10,a19))]. % 1.37/1.73 [140=param(32,22),[], % 1.37/1.73 product(product(a11,X10),a5) = product(a12,product(X10,a5))]. % 1.37/1.73 [141=param(32,23),[], % 1.37/1.73 product(product(a10,X10),a7) = product(a11,product(X10,a7))]. % 1.37/1.73 [143=param(32,24),[], % 1.37/1.73 product(product(a9,X10),a17) = product(a10,product(X10,a17))]. % 1.37/1.73 [144=param(32,25),[], % 1.37/1.73 product(product(a8,X10),a5) = product(a9,product(X10,a5))]. % 1.37/1.73 [146=param(32,26),[], % 1.37/1.73 product(product(a7,X10),a19) = product(a8,product(X10,a19))]. % 1.37/1.73 [147=param(32,27),[], % 1.37/1.73 product(product(a5,X10),a15) = product(a6,product(X10,a15))]. % 1.37/1.73 [149=param(32,29),[], % 1.37/1.73 product(product(a3,X10),a29) = product(a4,product(X10,a29))]. % 1.37/1.73 [150=param(32,30),[], % 1.37/1.73 product(product(a2,X10),a25) = product(a3,product(X10,a25))]. % 1.37/1.73 [151=param(32,31),[], % 1.37/1.73 product(product(a1,X10),a31) = product(a2,product(X10,a31))]. % 1.37/1.73 [152=param(32,33),[], % 1.37/1.73 product(product(product(X10,X12),X11),X12) = product(X10,product(X11,X12))]. % 1.37/1.73 [153=param(32,34),[], % 1.37/1.73 product(product(X10,X11),X10) = product(X10,product(X11,X10))]. % 1.37/1.73 [155=param(32,67),[], % 1.37/1.73 product(product(a2,X10),a31) = product(a1,product(X10,a31))]. % 1.37/1.73 [156=param(32,67),[], % 1.37/1.73 product(product(X10,a31),a1) = product(product(X10,a2),a31)]. % 1.37/1.73 [158=param(32,66),[], % 1.37/1.73 product(product(a3,X10),a25) = product(a2,product(X10,a25))]. % 1.37/1.73 [159=param(32,66),[115], % 1.37/1.73 product(product(X10,a25),a2) = product(product(X10,a24),a3)]. % 1.37/1.73 [160=param(32,37),[], % 1.37/1.73 product(product(a1,X10),product(a21,X10)) = product(a32,X10)]. % 1.37/1.73 [161=param(32,37),[], % 1.37/1.73 product(product(a1,X10),a21) = product(a32,product(X10,a21))]. % 1.37/1.73 [163=param(32,65),[], % 1.37/1.73 product(product(a4,X10),a29) = product(a3,product(X10,a29))]. % 1.37/1.73 [164=param(32,65),[], % 1.37/1.73 product(product(X10,a29),a3) = product(product(X10,a4),a29)]. % 1.37/1.73 [167=param(32,64),[], % 1.37/1.73 product(product(X10,a11),a4) = product(product(X10,a5),a11)]. % 1.37/1.73 [169=param(32,38),[], % 1.37/1.73 product(product(a32,X10),a3) = product(a31,product(X10,a3))]. % 1.37/1.73 [170=param(32,38),[], % 1.37/1.73 product(product(X10,a3),a31) = product(product(X10,a32),a3)]. % 1.37/1.73 [171=param(32,63),[], % 1.37/1.73 product(product(a6,X10),product(a15,X10)) = product(a5,X10)]. % 1.37/1.73 [172=param(32,63),[], % 1.37/1.73 product(product(a6,X10),a15) = product(a5,product(X10,a15))]. % 1.37/1.73 [175=param(32,62),[], % 1.37/1.73 product(product(a8,X10),a19) = product(a7,product(X10,a19))]. % 1.37/1.73 [176=param(32,62),[], % 1.37/1.73 product(product(X10,a19),a7) = product(product(X10,a8),a19)]. % 1.37/1.73 [177=param(32,39),[], % 1.37/1.73 product(product(a31,X10),product(a23,X10)) = product(a30,X10)]. % 1.37/1.73 [178=param(32,39),[], % 1.37/1.73 product(product(a31,X10),a23) = product(a30,product(X10,a23))]. % 1.37/1.73 [179=param(32,61),[], % 1.37/1.73 product(product(a9,X10),product(a5,X10)) = product(a8,X10)]. % 1.37/1.73 [180=param(32,61),[], % 1.37/1.73 product(product(a9,X10),a5) = product(a8,product(X10,a5))]. % 1.37/1.73 [181=param(32,61),[32], % 1.37/1.73 product(product(X10,a8),product(a5,a8)) = product(product(X10,a9),a5)]. % 1.37/1.73 [183=param(32,60),[], % 1.37/1.73 product(product(a10,X10),a17) = product(a9,product(X10,a17))]. % 1.37/1.73 [185=param(32,40),[], % 1.37/1.73 product(product(a30,X10),product(a1,X10)) = product(a29,X10)]. % 1.37/1.73 [187=param(32,40),[32], % 1.37/1.73 product(product(X10,a29),product(a1,a29)) = product(product(X10,a30),a1)]. % 1.37/1.73 [188=param(32,59),[], % 1.37/1.73 product(product(a11,X10),product(a7,X10)) = product(a10,X10)]. % 1.37/1.73 [190=param(32,58),[], % 1.37/1.73 product(product(a12,X10),product(a5,X10)) = product(a11,X10)]. % 1.37/1.73 [192=param(32,58),[], % 1.37/1.73 product(product(X10,a5),a11) = product(product(X10,a12),a5)]. % 1.37/1.73 [193=demod(167),[192], % 1.37/1.73 product(product(X10,a11),a4) = product(product(X10,a12),a5)]. % 1.37/1.73 [194=param(32,41),[], % 1.37/1.73 product(product(a29,X10),product(a3,X10)) = product(a28,X10)]. % 1.37/1.73 [195=param(32,41),[], % 1.37/1.73 product(product(a29,X10),a3) = product(a28,product(X10,a3))]. % 1.37/1.73 [196=param(32,41),[32,164], % 1.37/1.73 product(product(X10,a4),a29) = product(product(X10,a28),product(a3,a28))]. % 1.37/1.73 [200=param(32,57),[32], % 1.37/1.73 product(product(X10,a12),product(a19,a12)) = product(product(X10,a13),a19)]. % 1.37/1.73 [204=param(32,42),[], % 1.37/1.73 product(product(a28,X10),product(a21,X10)) = product(a27,X10)]. % 1.37/1.73 [206=param(32,42),[32], % 1.37/1.73 product(product(X10,a27),product(a21,a27)) = product(product(X10,a28),a21)]. % 1.37/1.73 [207=param(32,55),[], % 1.37/1.73 product(product(a15,X10),product(a17,X10)) = product(a14,X10)]. % 1.37/1.73 [210=param(32,54),[], % 1.37/1.73 product(product(a16,X10),a5) = product(a15,product(X10,a5))]. % 1.37/1.73 [211=param(32,54),[32,27,32], % 1.37/1.73 product(product(X10,a6),product(a15,a6)) = product(product(X10,a16),a5)]. % 1.37/1.73 [212=param(32,43),[], % 1.37/1.73 product(product(a27,X10),product(a1,X10)) = product(a26,X10)]. % 1.37/1.73 [213=param(32,43),[], % 1.37/1.73 product(product(a27,X10),a1) = product(a26,product(X10,a1))]. % 1.37/1.73 [214=param(32,43),[32], % 1.37/1.73 product(product(X10,a26),product(a1,a26)) = product(product(X10,a27),a1)]. % 1.37/1.73 [216=param(32,53),[], % 1.37/1.73 product(product(a17,X10),a19) = product(a16,product(X10,a19))]. % 1.37/1.73 [217=param(32,53),[32], % 1.37/1.73 product(product(X10,a17),a19) = product(product(X10,a16),product(a19,a16))]. % 1.37/1.73 [218=param(32,52),[], % 1.37/1.73 product(product(a18,X10),product(a9,X10)) = product(a17,X10)]. % 1.37/1.73 [219=param(32,52),[], % 1.37/1.73 product(product(a18,X10),a9) = product(a17,product(X10,a9))]. % 1.37/1.73 [220=param(32,52),[32,24,32], % 1.37/1.73 product(product(X10,a10),product(a17,a10)) = product(product(X10,a18),a9)]. % 1.37/1.73 [223=param(32,44),[], % 1.37/1.73 product(product(X10,a23),a25) = product(product(X10,a26),a23)]. % 1.37/1.73 [224=param(32,51),[], % 1.37/1.73 product(product(a19,X10),product(a15,X10)) = product(a18,X10)]. % 1.37/1.73 [225=param(32,51),[], % 1.37/1.73 product(product(a19,X10),a15) = product(a18,product(X10,a15))]. % 1.37/1.73 [228=param(32,50),[], % 1.37/1.73 product(product(a20,X10),a11) = product(a19,product(X10,a11))]. % 1.37/1.73 [230=param(32,45),[], % 1.37/1.73 product(product(a25,X10),product(a3,X10)) = product(a24,X10)]. % 1.37/1.73 [231=param(32,45),[], % 1.37/1.73 product(product(a25,X10),a3) = product(a24,product(X10,a3))]. % 1.37/1.73 [232=param(32,49),[], % 1.37/1.73 product(product(a21,X10),product(a29,X10)) = product(a20,X10)]. % 1.37/1.73 [234=param(32,49),[32], % 1.37/1.73 product(product(X10,a20),product(a29,a20)) = product(product(X10,a21),a29)]. % 1.37/1.73 [235=param(32,48),[], % 1.37/1.73 product(product(a22,X10),product(a25,X10)) = product(a21,X10)]. % 1.37/1.73 [236=param(32,48),[], % 1.37/1.73 product(product(a22,X10),a25) = product(a21,product(X10,a25))]. % 1.37/1.73 [238=param(32,46),[], % 1.37/1.73 product(product(a24,X10),product(a21,X10)) = product(a23,X10)]. % 1.37/1.73 [239=param(32,46),[], % 1.37/1.73 product(product(a24,X10),a21) = product(a23,product(X10,a21))]. % 1.37/1.73 [240=param(32,46),[32], % 1.37/1.73 product(product(X10,a23),product(a21,a23)) = product(product(X10,a24),a21)]. % 1.37/1.73 [242=param(32,47),[], % 1.37/1.73 product(product(a23,X10),a31) = product(a22,product(X10,a31))]. % 1.37/1.73 [243=param(32,47),[32,104], % 1.37/1.73 product(product(X10,a22),product(a31,a22)) = product(product(X10,a30),a23)]. % 1.37/1.73 [244=param(242,10),[], % 1.37/1.73 product(a22,product(a21,a31)) = product(a24,a31)]. % 1.37/1.73 [245=param(68,12),[32], % 1.37/1.73 product(product(a32,a22),product(a25,a22)) = product(a1,a25)]. % 1.37/1.73 [246=param(68,34),[], % 1.37/1.73 product(a1,a32) = product(a32,product(a21,a32))]. % 1.37/1.73 [247=param(68,38),[], % 1.37/1.73 product(a1,a3) = product(a31,product(a21,a3))]. % 1.37/1.73 [249=param(32,247),[], % 1.37/1.73 product(product(a1,X10),a3) = product(product(a31,product(a21,a3)),product(X10,a3))]. % 1.37/1.73 [251=param(32,246),[], % 1.37/1.73 product(product(a1,X10),a32) = product(product(a32,product(a21,a32)),product(X10,a32))]. % 1.37/1.73 [252=param(69,34),[], % 1.37/1.73 product(a31,product(a3,a31)) = product(a32,a31)]. % 1.37/1.73 [253=param(69,39),[], % 1.37/1.73 product(a30,product(a3,a23)) = product(a32,a23)]. % 1.37/1.73 [254=param(32,253),[], % 1.37/1.73 product(product(a30,X10),product(product(a3,a23),X10)) = product(product(a32,a23),X10)]. % 1.37/1.73 [257=param(70,10),[32], % 1.37/1.73 product(product(a30,a24),product(a21,a24)) = product(a31,a21)]. % 1.37/1.73 [258=param(70,34),[], % 1.37/1.73 product(a31,a30) = product(a30,product(a23,a30))]. % 1.37/1.73 [259=param(70,40),[], % 1.37/1.73 product(a31,a1) = product(a29,product(a23,a1))]. % 1.37/1.73 [263=param(32,259),[156], % 1.37/1.73 product(product(X10,a1),product(a29,product(a23,a1))) = product(product(X10,a2),a31)]. % 1.37/1.73 [268=param(71,31),[32], % 1.37/1.73 product(product(a29,a2),product(a31,a2)) = product(a30,a31)]. % 1.37/1.73 [269=param(71,34),[], % 1.37/1.73 product(a29,product(a1,a29)) = product(a30,a29)]. % 1.37/1.73 [270=param(71,37),[32], % 1.37/1.73 product(product(a29,a32),product(a21,a32)) = product(a30,a21)]. % 1.37/1.73 [273=param(32,269),[], % 1.37/1.73 product(product(a29,X10),product(product(a1,a29),X10)) = product(product(a30,a29),X10)]. % 1.37/1.73 [276=param(72,34),[], % 1.37/1.73 product(a28,product(a3,a28)) = product(a29,a28)]. % 1.37/1.73 [277=param(72,42),[], % 1.37/1.73 product(a27,product(a3,a21)) = product(a29,a21)]. % 1.37/1.73 [278=param(32,277),[], % 1.37/1.73 product(product(a27,X10),product(product(a3,a21),X10)) = product(product(a29,a21),X10)]. % 1.37/1.73 [281=param(73,12),[32], % 1.37/1.73 product(product(a27,a22),product(a25,a22)) = product(a28,a25)]. % 1.37/1.73 [282=param(73,34),[], % 1.37/1.73 product(a27,product(a21,a27)) = product(a28,a27)]. % 1.37/1.73 [283=param(73,43),[], % 1.37/1.73 product(a26,product(a21,a1)) = product(a28,a1)]. % 1.37/1.73 [291=param(74,44),[], % 1.37/1.73 product(a25,product(a1,a23)) = product(a27,a23)]. % 1.37/1.73 [300=param(75,45),[], % 1.37/1.73 product(a24,product(a23,a3)) = product(a26,a3)]. % 1.37/1.73 [302=param(32,300),[], % 1.37/1.73 product(product(a24,X10),product(product(a23,a3),X10)) = product(product(a26,a3),X10)]. % 1.37/1.73 [305=param(76,34),[], % 1.37/1.73 product(a25,a24) = product(a24,product(a3,a24))]. % 1.37/1.73 [307=param(76,46),[], % 1.37/1.73 product(a25,a21) = product(a23,product(a3,a21))]. % 1.37/1.73 [316=param(77,34),[], % 1.37/1.73 product(a23,product(a21,a23)) = product(a24,a23)]. % 1.37/1.73 [323=param(78,34),[], % 1.37/1.73 product(a22,product(a31,a22)) = product(a23,a22)]. % 1.37/1.73 [325=param(78,48),[], % 1.37/1.73 product(a21,product(a31,a25)) = product(a23,a25)]. % 1.37/1.73 [333=param(79,45),[32], % 1.37/1.73 product(product(a21,a24),product(a3,a24)) = product(a22,a3)]. % 1.37/1.73 [334=param(79,49),[], % 1.37/1.73 product(a20,product(a25,a29)) = product(a22,a29)]. % 1.37/1.73 [341=param(80,34),[], % 1.37/1.73 product(a20,product(a29,a20)) = product(a21,a20)]. % 1.37/1.73 [342=param(80,41),[32], % 1.37/1.73 product(product(a20,a28),product(a3,a28)) = product(a21,a3)]. % 1.37/1.73 [347=param(80,341),[], % 1.37/1.73 product(product(a21,a20),product(a29,product(a29,a20))) = product(a21,product(a29,a20))]. % 1.37/1.73 [359=param(82,55),[32], % 1.37/1.73 product(product(a18,a14),product(a17,a14)) = product(a19,a17)]. % 1.37/1.73 [364=param(83,24),[34], % 1.37/1.73 product(a17,a10) = product(a18,a17)]. % 1.37/1.73 [365=demod(220),[364], % 1.37/1.73 product(product(X10,a10),product(a18,a17)) = product(product(X10,a18),a9)]. % 1.37/1.73 [366=param(83,53),[], % 1.37/1.73 product(a16,product(a9,a19)) = product(a18,a19)]. % 1.37/1.73 [372=param(84,14),[32], % 1.37/1.73 product(product(a16,a20),product(a11,a20)) = product(a17,a11)]. % 1.37/1.73 [373=param(84,34),[], % 1.37/1.73 product(a16,product(a19,a16)) = product(a17,a16)]. % 1.37/1.73 [375=param(84,54),[], % 1.37/1.73 product(a15,product(a19,a5)) = product(a17,a5)]. % 1.37/1.73 [380=param(85,27),[34], % 1.37/1.73 product(a15,a6) = product(a16,a15)]. % 1.37/1.73 [381=demod(211),[380], % 1.37/1.73 product(product(X10,a6),product(a16,a15)) = product(product(X10,a16),a5)]. % 1.37/1.73 [382=param(85,55),[], % 1.37/1.73 product(a14,product(a5,a17)) = product(a16,a17)]. % 1.37/1.73 [392=param(86,34),[], % 1.37/1.73 product(a15,a14) = product(a14,product(a17,a14))]. % 1.37/1.73 [393=param(86,53),[32], % 1.37/1.73 product(product(a14,a16),product(a19,a16)) = product(a15,a19)]. % 1.37/1.73 [394=param(86,56),[], % 1.37/1.73 product(a15,a7) = product(a13,product(a17,a7))]. % 1.37/1.73 [396=param(32,394),[], % 1.37/1.73 product(product(a15,X10),product(a7,X10)) = product(product(a13,product(a17,a7)),X10)]. % 1.37/1.73 [402=param(82,392),[], % 1.37/1.73 product(product(a18,a14),product(a14,product(a17,a14))) = product(a19,a14)]. % 1.37/1.73 [404=param(87,26),[57], % 1.37/1.73 product(a12,a8) = product(a14,a19)]. % 1.37/1.73 [409=param(33,404),[32], % 1.37/1.73 product(product(a14,a8),product(a19,a8)) = a12]. % 1.37/1.73 [415=param(88,58),[], % 1.37/1.73 product(a11,product(a19,a5)) = product(a13,a5)]. % 1.37/1.73 [420=param(89,34),[64], % 1.37/1.73 product(a11,a4) = product(a12,a11)]. % 1.37/1.73 [424=param(32,420),[], % 1.37/1.73 product(product(a11,X10),a4) = product(product(a12,a11),product(X10,a4))]. % 1.37/1.73 [425=param(32,420),[193], % 1.37/1.73 product(product(X10,a4),product(a12,a11)) = product(product(X10,a12),a5)]. % 1.37/1.73 [426=param(81,420),[425], % 1.37/1.73 product(product(a19,a12),a5) = product(a20,a4)]. % 1.37/1.73 [428=param(32,426),[], % 1.37/1.73 product(product(product(a19,a12),X10),product(a5,X10)) = product(product(a20,a4),X10)]. % 1.37/1.73 [432=param(90,34),[], % 1.37/1.73 product(a11,a10) = product(a10,product(a7,a10))]. % 1.37/1.73 [442=param(91,16),[34], % 1.37/1.73 product(a9,a18) = product(a10,a9)]. % 1.37/1.73 [447=param(91,61),[], % 1.37/1.73 product(a8,product(a17,a5)) = product(a10,a5)]. % 1.37/1.73 [450=param(33,442),[32,442], % 1.37/1.73 product(product(a10,a18),product(a10,a9)) = a9]. % 1.37/1.73 [451=param(83,442),[34], % 1.37/1.73 product(product(a17,a18),product(a10,a9)) = a18]. % 1.37/1.73 [452=param(91,442),[], % 1.37/1.73 product(product(a10,a9),product(a17,a18)) = product(a10,a18)]. % 1.37/1.73 [455=param(92,62),[], % 1.37/1.73 product(a7,product(a5,a19)) = product(a9,a19)]. % 1.37/1.73 [461=param(93,34),[], % 1.37/1.73 product(a7,product(a19,a7)) = product(a8,a7)]. % 1.37/1.73 [472=param(94,55),[32], % 1.37/1.73 product(product(a5,a14),product(a17,a14)) = product(a6,a17)]. % 1.37/1.73 [487=param(95,65),[], % 1.37/1.73 product(a3,product(a11,a29)) = product(a5,a29)]. % 1.37/1.73 [496=param(96,34),[41], % 1.37/1.73 product(a3,a28) = product(a4,a3)]. % 1.37/1.73 [497=demod(342),[496], % 1.37/1.73 product(product(a20,a28),product(a4,a3)) = product(a21,a3)]. % 1.37/1.73 [500=demod(276),[496], % 1.37/1.73 product(a29,a28) = product(a28,product(a4,a3))]. % 1.37/1.73 [502=demod(196),[496], % 1.37/1.73 product(product(X10,a4),a29) = product(product(X10,a28),product(a4,a3))]. % 1.37/1.73 [503=param(96,66),[], % 1.37/1.73 product(a2,product(a29,a25)) = product(a4,a25)]. % 1.37/1.73 [505=param(32,496),[], % 1.37/1.73 product(product(a3,X10),product(a28,X10)) = product(product(a4,a3),X10)]. % 1.37/1.73 [506=param(32,496),[], % 1.37/1.73 product(product(a3,X10),a28) = product(product(a4,a3),product(X10,a28))]. % 1.37/1.73 [507=param(33,496),[32,496], % 1.37/1.73 product(product(a4,a28),product(a4,a3)) = a3]. % 1.37/1.73 [509=param(76,496),[], % 1.37/1.73 product(product(a24,a28),product(a4,a3)) = product(a25,a28)]. % 1.37/1.73 [510=param(96,496),[500], % 1.37/1.73 product(product(a4,a3),product(a28,product(a4,a3))) = product(a4,a28)]. % 1.37/1.73 [511=param(32,500),[], % 1.37/1.73 product(product(a29,X10),product(a28,X10)) = product(product(a28,product(a4,a3)),X10)]. % 1.37/1.73 [512=param(32,500),[], % 1.37/1.73 product(product(a29,X10),a28) = product(product(a28,product(a4,a3)),product(X10,a28))]. % 1.37/1.73 [513=param(71,500),[], % 1.37/1.73 product(product(a28,product(a4,a3)),product(a1,a28)) = product(a30,a28)]. % 1.37/1.73 [516=param(97,34),[], % 1.37/1.73 product(a2,product(a25,a2)) = product(a3,a2)]. % 1.37/1.73 [517=param(97,45),[32,34], % 1.37/1.73 product(product(a2,a24),product(a3,a24)) = a3]. % 1.37/1.73 [518=param(97,67),[], % 1.37/1.73 product(a1,product(a25,a31)) = product(a3,a31)]. % 1.37/1.73 [524=param(98,34),[259], % 1.37/1.73 product(a1,product(a29,product(a23,a1))) = product(a2,a1)]. % 1.37/1.73 [539=param(99,30),[32,30,32,45,32,32,153,9,66], % 1.37/1.73 product(product(product(X10,a24),a3),a2) = product(X10,a25)]. % 1.37/1.73 [540=param(99,34),[], % 1.37/1.73 product(product(X10,X11),product(X11,product(X10,X11))) = product(X10,product(X10,X11))]. % 1.37/1.73 [546=param(99,73),[], % 1.37/1.73 product(product(a28,X10),product(X10,product(a21,X10))) = product(a27,product(a21,X10))]. % 1.37/1.73 [561=param(99,88),[], % 1.37/1.73 product(product(a13,X10),product(X10,product(a19,X10))) = product(a12,product(a19,X10))]. % 1.37/1.73 [566=param(99,93),[], % 1.37/1.73 product(product(a8,X10),product(X10,product(a19,X10))) = product(a7,product(a19,X10))]. % 1.37/1.73 [590=param(99,461),[-32,176], % 1.37/1.73 product(product(product(X10,a8),a19),product(a8,a7)) = product(X10,product(a19,a7))]. % 1.37/1.73 [606=param(101,37),[246,100,153,1], % 1.37/1.73 product(a1,product(a21,a1)) = product(a32,a1)]. % 1.37/1.73 [607=param(32,606),[], % 1.37/1.73 product(product(a1,X10),product(product(a21,a1),X10)) = product(product(a32,a1),X10)]. % 1.37/1.73 [608=param(74,606),[283,-32], % 1.37/1.73 product(product(a28,a32),a1) = product(a27,product(a21,a1))]. % 1.37/1.73 [609=param(98,606),[], % 1.37/1.73 product(product(a32,a1),product(a31,product(a21,a1))) = product(a2,product(a21,a1))]. % 1.37/1.73 [613=param(102,252),[169,2,32,34,2], % 1.37/1.73 product(a31,a32) = product(a32,product(a3,a32))]. % 1.37/1.73 [626=param(33,608),[213,33], % 1.37/1.73 product(a26,a21) = product(a28,a32)]. % 1.37/1.73 [629=param(99,608),[32,-32], % 1.37/1.73 product(product(a27,product(a32,a1)),product(product(a21,a32),a1)) = product(a28,a1)]. % 1.37/1.73 [630=param(104,39),[258,103,153,3,47], % 1.37/1.73 product(a31,a22) = product(a30,a31)]. % 1.37/1.73 [634=demod(323),[630], % 1.37/1.73 product(a22,product(a30,a31)) = product(a23,a22)]. % 1.37/1.73 [635=demod(243),[630], % 1.37/1.73 product(product(X10,a22),product(a30,a31)) = product(product(X10,a30),a23)]. % 1.37/1.73 [641=param(102,630),[32,2,32], % 1.37/1.73 product(product(a30,a32),product(a3,a32)) = product(a32,product(a22,a3))]. % 1.37/1.73 [660=param(107,42),[], % 1.37/1.73 product(a29,product(a21,a3)) = product(a27,a3)]. % 1.37/1.73 [666=param(33,517),[], % 1.37/1.73 product(a2,a24) = product(a3,product(a3,a24))]. % 1.37/1.73 [668=param(108,34),[], % 1.37/1.73 product(product(a4,a28),a3) = product(a4,product(a29,a4))]. % 1.37/1.73 [684=param(668,32),[5,163,29], % 1.37/1.73 product(a3,a4) = product(a4,product(a29,a4))]. % 1.37/1.73 [691=param(111,44),[], % 1.37/1.73 product(a25,a1) = product(a27,product(a23,a1))]. % 1.37/1.73 [694=param(32,691),[], % 1.37/1.73 product(product(X10,a1),product(a27,product(a23,a1))) = product(product(X10,a25),a1)]. % 1.37/1.73 [696=param(33,507),[], % 1.37/1.73 product(a3,product(a4,a3)) = product(a4,a28)]. % 1.37/1.73 [697=param(99,507),[], % 1.37/1.73 product(a3,product(a28,product(a4,a3))) = product(a4,product(a4,a3))]. % 1.37/1.73 [698=param(99,507),[32,32,668,33,32,32,684,32,34,33,65,32,32,195,510], % 1.37/1.73 product(product(product(X10,a4),a3),product(a4,a28)) = product(X10,product(a4,a3))]. % 1.37/1.73 [699=param(112,33),[32], % 1.37/1.73 product(product(product(X10,a27),product(a26,a27)),product(a1,a27)) = product(X10,a1)]. % 1.37/1.73 [701=param(32,696),[], % 1.37/1.73 product(product(a3,X10),product(product(a4,a3),X10)) = product(product(a4,a28),X10)]. % 1.37/1.73 [702=param(96,696),[], % 1.37/1.73 product(product(a4,a28),product(a29,product(a4,a3))) = product(a4,product(a4,a3))]. % 1.37/1.73 [723=param(115,45),[305,114,153,9,66], % 1.37/1.73 product(a25,a2) = product(a24,a25)]. % 1.37/1.73 [727=demod(516),[723], % 1.37/1.73 product(a2,product(a24,a25)) = product(a3,a2)]. % 1.37/1.73 [730=param(32,723),[159], % 1.37/1.73 product(product(X10,a2),product(a24,a25)) = product(product(X10,a24),a3)]. % 1.37/1.73 [732=param(79,723),[730], % 1.37/1.73 product(product(a21,a24),a3) = product(a22,a2)]. % 1.37/1.73 [737=param(33,732),[32], % 1.37/1.73 product(product(a22,a3),product(a2,a3)) = product(a21,a24)]. % 1.37/1.73 [738=param(116,47),[], % 1.37/1.73 product(a24,product(a31,a21)) = product(a22,a21)]. % 1.37/1.73 [739=param(116,316),[239,10,117,34], % 1.37/1.73 product(a24,product(a21,a24)) = product(a23,a24)]. % 1.37/1.73 [743=param(32,738),[], % 1.37/1.73 product(product(a24,X10),product(product(a31,a21),X10)) = product(product(a22,a21),X10)]. % 1.37/1.73 [746=param(117,33),[32], % 1.37/1.73 product(product(product(X10,a24),product(a23,a24)),product(a21,a24)) = product(X10,a21)]. % 1.37/1.73 [753=param(118,104),[47], % 1.37/1.73 product(product(a22,a30),a23) = product(a23,a22)]. % 1.37/1.73 [756=param(33,753),[32,34], % 1.37/1.73 product(a23,product(a22,a23)) = product(a22,a30)]. % 1.37/1.73 [757=param(99,753),[3,119,34], % 1.37/1.73 product(a22,a23) = product(a23,a30)]. % 1.37/1.73 [758=demod(756),[757], % 1.37/1.73 product(a22,a30) = product(a23,product(a23,a30))]. % 1.37/1.73 [772=param(120,49),[], % 1.37/1.73 product(a22,product(a29,a25)) = product(a20,a25)]. % 1.37/1.73 [775=param(118,772),[], % 1.37/1.73 product(a23,product(product(a29,a25),a31)) = product(product(a20,a25),a31)]. % 1.37/1.73 [778=param(121,42),[], % 1.37/1.73 product(product(a28,a22),product(a25,a22)) = product(a27,a25)]. % 1.37/1.73 [785=param(122,50),[], % 1.37/1.73 product(a21,product(a11,a29)) = product(a19,a29)]. % 1.37/1.73 [796=param(120,785),[], % 1.37/1.73 product(a22,product(product(a11,a29),a25)) = product(product(a19,a29),a25)]. % 1.37/1.73 [807=param(125,33),[32], % 1.37/1.73 product(product(product(X10,a20),product(a19,a20)),product(a11,a20)) = product(X10,a11)]. % 1.37/1.73 [816=param(33,451),[], % 1.37/1.73 product(a17,a18) = product(a18,product(a10,a9))]. % 1.37/1.73 [817=demod(452),[816], % 1.37/1.73 product(product(a10,a9),product(a18,product(a10,a9))) = product(a10,a18)]. % 1.37/1.73 [826=param(127,17),[], % 1.37/1.73 product(product(a16,a18),a15) = product(a17,product(a15,a19))]. % 1.37/1.73 [829=param(33,127),[], % 1.37/1.73 product(product(product(X10,a18),a15),product(a15,a19)) = product(X10,a19)]. % 1.37/1.73 [830=param(127,53),[816,126], % 1.37/1.73 product(a19,product(product(a10,a9),a15)) = product(a16,product(a15,a19))]. % 1.37/1.73 [831=param(127,57),[], % 1.37/1.73 product(product(a13,a18),a15) = product(a12,product(a15,a19))]. % 1.37/1.73 [832=param(127,62),[], % 1.37/1.73 product(product(a8,a18),a15) = product(a7,product(a15,a19))]. % 1.37/1.73 [843=param(130,373),[216,17,153,17], % 1.37/1.73 product(a17,product(a19,a17)) = product(a16,a17)]. % 1.37/1.73 [845=param(83,843),[], % 1.37/1.73 product(product(a16,a17),product(a9,product(a19,a17))) = product(a18,product(a19,a17))]. % 1.37/1.73 [846=param(99,843),[131], % 1.37/1.73 product(product(product(X10,a16),a19),product(a16,a17)) = product(X10,product(a19,a17))]. % 1.37/1.73 [849=param(131,19),[], % 1.37/1.73 product(product(a14,a16),a19) = product(a15,product(a19,a17))]. % 1.37/1.73 [850=param(131,24),[], % 1.37/1.73 product(product(a9,a16),a19) = product(a10,product(a19,a17))]. % 1.37/1.73 [851=param(33,131),[], % 1.37/1.73 product(product(product(X10,a16),a19),product(a19,a17)) = product(X10,a17)]. % 1.37/1.73 [853=param(131,60),[], % 1.37/1.73 product(product(a10,a16),a19) = product(a9,product(a19,a17))]. % 1.37/1.73 [854=param(33,853),[32,217,34], % 1.37/1.73 product(product(a9,a19),product(a19,a16)) = product(a10,a16)]. % 1.37/1.73 [855=param(33,850),[32,217,34], % 1.37/1.73 product(product(a10,a19),product(a19,a16)) = product(a9,a16)]. % 1.37/1.73 [858=param(132,394),[32], % 1.37/1.73 product(product(a13,a5),product(product(a17,a7),a5)) = product(a16,product(a7,a5))]. % 1.37/1.73 [863=param(134,56),[], % 1.37/1.73 product(a15,product(a7,a17)) = product(a13,a17)]. % 1.37/1.73 [870=param(135,126),[], % 1.37/1.73 product(product(a18,a14),a17) = product(a19,product(a17,a15))]. % 1.37/1.73 [874=param(33,870),[32,32,34,55], % 1.37/1.73 product(product(a19,a17),product(a17,a14)) = product(a18,a14)]. % 1.37/1.73 [903=param(33,450),[], % 1.37/1.73 product(a9,product(a10,a9)) = product(a10,a18)]. % 1.37/1.73 [904=param(99,450),[], % 1.37/1.73 product(a9,product(a18,product(a10,a9))) = product(a10,product(a10,a9))]. % 1.37/1.73 [908=param(140,59),[], % 1.37/1.73 product(a12,product(a7,a5)) = product(a10,a5)]. % 1.37/1.73 [917=param(138,908),[32,146], % 1.37/1.73 product(product(a10,a19),product(a5,a19)) = product(a13,product(a8,product(a5,a19)))]. % 1.37/1.73 [918=param(141,60),[], % 1.37/1.73 product(a11,product(a17,a7)) = product(a9,a7)]. % 1.37/1.73 [923=param(140,918),[180], % 1.37/1.73 product(a12,product(product(a17,a7),a5)) = product(a8,product(a7,a5))]. % 1.37/1.73 [945=param(143,442),[183,24], % 1.37/1.73 product(a9,a10) = product(a10,product(a18,a17))]. % 1.37/1.73 [948=param(143,903),[183,183,24,945], % 1.37/1.73 product(a9,product(a18,a17)) = product(a10,product(a10,product(a18,a17)))]. % 1.37/1.73 [954=param(144,62),[], % 1.37/1.73 product(a7,a5) = product(a9,product(a19,a5))]. % 1.37/1.73 [955=demod(923),[954], % 1.37/1.73 product(a12,product(product(a17,a7),a5)) = product(a8,product(a9,product(a19,a5)))]. % 1.37/1.73 [959=demod(858),[954], % 1.37/1.73 product(product(a13,a5),product(product(a17,a7),a5)) = product(a16,product(a9,product(a19,a5)))]. % 1.37/1.73 [961=param(32,954),[], % 1.37/1.73 product(product(a7,X10),product(a5,X10)) = product(product(a9,product(a19,a5)),X10)]. % 1.37/1.73 [966=param(32,954),[], % 1.37/1.73 product(product(X10,a5),product(a9,product(a19,a5))) = product(product(X10,a7),a5)]. % 1.37/1.73 [977=param(146,461),[175,26,32,34,26], % 1.37/1.73 product(a7,a8) = product(a8,product(a19,a8))]. % 1.37/1.73 [980=param(87,977),[561], % 1.37/1.73 product(a12,product(a19,a8)) = product(a14,a8)]. % 1.37/1.73 [986=param(147,135),[], % 1.37/1.73 product(product(a5,a14),a17) = product(a6,product(a17,a15))]. % 1.37/1.73 [1009=param(149,66),[], % 1.37/1.73 product(a2,a29) = product(a4,product(a25,a29))]. % 1.37/1.73 [1010=param(149,496),[163,29,684], % 1.37/1.73 product(a4,product(a29,a4)) = product(a4,product(a28,a29))]. % 1.37/1.73 [1017=demod(684),[1010], % 1.37/1.73 product(a3,a4) = product(a4,product(a28,a29))]. % 1.37/1.73 [1019=param(149,696),[163,163,29,1017], % 1.37/1.73 product(a3,product(a28,a29)) = product(a4,product(a4,product(a28,a29)))]. % 1.37/1.73 [1023=param(150,67),[], % 1.37/1.73 product(a1,a25) = product(a3,product(a31,a25))]. % 1.37/1.73 [1024=demod(245),[1023], % 1.37/1.73 product(product(a32,a22),product(a25,a22)) = product(a3,product(a31,a25))]. % 1.37/1.73 [1026=param(150,727),[158,30,33], % 1.37/1.73 product(a2,a3) = product(a3,a24)]. % 1.37/1.73 [1027=demod(737),[1026], % 1.37/1.73 product(product(a22,a3),product(a3,a24)) = product(a21,a24)]. % 1.37/1.73 [1030=param(32,1026),[], % 1.37/1.73 product(product(a2,X10),a3) = product(product(a3,a24),product(X10,a3))]. % 1.37/1.73 [1035=param(74,1023),[], % 1.37/1.73 product(product(a26,a25),product(a3,product(a31,a25))) = product(a27,a25)]. % 1.37/1.73 [1038=param(151,247),[32,34,170], % 1.37/1.73 product(a31,product(product(a21,a32),a3)) = product(a2,product(a3,a31))]. % 1.37/1.73 [1053=param(152,732),[32,666], % 1.37/1.73 product(product(a22,a24),product(a3,product(a3,a24))) = product(a21,product(a3,a24))]. % 1.37/1.73 [1054=param(152,870),[32,32,392,540], % 1.37/1.73 product(product(a19,a14),product(a17,product(a17,a14))) = product(a18,product(a17,a14))]. % 1.37/1.73 [1057=param(153,41),[29], % 1.37/1.73 product(a29,a4) = product(a28,a29)]. % 1.37/1.73 [1061=demod(108),[1057], % 1.37/1.73 product(product(X10,a4),product(a28,a29)) = product(product(X10,a28),a3)]. % 1.37/1.73 [1062=param(153,43),[], % 1.37/1.73 product(a27,product(a1,a27)) = product(a26,a27)]. % 1.37/1.73 [1067=param(153,246),[32], % 1.37/1.73 product(product(a32,a1),product(product(a21,a32),a1)) = product(a1,product(a32,a1))]. % 1.37/1.73 [1068=param(153,258),[32,242,634], % 1.37/1.73 product(product(a30,a31),product(a23,a22)) = product(a31,product(a30,a31))]. % 1.37/1.73 [1069=param(153,259),[32,242,31,31], % 1.37/1.73 product(product(a29,a31),product(a22,a2)) = product(a31,a2)]. % 1.37/1.73 [1071=param(153,291),[223,223], % 1.37/1.73 product(a25,product(product(a1,a26),a23)) = product(product(a27,a26),a23)]. % 1.37/1.73 [1072=param(153,305),[32,158,727], % 1.37/1.73 product(product(a24,a25),product(a3,a2)) = product(a25,product(a24,a25))]. % 1.37/1.73 [1074=param(153,334),[32,234,32,234,307,32,149,49], % 1.37/1.73 product(product(a22,a21),a29) = product(a20,product(product(a23,a29),product(a4,a20)))]. % 1.37/1.73 [1078=param(153,375),[32,27,32,380,381,225,27], % 1.37/1.73 product(product(a17,a16),a5) = product(a15,product(a18,a6))]. % 1.37/1.73 [1079=param(153,382),[32,32,472], % 1.37/1.73 product(product(a16,a14),product(a17,a14)) = product(a14,product(a6,a17))]. % 1.37/1.73 [1082=param(153,404),[32,200], % 1.37/1.73 product(product(a14,a13),a19) = product(a12,product(a8,a12))]. % 1.37/1.73 [1084=param(153,432),[32], % 1.37/1.73 product(product(a10,a11),product(product(a7,a10),a11)) = product(a11,product(a10,a11))]. % 1.37/1.73 [1086=param(153,447),[32,181,32,181,16], % 1.37/1.73 product(product(a10,a9),a5) = product(a8,product(a18,a5))]. % 1.37/1.73 [1087=param(153,455),[176,176], % 1.37/1.73 product(a7,product(product(a5,a8),a19)) = product(product(a9,a8),a19)]. % 1.37/1.73 [1089=param(153,500),[32,163,29,1017], % 1.37/1.73 product(product(a28,a29),product(a4,product(a28,a29))) = product(a29,product(a28,a29))]. % 1.37/1.73 [1091=param(153,518),[156,156,723], % 1.37/1.73 product(product(a3,a2),a31) = product(a1,product(product(a24,a25),a31))]. % 1.37/1.73 [1142=param(155,503),[], % 1.37/1.73 product(a1,product(product(a29,a25),a31)) = product(product(a4,a25),a31)]. % 1.37/1.73 [1173=param(158,487),[], % 1.37/1.73 product(a2,product(product(a11,a29),a25)) = product(product(a5,a29),a25)]. % 1.37/1.73 [1178=param(159,48),[], % 1.37/1.73 product(product(a22,a24),a3) = product(a21,a2)]. % 1.37/1.73 [1182=param(33,1178),[32,1026], % 1.37/1.73 product(product(a21,a3),product(a3,a24)) = product(a22,a24)]. % 1.37/1.73 [1187=param(160,606),[], % 1.37/1.73 product(product(a32,a1),product(a21,product(a21,a1))) = product(a32,product(a21,a1))]. % 1.37/1.73 [1241=param(171,55),[32], % 1.37/1.73 product(product(a6,a14),product(a17,a14)) = product(a5,a17)]. % 1.37/1.73 [1249=param(172,135),[], % 1.37/1.73 product(product(a6,a14),a17) = product(a5,product(a17,a15))]. % 1.37/1.73 [1250=param(33,1249),[32,32,34,55], % 1.37/1.73 product(product(a5,a17),product(a17,a14)) = product(a6,a14)]. % 1.37/1.73 [1251=param(152,1249),[32,32,392,540], % 1.37/1.73 product(product(a5,a14),product(a17,product(a17,a14))) = product(a6,product(a17,a14))]. % 1.37/1.73 [1262=param(236,244),[32,120], % 1.37/1.73 product(product(a24,a25),product(a31,a25)) = product(a21,product(a22,product(a31,a25)))]. % 1.37/1.73 [1263=param(236,634),[32], % 1.37/1.73 product(product(a23,a22),a25) = product(a21,product(product(a30,a25),product(a31,a25)))]. % 1.37/1.73 [1266=param(175,447),[32,917,216], % 1.37/1.73 product(a7,product(a16,product(a5,a19))) = product(a13,product(a8,product(a5,a19)))]. % 1.37/1.73 [1269=param(176,33),[32,32,153,62], % 1.37/1.73 product(product(product(X10,a8),a19),product(a19,a7)) = product(X10,a7)]. % 1.37/1.73 [1278=param(177,630),[1068], % 1.37/1.73 product(a31,product(a30,a31)) = product(a30,a22)]. % 1.37/1.73 [1283=param(102,1278),[32,2,32,641], % 1.37/1.73 product(product(a30,a22),a3) = product(a32,product(a32,product(a22,a3)))]. % 1.37/1.73 [1286=param(152,228),[32,153], % 1.37/1.73 product(product(a19,X10),product(X10,product(a11,X10))) = product(a20,product(a11,X10))]. % 1.37/1.73 [1287=param(178,613),[32], % 1.37/1.73 product(product(a32,a23),product(product(a3,a32),a23)) = product(a30,product(a32,a23))]. % 1.37/1.73 [1291=param(225,135),[], % 1.37/1.73 product(product(a19,a14),a17) = product(a18,product(a17,a15))]. % 1.37/1.73 [1293=param(99,179),[], % 1.37/1.73 product(product(a8,X10),product(X10,product(a5,X10))) = product(a9,product(a5,X10))]. % 1.37/1.73 [1300=param(33,1291),[32,32,34,55], % 1.37/1.73 product(product(a18,a17),product(a17,a14)) = product(a19,a14)]. % 1.37/1.73 [1327=param(216,816),[32], % 1.37/1.73 product(product(a18,a19),product(product(a10,a9),a19)) = product(a16,product(a18,a19))]. % 1.37/1.73 [1335=param(185,246),[], % 1.37/1.73 product(product(a30,a32),product(a32,product(a21,a32))) = product(a29,a32)]. % 1.37/1.73 [1344=param(210,366),[180], % 1.37/1.73 product(product(a18,a19),a5) = product(a15,product(a8,product(a19,a5)))]. % 1.37/1.73 [1358=param(187,29),[], % 1.37/1.73 product(product(a3,a30),a1) = product(a4,product(a1,a29))]. % 1.37/1.73 [1360=param(187,65),[], % 1.37/1.73 product(product(a4,a30),a1) = product(a3,product(a1,a29))]. % 1.37/1.73 [1361=param(187,1009),[], % 1.37/1.73 product(product(a2,a30),a1) = product(product(a4,product(a25,a29)),product(a1,a29))]. % 1.37/1.73 [1362=param(33,1360),[32,106,34], % 1.37/1.73 product(product(a3,a1),product(a1,a30)) = product(a4,a30)]. % 1.37/1.73 [1366=param(188,415),[], % 1.37/1.73 product(product(a13,a5),product(a7,product(a19,a5))) = product(a10,product(a19,a5))]. % 1.37/1.73 [1369=param(188,977),[], % 1.37/1.73 product(product(a11,a8),product(a8,product(a19,a8))) = product(a10,a8)]. % 1.37/1.73 [1371=param(33,1358),[32,106,34], % 1.37/1.73 product(product(a4,a1),product(a1,a30)) = product(a3,a30)]. % 1.37/1.73 [1381=param(99,190),[], % 1.37/1.73 product(product(a11,X10),product(X10,product(a5,X10))) = product(a12,product(a5,X10))]. % 1.37/1.73 [1398=param(194,1017),[1057,1089], % 1.37/1.73 product(a29,product(a28,a29)) = product(a28,a4)]. % 1.37/1.73 [1404=param(195,1398),[107,107,41,500], % 1.37/1.73 product(a29,product(a4,a3)) = product(a28,product(a28,product(a4,a3)))]. % 1.37/1.73 [1405=demod(702),[1404], % 1.37/1.73 product(product(a4,a28),product(a28,product(a28,product(a4,a3)))) = product(a4,product(a4,a3))]. % 1.37/1.73 [1419=param(99,1371),[], % 1.37/1.73 product(product(a3,a30),product(a1,product(a1,a30))) = product(a4,product(a1,a30))]. % 1.37/1.73 [1424=param(99,1362),[], % 1.37/1.73 product(product(a4,a30),product(a1,product(a1,a30))) = product(a3,product(a1,a30))]. % 1.37/1.73 [1428=param(207,364),[365], % 1.37/1.73 product(product(a15,a18),a9) = product(a14,a10)]. % 1.37/1.73 [1429=param(207,375),[], % 1.37/1.73 product(product(a17,a5),product(a17,product(a19,a5))) = product(a14,product(a19,a5))]. % 1.37/1.73 [1431=param(207,816),[], % 1.37/1.73 product(product(a15,a18),product(a18,product(a10,a9))) = product(a14,a18)]. % 1.37/1.73 [1436=param(33,1428),[], % 1.37/1.73 product(product(a14,a10),a9) = product(a15,a18)]. % 1.37/1.73 [1440=param(152,1436),[945], % 1.37/1.73 product(product(a15,a18),a10) = product(a14,product(a10,product(a18,a17)))]. % 1.37/1.73 [1447=param(212,31),[32], % 1.37/1.73 product(product(a27,a2),product(a31,a2)) = product(a26,a31)]. % 1.37/1.73 [1454=param(33,1447),[], % 1.37/1.73 product(product(a26,a31),product(a31,a2)) = product(a27,a2)]. % 1.37/1.73 [1472=param(218,945),[364], % 1.37/1.73 product(product(a18,a10),product(a10,product(a18,a17))) = product(a18,a17)]. % 1.37/1.73 [1478=param(224,55),[32], % 1.37/1.73 product(product(a19,a14),product(a17,a14)) = product(a18,a17)]. % 1.37/1.73 [1480=param(224,380),[381], % 1.37/1.73 product(product(a19,a16),a5) = product(a18,a6)]. % 1.37/1.73 [1508=param(230,496),[], % 1.37/1.73 product(product(a25,a28),product(a4,a3)) = product(a24,a28)]. % 1.37/1.73 [1511=param(230,723),[1072], % 1.37/1.73 product(a25,product(a24,a25)) = product(a24,a2)]. % 1.37/1.73 [1521=param(231,1511),[114,1026,114,45,305], % 1.37/1.73 product(a25,product(a3,a24)) = product(a24,product(a24,product(a3,a24)))]. % 1.37/1.73 [1523=param(232,41),[32,496], % 1.37/1.73 product(product(a21,a28),product(a4,a3)) = product(a20,a3)]. % 1.37/1.73 [1525=param(232,500),[], % 1.37/1.73 product(product(a21,a28),product(a28,product(a4,a3))) = product(a20,a28)]. % 1.37/1.73 [1527=param(232,1057),[1061], % 1.37/1.73 product(product(a21,a28),a3) = product(a20,a4)]. % 1.37/1.73 [1537=param(99,1523),[], % 1.37/1.73 product(product(a20,a3),product(a28,product(a4,a3))) = product(a21,product(a4,a3))]. % 1.37/1.73 [1541=param(235,305),[], % 1.37/1.73 product(product(a22,a24),product(a24,product(a3,a24))) = product(a21,a24)]. % 1.37/1.73 [1553=param(238,739),[], % 1.37/1.73 product(product(a23,a24),product(a21,product(a21,a24))) = product(a23,product(a21,a24))]. % 1.37/1.73 [1557=param(240,3),[], % 1.37/1.73 product(product(a30,a24),a21) = product(a31,product(a21,a23))]. % 1.37/1.73 [1558=param(240,39),[], % 1.37/1.73 product(product(a31,a24),a21) = product(a30,product(a21,a23))]. % 1.37/1.73 [1560=param(240,757),[], % 1.37/1.73 product(product(a22,a24),a21) = product(product(a23,a30),product(a21,a23))]. % 1.37/1.73 [1561=param(33,1558),[32,117,34], % 1.37/1.73 product(product(a30,a21),product(a21,a24)) = product(a31,a24)]. % 1.37/1.73 [1562=param(33,1557),[32,117,34], % 1.37/1.73 product(product(a31,a21),product(a21,a24)) = product(a30,a24)]. % 1.37/1.73 [1571=param(33,1560),[32,116,117,34], % 1.37/1.73 product(product(a24,product(a30,a21)),product(a21,a24)) = product(a22,a24)]. % 1.37/1.73 [1572=param(249,1023),[32,34,102,45,45,32,32,333], % 1.37/1.73 product(product(a31,a24),product(a22,a3)) = product(a3,product(a32,a24))]. % 1.37/1.73 [1573=param(99,1508),[], % 1.37/1.73 product(product(a24,a28),product(a28,product(a4,a3))) = product(a25,product(a4,a3))]. % 1.37/1.73 [1577=param(251,606),[32,34,246,32,246,540,-32,1], % 1.37/1.73 product(a1,product(a21,a32)) = product(a32,product(a32,product(a21,a32)))]. % 1.37/1.73 [1579=param(161,1577),[100,100,153,1,606,153,1], % 1.37/1.73 product(a1,product(a32,a1)) = product(a32,product(a21,a1))]. % 1.37/1.73 [1580=demod(1067),[1579], % 1.37/1.73 product(product(a32,a1),product(product(a21,a32),a1)) = product(a32,product(a21,a1))]. % 1.37/1.73 [1585=param(254,149),[], % 1.37/1.73 product(product(a30,a29),product(a4,product(a23,a29))) = product(product(a32,a23),a29)]. % 1.37/1.73 [1607=param(263,691),[-32,723], % 1.37/1.73 product(product(a24,a25),a31) = product(product(a27,a29),product(a23,a1))]. % 1.37/1.73 [1608=demod(1091),[1607], % 1.37/1.73 product(product(a3,a2),a31) = product(a1,product(product(a27,a29),product(a23,a1)))]. % 1.37/1.73 [1612=param(99,1241),[], % 1.37/1.73 product(product(a5,a17),product(a14,product(a17,a14))) = product(a6,product(a17,a14))]. % 1.37/1.73 [1636=param(273,160),[49,49,32,234], % 1.37/1.73 product(product(a29,a20),product(a32,a29)) = product(product(a30,a21),a29)]. % 1.37/1.73 [1650=param(278,149),[49,153,49], % 1.37/1.73 product(product(a27,a29),product(a4,a20)) = product(a29,a20)]. % 1.37/1.73 [1651=param(99,1650),[], % 1.37/1.73 product(product(a29,a20),product(a29,product(a4,a20))) = product(a27,product(a4,a20))]. % 1.37/1.73 [1652=param(33,281),[], % 1.37/1.73 product(product(a28,a25),product(a25,a22)) = product(a27,a22)]. % 1.37/1.73 [1655=param(152,1652),[153,48,307], % 1.37/1.73 product(product(a27,a22),a25) = product(a28,product(a23,product(a3,a21)))]. % 1.37/1.73 [1670=param(153,1019),[32,32,107,41,500,510,107,41,500,697], % 1.37/1.73 product(product(a4,a3),product(a4,a28)) = product(a4,product(a4,a3))]. % 1.37/1.73 [1677=param(153,948),[32,32,219,16,816,817,219,16,816,904], % 1.37/1.73 product(product(a10,a9),product(a10,a18)) = product(a10,product(a10,a9))]. % 1.37/1.73 [1680=param(302,77),[9,32,115,732,-32,626,107,38], % 1.37/1.73 product(product(a24,a25),product(a22,a2)) = product(a29,a31)]. % 1.37/1.73 [1684=param(33,1680),[1069], % 1.37/1.73 product(a31,a2) = product(a24,a25)]. % 1.37/1.73 [1697=demod(1454),[1684], % 1.37/1.73 product(product(a26,a31),product(a24,a25)) = product(a27,a2)]. % 1.37/1.73 [1699=demod(1447),[1684,730], % 1.37/1.73 product(product(a27,a24),a3) = product(a26,a31)]. % 1.37/1.73 [1711=demod(268),[1684,730,195,9], % 1.37/1.73 product(a28,a25) = product(a30,a31)]. % 1.37/1.73 [1721=param(32,1711),[], % 1.37/1.73 product(product(a28,X10),product(a25,X10)) = product(product(a30,a31),X10)]. % 1.37/1.73 [1722=demod(778),[1721,32,630,635,34,3], % 1.37/1.73 product(a27,a25) = a31]. % 1.37/1.73 [1726=demod(1035),[1722], % 1.37/1.73 product(product(a26,a25),product(a3,product(a31,a25))) = a31]. % 1.37/1.74 [1731=param(33,1711),[32], % 1.37/1.74 product(product(a30,a25),product(a31,a25)) = a28]. % 1.37/1.74 [1732=demod(1263),[1731], % 1.37/1.74 product(product(a23,a22),a25) = product(a21,a28)]. % 1.37/1.74 [1745=param(107,1711),[32,2,32,641,45], % 1.37/1.74 product(a29,a24) = product(a32,product(a22,a3))]. % 1.37/1.74 [1755=param(32,1722),[], % 1.37/1.74 product(product(a27,X10),a25) = product(a31,product(X10,a25))]. % 1.37/1.74 [1756=demod(1655),[1755,48], % 1.37/1.74 product(a31,a21) = product(a28,product(a23,product(a3,a21)))]. % 1.37/1.74 [1759=demod(1562),[1756,32,32], % 1.37/1.74 product(product(a28,product(a21,a24)),product(product(a23,product(a21,a24)),product(product(a3,a21),product(a21,a24)))) = product(a30,a24)]. % 1.37/1.74 [1765=demod(743),[1756], % 1.37/1.74 product(product(a24,X10),product(product(a28,product(a23,product(a3,a21))),X10)) = product(product(a22,a21),X10)]. % 1.37/1.74 [1774=demod(257),[1756], % 1.37/1.74 product(product(a30,a24),product(a21,a24)) = product(a28,product(a23,product(a3,a21)))]. % 1.37/1.74 [1775=param(32,1722),[], % 1.37/1.74 product(product(X10,a25),a31) = product(product(X10,a27),a25)]. % 1.37/1.74 [1776=demod(775),[1775,1775], % 1.37/1.74 product(a23,product(product(a29,a27),a25)) = product(product(a20,a27),a25)]. % 1.37/1.74 [1777=demod(1142),[1775,1775], % 1.37/1.74 product(a1,product(product(a29,a27),a25)) = product(product(a4,a27),a25)]. % 1.37/1.74 [1778=demod(1607),[1775], % 1.37/1.74 product(product(a24,a27),a25) = product(product(a27,a29),product(a23,a1))]. % 1.37/1.74 [1780=param(33,1722),[], % 1.37/1.74 product(a31,a25) = a27]. % 1.37/1.74 [1782=demod(1726),[1780], % 1.37/1.74 product(product(a26,a25),product(a3,a27)) = a31]. % 1.37/1.74 [1788=demod(1262),[1780,32,1780], % 1.37/1.74 product(product(a24,a27),product(a25,a27)) = product(a21,product(a22,a27))]. % 1.37/1.74 [1795=demod(1024),[1780], % 1.37/1.74 product(product(a32,a22),product(a25,a22)) = product(a3,a27)]. % 1.37/1.74 [1798=demod(325),[1780], % 1.37/1.74 product(a21,a27) = product(a23,a25)]. % 1.37/1.74 [1806=demod(282),[1798], % 1.37/1.74 product(a27,product(a23,a25)) = product(a28,a27)]. % 1.37/1.74 [1807=demod(206),[1798], % 1.37/1.74 product(product(X10,a27),product(a23,a25)) = product(product(X10,a28),a21)]. % 1.37/1.74 [1809=param(159,1722),[1684,1699], % 1.37/1.74 product(a24,a25) = product(a26,a31)]. % 1.37/1.74 [1816=demod(1697),[1809,-32,34], % 1.37/1.74 product(a26,a31) = product(a27,a2)]. % 1.37/1.74 [1822=demod(1809),[1816], % 1.37/1.74 product(a24,a25) = product(a27,a2)]. % 1.37/1.74 [1862=demod(730),[1822,-32], % 1.37/1.74 product(product(X10,a24),a3) = product(product(X10,a27),a2)]. % 1.37/1.74 [1865=demod(539),[1862,33], % 1.37/1.74 product(X10,a25) = product(X10,a27)]. % 1.37/1.74 [1866=demod(12),[1865], % 1.37/1.74 product(a21,a27) = a22]. % 1.37/1.74 [1867=demod(30),[1865], % 1.37/1.74 product(a2,a27) = a3]. % 1.37/1.74 [1868=demod(48),[1865], % 1.37/1.74 product(a22,a27) = a21]. % 1.37/1.74 [1870=demod(1788),[1868,34], % 1.37/1.74 product(product(a24,a27),product(a25,a27)) = a21]. % 1.37/1.74 [1871=demod(66),[1865], % 1.37/1.74 product(a3,a27) = a2]. % 1.37/1.74 [1872=demod(1795),[1871], % 1.37/1.74 product(product(a32,a22),product(a25,a22)) = a2]. % 1.37/1.74 [1874=demod(121),[1865,32,1866], % 1.37/1.74 product(product(X10,a22),product(a25,a22)) = product(product(X10,a27),a22)]. % 1.37/1.74 [1875=demod(1872),[1874], % 1.37/1.74 product(product(a32,a27),a22) = a2]. % 1.37/1.74 [1877=demod(223),[1865,32], % 1.37/1.74 product(product(X10,a26),a23) = product(product(X10,a27),product(a23,a27))]. % 1.37/1.74 [1878=demod(1071),[1877,1877,34], % 1.37/1.74 product(a25,product(product(a1,a27),product(a23,a27))) = product(a27,product(a23,a27))]. % 1.37/1.74 [1883=demod(796),[1865,32,1865,32], % 1.37/1.74 product(a22,product(product(a11,a27),product(a29,a27))) = product(product(a19,a27),product(a29,a27))]. % 1.37/1.74 [1884=demod(1173),[1865,32,1865,32], % 1.37/1.74 product(a2,product(product(a11,a27),product(a29,a27))) = product(product(a5,a27),product(a29,a27))]. % 1.37/1.74 [1885=demod(1732),[1865,32,1868,116,6], % 1.37/1.74 product(a21,a28) = product(a24,a28)]. % 1.37/1.74 [1895=demod(1527),[1885,114,5], % 1.37/1.74 product(a25,a29) = product(a20,a4)]. % 1.37/1.74 [1897=demod(1361),[1895], % 1.37/1.74 product(product(a2,a30),a1) = product(product(a4,product(a20,a4)),product(a1,a29))]. % 1.37/1.74 [1904=demod(1525),[1885,1573], % 1.37/1.74 product(a25,product(a4,a3)) = product(a20,a28)]. % 1.37/1.74 [1905=demod(1573),[1904], % 1.37/1.74 product(product(a24,a28),product(a28,product(a4,a3))) = product(a20,a28)]. % 1.37/1.74 [1907=demod(1523),[1885,509], % 1.37/1.74 product(a25,a28) = product(a20,a3)]. % 1.37/1.74 [1911=demod(509),[1907], % 1.37/1.74 product(product(a24,a28),product(a4,a3)) = product(a20,a3)]. % 1.37/1.74 [1921=demod(1777),[1865,33,1865,33], % 1.37/1.74 product(a1,a29) = a4]. % 1.37/1.74 [1923=demod(1897),[1921,32,34,33], % 1.37/1.74 product(product(a2,a30),a1) = product(a4,a20)]. % 1.37/1.74 [1970=demod(1776),[1865,33,1865,33], % 1.37/1.74 product(a23,a29) = a20]. % 1.37/1.74 [1971=demod(1585),[1970], % 1.37/1.74 product(product(a30,a29),product(a4,a20)) = product(product(a32,a23),a29)]. % 1.37/1.74 [1972=demod(1074),[1970], % 1.37/1.74 product(product(a22,a21),a29) = product(a20,product(a20,product(a4,a20)))]. % 1.37/1.74 [1973=demod(1778),[1865,33], % 1.37/1.74 product(product(a27,a29),product(a23,a1)) = a24]. % 1.37/1.74 [1977=demod(1608),[1973], % 1.37/1.74 product(product(a3,a2),a31) = product(a1,a24)]. % 1.37/1.74 [1985=demod(694),[1865], % 1.37/1.74 product(product(X10,a1),product(a27,product(a23,a1))) = product(product(X10,a27),a1)]. % 1.37/1.74 [1989=demod(120),[1865,1865], % 1.37/1.74 product(product(a21,X10),a27) = product(a22,product(X10,a27))]. % 1.37/1.74 [1990=demod(1807),[1865], % 1.37/1.74 product(product(X10,a27),product(a23,a27)) = product(product(X10,a28),a21)]. % 1.37/1.74 [1993=demod(1878),[1990,161,42], % 1.37/1.74 product(a25,product(a32,a27)) = product(a27,product(a23,a27))]. % 1.37/1.74 [1994=demod(1806),[1865], % 1.37/1.74 product(a27,product(a23,a27)) = product(a28,a27)]. % 1.37/1.74 [1995=demod(1993),[1994], % 1.37/1.74 product(a25,product(a32,a27)) = product(a28,a27)]. % 1.37/1.74 [2004=demod(1798),[1866,1865], % 1.37/1.74 product(a23,a27) = a22]. % 1.37/1.74 [2015=demod(1990),[2004], % 1.37/1.74 product(product(X10,a27),a22) = product(product(X10,a28),a21)]. % 1.37/1.74 [2017=demod(1875),[2015,100,42], % 1.37/1.74 product(a1,a27) = a2]. % 1.37/1.74 [2023=demod(1062),[2017], % 1.37/1.74 product(a26,a27) = product(a27,a2)]. % 1.37/1.74 [2024=demod(699),[2023,2017,32,33,32,33,1867], % 1.37/1.74 product(X10,a1) = product(X10,a3)]. % 1.37/1.74 [2025=demod(4),[2024,41], % 1.37/1.74 a28 = a30]. % 1.37/1.74 [2038=demod(1995),[2025], % 1.37/1.74 product(a25,product(a32,a27)) = product(a30,a27)]. % 1.37/1.74 [2062=demod(1911),[2025], % 1.37/1.74 product(product(a24,a30),product(a4,a3)) = product(a20,a3)]. % 1.37/1.74 [2066=demod(1907),[2025], % 1.37/1.74 product(a25,a30) = product(a20,a3)]. % 1.37/1.74 [2070=demod(1905),[2025,2025,2025], % 1.37/1.74 product(product(a24,a30),product(a30,product(a4,a3))) = product(a20,a30)]. % 1.37/1.74 [2080=demod(1885),[2025,2025], % 1.37/1.74 product(a21,a30) = product(a24,a30)]. % 1.37/1.74 [2087=demod(1774),[2025], % 1.37/1.74 product(product(a30,a24),product(a21,a24)) = product(a30,product(a23,product(a3,a21)))]. % 1.37/1.74 [2095=demod(1765),[2025], % 1.37/1.74 product(product(a24,X10),product(product(a30,product(a23,product(a3,a21))),X10)) = product(product(a22,a21),X10)]. % 1.37/1.74 [2099=demod(1759),[2025], % 1.37/1.74 product(product(a30,product(a21,a24)),product(product(a23,product(a21,a24)),product(product(a3,a21),product(a21,a24)))) = product(a30,a24)]. % 1.37/1.74 [2104=demod(1670),[2025], % 1.37/1.74 product(product(a4,a3),product(a4,a30)) = product(a4,product(a4,a3))]. % 1.37/1.74 [2111=demod(1537),[2025], % 1.37/1.74 product(product(a20,a3),product(a30,product(a4,a3))) = product(a21,product(a4,a3))]. % 1.37/1.74 [2115=demod(1405),[2025,2025,2025], % 1.37/1.74 product(product(a4,a30),product(a30,product(a30,product(a4,a3)))) = product(a4,product(a4,a3))]. % 1.37/1.74 [2116=demod(1404),[2025,2025], % 1.37/1.74 product(a29,product(a4,a3)) = product(a30,product(a30,product(a4,a3)))]. % 1.37/1.74 [2134=demod(701),[2025], % 1.37/1.74 product(product(a3,X10),product(product(a4,a3),X10)) = product(product(a4,a30),X10)]. % 1.37/1.74 [2135=demod(698),[2025], % 1.37/1.74 product(product(product(X10,a4),a3),product(a4,a30)) = product(X10,product(a4,a3))]. % 1.37/1.74 [2137=demod(696),[2025], % 1.37/1.74 product(a3,product(a4,a3)) = product(a4,a30)]. % 1.37/1.74 [2150=demod(546),[2025], % 1.37/1.74 product(product(a30,X10),product(X10,product(a21,X10))) = product(a27,product(a21,X10))]. % 1.37/1.74 [2151=demod(1335),[2150], % 1.37/1.74 product(a29,a32) = product(a27,product(a21,a32))]. % 1.37/1.74 [2156=demod(270),[2151,33], % 1.37/1.74 product(a30,a21) = a27]. % 1.37/1.74 [2160=demod(1636),[2156], % 1.37/1.74 product(product(a29,a20),product(a32,a29)) = product(a27,a29)]. % 1.37/1.74 [2167=demod(1571),[2156], % 1.37/1.74 product(product(a24,a27),product(a21,a24)) = product(a22,a24)]. % 1.37/1.74 [2168=demod(1561),[2156], % 1.37/1.74 product(a31,a24) = product(a27,product(a21,a24))]. % 1.37/1.74 [2169=demod(1572),[2168,32], % 1.37/1.74 product(product(a27,product(a22,a3)),product(product(a21,a24),product(a22,a3))) = product(a3,product(a32,a24))]. % 1.37/1.74 [2175=demod(513),[2025,2025,2025,34], % 1.37/1.74 product(product(a30,product(a4,a3)),product(a1,a30)) = a30]. % 1.37/1.74 [2176=demod(512),[2025,2025,2025], % 1.37/1.74 product(product(a29,X10),a30) = product(product(a30,product(a4,a3)),product(X10,a30))]. % 1.37/1.74 [2177=demod(511),[2025,2025], % 1.37/1.74 product(product(a29,X10),product(a30,X10)) = product(product(a30,product(a4,a3)),X10)]. % 1.37/1.74 [2180=demod(507),[2025], % 1.37/1.74 product(product(a4,a30),product(a4,a3)) = a3]. % 1.37/1.74 [2181=demod(506),[2025,2025], % 1.37/1.74 product(product(a3,X10),a30) = product(product(a4,a3),product(X10,a30))]. % 1.37/1.74 [2182=demod(505),[2025], % 1.37/1.74 product(product(a3,X10),product(a30,X10)) = product(product(a4,a3),X10)]. % 1.37/1.74 [2183=demod(502),[2025], % 1.37/1.74 product(product(X10,a4),a29) = product(product(X10,a30),product(a4,a3))]. % 1.37/1.74 [2191=demod(497),[2025], % 1.37/1.74 product(product(a20,a30),product(a4,a3)) = product(a21,a3)]. % 1.37/1.74 [2192=demod(496),[2025], % 1.37/1.74 product(a3,a30) = product(a4,a3)]. % 1.37/1.74 [2196=demod(1419),[2192], % 1.37/1.74 product(product(a4,a3),product(a1,product(a1,a30))) = product(a4,product(a1,a30))]. % 1.37/1.74 [2206=demod(204),[2025], % 1.37/1.74 product(product(a30,X10),product(a21,X10)) = product(a27,X10)]. % 1.37/1.74 [2207=demod(2087),[2206], % 1.37/1.74 product(a30,product(a23,product(a3,a21))) = product(a27,a24)]. % 1.37/1.74 [2213=demod(2095),[2207], % 1.37/1.74 product(product(a24,X10),product(product(a27,a24),X10)) = product(product(a22,a21),X10)]. % 1.37/1.74 [2215=demod(1972),[-2213], % 1.37/1.74 product(product(a24,a29),product(product(a27,a24),a29)) = product(a20,product(a20,product(a4,a20)))]. % 1.37/1.74 [2246=demod(107),[2025], % 1.37/1.74 product(product(a30,X10),a3) = product(a29,product(X10,a3))]. % 1.37/1.74 [2247=demod(1283),[2246], % 1.37/1.74 product(a29,product(a22,a3)) = product(a32,product(a32,product(a22,a3)))]. % 1.37/1.74 [2254=demod(41),[2025], % 1.37/1.74 product(a29,a3) = a30]. % 1.37/1.74 [2256=demod(5),[2025], % 1.37/1.74 product(a30,a3) = a29]. % 1.37/1.74 [2271=demod(43),[2024], % 1.37/1.74 product(a27,a3) = a26]. % 1.37/1.74 [2277=demod(660),[2271], % 1.37/1.74 product(a29,product(a21,a3)) = a26]. % 1.37/1.74 [2280=demod(156),[2024,32,2,32], % 1.37/1.74 product(product(X10,a2),a31) = product(product(X10,a32),product(a3,a32))]. % 1.37/1.74 [2282=demod(1977),[2280,34], % 1.37/1.74 product(a1,a24) = product(a3,a32)]. % 1.37/1.74 [2287=demod(214),[2024], % 1.37/1.74 product(product(X10,a26),product(a1,a26)) = product(product(X10,a27),a3)]. % 1.37/1.74 [2296=demod(1923),[2024,1030,2256,149], % 1.37/1.74 product(a4,product(a24,a29)) = product(a4,a20)]. % 1.37/1.74 [2305=demod(1985),[2024,2024,2024], % 1.37/1.74 product(product(X10,a3),product(a27,product(a23,a3))) = product(product(X10,a27),a3)]. % 1.37/1.74 [2320=demod(259),[2024,2,2024], % 1.37/1.74 product(a29,product(a23,a3)) = a32]. % 1.37/1.74 [2327=demod(1362),[2024,34], % 1.37/1.74 product(a3,product(a1,a30)) = product(a4,a30)]. % 1.37/1.74 [2328=demod(1424),[2327], % 1.37/1.74 product(product(a4,a30),product(a1,product(a1,a30))) = product(a4,a30)]. % 1.37/1.74 [2331=demod(1580),[2024,38,2024,1038,2024], % 1.37/1.74 product(a2,product(a3,a31)) = product(a32,product(a21,a3))]. % 1.37/1.74 [2332=demod(1038),[2331], % 1.37/1.74 product(a31,product(product(a21,a32),a3)) = product(a32,product(a21,a3))]. % 1.37/1.74 [2333=demod(1579),[2024,38,31,2024], % 1.37/1.74 product(a32,product(a21,a3)) = a2]. % 1.37/1.74 [2334=demod(2332),[2333], % 1.37/1.74 product(a31,product(product(a21,a32),a3)) = a2]. % 1.37/1.74 [2340=demod(1187),[2024,38,2024,2024,2333], % 1.37/1.74 product(a31,product(a21,product(a21,a3))) = a2]. % 1.37/1.74 [2343=demod(609),[2024,38,2024,2024], % 1.37/1.74 product(a31,product(a31,product(a21,a3))) = product(a2,product(a21,a3))]. % 1.37/1.74 [2344=demod(608),[2025,2024,2246,38,2024], % 1.37/1.74 product(a29,a31) = product(a27,product(a21,a3))]. % 1.37/1.74 [2345=demod(607),[2024,2024,38], % 1.37/1.74 product(product(a1,X10),product(product(a21,a3),X10)) = product(a31,X10)]. % 1.37/1.74 [2346=demod(606),[2024,2024,38], % 1.37/1.74 product(a1,product(a21,a3)) = a31]. % 1.37/1.74 [2352=demod(629),[2024,38,2024,2025,2024,2256], % 1.37/1.74 product(product(a27,a31),product(product(a21,a32),a3)) = a29]. % 1.37/1.74 [2357=demod(524),[2024,2320,246,2024,1026], % 1.37/1.74 product(a3,a24) = product(a32,product(a21,a32))]. % 1.37/1.74 [2365=demod(1541),[2357], % 1.37/1.74 product(product(a22,a24),product(a24,product(a32,product(a21,a32)))) = product(a21,a24)]. % 1.37/1.74 [2367=demod(1521),[2357,2357], % 1.37/1.74 product(a25,product(a32,product(a21,a32))) = product(a24,product(a24,product(a32,product(a21,a32))))]. % 1.37/1.74 [2369=demod(1182),[2357], % 1.37/1.74 product(product(a21,a3),product(a32,product(a21,a32))) = product(a22,a24)]. % 1.37/1.74 [2373=demod(1053),[2357,2357], % 1.37/1.74 product(product(a22,a24),product(a3,product(a32,product(a21,a32)))) = product(a21,product(a32,product(a21,a32)))]. % 1.37/1.74 [2377=demod(1027),[2357], % 1.37/1.74 product(product(a22,a3),product(a32,product(a21,a32))) = product(a21,a24)]. % 1.37/1.74 [2378=demod(1026),[2357], % 1.37/1.74 product(a2,a3) = product(a32,product(a21,a32))]. % 1.37/1.74 [2383=demod(666),[2357], % 1.37/1.74 product(a2,a24) = product(a3,product(a32,product(a21,a32)))]. % 1.37/1.74 [2388=demod(305),[2357], % 1.37/1.74 product(a25,a24) = product(a24,product(a32,product(a21,a32)))]. % 1.37/1.74 [2391=demod(691),[2024,45,2024], % 1.37/1.74 product(a27,product(a23,a3)) = a24]. % 1.37/1.74 [2393=demod(2305),[2391,32,2357], % 1.37/1.74 product(product(X10,a24),product(a32,product(a21,a32))) = product(product(X10,a27),a3)]. % 1.37/1.74 [2410=demod(1782),[1865,2023,1871,33], % 1.37/1.74 a31 = a27]. % 1.37/1.74 [2416=demod(2352),[2410,34], % 1.37/1.74 product(a27,product(product(a21,a32),a3)) = a29]. % 1.37/1.74 [2417=demod(2346),[2410], % 1.37/1.74 product(a1,product(a21,a3)) = a27]. % 1.37/1.74 [2418=demod(2345),[2410], % 1.37/1.74 product(product(a1,X10),product(product(a21,a3),X10)) = product(a27,X10)]. % 1.37/1.74 [2419=demod(2344),[2410], % 1.37/1.74 product(a29,a27) = product(a27,product(a21,a3))]. % 1.37/1.74 [2421=demod(1884),[2419,2419], % 1.37/1.74 product(a2,product(product(a11,a27),product(a27,product(a21,a3)))) = product(product(a5,a27),product(a27,product(a21,a3)))]. % 1.37/1.74 [2422=demod(1883),[2419,2419], % 1.37/1.74 product(a22,product(product(a11,a27),product(a27,product(a21,a3)))) = product(product(a19,a27),product(a27,product(a21,a3)))]. % 1.37/1.74 [2424=demod(2343),[2410,2410], % 1.37/1.74 product(a2,product(a21,a3)) = product(a27,product(a27,product(a21,a3)))]. % 1.37/1.74 [2426=demod(2340),[2410], % 1.37/1.74 product(a27,product(a21,product(a21,a3))) = a2]. % 1.37/1.74 [2427=demod(2334),[2410,2416], % 1.37/1.74 a2 = a29]. % 1.37/1.74 [2428=demod(2426),[2427], % 1.37/1.74 product(a27,product(a21,product(a21,a3))) = a29]. % 1.37/1.74 [2429=demod(2424),[2427,2277], % 1.37/1.74 product(a27,product(a27,product(a21,a3))) = a26]. % 1.37/1.74 [2430=demod(2421),[2427], % 1.37/1.74 product(a29,product(product(a11,a27),product(a27,product(a21,a3)))) = product(product(a5,a27),product(a27,product(a21,a3)))]. % 1.37/1.74 [2448=demod(2383),[2427,1745], % 1.37/1.74 product(a3,product(a32,product(a21,a32))) = product(a32,product(a22,a3))]. % 1.37/1.74 [2449=demod(2373),[2448], % 1.37/1.74 product(product(a22,a24),product(a32,product(a22,a3))) = product(a21,product(a32,product(a21,a32)))]. % 1.37/1.74 [2454=demod(2378),[2427,2254], % 1.37/1.74 product(a32,product(a21,a32)) = a30]. % 1.37/1.74 [2456=demod(2449),[2454,2080], % 1.37/1.74 product(product(a22,a24),product(a32,product(a22,a3))) = product(a24,a30)]. % 1.37/1.74 [2457=demod(2448),[2454,2192], % 1.37/1.74 product(a4,a3) = product(a32,product(a22,a3))]. % 1.37/1.74 [2462=demod(2196),[2457], % 1.37/1.74 product(product(a32,product(a22,a3)),product(a1,product(a1,a30))) = product(a4,product(a1,a30))]. % 1.37/1.74 [2463=demod(2192),[2457], % 1.37/1.74 product(a3,a30) = product(a32,product(a22,a3))]. % 1.37/1.74 [2464=demod(2191),[2457], % 1.37/1.74 product(product(a20,a30),product(a32,product(a22,a3))) = product(a21,a3)]. % 1.37/1.74 [2470=demod(2183),[2457], % 1.37/1.74 product(product(X10,a4),a29) = product(product(X10,a30),product(a32,product(a22,a3)))]. % 1.37/1.74 [2471=demod(2182),[2457], % 1.37/1.74 product(product(a3,X10),product(a30,X10)) = product(product(a32,product(a22,a3)),X10)]. % 1.37/1.74 [2472=demod(2181),[2457], % 1.37/1.74 product(product(a3,X10),a30) = product(product(a32,product(a22,a3)),product(X10,a30))]. % 1.37/1.74 [2473=demod(2180),[2457], % 1.37/1.74 product(product(a4,a30),product(a32,product(a22,a3))) = a3]. % 1.37/1.74 [2476=demod(2177),[2457], % 1.37/1.74 product(product(a29,X10),product(a30,X10)) = product(product(a30,product(a32,product(a22,a3))),X10)]. % 1.37/1.74 [2477=demod(2176),[2457], % 1.37/1.74 product(product(a29,X10),a30) = product(product(a30,product(a32,product(a22,a3))),product(X10,a30))]. % 1.37/1.74 [2478=demod(2175),[2457], % 1.37/1.74 product(product(a30,product(a32,product(a22,a3))),product(a1,a30)) = a30]. % 1.37/1.74 [2480=demod(2137),[2457], % 1.37/1.74 product(a3,product(a32,product(a22,a3))) = product(a4,a30)]. % 1.37/1.74 [2482=demod(2135),[2457], % 1.37/1.74 product(product(product(X10,a4),a3),product(a4,a30)) = product(X10,product(a32,product(a22,a3)))]. % 1.37/1.74 [2483=demod(2134),[2457], % 1.37/1.74 product(product(a3,X10),product(product(a32,product(a22,a3)),X10)) = product(product(a4,a30),X10)]. % 1.37/1.74 [2487=demod(2116),[2457,2457], % 1.37/1.74 product(a29,product(a32,product(a22,a3))) = product(a30,product(a30,product(a32,product(a22,a3))))]. % 1.37/1.74 [2488=demod(2115),[2457,2457], % 1.37/1.74 product(product(a4,a30),product(a30,product(a30,product(a32,product(a22,a3))))) = product(a4,product(a32,product(a22,a3)))]. % 1.37/1.74 [2491=demod(2111),[2457,2457], % 1.37/1.74 product(product(a20,a3),product(a30,product(a32,product(a22,a3)))) = product(a21,product(a32,product(a22,a3)))]. % 1.37/1.74 [2495=demod(2104),[2457,2457], % 1.37/1.74 product(product(a32,product(a22,a3)),product(a4,a30)) = product(a4,product(a32,product(a22,a3)))]. % 1.37/1.74 [2498=demod(2070),[2457], % 1.37/1.74 product(product(a24,a30),product(a30,product(a32,product(a22,a3)))) = product(a20,a30)]. % 1.37/1.74 [2499=demod(2062),[2457], % 1.37/1.74 product(product(a24,a30),product(a32,product(a22,a3))) = product(a20,a3)]. % 1.37/1.74 [2502=demod(2393),[2454,32], % 1.37/1.74 product(product(X10,a27),a3) = product(product(X10,a30),product(a24,a30))]. % 1.37/1.74 [2503=demod(2287),[2502], % 1.37/1.74 product(product(X10,a26),product(a1,a26)) = product(product(X10,a30),product(a24,a30))]. % 1.37/1.74 [2506=demod(2388),[2454], % 1.37/1.74 product(a25,a24) = product(a24,a30)]. % 1.37/1.74 [2510=demod(2377),[2454,32,758,2463], % 1.37/1.74 product(product(a23,product(a23,a30)),product(a32,product(a22,a3))) = product(a21,a24)]. % 1.37/1.74 [2512=demod(2369),[2454,32,2080,2463,2499], % 1.37/1.74 product(a20,a3) = product(a22,a24)]. % 1.37/1.74 [2515=demod(2491),[2512], % 1.37/1.74 product(product(a22,a24),product(a30,product(a32,product(a22,a3)))) = product(a21,product(a32,product(a22,a3)))]. % 1.37/1.74 [2519=demod(2066),[2512], % 1.37/1.74 product(a25,a30) = product(a22,a24)]. % 1.37/1.74 [2521=demod(2367),[2454,2519,2454], % 1.37/1.74 product(a22,a24) = product(a24,product(a24,a30))]. % 1.37/1.74 [2523=demod(2519),[2521], % 1.37/1.74 product(a25,a30) = product(a24,product(a24,a30))]. % 1.37/1.74 [2527=demod(2515),[2521], % 1.37/1.74 product(product(a24,product(a24,a30)),product(a30,product(a32,product(a22,a3)))) = product(a21,product(a32,product(a22,a3)))]. % 1.37/1.74 [2530=demod(2512),[2521], % 1.37/1.74 product(a20,a3) = product(a24,product(a24,a30))]. % 1.37/1.74 [2532=demod(2456),[2521], % 1.37/1.74 product(product(a24,product(a24,a30)),product(a32,product(a22,a3))) = product(a24,a30)]. % 1.37/1.74 [2534=demod(2167),[2521], % 1.37/1.74 product(product(a24,a27),product(a21,a24)) = product(a24,product(a24,a30))]. % 1.37/1.74 [2536=demod(2365),[2521,2454,33], % 1.37/1.74 product(a21,a24) = a24]. % 1.37/1.74 [2537=demod(2534),[2536,153], % 1.37/1.74 product(a24,product(a24,a30)) = product(a24,product(a27,a24))]. % 1.37/1.74 [2538=demod(2532),[2537], % 1.37/1.74 product(product(a24,product(a27,a24)),product(a32,product(a22,a3))) = product(a24,a30)]. % 1.37/1.74 [2539=demod(2530),[2537], % 1.37/1.74 product(a20,a3) = product(a24,product(a27,a24))]. % 1.37/1.74 [2542=demod(2527),[2537], % 1.37/1.74 product(product(a24,product(a27,a24)),product(a30,product(a32,product(a22,a3)))) = product(a21,product(a32,product(a22,a3)))]. % 1.37/1.74 [2546=demod(2523),[2537], % 1.37/1.74 product(a25,a30) = product(a24,product(a27,a24))]. % 1.37/1.74 [2548=demod(2521),[2537], % 1.37/1.74 product(a22,a24) = product(a24,product(a27,a24))]. % 1.37/1.74 [2549=demod(2510),[2536], % 1.37/1.74 product(product(a23,product(a23,a30)),product(a32,product(a22,a3))) = a24]. % 1.37/1.74 [2552=demod(2169),[2536,-32], % 1.37/1.74 product(product(a27,a24),product(a22,a3)) = product(a3,product(a32,a24))]. % 1.37/1.74 [2554=demod(2099),[2536,2536,2536,32,2536,33], % 1.37/1.74 product(product(a30,a24),product(product(a23,a24),a3)) = product(a30,a24)]. % 1.37/1.74 [2555=demod(1553),[2536,2536,33,2536], % 1.37/1.74 product(a23,a24) = a23]. % 1.37/1.74 [2556=demod(2554),[2555], % 1.37/1.74 product(product(a30,a24),product(a23,a3)) = product(a30,a24)]. % 1.37/1.74 [2558=demod(746),[2555,2536,32,33,2555], % 1.37/1.74 product(X10,a21) = product(X10,a23)]. % 1.37/1.74 [2559=demod(1),[2558], % 1.37/1.74 product(a32,a23) = a1]. % 1.37/1.74 [2561=demod(1971),[2559,1921], % 1.37/1.74 product(product(a30,a29),product(a4,a20)) = a4]. % 1.37/1.74 [2564=demod(1287),[2559,2559,2024,2256], % 1.37/1.74 product(a1,product(product(a3,a32),a23)) = a29]. % 1.37/1.74 [2566=demod(253),[2559], % 1.37/1.74 product(a30,product(a3,a23)) = a1]. % 1.37/1.74 [2567=demod(10),[2558,34], % 1.37/1.74 a23 = a24]. % 1.37/1.74 [2568=demod(2566),[2567], % 1.37/1.74 product(a30,product(a3,a24)) = a1]. % 1.37/1.74 [2570=demod(2564),[2567], % 1.37/1.74 product(a1,product(product(a3,a32),a24)) = a29]. % 1.37/1.74 [2574=demod(2559),[2567], % 1.37/1.74 product(a32,a24) = a1]. % 1.37/1.74 [2575=demod(2552),[2574,2024,34], % 1.37/1.74 product(product(a27,a24),product(a22,a3)) = a3]. % 1.37/1.74 [2577=demod(2556),[2567,9,1865,32], % 1.37/1.74 product(product(a30,a27),product(a24,a27)) = product(a30,a24)]. % 1.37/1.74 [2579=demod(2549),[2567,2567,2537,2538], % 1.37/1.74 product(a24,a30) = a24]. % 1.37/1.74 [2581=demod(2538),[2579], % 1.37/1.74 product(product(a24,product(a27,a24)),product(a32,product(a22,a3))) = a24]. % 1.37/1.74 [2582=demod(2537),[2579,34], % 1.37/1.74 product(a24,product(a27,a24)) = a24]. % 1.37/1.74 [2583=demod(2581),[2582], % 1.37/1.74 product(a24,product(a32,product(a22,a3))) = a24]. % 1.37/1.74 [2585=demod(2548),[2582], % 1.37/1.74 product(a22,a24) = a24]. % 1.37/1.74 [2586=demod(2546),[2582], % 1.37/1.74 product(a25,a30) = a24]. % 1.37/1.74 [2588=demod(2542),[2582], % 1.37/1.74 product(a21,product(a32,product(a22,a3))) = product(a24,product(a30,product(a32,product(a22,a3))))]. % 1.37/1.74 [2590=demod(2539),[2582], % 1.37/1.74 product(a20,a3) = a24]. % 1.37/1.74 [2593=demod(2506),[2579], % 1.37/1.74 product(a25,a24) = a24]. % 1.37/1.74 [2596=demod(2503),[2579], % 1.37/1.74 product(product(X10,a26),product(a1,a26)) = product(product(X10,a30),a24)]. % 1.37/1.74 [2597=demod(2502),[2579], % 1.37/1.74 product(product(X10,a27),a3) = product(product(X10,a30),a24)]. % 1.37/1.74 [2600=demod(2498),[2579], % 1.37/1.74 product(a20,a30) = product(a24,product(a30,product(a32,product(a22,a3))))]. % 1.37/1.74 [2604=demod(2464),[2600,32,2583,33,2579], % 1.37/1.74 product(a21,a3) = a24]. % 1.37/1.74 [2605=demod(2430),[2604,2604], % 1.37/1.74 product(a29,product(product(a11,a27),product(a27,a24))) = product(product(a5,a27),product(a27,a24))]. % 1.37/1.74 [2606=demod(2429),[2604], % 1.37/1.74 product(a27,product(a27,a24)) = a26]. % 1.37/1.74 [2607=demod(2428),[2604,2536], % 1.37/1.74 product(a27,a24) = a29]. % 1.37/1.74 [2608=demod(2606),[2607], % 1.37/1.74 product(a27,a29) = a26]. % 1.37/1.74 [2610=demod(2160),[2608], % 1.37/1.74 product(product(a29,a20),product(a32,a29)) = a26]. % 1.37/1.74 [2612=demod(1650),[2608], % 1.37/1.74 product(a29,a20) = product(a26,product(a4,a20))]. % 1.37/1.74 [2613=demod(2610),[2612,32], % 1.37/1.74 product(product(a26,product(a32,a29)),product(product(a4,a20),product(a32,a29))) = a26]. % 1.37/1.74 [2614=demod(1651),[2612,-32], % 1.37/1.74 product(product(a26,a29),product(a4,a20)) = product(a27,product(a4,a20))]. % 1.37/1.74 [2617=demod(347),[2612,2612], % 1.37/1.74 product(product(a21,a20),product(a29,product(a26,product(a4,a20)))) = product(a21,product(a26,product(a4,a20)))]. % 1.37/1.74 [2619=demod(341),[2612], % 1.37/1.74 product(a20,product(a26,product(a4,a20))) = product(a21,a20)]. % 1.37/1.74 [2620=demod(2605),[2607,2607], % 1.37/1.74 product(a29,product(product(a11,a27),a29)) = product(product(a5,a27),a29)]. % 1.37/1.74 [2621=demod(2582),[2607], % 1.37/1.74 product(a24,a29) = a24]. % 1.37/1.74 [2622=demod(2296),[2621], % 1.37/1.74 product(a4,a20) = product(a4,a24)]. % 1.37/1.74 [2623=demod(2619),[2622], % 1.37/1.74 product(a20,product(a26,product(a4,a24))) = product(a21,a20)]. % 1.37/1.74 [2625=demod(2617),[2622,2622], % 1.37/1.74 product(product(a21,a20),product(a29,product(a26,product(a4,a24)))) = product(a21,product(a26,product(a4,a24)))]. % 1.37/1.74 [2627=demod(2614),[2622,2622], % 1.37/1.74 product(product(a26,a29),product(a4,a24)) = product(a27,product(a4,a24))]. % 1.37/1.74 [2628=demod(2613),[2622], % 1.37/1.74 product(product(a26,product(a32,a29)),product(product(a4,a24),product(a32,a29))) = a26]. % 1.37/1.74 [2629=demod(2612),[2622], % 1.37/1.74 product(a29,a20) = product(a26,product(a4,a24))]. % 1.37/1.74 [2630=demod(2561),[2622], % 1.37/1.74 product(product(a30,a29),product(a4,a24)) = a4]. % 1.37/1.74 [2632=demod(2575),[2607,2247], % 1.37/1.74 product(a32,product(a32,product(a22,a3))) = a3]. % 1.37/1.74 [2635=demod(2215),[2621,2607,34,2621,2622], % 1.37/1.74 product(a20,product(a20,product(a4,a24))) = a24]. % 1.37/1.74 [2637=demod(2422),[2604,2607,2604,2607], % 1.37/1.74 product(a22,product(product(a11,a27),a29)) = product(product(a19,a27),a29)]. % 1.37/1.74 [2640=demod(2418),[2604], % 1.37/1.74 product(product(a1,X10),product(a24,X10)) = product(a27,X10)]. % 1.37/1.74 [2641=demod(2417),[2604,2282], % 1.37/1.74 product(a3,a32) = a27]. % 1.37/1.74 [2643=demod(2570),[2641,2607,1921], % 1.37/1.74 a29 = a4]. % 1.37/1.74 [2647=demod(2637),[2643,424,2643], % 1.37/1.74 product(product(a19,a27),a4) = product(a22,product(product(a12,a11),product(a27,a4)))]. % 1.37/1.74 [2650=demod(2630),[2643], % 1.37/1.74 product(product(a30,a4),product(a4,a24)) = a4]. % 1.37/1.74 [2651=demod(2629),[2643,2622], % 1.37/1.74 product(a26,product(a4,a24)) = product(a4,a24)]. % 1.37/1.74 [2654=demod(2623),[2651], % 1.37/1.74 product(a20,product(a4,a24)) = product(a21,a20)]. % 1.37/1.74 [2655=demod(2635),[2654], % 1.37/1.74 product(a20,product(a21,a20)) = a24]. % 1.37/1.74 [2656=demod(2628),[2643,2643], % 1.37/1.74 product(product(a26,product(a32,a4)),product(product(a4,a24),product(a32,a4))) = a26]. % 1.37/1.74 [2657=demod(2627),[2643], % 1.37/1.74 product(product(a26,a4),product(a4,a24)) = product(a27,product(a4,a24))]. % 1.37/1.74 [2658=demod(2625),[2643,2651,2651], % 1.37/1.74 product(product(a21,a20),product(a4,product(a4,a24))) = product(a21,product(a4,a24))]. % 1.37/1.74 [2659=demod(2621),[2643], % 1.37/1.74 product(a24,a4) = a24]. % 1.37/1.74 [2660=demod(2620),[2643,2643,424,2643], % 1.37/1.74 product(product(a5,a27),a4) = product(a4,product(product(a12,a11),product(a27,a4)))]. % 1.37/1.74 [2662=demod(2608),[2643], % 1.37/1.74 product(a27,a4) = a26]. % 1.37/1.74 [2663=demod(2660),[2662,32], % 1.37/1.74 product(product(a5,a27),a4) = product(a4,product(product(a12,a26),product(a11,a26)))]. % 1.37/1.74 [2664=demod(2647),[2662,32], % 1.37/1.74 product(product(a19,a27),a4) = product(a22,product(product(a12,a26),product(a11,a26)))]. % 1.37/1.74 [2667=demod(2487),[2643], % 1.37/1.74 product(a4,product(a32,product(a22,a3))) = product(a30,product(a30,product(a32,product(a22,a3))))]. % 1.37/1.74 [2669=demod(2495),[2667], % 1.37/1.74 product(product(a32,product(a22,a3)),product(a4,a30)) = product(a30,product(a30,product(a32,product(a22,a3))))]. % 1.37/1.74 [2670=demod(2488),[2667], % 1.37/1.74 product(product(a4,a30),product(a30,product(a30,product(a32,product(a22,a3))))) = product(a30,product(a30,product(a32,product(a22,a3))))]. % 1.37/1.74 [2673=demod(2477),[2643], % 1.37/1.74 product(product(a4,X10),a30) = product(product(a30,product(a32,product(a22,a3))),product(X10,a30))]. % 1.37/1.74 [2674=demod(2476),[2643], % 1.37/1.74 product(product(a4,X10),product(a30,X10)) = product(product(a30,product(a32,product(a22,a3))),X10)]. % 1.37/1.74 [2675=demod(2470),[2643,33], % 1.37/1.74 product(product(X10,a30),product(a32,product(a22,a3))) = X10]. % 1.37/1.74 [2677=demod(2473),[2675], % 1.37/1.74 a3 = a4]. % 1.37/1.74 [2678=demod(2675),[2677], % 1.37/1.74 product(product(X10,a30),product(a32,product(a22,a4))) = X10]. % 1.37/1.74 [2679=demod(2674),[2677], % 1.37/1.74 product(product(a4,X10),product(a30,X10)) = product(product(a30,product(a32,product(a22,a4))),X10)]. % 1.37/1.74 [2680=demod(2673),[2677], % 1.37/1.74 product(product(a4,X10),a30) = product(product(a30,product(a32,product(a22,a4))),product(X10,a30))]. % 1.37/1.74 [2682=demod(2670),[2677,2677], % 1.37/1.74 product(product(a4,a30),product(a30,product(a30,product(a32,product(a22,a4))))) = product(a30,product(a30,product(a32,product(a22,a4))))]. % 1.37/1.74 [2683=demod(2669),[2677,2677], % 1.37/1.74 product(product(a32,product(a22,a4)),product(a4,a30)) = product(a30,product(a30,product(a32,product(a22,a4))))]. % 1.37/1.74 [2690=demod(2632),[2677,2677], % 1.37/1.74 product(a32,product(a32,product(a22,a4))) = a4]. % 1.37/1.74 [2692=demod(2604),[2677], % 1.37/1.74 product(a21,a4) = a24]. % 1.37/1.74 [2695=demod(2600),[2677], % 1.37/1.74 product(a20,a30) = product(a24,product(a30,product(a32,product(a22,a4))))]. % 1.37/1.74 [2697=demod(2597),[2677], % 1.37/1.74 product(product(X10,a27),a4) = product(product(X10,a30),a24)]. % 1.37/1.74 [2698=demod(2663),[2697], % 1.37/1.74 product(product(a5,a30),a24) = product(a4,product(product(a12,a26),product(a11,a26)))]. % 1.37/1.74 [2700=demod(2664),[2697], % 1.37/1.74 product(product(a19,a30),a24) = product(a22,product(product(a12,a26),product(a11,a26)))]. % 1.37/1.74 [2701=demod(2590),[2677], % 1.37/1.74 product(a20,a4) = a24]. % 1.37/1.74 [2705=demod(428),[2701], % 1.37/1.74 product(product(product(a19,a12),X10),product(a5,X10)) = product(a24,X10)]. % 1.37/1.74 [2707=demod(2588),[2677,2677], % 1.37/1.74 product(a21,product(a32,product(a22,a4))) = product(a24,product(a30,product(a32,product(a22,a4))))]. % 1.37/1.74 [2712=demod(2568),[2677], % 1.37/1.74 product(a30,product(a4,a24)) = a1]. % 1.37/1.74 [2715=demod(2483),[2677,2677], % 1.37/1.74 product(product(a4,X10),product(product(a32,product(a22,a4)),X10)) = product(product(a4,a30),X10)]. % 1.37/1.74 [2716=demod(2482),[2677,33,2677], % 1.37/1.74 product(X10,product(a4,a30)) = product(X10,product(a32,product(a22,a4)))]. % 1.37/1.74 [2717=demod(2683),[2716,-32,34], % 1.37/1.74 product(a30,product(a30,product(a32,product(a22,a4)))) = product(a32,product(a22,a4))]. % 1.37/1.74 [2719=demod(2682),[2717,2678,2717], % 1.37/1.74 product(a32,product(a22,a4)) = a4]. % 1.37/1.74 [2722=demod(2715),[2719,34], % 1.37/1.74 product(product(a4,a30),X10) = product(a4,X10)]. % 1.37/1.74 [2723=demod(2328),[2722], % 1.37/1.74 product(a4,product(a1,product(a1,a30))) = product(a4,a30)]. % 1.37/1.74 [2727=demod(2707),[2719,2692,2719], % 1.37/1.74 product(a24,product(a30,a4)) = a24]. % 1.37/1.74 [2728=demod(2695),[2719,2727], % 1.37/1.74 product(a20,a30) = a24]. % 1.37/1.74 [2730=demod(2690),[2719], % 1.37/1.74 product(a32,a4) = a4]. % 1.37/1.74 [2732=demod(2656),[2730,2730,153,2659,2657], % 1.37/1.74 product(a27,product(a4,a24)) = a26]. % 1.37/1.74 [2733=demod(2657),[2732], % 1.37/1.74 product(product(a26,a4),product(a4,a24)) = a26]. % 1.37/1.74 [2734=demod(2680),[2719], % 1.37/1.74 product(product(a4,X10),a30) = product(product(a30,a4),product(X10,a30))]. % 1.37/1.74 [2735=demod(2679),[2719], % 1.37/1.74 product(product(a4,X10),product(a30,X10)) = product(product(a30,a4),X10)]. % 1.37/1.74 [2738=demod(2480),[2677,2677,2719,34], % 1.37/1.74 product(a4,a30) = a4]. % 1.37/1.74 [2739=demod(2723),[2738], % 1.37/1.74 product(a4,product(a1,product(a1,a30))) = a4]. % 1.37/1.74 [2740=demod(2478),[2677,2719], % 1.37/1.74 product(product(a30,a4),product(a1,a30)) = a30]. % 1.37/1.74 [2741=demod(2472),[2677,2734,2677,2719], % 1.37/1.74 product(product(a30,a4),product(X10,a30)) = product(a4,product(X10,a30))]. % 1.37/1.74 [2743=demod(2740),[2741], % 1.37/1.74 product(a4,product(a1,a30)) = a30]. % 1.37/1.74 [2744=demod(2471),[2677,2735,2677,2719], % 1.37/1.74 product(product(a30,a4),X10) = product(a4,X10)]. % 1.37/1.74 [2745=demod(2650),[2744], % 1.37/1.74 product(a4,product(a4,a24)) = a4]. % 1.37/1.74 [2747=demod(2658),[2745], % 1.37/1.74 product(product(a21,a20),a4) = product(a21,product(a4,a24))]. % 1.37/1.74 [2751=demod(2462),[2677,2719,2739,2743], % 1.37/1.74 a4 = a30]. % 1.37/1.74 [2754=demod(2747),[2751,32,2728,2751], % 1.37/1.74 product(product(a21,a30),a24) = product(a21,product(a30,a24))]. % 1.37/1.74 [2756=demod(2745),[2751,2751,2751], % 1.37/1.74 product(a30,product(a30,a24)) = a30]. % 1.37/1.74 [2760=demod(2733),[2751,2751], % 1.37/1.74 product(product(a26,a30),product(a30,a24)) = a26]. % 1.37/1.74 [2761=demod(2732),[2751], % 1.37/1.74 product(a27,product(a30,a24)) = a26]. % 1.37/1.74 [2762=demod(2730),[2751,2751], % 1.37/1.74 product(a32,a30) = a30]. % 1.37/1.74 [2765=demod(2712),[2751,2756], % 1.37/1.74 a1 = a30]. % 1.37/1.74 [2766=demod(2640),[2765], % 1.37/1.74 product(product(a30,X10),product(a24,X10)) = product(a27,X10)]. % 1.37/1.74 [2767=demod(2577),[2766,34], % 1.37/1.74 product(a30,a24) = a27]. % 1.37/1.74 [2768=demod(2761),[2767,34], % 1.37/1.74 a26 = a27]. % 1.37/1.74 [2770=demod(2700),[2768,2768], % 1.37/1.74 product(product(a19,a30),a24) = product(a22,product(product(a12,a27),product(a11,a27)))]. % 1.37/1.74 [2777=demod(2760),[2768,2767,153,2768], % 1.37/1.74 product(a27,product(a30,a27)) = a27]. % 1.37/1.74 [2778=demod(2756),[2767], % 1.37/1.74 product(a30,a27) = a30]. % 1.37/1.74 [2779=demod(2777),[2778], % 1.37/1.74 product(a27,a30) = a27]. % 1.37/1.74 [2783=demod(2038),[2778], % 1.37/1.74 product(a25,product(a32,a27)) = a30]. % 1.37/1.74 [2787=demod(2754),[2767,1866], % 1.37/1.74 product(product(a21,a30),a24) = a22]. % 1.37/1.74 [2789=demod(2596),[2768,2765,2768,2778,32,2779], % 1.37/1.74 product(product(X10,a30),a24) = product(product(X10,a30),a27)]. % 1.37/1.74 [2790=demod(2770),[2789], % 1.37/1.74 product(product(a19,a30),a27) = product(a22,product(product(a12,a27),product(a11,a27)))]. % 1.37/1.74 [2791=demod(2787),[2789,1989,2778], % 1.37/1.74 product(a22,a30) = a22]. % 1.37/1.74 [2801=demod(160),[2765,2206], % 1.37/1.74 product(a27,X10) = product(a32,X10)]. % 1.37/1.74 [2812=demod(2779),[2801,2762], % 1.37/1.74 a27 = a30]. % 1.37/1.74 [2813=demod(2801),[2812], % 1.37/1.74 product(a30,X10) = product(a32,X10)]. % 1.37/1.74 [2820=demod(2790),[2812,33,2812,2812], % 1.37/1.74 product(a22,product(product(a12,a30),product(a11,a30))) = a19]. % 1.37/1.74 [2822=demod(2783),[2812,2762,2586], % 1.37/1.74 a24 = a30]. % 1.37/1.74 [2825=demod(2728),[2822], % 1.37/1.74 product(a20,a30) = a30]. % 1.37/1.74 [2827=demod(2705),[2822,2813], % 1.37/1.74 product(product(product(a19,a12),X10),product(a5,X10)) = product(a32,X10)]. % 1.37/1.74 [2830=demod(2655),[2822], % 1.37/1.74 product(a20,product(a21,a20)) = a30]. % 1.37/1.74 [2831=demod(2593),[2822,2822], % 1.37/1.74 product(a25,a30) = a30]. % 1.37/1.74 [2833=demod(2585),[2822,2791,2822], % 1.37/1.74 a22 = a30]. % 1.37/1.74 [2834=demod(2820),[2833,2813], % 1.37/1.74 product(a32,product(product(a12,a30),product(a11,a30))) = a19]. % 1.37/1.74 [2841=demod(2567),[2822], % 1.37/1.74 a23 = a30]. % 1.37/1.74 [2843=demod(2768),[2812], % 1.37/1.74 a26 = a30]. % 1.37/1.74 [2844=demod(2410),[2812], % 1.37/1.74 a31 = a30]. % 1.37/1.74 [2847=demod(1870),[2822,2812,34,2812,2831,34], % 1.37/1.74 a21 = a30]. % 1.37/1.74 [2851=demod(2830),[2847,2813], % 1.37/1.74 product(a20,product(a32,a20)) = a30]. % 1.37/1.74 [2853=demod(2454),[2847,2813,34,34], % 1.37/1.74 a30 = a32]. % 1.37/1.74 [2854=demod(2851),[2853], % 1.37/1.74 product(a20,product(a32,a20)) = a32]. % 1.37/1.74 [2855=demod(2847),[2853], % 1.37/1.74 a21 = a32]. % 1.37/1.74 [2856=demod(2844),[2853], % 1.37/1.74 a31 = a32]. % 1.37/1.74 [2857=demod(2843),[2853], % 1.37/1.74 a26 = a32]. % 1.37/1.74 [2858=demod(2841),[2853], % 1.37/1.74 a23 = a32]. % 1.37/1.74 [2859=demod(2834),[2853,2853], % 1.37/1.74 product(a32,product(product(a12,a32),product(a11,a32))) = a19]. % 1.37/1.74 [2860=demod(2833),[2853], % 1.37/1.74 a22 = a32]. % 1.37/1.74 [2865=demod(2825),[2853,2853], % 1.37/1.74 product(a20,a32) = a32]. % 1.37/1.74 [2866=demod(2822),[2853], % 1.37/1.74 a24 = a32]. % 1.37/1.74 [2867=demod(2812),[2853], % 1.37/1.74 a27 = a32]. % 1.37/1.74 [2868=demod(2765),[2853], % 1.37/1.74 a1 = a32]. % 1.37/1.74 [2869=demod(2751),[2853], % 1.37/1.74 a4 = a32]. % 1.37/1.74 [2870=demod(2025),[2853], % 1.37/1.74 a28 = a32]. % 1.37/1.74 [2873=demod(2698),[2853,2866,33,2869,2857,2857,2859], % 1.37/1.74 a5 = a19]. % 1.37/1.74 [2885=demod(2827),[2873], % 1.37/1.74 product(product(product(a19,a12),X10),product(a19,X10)) = product(a32,X10)]. % 1.37/1.74 [2888=demod(1612),[2873], % 1.37/1.74 product(product(a19,a17),product(a14,product(a17,a14))) = product(a6,product(a17,a14))]. % 1.37/1.74 [2903=demod(1480),[2873,153,17], % 1.37/1.74 product(a19,a17) = product(a18,a6)]. % 1.37/1.74 [2904=demod(2888),[2903], % 1.37/1.74 product(product(a18,a6),product(a14,product(a17,a14))) = product(a6,product(a17,a14))]. % 1.37/1.74 [2908=demod(874),[2903], % 1.37/1.74 product(product(a18,a6),product(a17,a14)) = product(a18,a14)]. % 1.37/1.74 [2909=demod(853),[2903], % 1.37/1.74 product(product(a10,a16),a19) = product(a9,product(a18,a6))]. % 1.37/1.74 [2910=demod(851),[2903], % 1.37/1.74 product(product(product(X10,a16),a19),product(a18,a6)) = product(X10,a17)]. % 1.37/1.74 [2912=demod(849),[2903], % 1.37/1.74 product(product(a14,a16),a19) = product(a15,product(a18,a6))]. % 1.37/1.74 [2913=demod(846),[2903], % 1.37/1.74 product(product(product(X10,a16),a19),product(a16,a17)) = product(X10,product(a18,a6))]. % 1.37/1.74 [2914=demod(845),[2903,2903], % 1.37/1.74 product(product(a16,a17),product(a9,product(a18,a6))) = product(a18,product(a18,a6))]. % 1.37/1.74 [2918=demod(359),[2903], % 1.37/1.74 product(product(a18,a14),product(a17,a14)) = product(a18,a6)]. % 1.37/1.74 [2924=demod(1429),[2873,53,2873,34,53,34,2873,34], % 1.37/1.74 product(a14,a19) = a16]. % 1.37/1.74 [2929=demod(404),[2924], % 1.37/1.74 product(a12,a8) = a16]. % 1.37/1.74 [2942=demod(1381),[2873,2873], % 1.37/1.74 product(product(a11,X10),product(X10,product(a19,X10))) = product(a12,product(a19,X10))]. % 1.37/1.74 [2943=demod(1369),[2942,980], % 1.37/1.74 product(a10,a8) = product(a14,a8)]. % 1.37/1.74 [2949=demod(1366),[2873,57,2873,34,26,2929,2873,34], % 1.37/1.74 product(a10,a19) = a16]. % 1.37/1.74 [2952=demod(855),[2949,373], % 1.37/1.74 product(a9,a16) = product(a17,a16)]. % 1.37/1.74 [2956=demod(1344),[2873,33,2873,34,62,394], % 1.37/1.74 product(a13,product(a17,a7)) = a18]. % 1.37/1.74 [2960=demod(396),[2956], % 1.37/1.74 product(product(a15,X10),product(a7,X10)) = product(a18,X10)]. % 1.37/1.74 [2974=demod(1293),[2873,566,2873], % 1.37/1.74 product(a7,product(a19,X10)) = product(a9,product(a19,X10))]. % 1.37/1.74 [2975=demod(461),[2974], % 1.37/1.74 product(a9,product(a19,a7)) = product(a8,a7)]. % 1.37/1.74 [2979=demod(1266),[2873,34,17,2873,34,62,20], % 1.37/1.74 product(a7,a17) = a14]. % 1.37/1.74 [2986=demod(863),[2979,392], % 1.37/1.74 product(a14,product(a17,a14)) = product(a13,a17)]. % 1.37/1.74 [2987=demod(2904),[2986], % 1.37/1.74 product(product(a18,a6),product(a13,a17)) = product(a6,product(a17,a14))]. % 1.37/1.74 [2990=demod(402),[2986], % 1.37/1.74 product(product(a18,a14),product(a13,a17)) = product(a19,a14)]. % 1.37/1.74 [2997=demod(1251),[2873,1054], % 1.37/1.74 product(a6,product(a17,a14)) = product(a18,product(a17,a14))]. % 1.37/1.74 [2998=demod(2987),[2997], % 1.37/1.74 product(product(a18,a6),product(a13,a17)) = product(a18,product(a17,a14))]. % 1.37/1.74 [2999=demod(1250),[2873,2903,2908], % 1.37/1.74 product(a6,a14) = product(a18,a14)]. % 1.37/1.74 [3007=demod(1087),[2873,153,62,2974,2975], % 1.37/1.74 product(product(a9,a8),a19) = product(a8,a7)]. % 1.37/1.74 [3008=demod(1086),[2873,2873], % 1.37/1.74 product(product(a10,a9),a19) = product(a8,product(a18,a19))]. % 1.37/1.74 [3009=demod(1327),[3008], % 1.37/1.74 product(product(a18,a19),product(a8,product(a18,a19))) = product(a16,product(a18,a19))]. % 1.37/1.74 [3010=demod(1078),[2873,216,17], % 1.37/1.74 product(a15,product(a18,a6)) = product(a16,a17)]. % 1.37/1.74 [3012=demod(2912),[3010], % 1.37/1.74 product(product(a14,a16),a19) = product(a16,a17)]. % 1.37/1.74 [3032=demod(986),[2873,1291], % 1.37/1.74 product(a6,product(a17,a15)) = product(a18,product(a17,a15))]. % 1.37/1.74 [3042=demod(966),[2873,2873,34,-32,2873,32,26,32], % 1.37/1.74 product(product(X10,a8),product(a19,a8)) = product(product(X10,a9),a19)]. % 1.37/1.74 [3043=demod(409),[3042], % 1.37/1.74 product(product(a14,a9),a19) = a12]. % 1.37/1.74 [3048=demod(961),[2873,93,2873,34], % 1.37/1.74 product(product(a9,a19),X10) = product(a8,X10)]. % 1.37/1.74 [3049=demod(854),[3048], % 1.37/1.74 product(a8,product(a19,a16)) = product(a10,a16)]. % 1.37/1.74 [3053=demod(959),[2873,57,2873,216,26,2873,34,366], % 1.37/1.74 product(a12,product(a16,a8)) = product(a18,a19)]. % 1.37/1.74 [3056=demod(955),[2873,216,26,3053,2873,34], % 1.37/1.74 product(a8,product(a9,a19)) = product(a18,a19)]. % 1.37/1.74 [3057=demod(954),[2873,26,2873,34], % 1.37/1.74 product(a9,a19) = a8]. % 1.37/1.74 [3058=demod(3056),[3057,34], % 1.37/1.74 product(a18,a19) = a8]. % 1.37/1.74 [3059=demod(3053),[3058], % 1.37/1.74 product(a12,product(a16,a8)) = a8]. % 1.37/1.74 [3061=demod(3009),[3058,3058,34,34,3058], % 1.37/1.74 product(a16,a8) = a8]. % 1.37/1.74 [3062=demod(3059),[3061,2929], % 1.37/1.74 a8 = a16]. % 1.37/1.74 [3067=demod(3049),[3062,373], % 1.37/1.74 product(a17,a16) = product(a10,a16)]. % 1.37/1.74 [3071=demod(2952),[3067], % 1.37/1.74 product(a9,a16) = product(a10,a16)]. % 1.37/1.74 [3077=demod(3042),[3062,3062], % 1.37/1.74 product(product(X10,a9),a19) = product(product(X10,a16),product(a19,a16))]. % 1.37/1.74 [3078=demod(3043),[3077,393], % 1.37/1.74 product(a15,a19) = a12]. % 1.37/1.74 [3080=demod(831),[3078,34], % 1.37/1.74 product(product(a13,a18),a15) = a12]. % 1.37/1.74 [3081=demod(830),[3078], % 1.37/1.74 product(a19,product(product(a10,a9),a15)) = product(a16,a12)]. % 1.37/1.74 [3082=demod(829),[3078,32], % 1.37/1.74 product(product(product(X10,a18),a12),product(a15,a12)) = product(X10,a19)]. % 1.37/1.74 [3084=demod(826),[3078], % 1.37/1.74 product(product(a16,a18),a15) = product(a17,a12)]. % 1.37/1.74 [3086=demod(127),[3078,32,200], % 1.37/1.74 product(product(X10,a13),a19) = product(product(X10,a18),a15)]. % 1.37/1.74 [3096=demod(3007),[3062,3071,2909,3062], % 1.37/1.74 product(a9,product(a18,a6)) = product(a16,a7)]. % 1.37/1.74 [3097=demod(2914),[3096], % 1.37/1.74 product(product(a16,a17),product(a16,a7)) = product(a18,product(a18,a6))]. % 1.37/1.74 [3098=demod(2909),[3096], % 1.37/1.74 product(product(a10,a16),a19) = product(a16,a7)]. % 1.37/1.74 [3120=demod(2943),[3062,3062], % 1.37/1.74 product(a10,a16) = product(a14,a16)]. % 1.37/1.74 [3121=demod(3098),[3120,3012], % 1.37/1.74 product(a16,a7) = product(a16,a17)]. % 1.37/1.74 [3124=demod(3097),[3121,-32,34], % 1.37/1.74 product(a16,a17) = product(a18,product(a18,a6))]. % 1.37/1.74 [3127=demod(3121),[3124], % 1.37/1.74 product(a16,a7) = product(a18,product(a18,a6))]. % 1.37/1.74 [3137=demod(2913),[3124], % 1.37/1.74 product(product(product(X10,a16),a19),product(a18,product(a18,a6))) = product(X10,product(a18,a6))]. % 1.37/1.74 [3139=demod(3096),[3127], % 1.37/1.74 product(a9,product(a18,a6)) = product(a18,product(a18,a6))]. % 1.37/1.74 [3165=demod(1269),[3062], % 1.37/1.74 product(product(product(X10,a16),a19),product(a19,a7)) = product(X10,a7)]. % 1.37/1.74 [3178=demod(1082),[3086,3062], % 1.37/1.74 product(product(a14,a18),a15) = product(a12,product(a16,a12))]. % 1.37/1.74 [3187=demod(832),[3062,3084,3078], % 1.37/1.74 product(a7,a12) = product(a17,a12)]. % 1.37/1.74 [3198=demod(590),[3062,3062,3127,3137], % 1.37/1.74 product(X10,product(a19,a7)) = product(X10,product(a18,a6))]. % 1.37/1.74 [3199=demod(3165),[3198,2910], % 1.37/1.74 product(X10,a7) = product(X10,a17)]. % 1.37/1.74 [3200=demod(20),[3199], % 1.37/1.74 product(a13,a17) = a14]. % 1.37/1.74 [3201=demod(2998),[3200,32,2999,-32,34], % 1.37/1.74 product(a18,product(a17,a14)) = product(a18,a14)]. % 1.37/1.74 [3205=demod(2990),[3200,33], % 1.37/1.74 product(a19,a14) = a18]. % 1.37/1.74 [3209=demod(1478),[3205,3201], % 1.37/1.74 product(a18,a17) = product(a18,a14)]. % 1.37/1.74 [3213=demod(1472),[3209,3209], % 1.37/1.74 product(product(a18,a10),product(a10,product(a18,a14))) = product(a18,a14)]. % 1.37/1.74 [3216=demod(1440),[3209], % 1.37/1.74 product(product(a15,a18),a10) = product(a14,product(a10,product(a18,a14)))]. % 1.37/1.74 [3233=demod(1300),[3209,2918,3205], % 1.37/1.74 product(a18,a6) = a18]. % 1.37/1.74 [3234=demod(3139),[3233,442,3233,34], % 1.37/1.74 product(a10,a9) = a18]. % 1.37/1.74 [3238=demod(3081),[3234,15,34], % 1.37/1.74 product(a16,a12) = a19]. % 1.37/1.74 [3240=demod(3178),[3238,21], % 1.37/1.74 product(product(a14,a18),a15) = a13]. % 1.37/1.74 [3241=demod(1677),[3234,3234], % 1.37/1.74 product(a18,product(a10,a18)) = product(a10,a18)]. % 1.37/1.74 [3259=demod(1431),[3234,34,33], % 1.37/1.74 product(a14,a18) = a15]. % 1.37/1.74 [3261=demod(3240),[3259,34], % 1.37/1.74 a15 = a13]. % 1.37/1.74 [3263=demod(3259),[3261], % 1.37/1.74 product(a14,a18) = a13]. % 1.37/1.74 [3280=demod(3216),[3261], % 1.37/1.74 product(product(a13,a18),a10) = product(a14,product(a10,product(a18,a14)))]. % 1.37/1.74 [3299=demod(3082),[3261,-32], % 1.37/1.74 product(product(product(X10,a18),a13),a12) = product(X10,a19)]. % 1.37/1.74 [3300=demod(3080),[3261,153], % 1.37/1.74 product(a13,product(a18,a13)) = a12]. % 1.37/1.74 [3301=demod(3032),[3261,3261], % 1.37/1.74 product(a6,product(a17,a13)) = product(a18,product(a17,a13))]. % 1.37/1.74 [3315=demod(2960),[3261,87], % 1.37/1.74 product(a14,X10) = product(a18,X10)]. % 1.37/1.74 [3319=demod(87),[3315], % 1.37/1.74 product(product(a13,X10),product(a7,X10)) = product(a18,X10)]. % 1.37/1.74 [3320=demod(1079),[3315], % 1.37/1.74 product(product(a16,a14),product(a17,a14)) = product(a18,product(a6,a17))]. % 1.37/1.74 [3325=demod(3280),[3315], % 1.37/1.74 product(product(a13,a18),a10) = product(a18,product(a10,product(a18,a14)))]. % 1.37/1.74 [3326=demod(3263),[3315,34], % 1.37/1.74 a13 = a18]. % 1.37/1.74 [3327=demod(3325),[3326,34], % 1.37/1.74 product(a18,product(a10,product(a18,a14))) = product(a18,a10)]. % 1.37/1.74 [3330=demod(3319),[3326], % 1.37/1.74 product(product(a18,X10),product(a7,X10)) = product(a18,X10)]. % 1.37/1.74 [3340=demod(3301),[3326,3326], % 1.37/1.74 product(a6,product(a17,a18)) = product(a18,product(a17,a18))]. % 1.37/1.74 [3341=demod(3300),[3326,3326,34,34], % 1.37/1.74 a12 = a18]. % 1.37/1.74 [3350=demod(3238),[3341], % 1.37/1.74 product(a16,a18) = a19]. % 1.37/1.74 [3362=demod(3187),[3341,3341], % 1.37/1.74 product(a7,a18) = product(a17,a18)]. % 1.37/1.74 [3372=demod(2885),[3341], % 1.37/1.74 product(product(product(a19,a18),X10),product(a19,X10)) = product(a32,X10)]. % 1.37/1.74 [3374=demod(3299),[3326,33,3341], % 1.37/1.74 product(X10,a19) = product(X10,a18)]. % 1.37/1.74 [3375=demod(17),[3374,3350], % 1.37/1.74 a19 = a17]. % 1.37/1.74 [3376=demod(3374),[3375], % 1.37/1.74 product(X10,a17) = product(X10,a18)]. % 1.37/1.74 [3377=demod(24),[3376], % 1.37/1.74 product(a9,a18) = a10]. % 1.37/1.74 [3378=demod(60),[3376], % 1.37/1.74 product(a10,a18) = a9]. % 1.37/1.74 [3379=demod(3241),[3378,52,3378], % 1.37/1.74 a9 = a17]. % 1.37/1.74 [3380=demod(3378),[3379], % 1.37/1.74 product(a10,a18) = a17]. % 1.37/1.74 [3381=demod(3377),[3379], % 1.37/1.74 product(a17,a18) = a10]. % 1.37/1.74 [3382=demod(3362),[3381], % 1.37/1.74 product(a7,a18) = a10]. % 1.37/1.74 [3383=demod(3340),[3381,3381], % 1.37/1.74 product(a6,a10) = product(a18,a10)]. % 1.37/1.74 [3384=demod(3234),[3379,3376,3380], % 1.37/1.74 a17 = a18]. % 1.37/1.74 [3385=demod(3381),[3384,34], % 1.37/1.74 a10 = a18]. % 1.37/1.74 [3386=demod(3383),[3385,3385,34], % 1.37/1.74 product(a6,a18) = a18]. % 1.37/1.74 [3387=demod(3382),[3385], % 1.37/1.74 product(a7,a18) = a18]. % 1.37/1.74 [3388=demod(3327),[3385,3385,34], % 1.37/1.74 product(a18,product(a18,product(a18,a14))) = a18]. % 1.37/1.74 [3390=demod(3213),[3385,34,3385,3388], % 1.37/1.74 product(a18,a14) = a18]. % 1.37/1.74 [3393=demod(1084),[3385,3385,3387,-32,34,3385], % 1.37/1.74 product(a11,product(a18,a11)) = product(a18,a11)]. % 1.37/1.74 [3399=demod(90),[3385,3330], % 1.37/1.74 product(a11,X10) = product(a18,X10)]. % 1.37/1.74 [3400=demod(3393),[3399], % 1.37/1.74 product(a18,product(a18,a11)) = product(a18,a11)]. % 1.37/1.74 [3401=demod(3379),[3384], % 1.37/1.74 a9 = a18]. % 1.37/1.74 [3402=demod(3375),[3384], % 1.37/1.74 a19 = a18]. % 1.37/1.74 [3408=demod(372),[3399,3384], % 1.37/1.74 product(product(a16,a20),product(a18,a20)) = product(a18,a11)]. % 1.37/1.74 [3410=demod(3199),[3384], % 1.37/1.74 product(X10,a7) = product(X10,a18)]. % 1.37/1.74 [3411=demod(3320),[3384,3390,32,3315,34,33,3384,3386,34], % 1.37/1.74 a16 = a18]. % 1.37/1.74 [3412=demod(3408),[3411,34], % 1.37/1.74 product(a18,a11) = product(a18,a20)]. % 1.37/1.74 [3416=demod(3400),[3412,3412], % 1.37/1.74 product(a18,product(a18,a20)) = product(a18,a20)]. % 1.37/1.74 [3417=demod(3062),[3411], % 1.37/1.74 a8 = a18]. % 1.37/1.74 [3418=demod(2979),[3384,3387], % 1.37/1.74 a14 = a18]. % 1.37/1.74 [3419=demod(3372),[3402,34,3402,34], % 1.37/1.74 product(a18,X10) = product(a32,X10)]. % 1.37/1.74 [3420=demod(3399),[3419], % 1.37/1.74 product(a11,X10) = product(a32,X10)]. % 1.37/1.74 [3425=demod(3416),[3419,3419,3419], % 1.37/1.74 product(a32,product(a32,a20)) = product(a32,a20)]. % 1.37/1.74 [3434=demod(2873),[3402], % 1.37/1.74 a5 = a18]. % 1.37/1.74 [3435=demod(1286),[3402,3419,3420,540,3420], % 1.37/1.74 product(a20,product(a32,X10)) = product(a32,product(a32,X10))]. % 1.37/1.74 [3436=demod(2854),[3435,3425], % 1.37/1.74 product(a32,a20) = a32]. % 1.37/1.74 [3440=demod(807),[3402,3419,3436,32,2865,33,3420,3436], % 1.37/1.74 product(X10,a11) = product(X10,a32)]. % 1.37/1.74 [3446=demod(81),[3402,3419,3420,34], % 1.37/1.74 product(a20,X10) = product(a32,X10)]. % 1.37/1.74 [3447=demod(50),[3440,3446,34,3402], % 1.37/1.74 a18 = a32]. % 1.37/1.74 [3448=demod(3434),[3447], % 1.37/1.74 a5 = a32]. % 1.37/1.74 [3450=demod(3418),[3447], % 1.37/1.74 a14 = a32]. % 1.37/1.74 [3451=demod(3417),[3447], % 1.37/1.74 a8 = a32]. % 1.37/1.74 [3452=demod(3411),[3447], % 1.37/1.74 a16 = a32]. % 1.37/1.74 [3453=demod(3410),[3447], % 1.37/1.74 product(X10,a7) = product(X10,a32)]. % 1.37/1.74 [3455=demod(3402),[3447], % 1.37/1.74 a19 = a32]. % 1.37/1.74 [3456=demod(3401),[3447], % 1.37/1.74 a9 = a32]. % 1.37/1.74 [3458=demod(3385),[3447], % 1.37/1.74 a10 = a32]. % 1.37/1.74 [3459=demod(3384),[3447], % 1.37/1.74 a17 = a32]. % 1.37/1.74 [3460=demod(3341),[3447], % 1.37/1.74 a12 = a32]. % 1.37/1.74 [3461=demod(3326),[3447], % 1.37/1.74 a13 = a32]. % 1.37/1.74 [3462=demod(14),[3455,3440,34], % 1.37/1.74 a20 = a32]. % 1.37/1.74 [3464=demod(3261),[3461], % 1.37/1.74 a15 = a32]. % 1.37/1.74 [3468=demod(23),[3458,3453,34], % 1.37/1.74 a11 = a32]. % 1.37/1.74 [3471=demod(62),[3451,3455,34], % 1.37/1.74 a7 = a32]. % 1.37/1.74 [3477=demod(27),[3448,3464,34], % 1.37/1.74 a6 = a32]. % 1.37/1.74 [3478=demod(2677),[2869], % 1.37/1.74 a3 = a32]. % 1.37/1.74 [3479=demod(2643),[2869], % 1.37/1.74 a29 = a32]. % 1.37/1.74 [3484=demod(9),[2866,3478,34], % 1.37/1.74 a25 = a32]. % 1.37/1.74 [3485=demod(2427),[3479], % 1.37/1.74 a2 = a32]. % 1.37/1.74 [3581=param(36,3479),[2868,2853,2856,3485,2866,3484,3478,2870,2869,3458,3468,3448,3450,3464,3477,3471,3447,3455,3451,3456,3452,3459,3460,3461,3462,2855,2860,2858,2857,2867,3485,2856,3478,3484,2857,2869,3479,2853,3448,3468,3460,3477,3464,3452,3471,3451,3455,3462,3456,3458,3459,3447,3461,3450,2855,2860,2858,2866,2867,2870,35], % 1.37/1.74 thmtrue = thmfalse]. % 1.37/1.74 % SZS output end CNFRefutation % 1.37/1.74 Space: 3094 KB %------------------------------------------------------------------------------