%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : TOP052-1 : TPTP v8.1.0. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n004.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 : 300s % DateTime : Wed Jul 27 13:27:00 EDT 2022 % Result : Unknown 1.96s 2.16s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : TOP052-1 : TPTP v8.1.0. Released v8.1.0. % 0.06/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n004.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 : 300 % 0.12/0.33 % DateTime : Wed Jul 27 01:44:51 EDT 2022 % 0.12/0.33 % CPUTime : % 1.90/2.10 ----- Otter 3.3f, August 2004 ----- % 1.90/2.10 The process was started by sandbox2 on n004.cluster.edu, % 1.90/2.10 Wed Jul 27 01:44:51 2022 % 1.90/2.10 The command was "./otter". The process ID is 28157. % 1.90/2.10 % 1.90/2.10 set(prolog_style_variables). % 1.90/2.10 set(auto). % 1.90/2.10 dependent: set(auto1). % 1.90/2.10 dependent: set(process_input). % 1.90/2.10 dependent: clear(print_kept). % 1.90/2.10 dependent: clear(print_new_demod). % 1.90/2.10 dependent: clear(print_back_demod). % 1.90/2.10 dependent: clear(print_back_sub). % 1.90/2.10 dependent: set(control_memory). % 1.90/2.10 dependent: assign(max_mem, 12000). % 1.90/2.10 dependent: assign(pick_given_ratio, 4). % 1.90/2.10 dependent: assign(stats_level, 1). % 1.90/2.10 dependent: assign(max_seconds, 10800). % 1.90/2.10 clear(print_given). % 1.90/2.10 % 1.90/2.10 list(usable). % 1.90/2.10 0 [] A=A. % 1.90/2.10 0 [] product(X,X)=X. % 1.90/2.10 0 [] product(product(X,Y),Y)=X. % 1.90/2.10 0 [] product(product(X,Y),Z)=product(product(X,Z),product(Y,Z)). % 1.90/2.10 0 [] a2=product(a1,a42). % 1.90/2.10 0 [] a3=product(a2,a41). % 1.90/2.10 0 [] a4=product(a3,a14). % 1.90/2.10 0 [] a5=product(a4,a39). % 1.90/2.10 0 [] a6=product(a5,a136). % 1.90/2.10 0 [] a7=product(a6,a52). % 1.90/2.10 0 [] a8=product(a7,a17). % 1.90/2.10 0 [] a9=product(a8,a56). % 1.90/2.10 0 [] a10=product(a9,a134). % 1.90/2.10 0 [] a11=product(a10,a37). % 1.90/2.10 0 [] a12=product(a11,a21). % 1.90/2.10 0 [] a13=product(a12,a23). % 1.90/2.10 0 [] a14=product(a13,a32). % 1.90/2.10 0 [] a15=product(a14,a53). % 1.90/2.10 0 [] a16=product(a15,a136). % 1.90/2.10 0 [] a17=product(a16,a29). % 1.90/2.10 0 [] a18=product(a17,a133). % 1.90/2.10 0 [] a19=product(a18,a58). % 1.90/2.10 0 [] a20=product(a19,a26). % 1.90/2.10 0 [] a21=product(a20,a35). % 1.90/2.10 0 [] a22=product(a21,a141). % 1.90/2.10 0 [] a23=product(a22,a45). % 1.90/2.10 0 [] a24=product(a23,a35). % 1.90/2.10 0 [] a25=product(a24,a49). % 1.90/2.10 0 [] a26=product(a25,a138). % 1.90/2.10 0 [] a27=product(a26,a8). % 1.90/2.10 0 [] a28=product(a27,a37). % 1.90/2.10 0 [] a29=product(a28,a17). % 1.90/2.10 0 [] a30=product(a29,a14). % 1.90/2.10 0 [] a31=product(a30,a5). % 1.90/2.10 0 [] a32=product(a31,a39). % 1.90/2.10 0 [] a33=product(a32,a13). % 1.90/2.10 0 [] a34=product(a33,a131). % 1.90/2.10 0 [] a35=product(a34,a60). % 1.90/2.10 0 [] a36=product(a35,a139). % 1.90/2.10 0 [] a37=product(a36,a47). % 1.90/2.10 0 [] a38=product(a37,a17). % 1.90/2.10 0 [] a39=product(a38,a7). % 1.90/2.10 0 [] a40=product(a39,a4). % 1.90/2.10 0 [] a41=product(a40,a14). % 1.90/2.10 0 [] a42=product(a41,a2). % 1.90/2.10 0 [] a43=product(a42,a62). % 1.90/2.10 0 [] a44=product(a43,a128). % 1.90/2.10 0 [] a45=product(a44,a23). % 1.90/2.10 0 [] a46=product(a45,a141). % 1.90/2.10 0 [] a47=product(a46,a11). % 1.90/2.10 0 [] a48=product(a47,a20). % 1.90/2.10 0 [] a49=product(a48,a138). % 1.90/2.10 0 [] a50=product(a49,a131). % 1.90/2.10 0 [] a51=product(a50,a59). % 1.90/2.10 0 [] a52=product(a51,a39). % 1.90/2.10 0 [] a53=product(a52,a136). % 1.90/2.10 0 [] a54=product(a53,a29). % 1.90/2.10 0 [] a55=product(a54,a135). % 1.90/2.10 0 [] a56=product(a55,a37). % 1.90/2.10 0 [] a57=product(a56,a134). % 1.90/2.10 0 [] a58=product(a57,a26). % 1.90/2.10 0 [] a59=product(a58,a138). % 1.90/2.10 0 [] a60=product(a59,a131). % 1.90/2.10 0 [] a61=product(a60,a13). % 1.90/2.10 0 [] a62=product(a61,a1). % 1.90/2.10 0 [] a63=product(a62,a96). % 1.90/2.10 0 [] a64=product(a63,a127). % 1.90/2.10 0 [] a65=product(a64,a41). % 1.90/2.10 0 [] a66=product(a65,a2). % 1.90/2.10 0 [] a67=product(a66,a92). % 1.90/2.10 0 [] a68=product(a67,a98). % 1.90/2.10 0 [] a69=product(a68,a32). % 1.90/2.10 0 [] a70=product(a69,a13). % 1.90/2.10 0 [] a71=product(a70,a118). % 1.90/2.10 0 [] a72=product(a71,a109). % 1.90/2.10 0 [] a73=product(a72,a82). % 1.90/2.10 0 [] a74=product(a73,a32). % 1.90/2.10 0 [] a75=product(a74,a14). % 1.90/2.10 0 [] a76=product(a75,a68). % 1.90/2.10 0 [] a77=product(a76,a114). % 1.90/2.10 0 [] a78=product(a77,a13). % 1.90/2.10 0 [] a79=product(a78,a33). % 1.90/2.10 0 [] a80=product(a79,a119). % 1.90/2.10 0 [] a81=product(a80,a70). % 1.90/2.10 0 [] a82=product(a81,a109). % 1.90/2.10 0 [] a83=product(a82,a118). % 1.90/2.10 0 [] a84=product(a83,a39). % 1.90/2.10 0 [] a85=product(a84,a5). % 1.90/2.10 0 [] a86=product(a85,a30). % 1.90/2.10 0 [] a87=product(a86,a104). % 1.90/2.10 0 [] a88=product(a87,a4). % 1.90/2.10 0 [] a89=product(a88,a14). % 1.90/2.10 0 [] a90=product(a89,a41). % 1.90/2.10 0 [] a91=product(a90,a100). % 1.90/2.10 0 [] a92=product(a91,a124). % 1.90/2.10 0 [] a93=product(a92,a2). % 1.90/2.10 0 [] a94=product(a93,a41). % 1.90/2.10 0 [] a95=product(a94,a127). % 1.90/2.10 0 [] a96=product(a95,a64). % 1.90/2.10 0 [] a97=product(a96,a42). % 1.90/2.10 0 [] a98=product(a97,a1). % 1.90/2.10 0 [] a99=product(a98,a92). % 1.90/2.10 0 [] a100=product(a99,a124). % 1.90/2.10 0 [] a101=product(a100,a14). % 1.90/2.10 0 [] a102=product(a101,a40). % 1.90/2.10 0 [] a103=product(a102,a4). % 1.90/2.10 0 [] a104=product(a103,a87). % 1.90/2.10 0 [] a105=product(a104,a30). % 1.90/2.10 0 [] a106=product(a105,a5). % 1.90/2.10 0 [] a107=product(a106,a84). % 1.90/2.10 0 [] a108=product(a107,a39). % 1.90/2.10 0 [] a109=product(a108,a118). % 1.90/2.10 0 [] a110=product(a109,a70). % 1.90/2.10 0 [] a111=product(a110,a119). % 1.90/2.10 0 [] a112=product(a111,a79). % 1.90/2.10 0 [] a113=product(a112,a33). % 1.90/2.10 0 [] a114=product(a113,a13). % 1.90/2.10 0 [] a115=product(a114,a68). % 1.90/2.10 0 [] a116=product(a115,a14). % 1.90/2.10 0 [] a117=product(a116,a74). % 1.90/2.10 0 [] a118=product(a117,a32). % 1.90/2.10 0 [] a119=product(a118,a70). % 1.90/2.10 0 [] a120=product(a119,a13). % 1.90/2.10 0 [] a121=product(a120,a32). % 1.90/2.10 0 [] a122=product(a121,a68). % 1.90/2.10 0 [] a123=product(a122,a115). % 1.90/2.10 0 [] a124=product(a123,a75). % 1.90/2.10 0 [] a125=product(a124,a2). % 1.90/2.10 0 [] a126=product(a125,a65). % 1.90/2.10 0 [] a127=product(a126,a41). % 1.90/2.10 0 [] a128=product(a127,a96). % 1.90/2.10 0 [] a129=product(a128,a62). % 1.90/2.10 0 [] a130=product(a129,a1). % 1.90/2.10 0 [] a131=product(a130,a13). % 1.90/2.10 0 [] a132=product(a131,a138). % 1.90/2.10 0 [] a133=product(a132,a58). % 1.90/2.10 0 [] a134=product(a133,a26). % 1.90/2.10 0 [] a135=product(a134,a37). % 1.90/2.10 0 [] a136=product(a135,a29). % 1.90/2.10 0 [] a137=product(a136,a39). % 1.90/2.10 0 [] a138=product(a137,a51). % 1.90/2.10 0 [] a139=product(a138,a20). % 1.90/2.10 0 [] a140=product(a139,a47). % 1.90/2.10 0 [] a141=product(a140,a11). % 1.90/2.10 0 [] a1=product(a141,a23). % 1.90/2.10 0 [] tuple(a1,a2,a41,a42,a3,a40,a4,a13,a14,a5,a38,a39,a6,a135,a136,a7,a52,a51,a8,a16,a17,a9,a55,a56,a10,a133,a134,a11,a36,a37,a12,a21,a20,a23,a31,a32,a15,a53,a28,a29,a18,a132,a19,a58,a57,a20,a25,a26,a34,a35,a140,a44,a45,a24,a48,a49,a138,a137,a27,a30,a33,a130,a131,a59,a60,a139,a46,a47,a43,a61,a62,a127,a128,a50,a54,a63,a95,a96,a64,a126,a65,a66,a67,a91,a92,a68,a97,a98,a69,a70,a71,a118,a117,a72,a108,a109,a73,a81,a82,a74,a75,a76,a77,a113,a114,a78,a79,a80,a119,a83,a84,a85,a86,a87,a103,a104,a88,a89,a90,a99,a100,a123,a124,a93,a94,a101,a102,a105,a106,a107,a110,a111,a112,a115,a116,a120,a121,a122,a125,a129)!=tuple(a2,a3,a42,a43,a4,a41,a5,a14,a15,a6,a39,a40,a7,a136,a137,a8,a53,a52,a9,a17,a18,a10,a56,a57,a11,a134,a135,a12,a37,a38,a13,a23,a21,a24,a32,a33,a16,a54,a29,a30,a19,a133,a20,a59,a58,a22,a26,a27,a35,a36,a141,a45,a46,a25,a49,a50,a139,a138,a28,a31,a34,a131,a132,a60,a61,a140,a47,a48,a44,a62,a63,a128,a129,a51,a55,a64,a96,a97,a65,a127,a66,a67,a68,a92,a93,a69,a98,a99,a70,a71,a72,a119,a118,a73,a109,a110,a74,a82,a83,a75,a76,a77,a78,a114,a115,a79,a80,a81,a120,a84,a85,a86,a87,a88,a104,a105,a89,a90,a91,a100,a101,a124,a125,a94,a95,a102,a103,a106,a107,a108,a111,a112,a113,a116,a117,a121,a122,a123,a126,a130). % 1.90/2.10 end_of_list. % 1.90/2.10 % 1.90/2.10 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 1.90/2.10 % 1.90/2.10 All clauses are units, and equality is present; the % 1.90/2.10 strategy will be Knuth-Bendix with positive clauses in sos. % 1.90/2.10 % 1.90/2.10 dependent: set(knuth_bendix). % 1.90/2.10 dependent: set(anl_eq). % 1.90/2.10 dependent: set(para_from). % 1.90/2.10 dependent: set(para_into). % 1.90/2.10 dependent: clear(para_from_right). % 1.90/2.10 dependent: clear(para_into_right). % 1.90/2.10 dependent: set(para_from_vars). % 1.90/2.10 dependent: set(eq_units_both_ways). % 1.90/2.10 dependent: set(dynamic_demod_all). % 1.90/2.10 dependent: set(dynamic_demod). % 1.90/2.10 dependent: set(order_eq). % 1.90/2.10 dependent: set(back_demod). % 1.90/2.10 dependent: set(lrpo). % 1.90/2.10 % 1.90/2.10 ------------> process usable: % 1.90/2.10 ** KEPT (pick-wt=283): 2 [copy,1,flip.1] tuple(a2,a3,a42,a43,a4,a41,a5,a14,a15,a6,a39,a40,a7,a136,a137,a8,a53,a52,a9,a17,a18,a10,a56,a57,a11,a134,a135,a12,a37,a38,a13,a23,a21,a24,a32,a33,a16,a54,a29,a30,a19,a133,a20,a59,a58,a22,a26,a27,a35,a36,a141,a45,a46,a25,a49,a50,a139,a138,a28,a31,a34,a131,a132,a60,a61,a140,a47,a48,a44,a62,a63,a128,a129,a51,a55,a64,a96,a97,a65,a127,a66,a67,a68,a92,a93,a69,a98,a99,a70,a71,a72,a119,a118,a73,a109,a110,a74,a82,a83,a75,a76,a77,a78,a114,a115,a79,a80,a81,a120,a84,a85,a86,a87,a88,a104,a105,a89,a90,a91,a100,a101,a124,a125,a94,a95,a102,a103,a106,a107,a108,a111,a112,a113,a116,a117,a121,a122,a123,a126,a130)!=tuple(a1,a2,a41,a42,a3,a40,a4,a13,a14,a5,a38,a39,a6,a135,a136,a7,a52,a51,a8,a16,a17,a9,a55,a56,a10,a133,a134,a11,a36,a37,a12,a21,a20,a23,a31,a32,a15,a53,a28,a29,a18,a132,a19,a58,a57,a20,a25,a26,a34,a35,a140,a44,a45,a24,a48,a49,a138,a137,a27,a30,a33,a130,a131,a59,a60,a139,a46,a47,a43,a61,a62,a127,a128,a50,a54,a63,a95,a96,a64,a126,a65,a66,a67,a91,a92,a68,a97,a98,a69,a70,a71,a118,a117,a72,a108,a109,a73,a81,a82,a74,a75,a76,a77,a113,a114,a78,a79,a80,a119,a83,a84,a85,a86,a87,a103,a104,a88,a89,a90,a99,a100,a123,a124,a93,a94,a101,a102,a105,a106,a107,a110,a111,a112,a115,a116,a120,a121,a122,a125,a129). % 1.90/2.10 % 1.90/2.10 ------------> process sos: % 1.90/2.10 ** KEPT (pick-wt=3): 3 [] A=A. % 1.90/2.10 ** KEPT (pick-wt=5): 4 [] product(A,A)=A. % 1.90/2.10 ---> New Demodulator: 5 [new_demod,4] product(A,A)=A. % 1.90/2.10 ** KEPT (pick-wt=7): 6 [] product(product(A,B),B)=A. % 1.90/2.10 ---> New Demodulator: 7 [new_demod,6] product(product(A,B),B)=A. % 1.90/2.10 ** KEPT (pick-wt=13): 8 [] product(product(A,B),C)=product(product(A,C),product(B,C)). % 1.90/2.10 ** KEPT (pick-wt=5): 10 [copy,9,flip.1] product(a1,a42)=a2. % 1.90/2.10 ---> New Demodulator: 11 [new_demod,10] product(a1,a42)=a2. % 1.90/2.11 ** KEPT (pick-wt=5): 13 [copy,12,flip.1] product(a2,a41)=a3. % 1.90/2.11 ---> New Demodulator: 14 [new_demod,13] product(a2,a41)=a3. % 1.90/2.11 ** KEPT (pick-wt=5): 16 [copy,15,flip.1] product(a3,a14)=a4. % 1.90/2.11 ---> New Demodulator: 17 [new_demod,16] product(a3,a14)=a4. % 1.90/2.11 ** KEPT (pick-wt=5): 19 [copy,18,flip.1] product(a4,a39)=a5. % 1.90/2.11 ---> New Demodulator: 20 [new_demod,19] product(a4,a39)=a5. % 1.90/2.11 ** KEPT (pick-wt=5): 22 [copy,21,flip.1] product(a5,a136)=a6. % 1.90/2.11 ---> New Demodulator: 23 [new_demod,22] product(a5,a136)=a6. % 1.90/2.11 ** KEPT (pick-wt=5): 25 [copy,24,flip.1] product(a6,a52)=a7. % 1.90/2.11 ---> New Demodulator: 26 [new_demod,25] product(a6,a52)=a7. % 1.90/2.11 ** KEPT (pick-wt=5): 28 [copy,27,flip.1] product(a7,a17)=a8. % 1.90/2.11 ---> New Demodulator: 29 [new_demod,28] product(a7,a17)=a8. % 1.90/2.11 ** KEPT (pick-wt=5): 31 [copy,30,flip.1] product(a8,a56)=a9. % 1.90/2.11 ---> New Demodulator: 32 [new_demod,31] product(a8,a56)=a9. % 1.90/2.11 ** KEPT (pick-wt=5): 34 [copy,33,flip.1] product(a9,a134)=a10. % 1.90/2.11 ---> New Demodulator: 35 [new_demod,34] product(a9,a134)=a10. % 1.90/2.11 ** KEPT (pick-wt=5): 37 [copy,36,flip.1] product(a10,a37)=a11. % 1.90/2.11 ---> New Demodulator: 38 [new_demod,37] product(a10,a37)=a11. % 1.90/2.11 ** KEPT (pick-wt=5): 40 [copy,39,flip.1] product(a11,a21)=a12. % 1.90/2.11 ---> New Demodulator: 41 [new_demod,40] product(a11,a21)=a12. % 1.90/2.11 ** KEPT (pick-wt=5): 43 [copy,42,flip.1] product(a12,a23)=a13. % 1.90/2.11 ---> New Demodulator: 44 [new_demod,43] product(a12,a23)=a13. % 1.90/2.11 ** KEPT (pick-wt=5): 46 [copy,45,flip.1] product(a13,a32)=a14. % 1.90/2.11 ---> New Demodulator: 47 [new_demod,46] product(a13,a32)=a14. % 1.90/2.11 ** KEPT (pick-wt=5): 49 [copy,48,flip.1] product(a14,a53)=a15. % 1.90/2.11 ---> New Demodulator: 50 [new_demod,49] product(a14,a53)=a15. % 1.90/2.11 ** KEPT (pick-wt=5): 52 [copy,51,flip.1] product(a15,a136)=a16. % 1.90/2.11 ---> New Demodulator: 53 [new_demod,52] product(a15,a136)=a16. % 1.90/2.11 ** KEPT (pick-wt=5): 55 [copy,54,flip.1] product(a16,a29)=a17. % 1.90/2.11 ---> New Demodulator: 56 [new_demod,55] product(a16,a29)=a17. % 1.90/2.11 ** KEPT (pick-wt=5): 58 [copy,57,flip.1] product(a17,a133)=a18. % 1.90/2.11 ---> New Demodulator: 59 [new_demod,58] product(a17,a133)=a18. % 1.90/2.11 ** KEPT (pick-wt=5): 61 [copy,60,flip.1] product(a18,a58)=a19. % 1.90/2.11 ---> New Demodulator: 62 [new_demod,61] product(a18,a58)=a19. % 1.90/2.11 ** KEPT (pick-wt=5): 64 [copy,63,flip.1] product(a19,a26)=a20. % 1.90/2.11 ---> New Demodulator: 65 [new_demod,64] product(a19,a26)=a20. % 1.90/2.11 ** KEPT (pick-wt=5): 67 [copy,66,flip.1] product(a20,a35)=a21. % 1.90/2.11 ---> New Demodulator: 68 [new_demod,67] product(a20,a35)=a21. % 1.90/2.11 ** KEPT (pick-wt=5): 70 [copy,69,flip.1] product(a21,a141)=a22. % 1.90/2.11 ---> New Demodulator: 71 [new_demod,70] product(a21,a141)=a22. % 1.90/2.11 ** KEPT (pick-wt=5): 73 [copy,72,flip.1] product(a22,a45)=a23. % 1.90/2.11 ---> New Demodulator: 74 [new_demod,73] product(a22,a45)=a23. % 1.90/2.11 ** KEPT (pick-wt=5): 76 [copy,75,flip.1] product(a23,a35)=a24. % 1.90/2.11 ---> New Demodulator: 77 [new_demod,76] product(a23,a35)=a24. % 1.90/2.11 ** KEPT (pick-wt=5): 79 [copy,78,flip.1] product(a24,a49)=a25. % 1.90/2.11 ---> New Demodulator: 80 [new_demod,79] product(a24,a49)=a25. % 1.90/2.11 ** KEPT (pick-wt=5): 82 [copy,81,flip.1] product(a25,a138)=a26. % 1.90/2.11 ---> New Demodulator: 83 [new_demod,82] product(a25,a138)=a26. % 1.90/2.11 ** KEPT (pick-wt=5): 85 [copy,84,flip.1] product(a26,a8)=a27. % 1.90/2.11 ---> New Demodulator: 86 [new_demod,85] product(a26,a8)=a27. % 1.90/2.11 ** KEPT (pick-wt=5): 88 [copy,87,flip.1] product(a27,a37)=a28. % 1.90/2.11 ---> New Demodulator: 89 [new_demod,88] product(a27,a37)=a28. % 1.90/2.11 ** KEPT (pick-wt=5): 91 [copy,90,flip.1] product(a28,a17)=a29. % 1.90/2.11 ---> New Demodulator: 92 [new_demod,91] product(a28,a17)=a29. % 1.90/2.11 ** KEPT (pick-wt=5): 94 [copy,93,flip.1] product(a29,a14)=a30. % 1.90/2.11 ---> New Demodulator: 95 [new_demod,94] product(a29,a14)=a30. % 1.90/2.11 ** KEPT (pick-wt=5): 97 [copy,96,flip.1] product(a30,a5)=a31. % 1.90/2.11 ---> New Demodulator: 98 [new_demod,97] product(a30,a5)=a31. % 1.90/2.11 ** KEPT (pick-wt=5): 100 [copy,99,flip.1] product(a31,a39)=a32. % 1.90/2.11 ---> New Demodulator: 101 [new_demod,100] product(a31,a39)=a32. % 1.90/2.11 ** KEPT (pick-wt=5): 103 [copy,102,flip.1] product(a32,a13)=a33. % 1.90/2.11 ---> New Demodulator: 104 [new_demod,103] product(a32,a13)=a33. % 1.90/2.11 ** KEPT (pick-wt=5): 106 [copy,105,flip.1] product(a33,a131)=a34. % 1.90/2.11 ---> New Demodulator: 107 [new_demod,106] product(a33,a131)=a34. % 1.90/2.11 ** KEPT (pick-wt=5): 109 [copy,108,flip.1] product(a34,a60)=a35. % 1.90/2.11 ---> New Demodulator: 110 [new_demod,109] product(a34,a60)=a35. % 1.90/2.11 ** KEPT (pick-wt=5): 112 [copy,111,flip.1] product(a35,a139)=a36. % 1.90/2.11 ---> New Demodulator: 113 [new_demod,112] product(a35,a139)=a36. % 1.90/2.11 ** KEPT (pick-wt=5): 115 [copy,114,flip.1] product(a36,a47)=a37. % 1.90/2.11 ---> New Demodulator: 116 [new_demod,115] product(a36,a47)=a37. % 1.90/2.11 ** KEPT (pick-wt=5): 118 [copy,117,flip.1] product(a37,a17)=a38. % 1.90/2.11 ---> New Demodulator: 119 [new_demod,118] product(a37,a17)=a38. % 1.90/2.11 ** KEPT (pick-wt=5): 121 [copy,120,flip.1] product(a38,a7)=a39. % 1.90/2.11 ---> New Demodulator: 122 [new_demod,121] product(a38,a7)=a39. % 1.90/2.11 ** KEPT (pick-wt=5): 124 [copy,123,flip.1] product(a39,a4)=a40. % 1.90/2.11 ---> New Demodulator: 125 [new_demod,124] product(a39,a4)=a40. % 1.90/2.11 ** KEPT (pick-wt=5): 127 [copy,126,flip.1] product(a40,a14)=a41. % 1.90/2.11 ---> New Demodulator: 128 [new_demod,127] product(a40,a14)=a41. % 1.90/2.11 ** KEPT (pick-wt=5): 130 [copy,129,flip.1] product(a41,a2)=a42. % 1.90/2.11 ---> New Demodulator: 131 [new_demod,130] product(a41,a2)=a42. % 1.90/2.11 ** KEPT (pick-wt=5): 133 [copy,132,flip.1] product(a42,a62)=a43. % 1.90/2.11 ---> New Demodulator: 134 [new_demod,133] product(a42,a62)=a43. % 1.90/2.11 ** KEPT (pick-wt=5): 136 [copy,135,flip.1] product(a43,a128)=a44. % 1.90/2.11 ---> New Demodulator: 137 [new_demod,136] product(a43,a128)=a44. % 1.90/2.11 ** KEPT (pick-wt=5): 139 [copy,138,flip.1] product(a44,a23)=a45. % 1.90/2.11 ---> New Demodulator: 140 [new_demod,139] product(a44,a23)=a45. % 1.90/2.11 ** KEPT (pick-wt=5): 142 [copy,141,flip.1] product(a45,a141)=a46. % 1.90/2.11 ---> New Demodulator: 143 [new_demod,142] product(a45,a141)=a46. % 1.90/2.11 ** KEPT (pick-wt=5): 145 [copy,144,flip.1] product(a46,a11)=a47. % 1.90/2.11 ---> New Demodulator: 146 [new_demod,145] product(a46,a11)=a47. % 1.90/2.11 ** KEPT (pick-wt=5): 148 [copy,147,flip.1] product(a47,a20)=a48. % 1.90/2.11 ---> New Demodulator: 149 [new_demod,148] product(a47,a20)=a48. % 1.90/2.11 ** KEPT (pick-wt=5): 151 [copy,150,flip.1] product(a48,a138)=a49. % 1.90/2.11 ---> New Demodulator: 152 [new_demod,151] product(a48,a138)=a49. % 1.90/2.11 ** KEPT (pick-wt=5): 154 [copy,153,flip.1] product(a49,a131)=a50. % 1.90/2.11 ---> New Demodulator: 155 [new_demod,154] product(a49,a131)=a50. % 1.90/2.11 ** KEPT (pick-wt=5): 157 [copy,156,flip.1] product(a50,a59)=a51. % 1.90/2.11 ---> New Demodulator: 158 [new_demod,157] product(a50,a59)=a51. % 1.90/2.11 ** KEPT (pick-wt=5): 160 [copy,159,flip.1] product(a51,a39)=a52. % 1.90/2.11 ---> New Demodulator: 161 [new_demod,160] product(a51,a39)=a52. % 1.90/2.11 ** KEPT (pick-wt=5): 163 [copy,162,flip.1] product(a52,a136)=a53. % 1.90/2.11 ---> New Demodulator: 164 [new_demod,163] product(a52,a136)=a53. % 1.90/2.11 ** KEPT (pick-wt=5): 166 [copy,165,flip.1] product(a53,a29)=a54. % 1.90/2.11 ---> New Demodulator: 167 [new_demod,166] product(a53,a29)=a54. % 1.90/2.11 ** KEPT (pick-wt=5): 169 [copy,168,flip.1] product(a54,a135)=a55. % 1.90/2.11 ---> New Demodulator: 170 [new_demod,169] product(a54,a135)=a55. % 1.90/2.11 ** KEPT (pick-wt=5): 172 [copy,171,flip.1] product(a55,a37)=a56. % 1.90/2.11 ---> New Demodulator: 173 [new_demod,172] product(a55,a37)=a56. % 1.90/2.11 ** KEPT (pick-wt=5): 175 [copy,174,flip.1] product(a56,a134)=a57. % 1.90/2.11 ---> New Demodulator: 176 [new_demod,175] product(a56,a134)=a57. % 1.90/2.11 ** KEPT (pick-wt=5): 178 [copy,177,flip.1] product(a57,a26)=a58. % 1.90/2.11 ---> New Demodulator: 179 [new_demod,178] product(a57,a26)=a58. % 1.90/2.11 ** KEPT (pick-wt=5): 181 [copy,180,flip.1] product(a58,a138)=a59. % 1.90/2.11 ---> New Demodulator: 182 [new_demod,181] product(a58,a138)=a59. % 1.90/2.11 ** KEPT (pick-wt=5): 184 [copy,183,flip.1] product(a59,a131)=a60. % 1.90/2.11 ---> New Demodulator: 185 [new_demod,184] product(a59,a131)=a60. % 1.90/2.11 ** KEPT (pick-wt=5): 187 [copy,186,flip.1] product(a60,a13)=a61. % 1.90/2.11 ---> New Demodulator: 188 [new_demod,187] product(a60,a13)=a61. % 1.90/2.11 ** KEPT (pick-wt=5): 190 [copy,189,flip.1] product(a61,a1)=a62. % 1.90/2.11 ---> New Demodulator: 191 [new_demod,190] product(a61,a1)=a62. % 1.90/2.11 ** KEPT (pick-wt=5): 193 [copy,192,flip.1] product(a62,a96)=a63. % 1.90/2.11 ---> New Demodulator: 194 [new_demod,193] product(a62,a96)=a63. % 1.90/2.11 ** KEPT (pick-wt=5): 196 [copy,195,flip.1] product(a63,a127)=a64. % 1.90/2.11 ---> New Demodulator: 197 [new_demod,196] product(a63,a127)=a64. % 1.90/2.11 ** KEPT (pick-wt=5): 199 [copy,198,flip.1] product(a64,a41)=a65. % 1.90/2.11 ---> New Demodulator: 200 [new_demod,199] product(a64,a41)=a65. % 1.90/2.11 ** KEPT (pick-wt=5): 202 [copy,201,flip.1] product(a65,a2)=a66. % 1.90/2.11 ---> New Demodulator: 203 [new_demod,202] product(a65,a2)=a66. % 1.90/2.11 ** KEPT (pick-wt=5): 205 [copy,204,flip.1] product(a66,a92)=a67. % 1.90/2.11 ---> New Demodulator: 206 [new_demod,205] product(a66,a92)=a67. % 1.90/2.11 ** KEPT (pick-wt=5): 208 [copy,207,flip.1] product(a67,a98)=a68. % 1.90/2.11 ---> New Demodulator: 209 [new_demod,208] product(a67,a98)=a68. % 1.90/2.11 ** KEPT (pick-wt=5): 211 [copy,210,flip.1] product(a68,a32)=a69. % 1.90/2.11 ---> New Demodulator: 212 [new_demod,211] product(a68,a32)=a69. % 1.90/2.11 ** KEPT (pick-wt=5): 214 [copy,213,flip.1] product(a69,a13)=a70. % 1.90/2.11 ---> New Demodulator: 215 [new_demod,214] product(a69,a13)=a70. % 1.90/2.11 ** KEPT (pick-wt=5): 217 [copy,216,flip.1] product(a70,a118)=a71. % 1.90/2.11 ---> New Demodulator: 218 [new_demod,217] product(a70,a118)=a71. % 1.90/2.11 ** KEPT (pick-wt=5): 220 [copy,219,flip.1] product(a71,a109)=a72. % 1.90/2.11 ---> New Demodulator: 221 [new_demod,220] product(a71,a109)=a72. % 1.90/2.11 ** KEPT (pick-wt=5): 223 [copy,222,flip.1] product(a72,a82)=a73. % 1.90/2.11 ---> New Demodulator: 224 [new_demod,223] product(a72,a82)=a73. % 1.90/2.11 ** KEPT (pick-wt=5): 226 [copy,225,flip.1] product(a73,a32)=a74. % 1.90/2.11 ---> New Demodulator: 227 [new_demod,226] product(a73,a32)=a74. % 1.90/2.11 ** KEPT (pick-wt=5): 229 [copy,228,flip.1] product(a74,a14)=a75. % 1.90/2.11 ---> New Demodulator: 230 [new_demod,229] product(a74,a14)=a75. % 1.90/2.11 ** KEPT (pick-wt=5): 232 [copy,231,flip.1] product(a75,a68)=a76. % 1.90/2.11 ---> New Demodulator: 233 [new_demod,232] product(a75,a68)=a76. % 1.90/2.11 ** KEPT (pick-wt=5): 235 [copy,234,flip.1] product(a76,a114)=a77. % 1.90/2.11 ---> New Demodulator: 236 [new_demod,235] product(a76,a114)=a77. % 1.90/2.11 ** KEPT (pick-wt=5): 238 [copy,237,flip.1] product(a77,a13)=a78. % 1.90/2.11 ---> New Demodulator: 239 [new_demod,238] product(a77,a13)=a78. % 1.90/2.11 ** KEPT (pick-wt=5): 241 [copy,240,flip.1] product(a78,a33)=a79. % 1.90/2.11 ---> New Demodulator: 242 [new_demod,241] product(a78,a33)=a79. % 1.90/2.11 ** KEPT (pick-wt=5): 244 [copy,243,flip.1] product(a79,a119)=a80. % 1.90/2.11 ---> New Demodulator: 245 [new_demod,244] product(a79,a119)=a80. % 1.90/2.11 ** KEPT (pick-wt=5): 247 [copy,246,flip.1] product(a80,a70)=a81. % 1.90/2.11 ---> New Demodulator: 248 [new_demod,247] product(a80,a70)=a81. % 1.90/2.11 ** KEPT (pick-wt=5): 250 [copy,249,flip.1] product(a81,a109)=a82. % 1.90/2.11 ---> New Demodulator: 251 [new_demod,250] product(a81,a109)=a82. % 1.90/2.11 ** KEPT (pick-wt=5): 253 [copy,252,flip.1] product(a82,a118)=a83. % 1.90/2.11 ---> New Demodulator: 254 [new_demod,253] product(a82,a118)=a83. % 1.90/2.11 ** KEPT (pick-wt=5): 256 [copy,255,flip.1] product(a83,a39)=a84. % 1.90/2.11 ---> New Demodulator: 257 [new_demod,256] product(a83,a39)=a84. % 1.90/2.11 ** KEPT (pick-wt=5): 259 [copy,258,flip.1] product(a84,a5)=a85. % 1.90/2.11 ---> New Demodulator: 260 [new_demod,259] product(a84,a5)=a85. % 1.90/2.11 ** KEPT (pick-wt=5): 262 [copy,261,flip.1] product(a85,a30)=a86. % 1.90/2.11 ---> New Demodulator: 263 [new_demod,262] product(a85,a30)=a86. % 1.90/2.11 ** KEPT (pick-wt=5): 265 [copy,264,flip.1] product(a86,a104)=a87. % 1.90/2.11 ---> New Demodulator: 266 [new_demod,265] product(a86,a104)=a87. % 1.90/2.11 ** KEPT (pick-wt=5): 268 [copy,267,flip.1] product(a87,a4)=a88. % 1.90/2.11 ---> New Demodulator: 269 [new_demod,268] product(a87,a4)=a88. % 1.90/2.11 ** KEPT (pick-wt=5): 271 [copy,270,flip.1] product(a88,a14)=a89. % 1.90/2.11 ---> New Demodulator: 272 [new_demod,271] product(a88,a14)=a89. % 1.90/2.11 ** KEPT (pick-wt=5): 274 [copy,273,flip.1] product(a89,a41)=a90. % 1.90/2.11 ---> New Demodulator: 275 [new_demod,274] product(a89,a41)=a90. % 1.90/2.11 ** KEPT (pick-wt=5): 277 [copy,276,flip.1] product(a90,a100)=a91. % 1.90/2.11 ---> New Demodulator: 278 [new_demod,277] product(a90,a100)=a91. % 1.90/2.11 ** KEPT (pick-wt=5): 280 [copy,279,flip.1] product(a91,a124)=a92. % 1.90/2.11 ---> New Demodulator: 281 [new_demod,280] product(a91,a124)=a92. % 1.90/2.11 ** KEPT (pick-wt=5): 283 [copy,282,flip.1] product(a92,a2)=a93. % 1.90/2.11 ---> New Demodulator: 284 [new_demod,283] product(a92,a2)=a93. % 1.90/2.11 ** KEPT (pick-wt=5): 286 [copy,285,flip.1] product(a93,a41)=a94. % 1.90/2.11 ---> New Demodulator: 287 [new_demod,286] product(a93,a41)=a94. % 1.90/2.11 ** KEPT (pick-wt=5): 289 [copy,288,flip.1] product(a94,a127)=a95. % 1.90/2.11 ---> New Demodulator: 290 [new_demod,289] product(a94,a127)=a95. % 1.90/2.11 ** KEPT (pick-wt=5): 292 [copy,291,flip.1] product(a95,a64)=a96. % 1.90/2.11 ---> New Demodulator: 293 [new_demod,292] product(a95,a64)=a96. % 1.90/2.11 ** KEPT (pick-wt=5): 295 [copy,294,flip.1] product(a96,a42)=a97. % 1.90/2.11 ---> New Demodulator: 296 [new_demod,295] product(a96,a42)=a97. % 1.90/2.11 ** KEPT (pick-wt=5): 298 [copy,297,flip.1] product(a97,a1)=a98. % 1.90/2.11 ---> New Demodulator: 299 [new_demod,298] product(a97,a1)=a98. % 1.90/2.11 ** KEPT (pick-wt=5): 301 [copy,300,flip.1] product(a98,a92)=a99. % 1.90/2.11 ---> New Demodulator: 302 [new_demod,301] product(a98,a92)=a99. % 1.90/2.11 ** KEPT (pick-wt=5): 304 [copy,303,flip.1] product(a99,a124)=a100. % 1.90/2.11 ---> New Demodulator: 305 [new_demod,304] product(a99,a124)=a100. % 1.90/2.11 ** KEPT (pick-wt=5): 307 [copy,306,flip.1] product(a100,a14)=a101. % 1.90/2.11 ---> New Demodulator: 308 [new_demod,307] product(a100,a14)=a101. % 1.90/2.11 ** KEPT (pick-wt=5): 310 [copy,309,flip.1] product(a101,a40)=a102. % 1.90/2.11 ---> New Demodulator: 311 [new_demod,310] product(a101,a40)=a102. % 1.90/2.11 ** KEPT (pick-wt=5): 313 [copy,312,flip.1] product(a102,a4)=a103. % 1.90/2.11 ---> New Demodulator: 314 [new_demod,313] product(a102,a4)=a103. % 1.90/2.11 ** KEPT (pick-wt=5): 316 [copy,315,flip.1] product(a103,a87)=a104. % 1.90/2.11 ---> New Demodulator: 317 [new_demod,316] product(a103,a87)=a104. % 1.90/2.11 ** KEPT (pick-wt=5): 319 [copy,318,flip.1] product(a104,a30)=a105. % 1.90/2.11 ---> New Demodulator: 320 [new_demod,319] product(a104,a30)=a105. % 1.90/2.11 ** KEPT (pick-wt=5): 322 [copy,321,flip.1] product(a105,a5)=a106. % 1.90/2.11 ---> New Demodulator: 323 [new_demod,322] product(a105,a5)=a106. % 1.90/2.11 ** KEPT (pick-wt=5): 325 [copy,324,flip.1] product(a106,a84)=a107. % 1.90/2.11 ---> New Demodulator: 326 [new_demod,325] product(a106,a84)=a107. % 1.90/2.11 ** KEPT (pick-wt=5): 328 [copy,327,flip.1] product(a107,a39)=a108. % 1.90/2.11 ---> New Demodulator: 329 [new_demod,328] product(a107,a39)=a108. % 1.90/2.11 ** KEPT (pick-wt=5): 331 [copy,330,flip.1] product(a108,a118)=a109. % 1.90/2.11 ---> New Demodulator: 332 [new_demod,331] product(a108,a118)=a109. % 1.90/2.11 ** KEPT (pick-wt=5): 334 [copy,333,flip.1] product(a109,a70)=a110. % 1.90/2.11 ---> New Demodulator: 335 [new_demod,334] product(a109,a70)=a110. % 1.90/2.11 ** KEPT (pick-wt=5): 337 [copy,336,flip.1] product(a110,a119)=a111. % 1.90/2.11 ---> New Demodulator: 338 [new_demod,337] product(a110,a119)=a111. % 1.90/2.11 ** KEPT (pick-wt=5): 340 [copy,339,flip.1] product(a111,a79)=a112. % 1.90/2.11 ---> New Demodulator: 341 [new_demod,340] product(a111,a79)=a112. % 1.90/2.11 ** KEPT (pick-wt=5): 343 [copy,342,flip.1] product(a112,a33)=a113. % 1.90/2.11 ---> New Demodulator: 344 [new_demod,343] product(a112,a33)=a113. % 1.90/2.11 ** KEPT (pick-wt=5): 346 [copy,345,flip.1] product(a113,a13)=a114. % 1.90/2.11 ---> New Demodulator: 347 [new_demod,346] product(a113,a13)=a114. % 1.90/2.11 ** KEPT (pick-wt=5): 349 [copy,348,flip.1] product(a114,a68)=a115. % 1.90/2.11 ---> New Demodulator: 350 [new_demod,349] product(a114,a68)=a115. % 1.90/2.11 ** KEPT (pick-wt=5): 352 [copy,351,flip.1] product(a115,a14)=a116. % 1.90/2.11 ---> New Demodulator: 353 [new_demod,352] product(a115,a14)=a116. % 1.90/2.11 ** KEPT (pick-wt=5): 355 [copy,354,flip.1] product(a116,a74)=a117. % 1.90/2.11 ---> New Demodulator: 356 [new_demod,355] product(a116,a74)=a117. % 1.90/2.11 ** KEPT (pick-wt=5): 358 [copy,357,flip.1] product(a117,a32)=a118. % 1.90/2.11 ---> New Demodulator: 359 [new_demod,358] product(a117,a32)=a118. % 1.90/2.11 ** KEPT (pick-wt=5): 361 [copy,360,flip.1] product(a118,a70)=a119. % 1.90/2.11 ---> New Demodulator: 362 [new_demod,361] product(a118,a70)=a119. % 1.90/2.11 ** KEPT (pick-wt=5): 364 [copy,363,flip.1] product(a119,a13)=a120. % 1.90/2.11 ---> New Demodulator: 365 [new_demod,364] product(a119,a13)=a120. % 1.90/2.11 ** KEPT (pick-wt=5): 367 [copy,366,flip.1] product(a120,a32)=a121. % 1.90/2.11 ---> New Demodulator: 368 [new_demod,367] product(a120,a32)=a121. % 1.90/2.11 ** KEPT (pick-wt=5): 370 [copy,369,flip.1] product(a121,a68)=a122. % 1.90/2.11 ---> New Demodulator: 371 [new_demod,370] product(a121,a68)=a122. % 1.90/2.11 ** KEPT (pick-wt=5): 373 [copy,372,flip.1] product(a122,a115)=a123. % 1.90/2.11 ---> New Demodulator: 374 [new_demod,373] product(a122,a115)=a123. % 1.90/2.11 ** KEPT (pick-wt=5): 376 [copy,375,flip.1] product(a123,a75)=a124. % 1.90/2.11 ---> New Demodulator: 377 [new_demod,376] product(a123,a75)=a124. % 1.90/2.11 ** KEPT (pick-wt=5): 379 [copy,378,flip.1] product(a124,a2)=a125. % 1.90/2.11 ---> New Demodulator: 380 [new_demod,379] product(a124,a2)=a125. % 1.90/2.11 ** KEPT (pick-wt=5): 382 [copy,381,flip.1] product(a125,a65)=a126. % 1.90/2.11 ---> New Demodulator: 383 [new_demod,382] product(a125,a65)=a126. % 1.90/2.11 ** KEPT (pick-wt=5): 385 [copy,384,flip.1] product(a126,a41)=a127. % 1.90/2.11 ---> New Demodulator: 386 [new_demod,385] product(a126,a41)=a127. % 1.90/2.11 ** KEPT (pick-wt=5): 388 [copy,387,flip.1] product(a127,a96)=a128. % 1.90/2.11 ---> New Demodulator: 389 [new_demod,388] product(a127,a96)=a128. % 1.90/2.11 ** KEPT (pick-wt=5): 391 [copy,390,flip.1] product(a128,a62)=a129. % 1.90/2.11 ---> New Demodulator: 392 [new_demod,391] product(a128,a62)=a129. % 1.90/2.11 ** KEPT (pick-wt=5): 394 [copy,393,flip.1] product(a129,a1)=a130. % 1.90/2.11 ---> New Demodulator: 395 [new_demod,394] product(a129,a1)=a130. % 1.90/2.11 ** KEPT (pick-wt=5): 397 [copy,396,flip.1] product(a130,a13)=a131. % 1.90/2.11 ---> New Demodulator: 398 [new_demod,397] product(a130,a13)=a131. % 1.90/2.11 ** KEPT (pick-wt=5): 400 [copy,399,flip.1] product(a131,a138)=a132. % 1.90/2.11 ---> New Demodulator: 401 [new_demod,400] product(a131,a138)=a132. % 1.90/2.11 ** KEPT (pick-wt=5): 403 [copy,402,flip.1] product(a132,a58)=a133. % 1.90/2.11 ---> New Demodulator: 404 [new_demod,403] product(a132,a58)=a133. % 1.90/2.11 ** KEPT (pick-wt=5): 406 [copy,405,flip.1] product(a133,a26)=a134. % 1.90/2.11 ---> New Demodulator: 407 [new_demod,406] product(a133,a26)=a134. % 1.90/2.11 ** KEPT (pick-wt=5): 409 [copy,408,flip.1] product(a134,a37)=a135. % 1.90/2.11 ---> New Demodulator: 410 [new_demod,409] product(a134,a37)=a135. % 1.90/2.11 ** KEPT (pick-wt=5): 412 [copy,411,flip.1] product(a135,a29)=a136. % 1.90/2.11 ---> New Demodulator: 413 [new_demod,412] product(a135,a29)=a136. % 1.90/2.11 ** KEPT (pick-wt=5): 415 [copy,414,flip.1] product(a136,a39)=a137. % 1.90/2.11 ---> New Demodulator: 416 [new_demod,415] product(a136,a39)=a137. % 1.90/2.11 ** KEPT (pick-wt=5): 418 [copy,417,flip.1] product(a137,a51)=a138. % 1.90/2.11 ---> New Demodulator: 419 [new_demod,418] product(a137,a51)=a138. % 1.90/2.11 ** KEPT (pick-wt=5): 421 [copy,420,flip.1] product(a138,a20)=a139. % 1.90/2.11 ---> New Demodulator: 422 [new_demod,421] product(a138,a20)=a139. % 1.90/2.11 ** KEPT (pick-wt=5): 424 [copy,423,flip.1] product(a139,a47)=a140. % 1.90/2.11 ---> New Demodulator: 425 [new_demod,424] product(a139,a47)=a140. % 1.90/2.11 ** KEPT (pick-wt=5): 427 [copy,426,flip.1] product(a140,a11)=a141. % 1.90/2.11 ---> New Demodulator: 428 [new_demod,427] product(a140,a11)=a141. % 1.90/2.11 ** KEPT (pick-wt=5): 430 [copy,429,flip.1] product(a141,a23)=a1. % 1.90/2.11 ---> New Demodulator: 431 [new_demod,430] product(a141,a23)=a1. % 1.90/2.11 Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] A=A. % 1.90/2.11 >>>> Starting back demodulation with 5. % 1.90/2.11 >>>> Starting back demodulation with 7. % 1.90/2.11 ** KEPT (pick-wt=13): 432 [copy,8,flip.1] product(product(A,B),product(C,B))=product(product(A,C),B). % 1.90/2.11 >>>> Starting back demodulation with 11. % 1.90/2.11 >>>> Starting back demodulation with 14. % 1.90/2.11 >>>> Starting back demodulation with 17. % 1.90/2.11 >>>> Starting back demodulation with 20. % 1.90/2.11 >>>> Starting back demodulation with 23. % 1.90/2.11 >>>> Starting back demodulation with 26. % 1.90/2.11 >>>> Starting back demodulation with 29. % 1.90/2.11 >>>> Starting back demodulation with 32. % 1.90/2.11 >>>> Starting back demodulation with 35. % 1.90/2.11 >>>> Starting back demodulation with 38. % 1.90/2.11 >>>> Starting back demodulation with 41. % 1.90/2.11 >>>> Starting back demodulation with 44. % 1.90/2.11 >>>> Starting back demodulation with 47. % 1.90/2.11 >>>> Starting back demodulation with 50. % 1.90/2.11 >>>> Starting back demodulation with 53. % 1.90/2.11 >>>> Starting back demodulation with 56. % 1.90/2.11 >>>> Starting back demodulation with 59. % 1.90/2.11 >>>> Starting back demodulation with 62. % 1.90/2.11 >>>> Starting back demodulation with 65. % 1.90/2.11 >>>> Starting back demodulation with 68. % 1.90/2.11 >>>> Starting back demodulation with 71. % 1.90/2.11 >>>> Starting back demodulation with 74. % 1.90/2.11 >>>> Starting back demodulation with 77. % 1.90/2.11 >>>> Starting back demodulation with 80. % 1.90/2.11 >>>> Starting back demodulation with 83. % 1.90/2.11 >>>> Starting back demodulation with 86. % 1.90/2.11 >>>> Starting back demodulation with 89. % 1.90/2.11 >>>> Starting back demodulation with 92. % 1.90/2.11 >>>> Starting back demodulation with 95. % 1.90/2.11 >>>> Starting back demodulation with 98. % 1.90/2.11 >>>> Starting back demodulation with 101. % 1.90/2.11 >>>> Starting back demodulation with 104. % 1.90/2.11 >>>> Starting back demodulation with 107. % 1.90/2.11 >>>> Starting back demodulation with 110. % 1.90/2.11 >>>> Starting back demodulation with 113. % 1.90/2.11 >>>> Starting back demodulation with 116. % 1.90/2.11 >>>> Starting back demodulation with 119. % 1.90/2.11 >>>> Starting back demodulation with 122. % 1.90/2.11 >>>> Starting back demodulation with 125. % 1.90/2.11 >>>> Starting back demodulation with 128. % 1.90/2.11 >>>> Starting back demodulation with 131. % 1.90/2.11 >>>> Starting back demodulation with 134. % 1.90/2.11 >>>> Starting back demodulation with 137. % 1.90/2.11 >>>> Starting back demodulation with 140. % 1.90/2.11 >>>> Starting back demodulation with 143. % 1.90/2.11 >>>> Starting back demodulation with 146. % 1.90/2.11 >>>> Starting back demodulation with 149. % 1.90/2.11 >>>> Starting back demodulation with 152. % 1.90/2.11 >>>> Starting back demodulation with 155. % 1.90/2.11 >>>> Starting back demodulation with 158. % 1.90/2.11 >>>> Starting back demodulation with 161. % 1.90/2.11 >>>> Starting back demodulation with 164. % 1.90/2.11 >>>> Starting back demodulation with 167. % 1.90/2.11 >>>> Starting back demodulation with 170. % 1.90/2.11 >>>> Starting back demodulation with 173. % 1.90/2.11 >>>> Starting back demodulation with 176. % 1.90/2.11 >>>> Starting back demodulation with 179. % 1.90/2.11 >>>> Starting back demodulation with 182. % 1.90/2.11 >>>> Starting back demodulation with 185. % 1.90/2.11 >>>> Starting back demodulation with 188. % 1.90/2.11 >>>> Starting back demodulation with 191. % 1.90/2.11 >>>> Starting back demodulation with 194. % 1.90/2.11 >>>> Starting back demodulation with 197. % 1.90/2.11 >>>> Starting back demodulation with 200. % 1.90/2.11 >>>> Starting back demodulation with 203. % 1.90/2.11 >>>> Starting back demodulation with 206. % 1.90/2.11 >>>> Starting back demodulation with 209. % 1.90/2.11 >>>> Starting back demodulation with 212. % 1.90/2.11 >>>> Starting back demodulation with 215. % 1.90/2.11 >>>> Starting back demodulation with 218. % 1.90/2.11 >>>> Starting back demodulation with 221. % 1.90/2.11 >>>> Starting back demodulation with 224. % 1.90/2.11 >>>> Starting back demodulation with 227. % 1.90/2.11 >>>> Starting back demodulation with 230. % 1.90/2.11 >>>> Starting back demodulation with 233. % 1.90/2.11 >>>> Starting back demodulation with 236. % 1.90/2.11 >>>> Starting back demodulation with 239. % 1.90/2.11 >>>> Starting back demodulation with 242. % 1.90/2.11 >>>> Starting back demodulation with 245. % 1.90/2.11 >>>> Starting back demodulation with 248. % 1.90/2.11 >>>> Starting back demodulation with 251. % 1.90/2.11 >>>> Starting back demodulation with 254. % 1.90/2.11 >>>> Starting back demodulation with 257. % 1.90/2.11 >>>> Starting back demodulation with 260. % 1.90/2.11 >>>> Starting back demodulation with 263. % 1.90/2.11 >>>> Starting back demodulation with 266. % 1.90/2.11 >>>> Starting back demodulation with 269. % 1.90/2.11 >>>> Starting back demodulation with 272. % 1.90/2.11 >>>> Starting back demodulation with 275. % 1.90/2.11 >>>> Starting back demodulation with 278. % 1.90/2.11 >>>> Starting back demodulation with 281. % 1.90/2.11 >>>> Starting back demodulation with 284. % 1.90/2.11 >>>> Starting back demodulation with 287. % 1.90/2.11 >>>> Starting back demodulation with 290. % 1.90/2.11 >>>> Starting back demodulation with 293. % 1.90/2.11 >>>> Starting back demodulation with 296. % 1.90/2.11 >>>> Starting back demodulation with 299. % 1.90/2.11 >>>> Starting back demodulation with 302. % 1.90/2.11 >>>> Starting back demodulation with 305. % 1.90/2.11 >>>> Starting back demodulation with 308. % 1.90/2.11 >>>> Starting back demodulation with 311. % 1.90/2.11 >>>> Starting back demodulation with 314. % 1.90/2.11 >>>> Starting back demodulation with 317. % 1.90/2.11 >>>> Starting back demodulation with 320. % 1.90/2.11 >>>> Starting back demodulation with 323. % 1.90/2.11 >>>> Starting back demodulation with 326. % 1.90/2.11 >>>> Starting back demodulation with 329. % 1.90/2.11 >>>> Starting back demodulation with 332. % 1.90/2.11 >>>> Starting back demodulation with 335. % 1.90/2.11 >>>> Starting back demodulation with 338. % 1.90/2.11 >>>> Starting back demodulation with 341. % 1.90/2.11 >>>> Starting back demodulation with 344. % 1.90/2.11 >>>> Starting back demodulation with 347. % 1.90/2.11 >>>> Starting back demodulation with 350. % 1.90/2.11 >>>> Starting back demodulation with 353. % 1.90/2.11 >>>> Starting back demodulation with 356. % 1.90/2.11 >>>> Starting back demodulation with 359. % 1.90/2.11 >>>> Starting back demodulation with 362. % 1.90/2.11 >>>> Starting back demodulation with 365. % 1.90/2.11 >>>> Starting back demodulation with 368. % 1.90/2.11 >>>> Starting back demodulation with 371. % 1.90/2.11 >>>> Starting back demodulation with 374. % 1.90/2.11 >>>> Starting back demodulation with 377. % 1.90/2.11 >>>> Starting back demodulation with 380. % 1.90/2.11 >>>> Starting back demodulation with 383. % 1.90/2.11 >>>> Starting back demodulation with 386. % 1.90/2.11 >>>> Starting back demodulation with 389. % 1.90/2.11 >>>> Starting back demodulation with 392. % 1.90/2.11 >>>> Starting back demodulation with 395. % 1.90/2.11 >>>> Starting back demodulation with 398. % 1.90/2.11 >>>> Starting back demodulation with 401. % 1.90/2.11 >>>> Starting back demodulation with 404. % 1.90/2.11 >>>> Starting back demodulation with 407. % 1.90/2.11 >>>> Starting back demodulation with 410. % 1.90/2.11 >>>> Starting back demodulation with 413. % 1.90/2.11 >>>> Starting back demodulation with 416. % 1.90/2.11 >>>> Starting back demodulation with 419. % 1.90/2.11 >>>> Starting back demodulation with 422. % 1.90/2.11 >>>> Starting back demodulation with 425. % 1.90/2.11 >>>> Starting back demodulation with 428. % 1.90/2.11 >>>> Starting back demodulation with 431. % 1.90/2.11 Following clause subsumed by 8 during input processing: 0 [copy,432,flip.1] product(product(A,B),C)=product(product(A,C),product(B,C)). % 1.90/2.11 % 1.90/2.11 ======= end of input processing ======= % 1.90/2.11 % 1.90/2.11 =========== start of search =========== % 1.90/2.11 % 1.90/2.11 % 1.90/2.11 Resetting weight limit to 5. % 1.96/2.15 % 1.96/2.15 % 1.96/2.15 Resetting weight limit to 5. % 1.96/2.15 % 1.96/2.15 sos_size=172 % 1.96/2.15 % 1.96/2.15 Search stopped because sos empty. % 1.96/2.15 % 1.96/2.15 % 1.96/2.15 Search stopped because sos empty. % 1.96/2.15 % 1.96/2.15 ============ end of search ============ % 1.96/2.15 % 1.96/2.15 -------------- statistics ------------- % 1.96/2.15 clauses given 320 % 1.96/2.15 clauses generated 5625 % 1.96/2.15 clauses kept 321 % 1.96/2.15 clauses forward subsumed 919 % 1.96/2.15 clauses back subsumed 0 % 1.96/2.15 Kbytes malloced 5859 % 1.96/2.15 % 1.96/2.15 ----------- times (seconds) ----------- % 1.96/2.15 user CPU time 0.05 (0 hr, 0 min, 0 sec) % 1.96/2.15 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 1.96/2.15 wall-clock time 2 (0 hr, 0 min, 2 sec) % 1.96/2.15 % 1.96/2.15 Process 28157 finished Wed Jul 27 01:44:53 2022 % 1.96/2.15 Otter interrupted % 1.96/2.15 PROOF NOT FOUND %------------------------------------------------------------------------------