%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV514-1.050 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n020.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:21:00 EDT 2022 % Result : Unknown 3.55s 3.70s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV514-1.050 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : otter-tptp-script %s % 0.14/0.33 % Computer : n020.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Wed Jul 27 05:47:53 EDT 2022 % 0.14/0.33 % CPUTime : % 2.09/2.26 ----- Otter 3.3f, August 2004 ----- % 2.09/2.26 The process was started by sandbox on n020.cluster.edu, % 2.09/2.26 Wed Jul 27 05:47:53 2022 % 2.09/2.26 The command was "./otter". The process ID is 12727. % 2.09/2.26 % 2.09/2.26 set(prolog_style_variables). % 2.09/2.26 set(auto). % 2.09/2.26 dependent: set(auto1). % 2.09/2.26 dependent: set(process_input). % 2.09/2.26 dependent: clear(print_kept). % 2.09/2.26 dependent: clear(print_new_demod). % 2.09/2.26 dependent: clear(print_back_demod). % 2.09/2.26 dependent: clear(print_back_sub). % 2.09/2.26 dependent: set(control_memory). % 2.09/2.26 dependent: assign(max_mem, 12000). % 2.09/2.26 dependent: assign(pick_given_ratio, 4). % 2.09/2.26 dependent: assign(stats_level, 1). % 2.09/2.26 dependent: assign(max_seconds, 10800). % 2.09/2.26 clear(print_given). % 2.09/2.26 % 2.09/2.26 list(usable). % 2.09/2.26 0 [] A=A. % 2.09/2.26 0 [] select(store(A,I,E),I)=E. % 2.09/2.26 0 [] I=J|select(store(A,I,E),J)=select(A,J). % 2.09/2.26 0 [] store(A,I,select(A,I))=A. % 2.09/2.26 0 [] store(store(A,I,E),I,F)=store(A,I,F). % 2.09/2.26 0 [] I=J|store(store(A,I,E),J,F)=store(store(A,J,F),I,E). % 2.09/2.26 0 [] a_1700=store(a1,n1,e1). % 2.09/2.26 0 [] a_1701=store(a_1700,n2,e2). % 2.09/2.26 0 [] a_1702=store(a_1701,n3,e3). % 2.09/2.26 0 [] a_1703=store(a_1702,n4,e4). % 2.09/2.26 0 [] a_1704=store(a_1703,n5,e5). % 2.09/2.26 0 [] a_1705=store(a_1704,n6,e6). % 2.09/2.26 0 [] a_1706=store(a_1705,n7,e7). % 2.09/2.26 0 [] a_1707=store(a_1706,n8,e8). % 2.09/2.26 0 [] a_1708=store(a_1707,n9,e9). % 2.09/2.26 0 [] a_1709=store(a_1708,n10,e10). % 2.09/2.26 0 [] a_1710=store(a_1709,n11,e11). % 2.09/2.26 0 [] a_1711=store(a_1710,n12,e12). % 2.09/2.26 0 [] a_1712=store(a_1711,n13,e13). % 2.09/2.26 0 [] a_1713=store(a_1712,n14,e14). % 2.09/2.26 0 [] a_1714=store(a_1713,n15,e15). % 2.09/2.26 0 [] a_1715=store(a_1714,n16,e16). % 2.09/2.26 0 [] a_1716=store(a_1715,n17,e17). % 2.09/2.26 0 [] a_1717=store(a_1716,n18,e18). % 2.09/2.26 0 [] a_1718=store(a_1717,n19,e19). % 2.09/2.26 0 [] a_1719=store(a_1718,n20,e20). % 2.09/2.26 0 [] a_1720=store(a_1719,n21,e21). % 2.09/2.26 0 [] a_1721=store(a_1720,n22,e22). % 2.09/2.26 0 [] a_1722=store(a_1721,n23,e23). % 2.09/2.26 0 [] a_1723=store(a_1722,n24,e24). % 2.09/2.26 0 [] a_1724=store(a_1723,n25,e25). % 2.09/2.26 0 [] a_1725=store(a_1724,n26,e26). % 2.09/2.26 0 [] a_1726=store(a_1725,n27,e27). % 2.09/2.26 0 [] a_1727=store(a_1726,n28,e28). % 2.09/2.26 0 [] a_1728=store(a_1727,n29,e29). % 2.09/2.26 0 [] a_1729=store(a_1728,n30,e30). % 2.09/2.26 0 [] a_1730=store(a_1729,n31,e31). % 2.09/2.26 0 [] a_1731=store(a_1730,n32,e32). % 2.09/2.26 0 [] a_1732=store(a_1731,n33,e33). % 2.09/2.26 0 [] a_1733=store(a_1732,n34,e34). % 2.09/2.26 0 [] a_1734=store(a_1733,n35,e35). % 2.09/2.26 0 [] a_1735=store(a_1734,n36,e36). % 2.09/2.26 0 [] a_1736=store(a_1735,n37,e37). % 2.09/2.26 0 [] a_1737=store(a_1736,n38,e38). % 2.09/2.26 0 [] a_1738=store(a_1737,n39,e39). % 2.09/2.26 0 [] a_1739=store(a_1738,n40,e40). % 2.09/2.26 0 [] a_1740=store(a_1739,n41,e41). % 2.09/2.26 0 [] a_1741=store(a_1740,n42,e42). % 2.09/2.26 0 [] a_1742=store(a_1741,n43,e43). % 2.09/2.26 0 [] a_1743=store(a_1742,n44,e44). % 2.09/2.26 0 [] a_1744=store(a_1743,n45,e45). % 2.09/2.26 0 [] a_1745=store(a_1744,n46,e46). % 2.09/2.26 0 [] a_1746=store(a_1745,n47,e47). % 2.09/2.26 0 [] a_1747=store(a_1746,n48,e48). % 2.09/2.26 0 [] a_1748=store(a_1747,n49,e49). % 2.09/2.26 0 [] a_1749=store(a_1748,n50,e50). % 2.09/2.26 0 [] a_1750=store(a1,n41,e41). % 2.09/2.26 0 [] a_1751=store(a_1750,n30,e30). % 2.09/2.26 0 [] a_1752=store(a_1751,n45,e45). % 2.09/2.26 0 [] a_1753=store(a_1752,n43,e43). % 2.09/2.26 0 [] a_1754=store(a_1753,n28,e28). % 2.09/2.26 0 [] a_1755=store(a_1754,n19,e19). % 2.09/2.26 0 [] a_1756=store(a_1755,n22,e22). % 2.09/2.26 0 [] a_1757=store(a_1756,n39,e39). % 2.09/2.26 0 [] a_1758=store(a_1757,n20,e20). % 2.09/2.26 0 [] a_1759=store(a_1758,n40,e40). % 2.09/2.26 0 [] a_1760=store(a_1759,n16,e16). % 2.09/2.26 0 [] a_1761=store(a_1760,n8,e8). % 2.09/2.26 0 [] a_1762=store(a_1761,n49,e49). % 2.09/2.26 0 [] a_1763=store(a_1762,n14,e14). % 2.09/2.26 0 [] a_1764=store(a_1763,n13,e13). % 2.09/2.26 0 [] a_1765=store(a_1764,n6,e6). % 2.09/2.26 0 [] a_1766=store(a_1765,n27,e27). % 2.09/2.26 0 [] a_1767=store(a_1766,n15,e15). % 2.09/2.26 0 [] a_1768=store(a_1767,n7,e7). % 2.09/2.26 0 [] a_1769=store(a_1768,n33,e33). % 2.09/2.26 0 [] a_1770=store(a_1769,n9,e9). % 2.09/2.26 0 [] a_1771=store(a_1770,n17,e17). % 2.09/2.26 0 [] a_1772=store(a_1771,n42,e42). % 2.09/2.26 0 [] a_1773=store(a_1772,n47,e47). % 2.09/2.26 0 [] a_1774=store(a_1773,n18,e18). % 2.09/2.26 0 [] a_1775=store(a_1774,n26,e26). % 2.09/2.26 0 [] a_1776=store(a_1775,n34,e34). % 2.09/2.26 0 [] a_1777=store(a_1776,n11,e11). % 2.09/2.26 0 [] a_1778=store(a_1777,n36,e36). % 2.09/2.26 0 [] a_1779=store(a_1778,n44,e44). % 2.09/2.26 0 [] a_1780=store(a_1779,n38,e38). % 2.09/2.26 0 [] a_1781=store(a_1780,n23,e23). % 2.09/2.26 0 [] a_1782=store(a_1781,n25,e25). % 2.09/2.26 0 [] a_1783=store(a_1782,n46,e46). % 2.09/2.26 0 [] a_1784=store(a_1783,n35,e35). % 2.09/2.26 0 [] a_1785=store(a_1784,n50,e50). % 2.09/2.26 0 [] a_1786=store(a_1785,n2,e2). % 2.09/2.26 0 [] a_1787=store(a_1786,n10,e10). % 2.09/2.26 0 [] a_1788=store(a_1787,n48,e48). % 2.09/2.26 0 [] a_1789=store(a_1788,n29,e29). % 2.09/2.26 0 [] a_1790=store(a_1789,n3,e3). % 2.09/2.26 0 [] a_1791=store(a_1790,n37,e37). % 2.09/2.26 0 [] a_1792=store(a_1791,n12,e12). % 2.09/2.26 0 [] a_1793=store(a_1792,n5,e5). % 2.09/2.26 0 [] a_1794=store(a_1793,n32,e32). % 2.09/2.26 0 [] a_1795=store(a_1794,n4,e4). % 2.09/2.26 0 [] a_1796=store(a_1795,n24,e24). % 2.09/2.26 0 [] a_1797=store(a_1796,n21,e21). % 2.09/2.26 0 [] a_1798=store(a_1797,n31,e31). % 2.09/2.26 0 [] a_1799=store(a_1798,n1,e1). % 2.09/2.26 0 [] a_1749!=a_1799. % 2.09/2.26 end_of_list. % 2.09/2.26 % 2.09/2.26 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=2. % 2.09/2.26 % 2.09/2.26 This ia a non-Horn set with equality. The strategy will be % 2.09/2.26 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.09/2.26 deletion, with positive clauses in sos and nonpositive % 2.09/2.26 clauses in usable. % 2.09/2.26 % 2.09/2.26 dependent: set(knuth_bendix). % 2.09/2.26 dependent: set(anl_eq). % 2.09/2.26 dependent: set(para_from). % 2.09/2.26 dependent: set(para_into). % 2.09/2.26 dependent: clear(para_from_right). % 2.09/2.26 dependent: clear(para_into_right). % 2.09/2.26 dependent: set(para_from_vars). % 2.09/2.26 dependent: set(eq_units_both_ways). % 2.09/2.26 dependent: set(dynamic_demod_all). % 2.09/2.26 dependent: set(dynamic_demod). % 2.09/2.26 dependent: set(order_eq). % 2.09/2.26 dependent: set(back_demod). % 2.09/2.26 dependent: set(lrpo). % 2.09/2.26 dependent: set(hyper_res). % 2.09/2.26 dependent: set(unit_deletion). % 2.09/2.26 dependent: set(factor). % 2.09/2.26 % 2.09/2.26 ------------> process usable: % 2.09/2.26 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] a_1799!=a_1749. % 2.09/2.26 % 2.09/2.26 ------------> process sos: % 2.09/2.26 ** KEPT (pick-wt=3): 3 [] A=A. % 2.09/2.26 ** KEPT (pick-wt=8): 4 [] select(store(A,B,C),B)=C. % 2.09/2.26 ---> New Demodulator: 5 [new_demod,4] select(store(A,B,C),B)=C. % 2.09/2.26 ** KEPT (pick-wt=13): 6 [] A=B|select(store(C,A,D),B)=select(C,B). % 2.09/2.26 ** KEPT (pick-wt=8): 7 [] store(A,B,select(A,B))=A. % 2.09/2.26 ---> New Demodulator: 8 [new_demod,7] store(A,B,select(A,B))=A. % 2.09/2.26 ** KEPT (pick-wt=12): 9 [] store(store(A,B,C),B,D)=store(A,B,D). % 2.09/2.26 ---> New Demodulator: 10 [new_demod,9] store(store(A,B,C),B,D)=store(A,B,D). % 2.09/2.26 ** KEPT (pick-wt=18): 11 [] A=B|store(store(C,A,D),B,E)=store(store(C,B,E),A,D). % 2.09/2.26 ** KEPT (pick-wt=6): 13 [copy,12,flip.1] store(a1,n1,e1)=a_1700. % 2.09/2.26 ---> New Demodulator: 14 [new_demod,13] store(a1,n1,e1)=a_1700. % 2.09/2.26 ** KEPT (pick-wt=6): 16 [copy,15,flip.1] store(a_1700,n2,e2)=a_1701. % 2.09/2.26 ---> New Demodulator: 17 [new_demod,16] store(a_1700,n2,e2)=a_1701. % 2.09/2.26 ** KEPT (pick-wt=6): 19 [copy,18,flip.1] store(a_1701,n3,e3)=a_1702. % 2.09/2.26 ---> New Demodulator: 20 [new_demod,19] store(a_1701,n3,e3)=a_1702. % 2.09/2.26 ** KEPT (pick-wt=6): 22 [copy,21,flip.1] store(a_1702,n4,e4)=a_1703. % 2.09/2.26 ---> New Demodulator: 23 [new_demod,22] store(a_1702,n4,e4)=a_1703. % 2.09/2.26 ** KEPT (pick-wt=6): 25 [copy,24,flip.1] store(a_1703,n5,e5)=a_1704. % 2.09/2.26 ---> New Demodulator: 26 [new_demod,25] store(a_1703,n5,e5)=a_1704. % 2.09/2.26 ** KEPT (pick-wt=6): 28 [copy,27,flip.1] store(a_1704,n6,e6)=a_1705. % 2.09/2.26 ---> New Demodulator: 29 [new_demod,28] store(a_1704,n6,e6)=a_1705. % 2.09/2.26 ** KEPT (pick-wt=6): 31 [copy,30,flip.1] store(a_1705,n7,e7)=a_1706. % 2.09/2.26 ---> New Demodulator: 32 [new_demod,31] store(a_1705,n7,e7)=a_1706. % 2.09/2.26 ** KEPT (pick-wt=6): 34 [copy,33,flip.1] store(a_1706,n8,e8)=a_1707. % 2.09/2.26 ---> New Demodulator: 35 [new_demod,34] store(a_1706,n8,e8)=a_1707. % 2.09/2.26 ** KEPT (pick-wt=6): 37 [copy,36,flip.1] store(a_1707,n9,e9)=a_1708. % 2.09/2.26 ---> New Demodulator: 38 [new_demod,37] store(a_1707,n9,e9)=a_1708. % 2.09/2.26 ** KEPT (pick-wt=6): 40 [copy,39,flip.1] store(a_1708,n10,e10)=a_1709. % 2.09/2.26 ---> New Demodulator: 41 [new_demod,40] store(a_1708,n10,e10)=a_1709. % 2.09/2.26 ** KEPT (pick-wt=6): 43 [copy,42,flip.1] store(a_1709,n11,e11)=a_1710. % 2.09/2.26 ---> New Demodulator: 44 [new_demod,43] store(a_1709,n11,e11)=a_1710. % 2.09/2.26 ** KEPT (pick-wt=6): 46 [copy,45,flip.1] store(a_1710,n12,e12)=a_1711. % 2.09/2.26 ---> New Demodulator: 47 [new_demod,46] store(a_1710,n12,e12)=a_1711. % 2.09/2.26 ** KEPT (pick-wt=6): 49 [copy,48,flip.1] store(a_1711,n13,e13)=a_1712. % 2.09/2.26 ---> New Demodulator: 50 [new_demod,49] store(a_1711,n13,e13)=a_1712. % 2.09/2.26 ** KEPT (pick-wt=6): 52 [copy,51,flip.1] store(a_1712,n14,e14)=a_1713. % 2.09/2.26 ---> New Demodulator: 53 [new_demod,52] store(a_1712,n14,e14)=a_1713. % 2.09/2.26 ** KEPT (pick-wt=6): 55 [copy,54,flip.1] store(a_1713,n15,e15)=a_1714. % 2.09/2.26 ---> New Demodulator: 56 [new_demod,55] store(a_1713,n15,e15)=a_1714. % 2.09/2.26 ** KEPT (pick-wt=6): 58 [copy,57,flip.1] store(a_1714,n16,e16)=a_1715. % 2.09/2.26 ---> New Demodulator: 59 [new_demod,58] store(a_1714,n16,e16)=a_1715. % 2.09/2.26 ** KEPT (pick-wt=6): 61 [copy,60,flip.1] store(a_1715,n17,e17)=a_1716. % 2.09/2.26 ---> New Demodulator: 62 [new_demod,61] store(a_1715,n17,e17)=a_1716. % 2.09/2.26 ** KEPT (pick-wt=6): 64 [copy,63,flip.1] store(a_1716,n18,e18)=a_1717. % 2.09/2.26 ---> New Demodulator: 65 [new_demod,64] store(a_1716,n18,e18)=a_1717. % 2.09/2.26 ** KEPT (pick-wt=6): 67 [copy,66,flip.1] store(a_1717,n19,e19)=a_1718. % 2.09/2.26 ---> New Demodulator: 68 [new_demod,67] store(a_1717,n19,e19)=a_1718. % 2.09/2.26 ** KEPT (pick-wt=6): 70 [copy,69,flip.1] store(a_1718,n20,e20)=a_1719. % 2.09/2.26 ---> New Demodulator: 71 [new_demod,70] store(a_1718,n20,e20)=a_1719. % 2.09/2.26 ** KEPT (pick-wt=6): 73 [copy,72,flip.1] store(a_1719,n21,e21)=a_1720. % 2.09/2.26 ---> New Demodulator: 74 [new_demod,73] store(a_1719,n21,e21)=a_1720. % 2.09/2.26 ** KEPT (pick-wt=6): 76 [copy,75,flip.1] store(a_1720,n22,e22)=a_1721. % 2.09/2.26 ---> New Demodulator: 77 [new_demod,76] store(a_1720,n22,e22)=a_1721. % 2.09/2.26 ** KEPT (pick-wt=6): 79 [copy,78,flip.1] store(a_1721,n23,e23)=a_1722. % 2.09/2.26 ---> New Demodulator: 80 [new_demod,79] store(a_1721,n23,e23)=a_1722. % 2.09/2.26 ** KEPT (pick-wt=6): 82 [copy,81,flip.1] store(a_1722,n24,e24)=a_1723. % 2.09/2.26 ---> New Demodulator: 83 [new_demod,82] store(a_1722,n24,e24)=a_1723. % 2.09/2.26 ** KEPT (pick-wt=6): 85 [copy,84,flip.1] store(a_1723,n25,e25)=a_1724. % 2.09/2.26 ---> New Demodulator: 86 [new_demod,85] store(a_1723,n25,e25)=a_1724. % 2.09/2.26 ** KEPT (pick-wt=6): 88 [copy,87,flip.1] store(a_1724,n26,e26)=a_1725. % 2.09/2.26 ---> New Demodulator: 89 [new_demod,88] store(a_1724,n26,e26)=a_1725. % 2.09/2.26 ** KEPT (pick-wt=6): 91 [copy,90,flip.1] store(a_1725,n27,e27)=a_1726. % 2.09/2.26 ---> New Demodulator: 92 [new_demod,91] store(a_1725,n27,e27)=a_1726. % 2.09/2.26 ** KEPT (pick-wt=6): 94 [copy,93,flip.1] store(a_1726,n28,e28)=a_1727. % 2.09/2.26 ---> New Demodulator: 95 [new_demod,94] store(a_1726,n28,e28)=a_1727. % 2.09/2.26 ** KEPT (pick-wt=6): 97 [copy,96,flip.1] store(a_1727,n29,e29)=a_1728. % 2.09/2.26 ---> New Demodulator: 98 [new_demod,97] store(a_1727,n29,e29)=a_1728. % 2.09/2.26 ** KEPT (pick-wt=6): 100 [copy,99,flip.1] store(a_1728,n30,e30)=a_1729. % 2.09/2.26 ---> New Demodulator: 101 [new_demod,100] store(a_1728,n30,e30)=a_1729. % 2.09/2.26 ** KEPT (pick-wt=6): 103 [copy,102,flip.1] store(a_1729,n31,e31)=a_1730. % 2.09/2.26 ---> New Demodulator: 104 [new_demod,103] store(a_1729,n31,e31)=a_1730. % 2.09/2.26 ** KEPT (pick-wt=6): 106 [copy,105,flip.1] store(a_1730,n32,e32)=a_1731. % 2.09/2.26 ---> New Demodulator: 107 [new_demod,106] store(a_1730,n32,e32)=a_1731. % 2.09/2.26 ** KEPT (pick-wt=6): 109 [copy,108,flip.1] store(a_1731,n33,e33)=a_1732. % 2.09/2.26 ---> New Demodulator: 110 [new_demod,109] store(a_1731,n33,e33)=a_1732. % 2.09/2.26 ** KEPT (pick-wt=6): 112 [copy,111,flip.1] store(a_1732,n34,e34)=a_1733. % 2.09/2.26 ---> New Demodulator: 113 [new_demod,112] store(a_1732,n34,e34)=a_1733. % 2.09/2.26 ** KEPT (pick-wt=6): 115 [copy,114,flip.1] store(a_1733,n35,e35)=a_1734. % 2.09/2.26 ---> New Demodulator: 116 [new_demod,115] store(a_1733,n35,e35)=a_1734. % 2.09/2.26 ** KEPT (pick-wt=6): 118 [copy,117,flip.1] store(a_1734,n36,e36)=a_1735. % 2.09/2.26 ---> New Demodulator: 119 [new_demod,118] store(a_1734,n36,e36)=a_1735. % 2.09/2.26 ** KEPT (pick-wt=6): 121 [copy,120,flip.1] store(a_1735,n37,e37)=a_1736. % 2.09/2.26 ---> New Demodulator: 122 [new_demod,121] store(a_1735,n37,e37)=a_1736. % 2.09/2.26 ** KEPT (pick-wt=6): 124 [copy,123,flip.1] store(a_1736,n38,e38)=a_1737. % 2.09/2.26 ---> New Demodulator: 125 [new_demod,124] store(a_1736,n38,e38)=a_1737. % 2.09/2.26 ** KEPT (pick-wt=6): 127 [copy,126,flip.1] store(a_1737,n39,e39)=a_1738. % 2.09/2.26 ---> New Demodulator: 128 [new_demod,127] store(a_1737,n39,e39)=a_1738. % 2.09/2.26 ** KEPT (pick-wt=6): 130 [copy,129,flip.1] store(a_1738,n40,e40)=a_1739. % 2.09/2.26 ---> New Demodulator: 131 [new_demod,130] store(a_1738,n40,e40)=a_1739. % 2.09/2.26 ** KEPT (pick-wt=6): 133 [copy,132,flip.1] store(a_1739,n41,e41)=a_1740. % 2.09/2.26 ---> New Demodulator: 134 [new_demod,133] store(a_1739,n41,e41)=a_1740. % 2.09/2.26 ** KEPT (pick-wt=6): 136 [copy,135,flip.1] store(a_1740,n42,e42)=a_1741. % 2.09/2.26 ---> New Demodulator: 137 [new_demod,136] store(a_1740,n42,e42)=a_1741. % 2.09/2.26 ** KEPT (pick-wt=6): 139 [copy,138,flip.1] store(a_1741,n43,e43)=a_1742. % 2.09/2.26 ---> New Demodulator: 140 [new_demod,139] store(a_1741,n43,e43)=a_1742. % 2.09/2.26 ** KEPT (pick-wt=6): 142 [copy,141,flip.1] store(a_1742,n44,e44)=a_1743. % 2.09/2.26 ---> New Demodulator: 143 [new_demod,142] store(a_1742,n44,e44)=a_1743. % 2.09/2.26 ** KEPT (pick-wt=6): 145 [copy,144,flip.1] store(a_1743,n45,e45)=a_1744. % 2.09/2.26 ---> New Demodulator: 146 [new_demod,145] store(a_1743,n45,e45)=a_1744. % 2.09/2.26 ** KEPT (pick-wt=6): 148 [copy,147,flip.1] store(a_1744,n46,e46)=a_1745. % 2.09/2.26 ---> New Demodulator: 149 [new_demod,148] store(a_1744,n46,e46)=a_1745. % 2.09/2.26 ** KEPT (pick-wt=6): 151 [copy,150,flip.1] store(a_1745,n47,e47)=a_1746. % 2.09/2.26 ---> New Demodulator: 152 [new_demod,151] store(a_1745,n47,e47)=a_1746. % 2.09/2.26 ** KEPT (pick-wt=6): 154 [copy,153,flip.1] store(a_1746,n48,e48)=a_1747. % 2.09/2.26 ---> New Demodulator: 155 [new_demod,154] store(a_1746,n48,e48)=a_1747. % 2.09/2.26 ** KEPT (pick-wt=6): 157 [copy,156,flip.1] store(a_1747,n49,e49)=a_1748. % 2.09/2.26 ---> New Demodulator: 158 [new_demod,157] store(a_1747,n49,e49)=a_1748. % 2.09/2.26 ** KEPT (pick-wt=6): 160 [copy,159,flip.1] store(a_1748,n50,e50)=a_1749. % 2.09/2.26 ---> New Demodulator: 161 [new_demod,160] store(a_1748,n50,e50)=a_1749. % 2.09/2.26 ** KEPT (pick-wt=6): 163 [copy,162,flip.1] store(a1,n41,e41)=a_1750. % 2.09/2.26 ---> New Demodulator: 164 [new_demod,163] store(a1,n41,e41)=a_1750. % 2.09/2.26 ** KEPT (pick-wt=6): 166 [copy,165,flip.1] store(a_1750,n30,e30)=a_1751. % 2.09/2.26 ---> New Demodulator: 167 [new_demod,166] store(a_1750,n30,e30)=a_1751. % 2.09/2.26 ** KEPT (pick-wt=6): 169 [copy,168,flip.1] store(a_1751,n45,e45)=a_1752. % 2.09/2.26 ---> New Demodulator: 170 [new_demod,169] store(a_1751,n45,e45)=a_1752. % 2.09/2.26 ** KEPT (pick-wt=6): 172 [copy,171,flip.1] store(a_1752,n43,e43)=a_1753. % 2.09/2.26 ---> New Demodulator: 173 [new_demod,172] store(a_1752,n43,e43)=a_1753. % 2.09/2.26 ** KEPT (pick-wt=6): 175 [copy,174,flip.1] store(a_1753,n28,e28)=a_1754. % 2.09/2.26 ---> New Demodulator: 176 [new_demod,175] store(a_1753,n28,e28)=a_1754. % 2.09/2.26 ** KEPT (pick-wt=6): 178 [copy,177,flip.1] store(a_1754,n19,e19)=a_1755. % 2.09/2.26 ---> New Demodulator: 179 [new_demod,178] store(a_1754,n19,e19)=a_1755. % 2.09/2.26 ** KEPT (pick-wt=6): 181 [copy,180,flip.1] store(a_1755,n22,e22)=a_1756. % 2.09/2.26 ---> New Demodulator: 182 [new_demod,181] store(a_1755,n22,e22)=a_1756. % 2.09/2.26 ** KEPT (pick-wt=6): 184 [copy,183,flip.1] store(a_1756,n39,e39)=a_1757. % 2.09/2.26 ---> New Demodulator: 185 [new_demod,184] store(a_1756,n39,e39)=a_1757. % 2.09/2.26 ** KEPT (pick-wt=6): 187 [copy,186,flip.1] store(a_1757,n20,e20)=a_1758. % 2.09/2.26 ---> New Demodulator: 188 [new_demod,187] store(a_1757,n20,e20)=a_1758. % 2.09/2.26 ** KEPT (pick-wt=6): 190 [copy,189,flip.1] store(a_1758,n40,e40)=a_1759. % 2.09/2.26 ---> New Demodulator: 191 [new_demod,190] store(a_1758,n40,e40)=a_1759. % 2.09/2.26 ** KEPT (pick-wt=6): 193 [copy,192,flip.1] store(a_1759,n16,e16)=a_1760. % 2.09/2.26 ---> New Demodulator: 194 [new_demod,193] store(a_1759,n16,e16)=a_1760. % 2.09/2.26 ** KEPT (pick-wt=6): 196 [copy,195,flip.1] store(a_1760,n8,e8)=a_1761. % 2.09/2.26 ---> New Demodulator: 197 [new_demod,196] store(a_1760,n8,e8)=a_1761. % 2.09/2.26 ** KEPT (pick-wt=6): 199 [copy,198,flip.1] store(a_1761,n49,e49)=a_1762. % 2.09/2.26 ---> New Demodulator: 200 [new_demod,199] store(a_1761,n49,e49)=a_1762. % 2.09/2.26 ** KEPT (pick-wt=6): 202 [copy,201,flip.1] store(a_1762,n14,e14)=a_1763. % 2.09/2.26 ---> New Demodulator: 203 [new_demod,202] store(a_1762,n14,e14)=a_1763. % 2.09/2.26 ** KEPT (pick-wt=6): 205 [copy,204,flip.1] store(a_1763,n13,e13)=a_1764. % 2.09/2.26 ---> New Demodulator: 206 [new_demod,205] store(a_1763,n13,e13)=a_1764. % 2.09/2.26 ** KEPT (pick-wt=6): 208 [copy,207,flip.1] store(a_1764,n6,e6)=a_1765. % 2.09/2.26 ---> New Demodulator: 209 [new_demod,208] store(a_1764,n6,e6)=a_1765. % 2.09/2.26 ** KEPT (pick-wt=6): 211 [copy,210,flip.1] store(a_1765,n27,e27)=a_1766. % 2.09/2.26 ---> New Demodulator: 212 [new_demod,211] store(a_1765,n27,e27)=a_1766. % 2.09/2.26 ** KEPT (pick-wt=6): 214 [copy,213,flip.1] store(a_1766,n15,e15)=a_1767. % 2.09/2.26 ---> New Demodulator: 215 [new_demod,214] store(a_1766,n15,e15)=a_1767. % 2.09/2.26 ** KEPT (pick-wt=6): 217 [copy,216,flip.1] store(a_1767,n7,e7)=a_1768. % 2.09/2.26 ---> New Demodulator: 218 [new_demod,217] store(a_1767,n7,e7)=a_1768. % 2.09/2.26 ** KEPT (pick-wt=6): 220 [copy,219,flip.1] store(a_1768,n33,e33)=a_1769. % 2.09/2.26 ---> New Demodulator: 221 [new_demod,220] store(a_1768,n33,e33)=a_1769. % 2.09/2.26 ** KEPT (pick-wt=6): 223 [copy,222,flip.1] store(a_1769,n9,e9)=a_1770. % 2.09/2.26 ---> New Demodulator: 224 [new_demod,223] store(a_1769,n9,e9)=a_1770. % 2.09/2.26 ** KEPT (pick-wt=6): 226 [copy,225,flip.1] store(a_1770,n17,e17)=a_1771. % 2.09/2.26 ---> New Demodulator: 227 [new_demod,226] store(a_1770,n17,e17)=a_1771. % 2.09/2.26 ** KEPT (pick-wt=6): 229 [copy,228,flip.1] store(a_1771,n42,e42)=a_1772. % 2.09/2.26 ---> New Demodulator: 230 [new_demod,229] store(a_1771,n42,e42)=a_1772. % 2.09/2.26 ** KEPT (pick-wt=6): 232 [copy,231,flip.1] store(a_1772,n47,e47)=a_1773. % 2.09/2.26 ---> New Demodulator: 233 [new_demod,232] store(a_1772,n47,e47)=a_1773. % 2.09/2.26 ** KEPT (pick-wt=6): 235 [copy,234,flip.1] store(a_1773,n18,e18)=a_1774. % 2.09/2.26 ---> New Demodulator: 236 [new_demod,235] store(a_1773,n18,e18)=a_1774. % 2.09/2.26 ** KEPT (pick-wt=6): 238 [copy,237,flip.1] store(a_1774,n26,e26)=a_1775. % 2.09/2.26 ---> New Demodulator: 239 [new_demod,238] store(a_1774,n26,e26)=a_1775. % 2.09/2.26 ** KEPT (pick-wt=6): 241 [copy,240,flip.1] store(a_1775,n34,e34)=a_1776. % 2.09/2.26 ---> New Demodulator: 242 [new_demod,241] store(a_1775,n34,e34)=a_1776. % 2.09/2.26 ** KEPT (pick-wt=6): 244 [copy,243,flip.1] store(a_1776,n11,e11)=a_1777. % 2.09/2.26 ---> New Demodulator: 245 [new_demod,244] store(a_1776,n11,e11)=a_1777. % 2.09/2.26 ** KEPT (pick-wt=6): 247 [copy,246,flip.1] store(a_1777,n36,e36)=a_1778. % 2.09/2.26 ---> New Demodulator: 248 [new_demod,247] store(a_1777,n36,e36)=a_1778. % 2.09/2.26 ** KEPT (pick-wt=6): 250 [copy,249,flip.1] store(a_1778,n44,e44)=a_1779. % 2.09/2.26 ---> New Demodulator: 251 [new_demod,250] store(a_1778,n44,e44)=a_1779. % 2.09/2.26 ** KEPT (pick-wt=6): 253 [copy,252,flip.1] store(a_1779,n38,e38)=a_1780. % 2.09/2.26 ---> New Demodulator: 254 [new_demod,253] store(a_1779,n38,e38)=a_1780. % 2.09/2.26 ** KEPT (pick-wt=6): 256 [copy,255,flip.1] store(a_1780,n23,e23)=a_1781. % 2.09/2.26 ---> New Demodulator: 257 [new_demod,256] store(a_1780,n23,e23)=a_1781. % 2.09/2.26 ** KEPT (pick-wt=6): 259 [copy,258,flip.1] store(a_1781,n25,e25)=a_1782. % 2.09/2.26 ---> New Demodulator: 260 [new_demod,259] store(a_1781,n25,e25)=a_1782. % 2.09/2.26 ** KEPT (pick-wt=6): 262 [copy,261,flip.1] store(a_1782,n46,e46)=a_1783. % 2.09/2.26 ---> New Demodulator: 263 [new_demod,262] store(a_1782,n46,e46)=a_1783. % 2.09/2.26 ** KEPT (pick-wt=6): 265 [copy,264,flip.1] store(a_1783,n35,e35)=a_1784. % 2.09/2.26 ---> New Demodulator: 266 [new_demod,265] store(a_1783,n35,e35)=a_1784. % 2.09/2.26 ** KEPT (pick-wt=6): 268 [copy,267,flip.1] store(a_1784,n50,e50)=a_1785. % 2.09/2.26 ---> New Demodulator: 269 [new_demod,268] store(a_1784,n50,e50)=a_1785. % 2.09/2.26 ** KEPT (pick-wt=6): 271 [copy,270,flip.1] store(a_1785,n2,e2)=a_1786. % 2.09/2.26 ---> New Demodulator: 272 [new_demod,271] store(a_1785,n2,e2)=a_1786. % 2.09/2.26 ** KEPT (pick-wt=6): 274 [copy,273,flip.1] store(a_1786,n10,e10)=a_1787. % 2.09/2.26 ---> New Demodulator: 275 [new_demod,274] store(a_1786,n10,e10)=a_1787. % 2.09/2.26 ** KEPT (pick-wt=6): 277 [copy,276,flip.1] store(a_1787,n48,e48)=a_1788. % 2.09/2.26 ---> New Demodulator: 278 [new_demod,277] store(a_1787,n48,e48)=a_1788. % 2.09/2.26 ** KEPT (pick-wt=6): 280 [copy,279,flip.1] store(a_1788,n29,e29)=a_1789. % 2.09/2.26 ---> New Demodulator: 281 [new_demod,280] store(a_1788,n29,e29)=a_1789. % 2.09/2.26 ** KEPT (pick-wt=6): 283 [copy,282,flip.1] store(a_1789,n3,e3)=a_1790. % 2.09/2.26 ---> New Demodulator: 284 [new_demod,283] store(a_1789,n3,e3)=a_1790. % 2.09/2.26 ** KEPT (pick-wt=6): 286 [copy,285,flip.1] store(a_1790,n37,e37)=a_1791. % 2.09/2.26 ---> New Demodulator: 287 [new_demod,286] store(a_1790,n37,e37)=a_1791. % 2.09/2.26 ** KEPT (pick-wt=6): 289 [copy,288,flip.1] store(a_1791,n12,e12)=a_1792. % 2.09/2.26 ---> New Demodulator: 290 [new_demod,289] store(a_1791,n12,e12)=a_1792. % 2.09/2.26 ** KEPT (pick-wt=6): 292 [copy,291,flip.1] store(a_1792,n5,e5)=a_1793. % 2.09/2.26 ---> New Demodulator: 293 [new_demod,292] store(a_1792,n5,e5)=a_1793. % 2.09/2.26 ** KEPT (pick-wt=6): 295 [copy,294,flip.1] store(a_1793,n32,e32)=a_1794. % 2.09/2.26 ---> New Demodulator: 296 [new_demod,295] store(a_1793,n32,e32)=a_1794. % 2.09/2.26 ** KEPT (pick-wt=6): 298 [copy,297,flip.1] store(a_1794,n4,e4)=a_1795. % 2.09/2.26 ---> New Demodulator: 299 [new_demod,298] store(a_1794,n4,e4)=a_1795. % 2.09/2.26 ** KEPT (pick-wt=6): 301 [copy,300,flip.1] store(a_1795,n24,e24)=a_1796. % 2.09/2.26 ---> New Demodulator: 302 [new_demod,301] store(a_1795,n24,e24)=a_1796. % 2.09/2.26 ** KEPT (pick-wt=6): 304 [copy,303,flip.1] store(a_1796,n21,e21)=a_1797. % 2.09/2.26 ---> New Demodulator: 305 [new_demod,304] store(a_1796,n21,e21)=a_1797. % 2.09/2.26 ** KEPT (pick-wt=6): 307 [copy,306,flip.1] store(a_1797,n31,e31)=a_1798. % 2.09/2.26 ---> New Demodulator: 308 [new_demod,307] store(a_1797,n31,e31)=a_1798. % 2.09/2.26 ** KEPT (pick-wt=6): 310 [copy,309,flip.1] store(a_1798,n1,e1)=a_1799. % 2.09/2.26 ---> New Demodulator: 311 [new_demod,310] store(a_1798,n1,e1)=a_1799. % 2.09/2.26 Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] A=A. % 2.09/2.26 >>>> Starting back demodulation with 5. % 2.09/2.26 >>>> Starting back demodulation with 8. % 2.09/2.26 >>>> Starting back demodulation with 10. % 2.09/2.26 >>>> Starting back demodulation with 14. % 2.09/2.26 >>>> Starting back demodulation with 17. % 2.09/2.26 >>>> Starting back demodulation with 20. % 2.09/2.26 >>>> Starting back demodulation with 23. % 2.09/2.26 >>>> Starting back demodulation with 26. % 2.09/2.28 >>>> Starting back demodulation with 29. % 2.09/2.28 >>>> Starting back demodulation with 32. % 2.09/2.28 >>>> Starting back demodulation with 35. % 2.09/2.28 >>>> Starting back demodulation with 38. % 2.09/2.28 >>>> Starting back demodulation with 41. % 2.09/2.28 >>>> Starting back demodulation with 44. % 2.09/2.28 >>>> Starting back demodulation with 47. % 2.09/2.28 >>>> Starting back demodulation with 50. % 2.09/2.28 >>>> Starting back demodulation with 53. % 2.09/2.28 >>>> Starting back demodulation with 56. % 2.09/2.28 >>>> Starting back demodulation with 59. % 2.09/2.28 >>>> Starting back demodulation with 62. % 2.09/2.28 >>>> Starting back demodulation with 65. % 2.09/2.28 >>>> Starting back demodulation with 68. % 2.09/2.28 >>>> Starting back demodulation with 71. % 2.09/2.28 >>>> Starting back demodulation with 74. % 2.09/2.28 >>>> Starting back demodulation with 77. % 2.09/2.28 >>>> Starting back demodulation with 80. % 2.09/2.28 >>>> Starting back demodulation with 83. % 2.09/2.28 >>>> Starting back demodulation with 86. % 2.09/2.28 >>>> Starting back demodulation with 89. % 2.09/2.28 >>>> Starting back demodulation with 92. % 2.09/2.28 >>>> Starting back demodulation with 95. % 2.09/2.28 >>>> Starting back demodulation with 98. % 2.09/2.28 >>>> Starting back demodulation with 101. % 2.09/2.28 >>>> Starting back demodulation with 104. % 2.09/2.28 >>>> Starting back demodulation with 107. % 2.09/2.28 >>>> Starting back demodulation with 110. % 2.09/2.28 >>>> Starting back demodulation with 113. % 2.09/2.28 >>>> Starting back demodulation with 116. % 2.09/2.28 >>>> Starting back demodulation with 119. % 2.09/2.28 >>>> Starting back demodulation with 122. % 2.09/2.28 >>>> Starting back demodulation with 125. % 2.09/2.28 >>>> Starting back demodulation with 128. % 2.09/2.28 >>>> Starting back demodulation with 131. % 2.09/2.28 >>>> Starting back demodulation with 134. % 2.09/2.28 >>>> Starting back demodulation with 137. % 2.09/2.28 >>>> Starting back demodulation with 140. % 2.09/2.28 >>>> Starting back demodulation with 143. % 2.09/2.28 >>>> Starting back demodulation with 146. % 2.09/2.28 >>>> Starting back demodulation with 149. % 2.09/2.28 >>>> Starting back demodulation with 152. % 2.09/2.28 >>>> Starting back demodulation with 155. % 2.09/2.28 >>>> Starting back demodulation with 158. % 2.09/2.28 >>>> Starting back demodulation with 161. % 2.09/2.28 >>>> Starting back demodulation with 164. % 2.09/2.28 >>>> Starting back demodulation with 167. % 2.09/2.28 >>>> Starting back demodulation with 170. % 2.09/2.28 >>>> Starting back demodulation with 173. % 2.09/2.28 >>>> Starting back demodulation with 176. % 2.09/2.28 >>>> Starting back demodulation with 179. % 2.09/2.28 >>>> Starting back demodulation with 182. % 2.09/2.28 >>>> Starting back demodulation with 185. % 2.09/2.28 >>>> Starting back demodulation with 188. % 2.09/2.28 >>>> Starting back demodulation with 191. % 2.09/2.28 >>>> Starting back demodulation with 194. % 2.09/2.28 >>>> Starting back demodulation with 197. % 2.09/2.28 >>>> Starting back demodulation with 200. % 2.09/2.28 >>>> Starting back demodulation with 203. % 2.09/2.28 >>>> Starting back demodulation with 206. % 2.09/2.28 >>>> Starting back demodulation with 209. % 2.09/2.28 >>>> Starting back demodulation with 212. % 2.09/2.28 >>>> Starting back demodulation with 215. % 2.09/2.28 >>>> Starting back demodulation with 218. % 2.09/2.28 >>>> Starting back demodulation with 221. % 2.09/2.28 >>>> Starting back demodulation with 224. % 2.09/2.28 >>>> Starting back demodulation with 227. % 2.09/2.28 >>>> Starting back demodulation with 230. % 2.09/2.28 >>>> Starting back demodulation with 233. % 2.09/2.28 >>>> Starting back demodulation with 236. % 2.09/2.28 >>>> Starting back demodulation with 239. % 2.09/2.28 >>>> Starting back demodulation with 242. % 2.09/2.28 >>>> Starting back demodulation with 245. % 2.09/2.28 >>>> Starting back demodulation with 248. % 2.09/2.28 >>>> Starting back demodulation with 251. % 2.09/2.28 >>>> Starting back demodulation with 254. % 2.09/2.28 >>>> Starting back demodulation with 257. % 2.09/2.28 >>>> Starting back demodulation with 260. % 2.09/2.28 >>>> Starting back demodulation with 263. % 2.09/2.28 >>>> Starting back demodulation with 266. % 2.09/2.28 >>>> Starting back demodulation with 269. % 2.09/2.28 >>>> Starting back demodulation with 272. % 2.09/2.28 >>>> Starting back demodulation with 275. % 2.09/2.28 >>>> Starting back demodulation with 278. % 2.09/2.28 >>>> Starting back demodulation with 281. % 2.09/2.28 >>>> Starting back demodulation with 284. % 2.09/2.28 >>>> Starting back demodulation with 287. % 2.09/2.28 >>>> Starting back demodulation with 290. % 2.09/2.28 >>>> Starting back demodulation with 293. % 2.09/2.28 >>>> Starting back demodulation with 296. % 2.09/2.28 >>>> Starting back demodulation with 299. % 2.09/2.28 >>>> Starting back demodulation with 302. % 2.09/2.28 >>>> Starting back demodulation with 305. % 2.09/2.28 >>>> Starting back demodulation with 308. % 2.09/2.28 >>>> Starting back demodulation with 311. % 2.09/2.28 % 2.09/2.28 ======= end of input processing ======= % 2.09/2.28 % 2.09/2.28 =========== start of search =========== % 2.09/2.28 % 2.09/2.28 % 2.09/2.28 Resetting weight limit to 6. % 3.55/3.70 % 3.55/3.70 % 3.55/3.70 Resetting weight limit to 6. % 3.55/3.70 % 3.55/3.70 sos_size=406 % 3.55/3.70 % 3.55/3.70 Search stopped because sos empty. % 3.55/3.70 % 3.55/3.70 % 3.55/3.70 Search stopped because sos empty. % 3.55/3.70 % 3.55/3.70 ============ end of search ============ % 3.55/3.70 % 3.55/3.70 -------------- statistics ------------- % 3.55/3.70 clauses given 613 % 3.55/3.70 clauses generated 195075 % 3.55/3.70 clauses kept 651 % 3.55/3.70 clauses forward subsumed 1181 % 3.55/3.70 clauses back subsumed 29 % 3.55/3.70 Kbytes malloced 7812 % 3.55/3.70 % 3.55/3.70 ----------- times (seconds) ----------- % 3.55/3.70 user CPU time 1.43 (0 hr, 0 min, 1 sec) % 3.55/3.70 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 3.55/3.70 wall-clock time 4 (0 hr, 0 min, 4 sec) % 3.55/3.70 % 3.55/3.70 Process 12727 finished Wed Jul 27 05:47:57 2022 % 3.55/3.70 Otter interrupted % 3.55/3.70 PROOF NOT FOUND %------------------------------------------------------------------------------