%------------------------------------------------------------------------------ % File : EQP---0.9e % Problem : TOP052-1 : TPTP v8.1.0. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_eqp %s % Computer : n017.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:24:50 EDT 2022 % Result : Unknown 20.41s 20.80s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : TOP052-1 : TPTP v8.1.0. Released v8.1.0. % 0.11/0.12 % Command : tptp2X_and_run_eqp %s % 0.11/0.33 % Computer : n017.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Sun May 29 09:08:24 EDT 2022 % 0.11/0.33 % CPUTime : % 0.41/1.07 ----- EQP 0.9e, May 2009 ----- % 0.41/1.07 The job began on n017.cluster.edu, Sun May 29 09:08:24 2022 % 0.41/1.07 The command was "./eqp09e". % 0.41/1.07 % 0.41/1.07 set(prolog_style_variables). % 0.41/1.07 set(lrpo). % 0.41/1.07 set(basic_paramod). % 0.41/1.07 set(functional_subsume). % 0.41/1.07 set(ordered_paramod). % 0.41/1.07 set(prime_paramod). % 0.41/1.07 set(para_pairs). % 0.41/1.07 assign(pick_given_ratio,4). % 0.41/1.07 clear(print_kept). % 0.41/1.07 clear(print_new_demod). % 0.41/1.07 clear(print_back_demod). % 0.41/1.07 clear(print_given). % 0.41/1.07 assign(max_mem,64000). % 0.41/1.07 end_of_commands. % 0.41/1.07 % 0.41/1.07 Usable: % 0.41/1.07 end_of_list. % 0.41/1.07 % 0.41/1.07 Sos: % 0.41/1.07 0 (wt=-1) [] product(A,A) = A. % 0.41/1.07 0 (wt=-1) [] product(product(A,B),B) = A. % 0.41/1.07 0 (wt=-1) [] product(product(A,B),C) = product(product(A,C),product(B,C)). % 0.41/1.07 0 (wt=-1) [] a2 = product(a1,a42). % 0.41/1.07 0 (wt=-1) [] a3 = product(a2,a41). % 0.41/1.07 0 (wt=-1) [] a4 = product(a3,a14). % 0.41/1.07 0 (wt=-1) [] a5 = product(a4,a39). % 0.41/1.07 0 (wt=-1) [] a6 = product(a5,a136). % 0.41/1.07 0 (wt=-1) [] a7 = product(a6,a52). % 0.41/1.07 0 (wt=-1) [] a8 = product(a7,a17). % 0.41/1.07 0 (wt=-1) [] a9 = product(a8,a56). % 0.41/1.07 0 (wt=-1) [] a10 = product(a9,a134). % 0.41/1.07 0 (wt=-1) [] a11 = product(a10,a37). % 0.41/1.07 0 (wt=-1) [] a12 = product(a11,a21). % 0.41/1.07 0 (wt=-1) [] a13 = product(a12,a23). % 0.41/1.07 0 (wt=-1) [] a14 = product(a13,a32). % 0.41/1.07 0 (wt=-1) [] a15 = product(a14,a53). % 0.41/1.07 0 (wt=-1) [] a16 = product(a15,a136). % 0.41/1.07 0 (wt=-1) [] a17 = product(a16,a29). % 0.41/1.07 0 (wt=-1) [] a18 = product(a17,a133). % 0.41/1.07 0 (wt=-1) [] a19 = product(a18,a58). % 0.41/1.07 0 (wt=-1) [] a20 = product(a19,a26). % 0.41/1.07 0 (wt=-1) [] a21 = product(a20,a35). % 0.41/1.07 0 (wt=-1) [] a22 = product(a21,a141). % 0.41/1.07 0 (wt=-1) [] a23 = product(a22,a45). % 0.41/1.07 0 (wt=-1) [] a24 = product(a23,a35). % 0.41/1.07 0 (wt=-1) [] a25 = product(a24,a49). % 0.41/1.07 0 (wt=-1) [] a26 = product(a25,a138). % 0.41/1.07 0 (wt=-1) [] a27 = product(a26,a8). % 0.41/1.07 0 (wt=-1) [] a28 = product(a27,a37). % 0.41/1.07 0 (wt=-1) [] a29 = product(a28,a17). % 0.41/1.07 0 (wt=-1) [] a30 = product(a29,a14). % 0.41/1.07 0 (wt=-1) [] a31 = product(a30,a5). % 0.41/1.07 0 (wt=-1) [] a32 = product(a31,a39). % 0.41/1.07 0 (wt=-1) [] a33 = product(a32,a13). % 0.41/1.07 0 (wt=-1) [] a34 = product(a33,a131). % 0.41/1.07 0 (wt=-1) [] a35 = product(a34,a60). % 0.41/1.07 0 (wt=-1) [] a36 = product(a35,a139). % 0.41/1.07 0 (wt=-1) [] a37 = product(a36,a47). % 0.41/1.07 0 (wt=-1) [] a38 = product(a37,a17). % 0.41/1.07 0 (wt=-1) [] a39 = product(a38,a7). % 0.41/1.07 0 (wt=-1) [] a40 = product(a39,a4). % 0.41/1.07 0 (wt=-1) [] a41 = product(a40,a14). % 0.41/1.07 0 (wt=-1) [] a42 = product(a41,a2). % 0.41/1.07 0 (wt=-1) [] a43 = product(a42,a62). % 0.41/1.07 0 (wt=-1) [] a44 = product(a43,a128). % 0.41/1.07 0 (wt=-1) [] a45 = product(a44,a23). % 0.41/1.07 0 (wt=-1) [] a46 = product(a45,a141). % 0.41/1.07 0 (wt=-1) [] a47 = product(a46,a11). % 0.41/1.07 0 (wt=-1) [] a48 = product(a47,a20). % 0.41/1.07 0 (wt=-1) [] a49 = product(a48,a138). % 0.41/1.07 0 (wt=-1) [] a50 = product(a49,a131). % 0.41/1.07 0 (wt=-1) [] a51 = product(a50,a59). % 0.41/1.07 0 (wt=-1) [] a52 = product(a51,a39). % 0.41/1.07 0 (wt=-1) [] a53 = product(a52,a136). % 0.41/1.07 0 (wt=-1) [] a54 = product(a53,a29). % 0.41/1.07 0 (wt=-1) [] a55 = product(a54,a135). % 0.41/1.07 0 (wt=-1) [] a56 = product(a55,a37). % 0.41/1.07 0 (wt=-1) [] a57 = product(a56,a134). % 0.41/1.07 0 (wt=-1) [] a58 = product(a57,a26). % 0.41/1.07 0 (wt=-1) [] a59 = product(a58,a138). % 0.41/1.07 0 (wt=-1) [] a60 = product(a59,a131). % 0.41/1.07 0 (wt=-1) [] a61 = product(a60,a13). % 0.41/1.07 0 (wt=-1) [] a62 = product(a61,a1). % 0.41/1.07 0 (wt=-1) [] a63 = product(a62,a96). % 0.41/1.07 0 (wt=-1) [] a64 = product(a63,a127). % 0.41/1.07 0 (wt=-1) [] a65 = product(a64,a41). % 0.41/1.07 0 (wt=-1) [] a66 = product(a65,a2). % 0.41/1.07 0 (wt=-1) [] a67 = product(a66,a92). % 0.41/1.07 0 (wt=-1) [] a68 = product(a67,a98). % 0.41/1.07 0 (wt=-1) [] a69 = product(a68,a32). % 0.41/1.07 0 (wt=-1) [] a70 = product(a69,a13). % 0.41/1.07 0 (wt=-1) [] a71 = product(a70,a118). % 0.41/1.07 0 (wt=-1) [] a72 = product(a71,a109). % 0.41/1.07 0 (wt=-1) [] a73 = product(a72,a82). % 0.41/1.07 0 (wt=-1) [] a74 = product(a73,a32). % 0.41/1.07 0 (wt=-1) [] a75 = product(a74,a14). % 0.41/1.07 0 (wt=-1) [] a76 = product(a75,a68). % 0.41/1.07 0 (wt=-1) [] a77 = product(a76,a114). % 0.41/1.07 0 (wt=-1) [] a78 = product(a77,a13). % 0.41/1.07 0 (wt=-1) [] a79 = product(a78,a33). % 0.41/1.07 0 (wt=-1) [] a80 = product(a79,a119). % 0.41/1.07 0 (wt=-1) [] a81 = product(a80,a70). % 0.41/1.07 0 (wt=-1) [] a82 = product(a81,a109). % 0.41/1.07 0 (wt=-1) [] a83 = product(a82,a118). % 0.41/1.07 0 (wt=-1) [] a84 = product(a83,a39). % 0.41/1.07 0 (wt=-1) [] a85 = product(a84,a5). % 0.41/1.07 0 (wt=-1) [] a86 = product(a85,a30). % 0.41/1.07 0 (wt=-1) [] a87 = product(a86,a104). % 0.41/1.07 0 (wt=-1) [] a88 = product(a87,a4). % 0.41/1.07 0 (wt=-1) [] a89 = product(a88,a14). % 0.41/1.07 0 (wt=-1) [] a90 = product(a89,a41). % 0.41/1.07 0 (wt=-1) [] a91 = product(a90,a100). % 0.41/1.07 0 (wt=-1) [] a92 = product(a91,a124). % 0.41/1.07 0 (wt=-1) [] a93 = product(a92,a2). % 0.41/1.07 0 (wt=-1) [] a94 = product(a93,a41). % 0.41/1.07 0 (wt=-1) [] a95 = product(a94,a127). % 0.41/1.07 0 (wt=-1) [] a96 = product(a95,a64). % 0.41/1.07 0 (wt=-1) [] a97 = product(a96,a42). % 0.41/1.07 0 (wt=-1) [] a98 = product(a97,a1). % 0.41/1.07 0 (wt=-1) [] a99 = product(a98,a92). % 0.41/1.07 0 (wt=-1) [] a100 = product(a99,a124). % 0.41/1.07 0 (wt=-1) [] a101 = product(a100,a14). % 0.41/1.07 0 (wt=-1) [] a102 = product(a101,a40). % 0.41/1.07 0 (wt=-1) [] a103 = product(a102,a4). % 0.41/1.07 0 (wt=-1) [] a104 = product(a103,a87). % 0.41/1.07 0 (wt=-1) [] a105 = product(a104,a30). % 0.41/1.07 0 (wt=-1) [] a106 = product(a105,a5). % 0.41/1.07 0 (wt=-1) [] a107 = product(a106,a84). % 0.41/1.07 0 (wt=-1) [] a108 = product(a107,a39). % 0.41/1.07 0 (wt=-1) [] a109 = product(a108,a118). % 0.41/1.07 0 (wt=-1) [] a110 = product(a109,a70). % 0.41/1.07 0 (wt=-1) [] a111 = product(a110,a119). % 0.41/1.07 0 (wt=-1) [] a112 = product(a111,a79). % 0.41/1.07 0 (wt=-1) [] a113 = product(a112,a33). % 0.41/1.07 0 (wt=-1) [] a114 = product(a113,a13). % 0.41/1.07 0 (wt=-1) [] a115 = product(a114,a68). % 0.41/1.07 0 (wt=-1) [] a116 = product(a115,a14). % 0.41/1.07 0 (wt=-1) [] a117 = product(a116,a74). % 0.41/1.07 0 (wt=-1) [] a118 = product(a117,a32). % 0.41/1.07 0 (wt=-1) [] a119 = product(a118,a70). % 0.41/1.07 0 (wt=-1) [] a120 = product(a119,a13). % 0.41/1.07 0 (wt=-1) [] a121 = product(a120,a32). % 0.41/1.07 0 (wt=-1) [] a122 = product(a121,a68). % 0.41/1.07 0 (wt=-1) [] a123 = product(a122,a115). % 0.41/1.07 0 (wt=-1) [] a124 = product(a123,a75). % 0.41/1.07 0 (wt=-1) [] a125 = product(a124,a2). % 0.41/1.07 0 (wt=-1) [] a126 = product(a125,a65). % 0.41/1.07 0 (wt=-1) [] a127 = product(a126,a41). % 0.41/1.07 0 (wt=-1) [] a128 = product(a127,a96). % 0.41/1.07 0 (wt=-1) [] a129 = product(a128,a62). % 0.41/1.07 0 (wt=-1) [] a130 = product(a129,a1). % 0.41/1.07 0 (wt=-1) [] a131 = product(a130,a13). % 0.41/1.07 0 (wt=-1) [] a132 = product(a131,a138). % 0.41/1.07 0 (wt=-1) [] a133 = product(a132,a58). % 0.41/1.07 0 (wt=-1) [] a134 = product(a133,a26). % 0.41/1.07 0 (wt=-1) [] a135 = product(a134,a37). % 0.41/1.07 0 (wt=-1) [] a136 = product(a135,a29). % 0.41/1.07 0 (wt=-1) [] a137 = product(a136,a39). % 0.41/1.07 0 (wt=-1) [] a138 = product(a137,a51). % 0.41/1.07 0 (wt=-1) [] a139 = product(a138,a20). % 0.41/1.07 0 (wt=-1) [] a140 = product(a139,a47). % 0.41/1.07 0 (wt=-1) [] a141 = product(a140,a11). % 0.41/1.07 0 (wt=-1) [] a1 = product(a141,a23). % 0.41/1.07 0 (wt=-1) [] -(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)). % 0.41/1.07 end_of_list. % 0.41/1.07 % 0.41/1.07 Demodulators: % 0.41/1.07 end_of_list. % 0.41/1.07 % 0.41/1.07 Passive: % 0.41/1.07 end_of_list. % 0.41/1.07 % 0.41/1.07 Starting to process input. % 0.41/1.07 % 0.41/1.07 ** KEPT: 1 (wt=5) [] product(A,A) = A. % 0.41/1.07 1 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 2 (wt=7) [] product(product(A,B),B) = A. % 0.41/1.07 2 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 3 (wt=13) [] product(product(A,B),C) = product(product(A,C),product(B,C)). % 0.41/1.07 % 0.41/1.07 ** KEPT: 4 (wt=13) [flip(3)] product(product(A,B),product(C,B)) = product(product(A,C),B). % 0.41/1.07 clause forward subsumed: 0 (wt=13) [flip(4)] product(product(A,C),B) = product(product(A,B),product(C,B)). % 0.41/1.07 % 0.41/1.07 ** KEPT: 5 (wt=5) [flip(1)] product(a1,a42) = a2. % 0.41/1.07 5 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 6 (wt=5) [flip(1)] product(a2,a41) = a3. % 0.41/1.07 6 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 7 (wt=5) [flip(1)] product(a3,a14) = a4. % 0.41/1.07 7 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 8 (wt=5) [flip(1)] product(a4,a39) = a5. % 0.41/1.07 8 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 9 (wt=5) [flip(1)] product(a5,a136) = a6. % 0.41/1.07 9 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 10 (wt=5) [flip(1)] product(a6,a52) = a7. % 0.41/1.07 10 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 11 (wt=5) [flip(1)] product(a7,a17) = a8. % 0.41/1.07 11 is a new demodulator. % 0.41/1.07 % 0.41/1.07 ** KEPT: 12 (wt=5) [flip(1)] product(a8,a56) = a9. % 0.41/1.08 12 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 13 (wt=5) [flip(1)] product(a9,a134) = a10. % 0.41/1.08 13 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 14 (wt=5) [flip(1)] product(a10,a37) = a11. % 0.41/1.08 14 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 15 (wt=5) [flip(1)] product(a11,a21) = a12. % 0.41/1.08 15 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 16 (wt=5) [flip(1)] product(a12,a23) = a13. % 0.41/1.08 16 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 17 (wt=5) [flip(1)] product(a13,a32) = a14. % 0.41/1.08 17 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 18 (wt=5) [flip(1)] product(a14,a53) = a15. % 0.41/1.08 18 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 19 (wt=5) [flip(1)] product(a15,a136) = a16. % 0.41/1.08 19 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 20 (wt=5) [flip(1)] product(a16,a29) = a17. % 0.41/1.08 20 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 21 (wt=5) [flip(1)] product(a17,a133) = a18. % 0.41/1.08 21 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 22 (wt=5) [flip(1)] product(a18,a58) = a19. % 0.41/1.08 22 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 23 (wt=5) [flip(1)] product(a19,a26) = a20. % 0.41/1.08 23 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 24 (wt=5) [flip(1)] product(a20,a35) = a21. % 0.41/1.08 24 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 25 (wt=5) [flip(1)] product(a21,a141) = a22. % 0.41/1.08 25 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 26 (wt=5) [flip(1)] product(a22,a45) = a23. % 0.41/1.08 26 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 27 (wt=5) [flip(1)] product(a23,a35) = a24. % 0.41/1.08 27 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 28 (wt=5) [flip(1)] product(a24,a49) = a25. % 0.41/1.08 28 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 29 (wt=5) [flip(1)] product(a25,a138) = a26. % 0.41/1.08 29 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 30 (wt=5) [flip(1)] product(a26,a8) = a27. % 0.41/1.08 30 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 31 (wt=5) [flip(1)] product(a27,a37) = a28. % 0.41/1.08 31 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 32 (wt=5) [flip(1)] product(a28,a17) = a29. % 0.41/1.08 32 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 33 (wt=5) [flip(1)] product(a29,a14) = a30. % 0.41/1.08 33 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 34 (wt=5) [flip(1)] product(a30,a5) = a31. % 0.41/1.08 34 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 35 (wt=5) [flip(1)] product(a31,a39) = a32. % 0.41/1.08 35 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 36 (wt=5) [flip(1)] product(a32,a13) = a33. % 0.41/1.08 36 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 37 (wt=5) [flip(1)] product(a33,a131) = a34. % 0.41/1.08 37 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 38 (wt=5) [flip(1)] product(a34,a60) = a35. % 0.41/1.08 38 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 39 (wt=5) [flip(1)] product(a35,a139) = a36. % 0.41/1.08 39 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 40 (wt=5) [flip(1)] product(a36,a47) = a37. % 0.41/1.08 40 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 41 (wt=5) [flip(1)] product(a37,a17) = a38. % 0.41/1.08 41 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 42 (wt=5) [flip(1)] product(a38,a7) = a39. % 0.41/1.08 42 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 43 (wt=5) [flip(1)] product(a39,a4) = a40. % 0.41/1.08 43 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 44 (wt=5) [flip(1)] product(a40,a14) = a41. % 0.41/1.08 44 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 45 (wt=5) [flip(1)] product(a41,a2) = a42. % 0.41/1.08 45 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 46 (wt=5) [flip(1)] product(a42,a62) = a43. % 0.41/1.08 46 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 47 (wt=5) [flip(1)] product(a43,a128) = a44. % 0.41/1.08 47 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 48 (wt=5) [flip(1)] product(a44,a23) = a45. % 0.41/1.08 48 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 49 (wt=5) [flip(1)] product(a45,a141) = a46. % 0.41/1.08 49 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 50 (wt=5) [flip(1)] product(a46,a11) = a47. % 0.41/1.08 50 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 51 (wt=5) [flip(1)] product(a47,a20) = a48. % 0.41/1.08 51 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 52 (wt=5) [flip(1)] product(a48,a138) = a49. % 0.41/1.08 52 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 53 (wt=5) [flip(1)] product(a49,a131) = a50. % 0.41/1.08 53 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 54 (wt=5) [flip(1)] product(a50,a59) = a51. % 0.41/1.08 54 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 55 (wt=5) [flip(1)] product(a51,a39) = a52. % 0.41/1.08 55 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 56 (wt=5) [flip(1)] product(a52,a136) = a53. % 0.41/1.08 56 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 57 (wt=5) [flip(1)] product(a53,a29) = a54. % 0.41/1.08 57 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 58 (wt=5) [flip(1)] product(a54,a135) = a55. % 0.41/1.08 58 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 59 (wt=5) [flip(1)] product(a55,a37) = a56. % 0.41/1.08 59 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 60 (wt=5) [flip(1)] product(a56,a134) = a57. % 0.41/1.08 60 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 61 (wt=5) [flip(1)] product(a57,a26) = a58. % 0.41/1.08 61 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 62 (wt=5) [flip(1)] product(a58,a138) = a59. % 0.41/1.08 62 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 63 (wt=5) [flip(1)] product(a59,a131) = a60. % 0.41/1.08 63 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 64 (wt=5) [flip(1)] product(a60,a13) = a61. % 0.41/1.08 64 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 65 (wt=5) [flip(1)] product(a61,a1) = a62. % 0.41/1.08 65 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 66 (wt=5) [flip(1)] product(a62,a96) = a63. % 0.41/1.08 66 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 67 (wt=5) [flip(1)] product(a63,a127) = a64. % 0.41/1.08 67 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 68 (wt=5) [flip(1)] product(a64,a41) = a65. % 0.41/1.08 68 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 69 (wt=5) [flip(1)] product(a65,a2) = a66. % 0.41/1.08 69 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 70 (wt=5) [flip(1)] product(a66,a92) = a67. % 0.41/1.08 70 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 71 (wt=5) [flip(1)] product(a67,a98) = a68. % 0.41/1.08 71 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 72 (wt=5) [flip(1)] product(a68,a32) = a69. % 0.41/1.08 72 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 73 (wt=5) [flip(1)] product(a69,a13) = a70. % 0.41/1.08 73 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 74 (wt=5) [flip(1)] product(a70,a118) = a71. % 0.41/1.08 74 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 75 (wt=5) [flip(1)] product(a71,a109) = a72. % 0.41/1.08 75 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 76 (wt=5) [flip(1)] product(a72,a82) = a73. % 0.41/1.08 76 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 77 (wt=5) [flip(1)] product(a73,a32) = a74. % 0.41/1.08 77 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 78 (wt=5) [flip(1)] product(a74,a14) = a75. % 0.41/1.08 78 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 79 (wt=5) [flip(1)] product(a75,a68) = a76. % 0.41/1.08 79 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 80 (wt=5) [flip(1)] product(a76,a114) = a77. % 0.41/1.08 80 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 81 (wt=5) [flip(1)] product(a77,a13) = a78. % 0.41/1.08 81 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 82 (wt=5) [flip(1)] product(a78,a33) = a79. % 0.41/1.08 82 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 83 (wt=5) [flip(1)] product(a79,a119) = a80. % 0.41/1.08 83 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 84 (wt=5) [flip(1)] product(a80,a70) = a81. % 0.41/1.08 84 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 85 (wt=5) [flip(1)] product(a81,a109) = a82. % 0.41/1.08 85 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 86 (wt=5) [flip(1)] product(a82,a118) = a83. % 0.41/1.08 86 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 87 (wt=5) [flip(1)] product(a83,a39) = a84. % 0.41/1.08 87 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 88 (wt=5) [flip(1)] product(a84,a5) = a85. % 0.41/1.08 88 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 89 (wt=5) [flip(1)] product(a85,a30) = a86. % 0.41/1.08 89 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 90 (wt=5) [flip(1)] product(a86,a104) = a87. % 0.41/1.08 90 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 91 (wt=5) [flip(1)] product(a87,a4) = a88. % 0.41/1.08 91 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 92 (wt=5) [flip(1)] product(a88,a14) = a89. % 0.41/1.08 92 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 93 (wt=5) [flip(1)] product(a89,a41) = a90. % 0.41/1.08 93 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 94 (wt=5) [flip(1)] product(a90,a100) = a91. % 0.41/1.08 94 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 95 (wt=5) [flip(1)] product(a91,a124) = a92. % 0.41/1.08 95 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 96 (wt=5) [flip(1)] product(a92,a2) = a93. % 0.41/1.08 96 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 97 (wt=5) [flip(1)] product(a93,a41) = a94. % 0.41/1.08 97 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 98 (wt=5) [flip(1)] product(a94,a127) = a95. % 0.41/1.08 98 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 99 (wt=5) [flip(1)] product(a95,a64) = a96. % 0.41/1.08 99 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 100 (wt=5) [flip(1)] product(a96,a42) = a97. % 0.41/1.08 100 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 101 (wt=5) [flip(1)] product(a97,a1) = a98. % 0.41/1.08 101 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 102 (wt=5) [flip(1)] product(a98,a92) = a99. % 0.41/1.08 102 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 103 (wt=5) [flip(1)] product(a99,a124) = a100. % 0.41/1.08 103 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 104 (wt=5) [flip(1)] product(a100,a14) = a101. % 0.41/1.08 104 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 105 (wt=5) [flip(1)] product(a101,a40) = a102. % 0.41/1.08 105 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 106 (wt=5) [flip(1)] product(a102,a4) = a103. % 0.41/1.08 106 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 107 (wt=5) [flip(1)] product(a103,a87) = a104. % 0.41/1.08 107 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 108 (wt=5) [flip(1)] product(a104,a30) = a105. % 0.41/1.08 108 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 109 (wt=5) [flip(1)] product(a105,a5) = a106. % 0.41/1.08 109 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 110 (wt=5) [flip(1)] product(a106,a84) = a107. % 0.41/1.08 110 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 111 (wt=5) [flip(1)] product(a107,a39) = a108. % 0.41/1.08 111 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 112 (wt=5) [flip(1)] product(a108,a118) = a109. % 0.41/1.08 112 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 113 (wt=5) [flip(1)] product(a109,a70) = a110. % 0.41/1.08 113 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 114 (wt=5) [flip(1)] product(a110,a119) = a111. % 0.41/1.08 114 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 115 (wt=5) [flip(1)] product(a111,a79) = a112. % 0.41/1.08 115 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 116 (wt=5) [flip(1)] product(a112,a33) = a113. % 0.41/1.08 116 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 117 (wt=5) [flip(1)] product(a113,a13) = a114. % 0.41/1.08 117 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 118 (wt=5) [flip(1)] product(a114,a68) = a115. % 0.41/1.08 118 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 119 (wt=5) [flip(1)] product(a115,a14) = a116. % 0.41/1.08 119 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 120 (wt=5) [flip(1)] product(a116,a74) = a117. % 0.41/1.08 120 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 121 (wt=5) [flip(1)] product(a117,a32) = a118. % 0.41/1.08 121 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 122 (wt=5) [flip(1)] product(a118,a70) = a119. % 0.41/1.08 122 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 123 (wt=5) [flip(1)] product(a119,a13) = a120. % 0.41/1.08 123 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 124 (wt=5) [flip(1)] product(a120,a32) = a121. % 0.41/1.08 124 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 125 (wt=5) [flip(1)] product(a121,a68) = a122. % 0.41/1.08 125 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 126 (wt=5) [flip(1)] product(a122,a115) = a123. % 0.41/1.08 126 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 127 (wt=5) [flip(1)] product(a123,a75) = a124. % 0.41/1.08 127 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 128 (wt=5) [flip(1)] product(a124,a2) = a125. % 0.41/1.08 128 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 129 (wt=5) [flip(1)] product(a125,a65) = a126. % 0.41/1.08 129 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 130 (wt=5) [flip(1)] product(a126,a41) = a127. % 0.41/1.08 130 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 131 (wt=5) [flip(1)] product(a127,a96) = a128. % 0.41/1.08 131 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 132 (wt=5) [flip(1)] product(a128,a62) = a129. % 0.41/1.08 132 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 133 (wt=5) [flip(1)] product(a129,a1) = a130. % 0.41/1.08 133 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 134 (wt=5) [flip(1)] product(a130,a13) = a131. % 0.41/1.08 134 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 135 (wt=5) [flip(1)] product(a131,a138) = a132. % 0.41/1.08 135 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 136 (wt=5) [flip(1)] product(a132,a58) = a133. % 0.41/1.08 136 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 137 (wt=5) [flip(1)] product(a133,a26) = a134. % 0.41/1.08 137 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 138 (wt=5) [flip(1)] product(a134,a37) = a135. % 0.41/1.08 138 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 139 (wt=5) [flip(1)] product(a135,a29) = a136. % 0.41/1.08 139 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 140 (wt=5) [flip(1)] product(a136,a39) = a137. % 0.41/1.08 140 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 141 (wt=5) [flip(1)] product(a137,a51) = a138. % 0.41/1.08 141 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 142 (wt=5) [flip(1)] product(a138,a20) = a139. % 0.41/1.08 142 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 143 (wt=5) [flip(1)] product(a139,a47) = a140. % 0.41/1.08 143 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 144 (wt=5) [flip(1)] product(a140,a11) = a141. % 0.41/1.08 144 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 145 (wt=5) [flip(1)] product(a141,a23) = a1. % 0.41/1.08 145 is a new demodulator. % 0.41/1.08 % 0.41/1.08 ** KEPT: 146 (wt=283) [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)). % 0.41/1.08 % 0.41/1.08 After processing input: % 0.41/1.08 % 0.41/1.08 Usable: % 0.41/1.08 end_of_list. % 0.41/1.08 % 0.41/1.08 Sos: % 0.41/1.08 1 (wt=5) [] product(A,A) = A. % 0.41/1.08 5 (wt=5) [flip(1)] product(a1,a42) = a2. % 0.41/1.08 6 (wt=5) [flip(1)] product(a2,a41) = a3. % 0.41/1.08 7 (wt=5) [flip(1)] product(a3,a14) = a4. % 0.41/1.08 8 (wt=5) [flip(1)] product(a4,a39) = a5. % 0.41/1.08 9 (wt=5) [flip(1)] product(a5,a136) = a6. % 0.41/1.08 10 (wt=5) [flip(1)] product(a6,a52) = a7. % 0.41/1.08 11 (wt=5) [flip(1)] product(a7,a17) = a8. % 0.41/1.08 12 (wt=5) [flip(1)] product(a8,a56) = a9. % 0.41/1.08 13 (wt=5) [flip(1)] product(a9,a134) = a10. % 0.41/1.08 14 (wt=5) [flip(1)] product(a10,a37) = a11. % 0.41/1.08 15 (wt=5) [flip(1)] product(a11,a21) = a12. % 0.41/1.08 16 (wt=5) [flip(1)] product(a12,a23) = a13. % 0.41/1.08 17 (wt=5) [flip(1)] product(a13,a32) = a14. % 0.41/1.08 18 (wt=5) [flip(1)] product(a14,a53) = a15. % 0.41/1.08 19 (wt=5) [flip(1)] product(a15,a136) = a16. % 0.41/1.08 20 (wt=5) [flip(1)] product(a16,a29) = a17. % 0.41/1.08 21 (wt=5) [flip(1)] product(a17,a133) = a18. % 0.41/1.08 22 (wt=5) [flip(1)] product(a18,a58) = a19. % 0.41/1.08 23 (wt=5) [flip(1)] product(a19,a26) = a20. % 0.41/1.08 24 (wt=5) [flip(1)] product(a20,a35) = a21. % 0.41/1.08 25 (wt=5) [flip(1)] product(a21,a141) = a22. % 0.41/1.08 26 (wt=5) [flip(1)] product(a22,a45) = a23. % 0.41/1.08 27 (wt=5) [flip(1)] product(a23,a35) = a24. % 0.41/1.08 28 (wt=5) [flip(1)] product(a24,a49) = a25. % 0.41/1.08 29 (wt=5) [flip(1)] product(a25,a138) = a26. % 0.41/1.08 30 (wt=5) [flip(1)] product(a26,a8) = a27. % 0.41/1.08 31 (wt=5) [flip(1)] product(a27,a37) = a28. % 0.41/1.08 32 (wt=5) [flip(1)] product(a28,a17) = a29. % 0.41/1.08 33 (wt=5) [flip(1)] product(a29,a14) = a30. % 0.71/1.08 34 (wt=5) [flip(1)] product(a30,a5) = a31. % 0.71/1.08 35 (wt=5) [flip(1)] product(a31,a39) = a32. % 0.71/1.08 36 (wt=5) [flip(1)] product(a32,a13) = a33. % 0.71/1.08 37 (wt=5) [flip(1)] product(a33,a131) = a34. % 0.71/1.08 38 (wt=5) [flip(1)] product(a34,a60) = a35. % 0.71/1.08 39 (wt=5) [flip(1)] product(a35,a139) = a36. % 0.71/1.08 40 (wt=5) [flip(1)] product(a36,a47) = a37. % 0.71/1.08 41 (wt=5) [flip(1)] product(a37,a17) = a38. % 0.71/1.08 42 (wt=5) [flip(1)] product(a38,a7) = a39. % 0.71/1.08 43 (wt=5) [flip(1)] product(a39,a4) = a40. % 0.71/1.08 44 (wt=5) [flip(1)] product(a40,a14) = a41. % 0.71/1.08 45 (wt=5) [flip(1)] product(a41,a2) = a42. % 0.71/1.08 46 (wt=5) [flip(1)] product(a42,a62) = a43. % 0.71/1.08 47 (wt=5) [flip(1)] product(a43,a128) = a44. % 0.71/1.08 48 (wt=5) [flip(1)] product(a44,a23) = a45. % 0.71/1.08 49 (wt=5) [flip(1)] product(a45,a141) = a46. % 0.71/1.08 50 (wt=5) [flip(1)] product(a46,a11) = a47. % 0.71/1.08 51 (wt=5) [flip(1)] product(a47,a20) = a48. % 0.71/1.08 52 (wt=5) [flip(1)] product(a48,a138) = a49. % 0.71/1.08 53 (wt=5) [flip(1)] product(a49,a131) = a50. % 0.71/1.08 54 (wt=5) [flip(1)] product(a50,a59) = a51. % 0.71/1.08 55 (wt=5) [flip(1)] product(a51,a39) = a52. % 0.71/1.08 56 (wt=5) [flip(1)] product(a52,a136) = a53. % 0.71/1.08 57 (wt=5) [flip(1)] product(a53,a29) = a54. % 0.71/1.08 58 (wt=5) [flip(1)] product(a54,a135) = a55. % 0.71/1.08 59 (wt=5) [flip(1)] product(a55,a37) = a56. % 0.71/1.08 60 (wt=5) [flip(1)] product(a56,a134) = a57. % 0.71/1.08 61 (wt=5) [flip(1)] product(a57,a26) = a58. % 0.71/1.08 62 (wt=5) [flip(1)] product(a58,a138) = a59. % 0.71/1.08 63 (wt=5) [flip(1)] product(a59,a131) = a60. % 0.71/1.08 64 (wt=5) [flip(1)] product(a60,a13) = a61. % 0.71/1.08 65 (wt=5) [flip(1)] product(a61,a1) = a62. % 0.71/1.08 66 (wt=5) [flip(1)] product(a62,a96) = a63. % 0.71/1.08 67 (wt=5) [flip(1)] product(a63,a127) = a64. % 0.71/1.08 68 (wt=5) [flip(1)] product(a64,a41) = a65. % 0.71/1.08 69 (wt=5) [flip(1)] product(a65,a2) = a66. % 0.71/1.08 70 (wt=5) [flip(1)] product(a66,a92) = a67. % 0.71/1.08 71 (wt=5) [flip(1)] product(a67,a98) = a68. % 0.71/1.08 72 (wt=5) [flip(1)] product(a68,a32) = a69. % 0.71/1.08 73 (wt=5) [flip(1)] product(a69,a13) = a70. % 0.71/1.08 74 (wt=5) [flip(1)] product(a70,a118) = a71. % 0.71/1.08 75 (wt=5) [flip(1)] product(a71,a109) = a72. % 0.71/1.08 76 (wt=5) [flip(1)] product(a72,a82) = a73. % 0.71/1.08 77 (wt=5) [flip(1)] product(a73,a32) = a74. % 0.71/1.08 78 (wt=5) [flip(1)] product(a74,a14) = a75. % 0.71/1.08 79 (wt=5) [flip(1)] product(a75,a68) = a76. % 0.71/1.08 80 (wt=5) [flip(1)] product(a76,a114) = a77. % 0.71/1.08 81 (wt=5) [flip(1)] product(a77,a13) = a78. % 0.71/1.08 82 (wt=5) [flip(1)] product(a78,a33) = a79. % 0.71/1.08 83 (wt=5) [flip(1)] product(a79,a119) = a80. % 0.71/1.08 84 (wt=5) [flip(1)] product(a80,a70) = a81. % 0.71/1.08 85 (wt=5) [flip(1)] product(a81,a109) = a82. % 0.71/1.08 86 (wt=5) [flip(1)] product(a82,a118) = a83. % 0.71/1.08 87 (wt=5) [flip(1)] product(a83,a39) = a84. % 0.71/1.08 88 (wt=5) [flip(1)] product(a84,a5) = a85. % 0.71/1.08 89 (wt=5) [flip(1)] product(a85,a30) = a86. % 0.71/1.08 90 (wt=5) [flip(1)] product(a86,a104) = a87. % 0.71/1.08 91 (wt=5) [flip(1)] product(a87,a4) = a88. % 0.71/1.08 92 (wt=5) [flip(1)] product(a88,a14) = a89. % 0.71/1.08 93 (wt=5) [flip(1)] product(a89,a41) = a90. % 0.71/1.08 94 (wt=5) [flip(1)] product(a90,a100) = a91. % 0.71/1.08 95 (wt=5) [flip(1)] product(a91,a124) = a92. % 0.71/1.08 96 (wt=5) [flip(1)] product(a92,a2) = a93. % 0.71/1.08 97 (wt=5) [flip(1)] product(a93,a41) = a94. % 0.71/1.08 98 (wt=5) [flip(1)] product(a94,a127) = a95. % 0.71/1.08 99 (wt=5) [flip(1)] product(a95,a64) = a96. % 0.71/1.08 100 (wt=5) [flip(1)] product(a96,a42) = a97. % 0.71/1.08 101 (wt=5) [flip(1)] product(a97,a1) = a98. % 0.71/1.08 102 (wt=5) [flip(1)] product(a98,a92) = a99. % 0.71/1.08 103 (wt=5) [flip(1)] product(a99,a124) = a100. % 0.71/1.08 104 (wt=5) [flip(1)] product(a100,a14) = a101. % 0.71/1.08 105 (wt=5) [flip(1)] product(a101,a40) = a102. % 0.71/1.08 106 (wt=5) [flip(1)] product(a102,a4) = a103. % 0.71/1.08 107 (wt=5) [flip(1)] product(a103,a87) = a104. % 0.71/1.08 108 (wt=5) [flip(1)] product(a104,a30) = a105. % 0.71/1.08 109 (wt=5) [flip(1)] product(a105,a5) = a106. % 0.71/1.08 110 (wt=5) [flip(1)] product(a106,a84) = a107. % 0.71/1.08 111 (wt=5) [flip(1)] product(a107,a39) = a108. % 0.71/1.08 112 (wt=5) [flip(1)] product(a108,a118) = a109. % 0.71/1.08 113 (wt=5) [flip(1)] product(a109,a70) = a110. % 0.71/1.08 114 (wt=5) [flip(1)] product(a110,a119) = a111. % 0.71/1.08 115 (wt=5) [flip(1)] product(a111,a79) = a112. % 0.71/1.08 116 (wt=5) [flip(1)] product(a112,a33) = a113. % 0.71/1.08 117 (wt=5) [flip(1)] product(a113,a13) = a114. % 0.71/1.08 118 (wt=5) [flip(1)] product(a114,a68) = a115. % 0.71/1.08 119 (wt=5) [flip(1)] product(a115,a14) = a116. % 0.71/1.08 120 (wt=5) [flip(1)] product(a116,a74) = a117. % 0.71/1.08 121 (wt=5) [flip(1)] product(a117,a32) = a118. % 0.71/1.08 122 (wt=5) [flip(1)] product(a118,a70) = a119. % 0.71/1.08 123 (wt=5) [flip(1)] product(a119,a13) = a120. % 0.71/1.08 124 (wt=5) [flip(1)] product(a120,a32) = a121. % 0.71/1.08 125 (wt=5) [flip(1)] product(a121,a68) = a122. % 0.71/1.08 126 (wt=5) [flip(1)] product(a122,a115) = a123. % 0.71/1.08 127 (wt=5) [flip(1)] product(a123,a75) = a124. % 0.71/1.08 128 (wt=5) [flip(1)] product(a124,a2) = a125. % 0.71/1.08 129 (wt=5) [flip(1)] product(a125,a65) = a126. % 0.71/1.08 130 (wt=5) [flip(1)] product(a126,a41) = a127. % 0.71/1.08 131 (wt=5) [flip(1)] product(a127,a96) = a128. % 0.71/1.08 132 (wt=5) [flip(1)] product(a128,a62) = a129. % 0.71/1.08 133 (wt=5) [flip(1)] product(a129,a1) = a130. % 0.71/1.08 134 (wt=5) [flip(1)] product(a130,a13) = a131. % 0.71/1.08 135 (wt=5) [flip(1)] product(a131,a138) = a132. % 0.71/1.08 136 (wt=5) [flip(1)] product(a132,a58) = a133. % 0.71/1.08 137 (wt=5) [flip(1)] product(a133,a26) = a134. % 0.71/1.08 138 (wt=5) [flip(1)] product(a134,a37) = a135. % 0.71/1.08 139 (wt=5) [flip(1)] product(a135,a29) = a136. % 0.71/1.08 140 (wt=5) [flip(1)] product(a136,a39) = a137. % 0.71/1.08 141 (wt=5) [flip(1)] product(a137,a51) = a138. % 0.71/1.08 142 (wt=5) [flip(1)] product(a138,a20) = a139. % 0.71/1.08 143 (wt=5) [flip(1)] product(a139,a47) = a140. % 0.71/1.08 144 (wt=5) [flip(1)] product(a140,a11) = a141. % 0.71/1.08 145 (wt=5) [flip(1)] product(a141,a23) = a1. % 0.71/1.08 2 (wt=7) [] product(product(A,B),B) = A. % 0.71/1.08 3 (wt=13) [] product(product(A,B),C) = product(product(A,C),product(B,C)). % 0.71/1.08 4 (wt=13) [flip(3)] product(product(A,B),product(C,B)) = product(product(A,C),B). % 0.71/1.08 146 (wt=283) [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)). % 0.71/1.08 end_of_list. % 0.71/1.08 % 0.71/1.08 Demodulators: % 0.71/1.08 1 (wt=5) [] product(A,A) = A. % 0.71/1.08 2 (wt=7) [] product(product(A,B),B) = A. % 0.71/1.08 5 (wt=5) [flip(1)] product(a1,a42) = a2. % 0.71/1.08 6 (wt=5) [flip(1)] product(a2,a41) = a3. % 0.71/1.08 7 (wt=5) [flip(1)] product(a3,a14) = a4. % 0.71/1.08 8 (wt=5) [flip(1)] product(a4,a39) = a5. % 0.71/1.08 9 (wt=5) [flip(1)] product(a5,a136) = a6. % 0.71/1.08 10 (wt=5) [flip(1)] product(a6,a52) = a7. % 0.71/1.08 11 (wt=5) [flip(1)] product(a7,a17) = a8. % 0.71/1.08 12 (wt=5) [flip(1)] product(a8,a56) = a9. % 0.71/1.08 13 (wt=5) [flip(1)] product(a9,a134) = a10. % 0.71/1.08 14 (wt=5) [flip(1)] product(a10,a37) = a11. % 0.71/1.08 15 (wt=5) [flip(1)] product(a11,a21) = a12. % 0.71/1.08 16 (wt=5) [flip(1)] product(a12,a23) = a13. % 0.71/1.08 17 (wt=5) [flip(1)] product(a13,a32) = a14. % 0.71/1.08 18 (wt=5) [flip(1)] product(a14,a53) = a15. % 20.41/20.80 19 (wt=5) [flip(1)] product(a15,a136) = a16. % 20.41/20.80 20 (wt=5) [flip(1)] product(a16,a29) = a17. % 20.41/20.80 21 (wt=5) [flip(1)] product(a17,a133) = a18. % 20.41/20.80 22 (wt=5) [flip(1)] product(a18,a58) = a19. % 20.41/20.80 23 (wt=5) [flip(1)] product(a19,a26) = a20. % 20.41/20.80 24 (wt=5) [flip(1)] product(a20,a35) = a21. % 20.41/20.80 25 (wt=5) [flip(1)] product(a21,a141) = a22. % 20.41/20.80 26 (wt=5) [flip(1)] product(a22,a45) = a23. % 20.41/20.80 27 (wt=5) [flip(1)] product(a23,a35) = a24. % 20.41/20.80 28 (wt=5) [flip(1)] product(a24,a49) = a25. % 20.41/20.80 29 (wt=5) [flip(1)] product(a25,a138) = a26. % 20.41/20.80 30 (wt=5) [flip(1)] product(a26,a8) = a27. % 20.41/20.80 31 (wt=5) [flip(1)] product(a27,a37) = a28. % 20.41/20.80 32 (wt=5) [flip(1)] product(a28,a17) = a29. % 20.41/20.80 33 (wt=5) [flip(1)] product(a29,a14) = a30. % 20.41/20.80 34 (wt=5) [flip(1)] product(a30,a5) = a31. % 20.41/20.80 35 (wt=5) [flip(1)] product(a31,a39) = a32. % 20.41/20.80 36 (wt=5) [flip(1)] product(a32,a13) = a33. % 20.41/20.80 37 (wt=5) [flip(1)] product(a33,a131) = a34. % 20.41/20.80 38 (wt=5) [flip(1)] product(a34,a60) = a35. % 20.41/20.80 39 (wt=5) [flip(1)] product(a35,a139) = a36. % 20.41/20.80 40 (wt=5) [flip(1)] product(a36,a47) = a37. % 20.41/20.80 41 (wt=5) [flip(1)] product(a37,a17) = a38. % 20.41/20.80 42 (wt=5) [flip(1)] product(a38,a7) = a39. % 20.41/20.80 43 (wt=5) [flip(1)] product(a39,a4) = a40. % 20.41/20.80 44 (wt=5) [flip(1)] product(a40,a14) = a41. % 20.41/20.80 45 (wt=5) [flip(1)] product(a41,a2) = a42. % 20.41/20.80 46 (wt=5) [flip(1)] product(a42,a62) = a43. % 20.41/20.80 47 (wt=5) [flip(1)] product(a43,a128) = a44. % 20.41/20.80 48 (wt=5) [flip(1)] product(a44,a23) = a45. % 20.41/20.80 49 (wt=5) [flip(1)] product(a45,a141) = a46. % 20.41/20.80 50 (wt=5) [flip(1)] product(a46,a11) = a47. % 20.41/20.80 51 (wt=5) [flip(1)] product(a47,a20) = a48. % 20.41/20.80 52 (wt=5) [flip(1)] product(a48,a138) = a49. % 20.41/20.80 53 (wt=5) [flip(1)] product(a49,a131) = a50. % 20.41/20.80 54 (wt=5) [flip(1)] product(a50,a59) = a51. % 20.41/20.80 55 (wt=5) [flip(1)] product(a51,a39) = a52. % 20.41/20.80 56 (wt=5) [flip(1)] product(a52,a136) = a53. % 20.41/20.80 57 (wt=5) [flip(1)] product(a53,a29) = a54. % 20.41/20.80 58 (wt=5) [flip(1)] product(a54,a135) = a55. % 20.41/20.80 59 (wt=5) [flip(1)] product(a55,a37) = a56. % 20.41/20.80 60 (wt=5) [flip(1)] product(a56,a134) = a57. % 20.41/20.80 61 (wt=5) [flip(1)] product(a57,a26) = a58. % 20.41/20.80 62 (wt=5) [flip(1)] product(a58,a138) = a59. % 20.41/20.80 63 (wt=5) [flip(1)] product(a59,a131) = a60. % 20.41/20.80 64 (wt=5) [flip(1)] product(a60,a13) = a61. % 20.41/20.80 65 (wt=5) [flip(1)] product(a61,a1) = a62. % 20.41/20.80 66 (wt=5) [flip(1)] product(a62,a96) = a63. % 20.41/20.80 67 (wt=5) [flip(1)] product(a63,a127) = a64. % 20.41/20.80 68 (wt=5) [flip(1)] product(a64,a41) = a65. % 20.41/20.80 69 (wt=5) [flip(1)] product(a65,a2) = a66. % 20.41/20.80 70 (wt=5) [flip(1)] product(a66,a92) = a67. % 20.41/20.80 71 (wt=5) [flip(1)] product(a67,a98) = a68. % 20.41/20.80 72 (wt=5) [flip(1)] product(a68,a32) = a69. % 20.41/20.80 73 (wt=5) [flip(1)] product(a69,a13) = a70. % 20.41/20.80 74 (wt=5) [flip(1)] product(a70,a118) = a71. % 20.41/20.80 75 (wt=5) [flip(1)] product(a71,a109) = a72. % 20.41/20.80 76 (wt=5) [flip(1)] product(a72,a82) = a73. % 20.41/20.80 77 (wt=5) [flip(1)] product(a73,a32) = a74. % 20.41/20.80 78 (wt=5) [flip(1)] product(a74,a14) = a75. % 20.41/20.80 79 (wt=5) [flip(1)] product(a75,a68) = a76. % 20.41/20.80 80 (wt=5) [flip(1)] product(a76,a114) = a77. % 20.41/20.80 81 (wt=5) [flip(1)] product(a77,a13) = a78. % 20.41/20.80 82 (wt=5) [flip(1)] product(a78,a33) = a79. % 20.41/20.80 83 (wt=5) [flip(1)] product(a79,a119) = a80. % 20.41/20.80 84 (wt=5) [flip(1)] product(a80,a70) = a81. % 20.41/20.80 85 (wt=5) [flip(1)] product(a81,a109) = a82. % 20.41/20.80 86 (wt=5) [flip(1)] product(a82,a118) = a83. % 20.41/20.80 87 (wt=5) [flip(1)] product(a83,a39) = a84. % 20.41/20.80 88 (wt=5) [flip(1)] product(a84,a5) = a85. % 20.41/20.80 89 (wt=5) [flip(1)] product(a85,a30) = a86. % 20.41/20.80 90 (wt=5) [flip(1)] product(a86,a104) = a87. % 20.41/20.80 91 (wt=5) [flip(1)] product(a87,a4) = a88. % 20.41/20.80 92 (wt=5) [flip(1)] product(a88,a14) = a89. % 20.41/20.80 93 (wt=5) [flip(1)] product(a89,a41) = a90. % 20.41/20.80 94 (wt=5) [flip(1)] product(a90,a100) = a91. % 20.41/20.80 95 (wt=5) [flip(1)] product(a91,a124) = a92. % 20.41/20.80 96 (wt=5) [flip(1)] product(a92,a2) = a93. % 20.41/20.80 97 (wt=5) [flip(1)] product(a93,a41) = a94. % 20.41/20.80 98 (wt=5) [flip(1)] product(a94,a127) = a95. % 20.41/20.80 99 (wt=5) [flip(1)] product(a95,a64) = a96. % 20.41/20.80 100 (wt=5) [flip(1)] product(a96,a42) = a97. % 20.41/20.80 101 (wt=5) [flip(1)] product(a97,a1) = a98. % 20.41/20.80 102 (wt=5) [flip(1)] product(a98,a92) = a99. % 20.41/20.80 103 (wt=5) [flip(1)] product(a99,a124) = a100. % 20.41/20.80 104 (wt=5) [flip(1)] product(a100,a14) = a101. % 20.41/20.80 105 (wt=5) [flip(1)] product(a101,a40) = a102. % 20.41/20.80 106 (wt=5) [flip(1)] product(a102,a4) = a103. % 20.41/20.80 107 (wt=5) [flip(1)] product(a103,a87) = a104. % 20.41/20.80 108 (wt=5) [flip(1)] product(a104,a30) = a105. % 20.41/20.80 109 (wt=5) [flip(1)] product(a105,a5) = a106. % 20.41/20.80 110 (wt=5) [flip(1)] product(a106,a84) = a107. % 20.41/20.80 111 (wt=5) [flip(1)] product(a107,a39) = a108. % 20.41/20.80 112 (wt=5) [flip(1)] product(a108,a118) = a109. % 20.41/20.80 113 (wt=5) [flip(1)] product(a109,a70) = a110. % 20.41/20.80 114 (wt=5) [flip(1)] product(a110,a119) = a111. % 20.41/20.80 115 (wt=5) [flip(1)] product(a111,a79) = a112. % 20.41/20.80 116 (wt=5) [flip(1)] product(a112,a33) = a113. % 20.41/20.80 117 (wt=5) [flip(1)] product(a113,a13) = a114. % 20.41/20.80 118 (wt=5) [flip(1)] product(a114,a68) = a115. % 20.41/20.80 119 (wt=5) [flip(1)] product(a115,a14) = a116. % 20.41/20.80 120 (wt=5) [flip(1)] product(a116,a74) = a117. % 20.41/20.80 121 (wt=5) [flip(1)] product(a117,a32) = a118. % 20.41/20.80 122 (wt=5) [flip(1)] product(a118,a70) = a119. % 20.41/20.80 123 (wt=5) [flip(1)] product(a119,a13) = a120. % 20.41/20.80 124 (wt=5) [flip(1)] product(a120,a32) = a121. % 20.41/20.80 125 (wt=5) [flip(1)] product(a121,a68) = a122. % 20.41/20.80 126 (wt=5) [flip(1)] product(a122,a115) = a123. % 20.41/20.80 127 (wt=5) [flip(1)] product(a123,a75) = a124. % 20.41/20.80 128 (wt=5) [flip(1)] product(a124,a2) = a125. % 20.41/20.80 129 (wt=5) [flip(1)] product(a125,a65) = a126. % 20.41/20.80 130 (wt=5) [flip(1)] product(a126,a41) = a127. % 20.41/20.80 131 (wt=5) [flip(1)] product(a127,a96) = a128. % 20.41/20.80 132 (wt=5) [flip(1)] product(a128,a62) = a129. % 20.41/20.80 133 (wt=5) [flip(1)] product(a129,a1) = a130. % 20.41/20.80 134 (wt=5) [flip(1)] product(a130,a13) = a131. % 20.41/20.80 135 (wt=5) [flip(1)] product(a131,a138) = a132. % 20.41/20.80 136 (wt=5) [flip(1)] product(a132,a58) = a133. % 20.41/20.80 137 (wt=5) [flip(1)] product(a133,a26) = a134. % 20.41/20.80 138 (wt=5) [flip(1)] product(a134,a37) = a135. % 20.41/20.80 139 (wt=5) [flip(1)] product(a135,a29) = a136. % 20.41/20.80 140 (wt=5) [flip(1)] product(a136,a39) = a137. % 20.41/20.80 141 (wt=5) [flip(1)] product(a137,a51) = a138. % 20.41/20.80 142 (wt=5) [flip(1)] product(a138,a20) = a139. % 20.41/20.80 143 (wt=5) [flip(1)] product(a139,a47) = a140. % 20.41/20.80 144 (wt=5) [flip(1)] product(a140,a11) = a141. % 20.41/20.80 145 (wt=5) [flip(1)] product(a141,a23) = a1. % 20.41/20.80 end_of_list. % 20.41/20.80 % 20.41/20.80 Passive: % 20.41/20.80 end_of_list. % 20.41/20.80 % 20.41/20.80 ------------- memory usage ------------ % 20.41/20.80 Memory dynamically allocated (tp_alloc): 63964. % 20.41/20.80 type (bytes each) gets frees in use avail bytes % 20.41/20.80 sym_ent ( 96) 194 0 194 0 18.2 K % 20.41/20.80 term ( 16) 3507612 2542427 965185 4 18706.5 K % 20.41/20.80 gen_ptr ( 8) 4573231 417389 4155842 0 32467.5 K % 20.41/20.80 context ( 808) 10197890 10197888 2 5 5.5 K % 20.41/20.80 trail ( 12) 350752 350752 0 7 0.1 K % 20.41/20.80 bt_node ( 68) 8673029 8673024 5 136 9.4 K % 20.41/20.80 ac_position (285432) 0 0 0 0 0.0 K % 20.41/20.80 ac_match_pos (14044) 0 0 0 0 0.0 K % 20.41/20.80 ac_match_free_vars_pos (4020) % 20.41/20.80 0 0 0 0 0.0 K % 20.41/20.80 discrim ( 12) 694550 46356 648194 0 7596.0 K % 20.41/20.80 flat ( 40) 9770737 9770737 0 93 3.6 K % 20.41/20.80 discrim_pos ( 12) 124087 124087 0 1 0.0 K % 20.41/20.80 fpa_head ( 12) 19212 0 19212 0 225.1 K % 20.41/20.80 fpa_tree ( 28) 107663 107663 0 27 0.7 K % 20.41/20.80 fpa_pos ( 36) 59176 59176 0 1 0.0 K % 20.41/20.80 literal ( 12) 172549 135200 37349 1 437.7 K % 20.41/20.80 clause ( 24) 172549 135200 37349 1 875.4 K % 20.41/20.80 list ( 12) 21886 21830 56 3 0.7 K % 20.41/20.80 list_pos ( 20) 139723 11880 127843 0 2496.9 K % 20.41/20.80 pair_index ( 40) 2 0 2 0 0.1 K % 20.41/20.80 % 20.41/20.80 -------------- statistics ------------- % 20.41/20.80 Clauses input 145 % 20.41/20.80 Usable input 0 % 20.41/20.80 Sos input 145 % 20.41/20.80 Demodulators input 0 % 20.41/20.80 Passive input 0 % 20.41/20.80 % 20.41/20.80 Processed BS (before search) 147 % 20.41/20.80 Forward subsumed BS 1 % 20.41/20.80 Kept BS 146 % 20.41/20.80 New demodulators BS 143 % 20.41/20.80 Back demodulated % 20.41/20.80 % 20.41/20.80 ********** ABNORMAL END ********** % 20.41/20.80 ********** in tp_alloc, max_mem parameter exceeded. % 20.41/20.80 BS 0 % 20.41/20.80 % 20.41/20.80 Clauses or pairs given 959945 % 20.41/20.80 Clauses generated 93294 % 20.41/20.80 Forward subsumed 56091 % 20.41/20.80 Deleted by weight 0 % 20.41/20.80 Deleted by variable count 0 % 20.41/20.80 Kept 37203 % 20.41/20.80 New demodulators 21684 % 20.41/20.80 Back demodulated 2851 % 20.41/20.80 Ordered paramod prunes 0 % 20.41/20.80 Basic paramod prunes 2745927 % 20.41/20.80 Prime paramod prunes 156 % 20.41/20.80 Semantic prunes 0 % 20.41/20.80 % 20.41/20.80 Rewrite attmepts 1938928 % 20.41/20.80 Rewrites 92049 % 20.41/20.80 % 20.41/20.80 FPA overloads 0 % 20.41/20.80 FPA underloads 0 % 20.41/20.80 % 20.41/20.80 Usable size 0 % 20.41/20.80 Sos size 34498 % 20.41/20.80 Demodulators size 21498 % 20.41/20.80 Passive size 0 % 20.41/20.80 Disabled size 2851 % 20.41/20.80 % 20.41/20.80 Proofs found 0 % 20.41/20.80 % 20.41/20.80 ----------- times (seconds) ----------- Sun May 29 09:08:44 2022 % 20.41/20.80 % 20.41/20.80 user CPU time 16.41 (0 hr, 0 min, 16 sec) % 20.41/20.80 system CPU time 3.29 (0 hr, 0 min, 3 sec) % 20.41/20.80 wall-clock time 20 (0 hr, 0 min, 20 sec) % 20.41/20.80 input time 0.01 % 20.41/20.80 paramodulation time 0.92 % 20.41/20.80 demodulation time 1.97 % 20.41/20.80 orient time 0.23 % 20.41/20.80 weigh time 0.06 % 20.41/20.80 forward subsume time 0.79 % 20.41/20.80 back demod find time 1.60 % 20.41/20.80 conflict time 0.02 % 20.41/20.80 LRPO time 0.10 % 20.41/20.80 store clause time 8.94 % 20.41/20.80 disable clause time 0.66 % 20.41/20.80 prime paramod time 0.12 % 20.41/20.80 semantics time 0.00 % 20.41/20.80 % 20.41/20.80 EQP interrupted %------------------------------------------------------------------------------