%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRA021+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 07:22:11 EDT 2022 % Result : CounterSatisfiable 0.92s 1.17s % Output : Saturation 0.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : GRA021+1 : TPTP v8.1.0. Released v3.2.0. % 0.11/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n025.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue May 31 00:01:27 EDT 2022 % 0.14/0.35 % CPUTime : % 0.92/1.17 % 0.92/1.17 SPASS V 3.9 % 0.92/1.17 SPASS beiseite: Completion found. % 0.92/1.17 % SZS status CounterSatisfiable % 0.92/1.17 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.92/1.17 SPASS derived 1697 clauses, backtracked 138 clauses, performed 58 splits and kept 1286 clauses. % 0.92/1.17 SPASS allocated 87891 KBytes. % 0.92/1.17 SPASS spent 0:00:00.82 on the problem. % 0.92/1.17 0:00:00.03 for the input. % 0.92/1.17 0:00:00.04 for the FLOTTER CNF translation. % 0.92/1.17 0:00:00.05 for inferences. % 0.92/1.17 0:00:00.00 for the backtracking. % 0.92/1.17 0:00:00.65 for the reduction. % 0.92/1.17 % 0.92/1.17 % 0.92/1.17 The saturated set of worked-off clauses is : % 0.92/1.17 % SZS output start Saturation % 0.92/1.17 15[0:Inp] || less_than(u,v)* less_than(v,w)* -> less_than(u,w)*. % 0.92/1.17 2105[58:Res:368.0,2054.0] || red(n10,n2)*+ red(u,n10) red(u,n2)* red(u,n11) red(v,n11) red(v,n2)* red(v,n10) red(v,u)* -> . % 0.92/1.17 2106[58:Res:440.0,2054.0] || red(n9,n2)*+ red(u,n9) red(u,n2)* red(u,n11) red(v,n11) red(v,n2)* red(v,n9) red(v,u)* -> . % 0.92/1.17 2108[58:Res:1132.0,2054.0] || red(n6,n2)*+ red(u,n6) red(u,n2)* red(u,n11) red(v,n11) red(v,n2)* red(v,n6) red(v,u)* -> . % 0.92/1.17 2103[56:MRR:2100.0,713.0] || red(u,n2)*+ red(u,n5) red(u,n12) red(v,n12) red(v,n5) red(v,n2)* red(v,u)* -> . % 0.92/1.17 2054[58:Res:2049.0,20.0] || red(u,n11)+ red(u,n2)* red(v,u)* red(v,n2)* red(v,n11) red(w,n11) red(w,n2)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1847[56:Res:1842.0,20.0] || red(u,n12)+ red(u,n5)* red(v,u)* red(v,n5)* red(v,n12) red(w,n12) red(w,n5)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1381[48:Res:1375.0,20.0] || red(u,n6)+ red(u,n1)* red(v,u)* red(v,n1)* red(v,n6) red(w,n6) red(w,n1)* red(w,u)* red(w,v)* -> . % 0.92/1.17 2081[29:Res:847.0,354.0] || green(n7,n1)*+ green(u,n7) green(u,n1)* green(u,n11) green(v,n11) green(v,n1)* green(v,n7) green(v,u)* -> red(n1,n11). % 0.92/1.17 2062[58:Res:2049.0,442.0] || red(n2,n9)*+ red(u,n2)* red(u,n9) red(u,n11) red(v,n11) red(v,n9) red(v,n2)* red(v,u)* -> . % 0.92/1.17 2082[54:Res:1672.0,354.0] || green(n4,n1)*+ green(u,n4) green(u,n1)* green(u,n11) green(v,n11) green(v,n1)* green(v,n4) green(v,u)* -> red(n1,n11). % 0.92/1.17 2065[58:MRR:2055.0,713.0] || red(u,n2)*+ red(u,n5) red(u,n11) red(v,n11) red(v,n5) red(v,n2)* red(v,u)* -> . % 0.92/1.17 2088[58:Res:1057.0,2064.0] || red(n1,n8)*+ red(n1,n11) red(u,n11) red(u,n8) red(u,n2) red(u,n1)* -> . % 0.92/1.17 2064[58:MRR:2058.0,1506.0] || red(u,n2)*+ red(u,n8) red(u,n11) red(v,n11) red(v,n8) red(v,n2)* red(v,u)* -> . % 0.92/1.17 2087[58:MRR:2086.1,1177.0] || red(n1,n11)*+ red(u,n12) red(u,n11) red(u,n2) red(u,n1)* -> . % 0.92/1.17 2083[57:Res:1955.0,354.0] || green(n3,n1)*+ green(u,n3) green(u,n1)* green(u,n11) green(v,n11) green(v,n1)* green(v,n3) green(v,u)* -> red(n1,n11). % 0.92/1.17 2050[58:MRR:1175.0,2049.0] || red(u,n2)*+ red(u,n11) red(u,n12) red(v,n12) red(v,n11) red(v,n2)* red(v,u)* -> . % 0.92/1.17 2085[0:Obv:2084.8] || green(n1,n1)*+ green(u,n1)* green(u,n11) green(v,n11) green(v,n1)* green(v,u)* -> red(n1,n11). % 0.92/1.17 2052[58:MRR:1516.1,2049.0] || red(n2,n9)*+ red(u,n11) red(u,n9) red(u,n8) red(u,n2)* -> . % 0.92/1.17 2079[58:Res:374.0,2053.0] || red(n11,n11)+ red(n11,n5) red(n11,n2)* -> . % 0.92/1.17 354[0:Res:352.0,19.0] || green(u,n11)+ green(u,n1)* green(v,u)* green(v,n1)* green(v,n11) green(w,n11) green(w,n1)* green(w,u)* green(w,v)* -> red(n1,n11). % 0.92/1.17 2080[58:MRR:2072.0,368.0] || red(n10,n5)+ red(n10,n2)* -> . % 0.92/1.17 2053[58:MRR:1918.0,2049.0] || red(u,n12)+ red(u,n11) red(u,n5) red(u,n2)* -> . % 0.92/1.17 2051[58:MRR:1512.0,2049.0] || red(u,n11)+ red(u,n8) red(u,n5) red(u,n2)* -> . % 0.92/1.17 2049[58:Spt:2009.9] || -> red(n2,n11)*. % 0.92/1.17 1359[47:Res:1356.0,20.0] || red(u,n11)+ red(u,n5)* red(v,u)* red(v,n5)* red(v,n11) red(w,n11) red(w,n5)* red(w,u)* red(w,v)* -> . % 0.92/1.17 2036[55:MRR:2033.0,2033.1,525.0,1735.0] || red(u,n10)+ red(u,n5) red(u,n4) red(u,n3)* -> . % 0.92/1.17 2022[50:MRR:2019.0,388.0] || red(u,n4)*+ red(u,n5) red(u,n10) red(v,n10) red(v,n5) red(v,n4)* red(v,u)* -> . % 0.92/1.17 2021[55:MRR:2020.0,525.0] || red(u,n3)*+ red(u,n5) red(u,n10) red(v,n10) red(v,n5) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1743[55:Res:1735.0,20.0] || red(u,n10)+ red(u,n3)* red(v,u)* red(v,n3)* red(v,n10) red(w,n10) red(w,n3)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1246[45:Res:1242.0,20.0] || red(u,n10)+ red(u,n5)* red(v,u)* red(v,n5)* red(v,n10) red(w,n10) red(w,n5)* red(w,u)* red(w,v)* -> . % 0.92/1.17 2011[30:Res:887.0,344.0] || green(n6,n1)*+ green(u,n6) green(u,n1)* green(u,n10) green(v,n10) green(v,n1)* green(v,n6) green(v,u)* -> red(n1,n10). % 0.92/1.17 2012[56:Res:1876.0,344.0] || green(n2,n1)*+ green(u,n2) green(u,n1)* green(u,n10) green(v,n10) green(v,n1)* green(v,n2) green(v,u)* -> red(n1,n10). % 0.92/1.17 2014[0:Obv:2013.8] || green(n1,n1)*+ green(u,n1)* green(u,n10) green(v,n10) green(v,n1)* green(v,u)* -> red(n1,n10). % 0.92/1.17 344[0:Res:342.0,19.0] || green(u,n10)+ green(u,n1)* green(v,u)* green(v,n1)* green(v,n10) green(w,n10) green(w,n1)* green(w,u)* green(w,v)* -> red(n1,n10). % 0.92/1.17 1220[44:Res:1215.0,20.0] || red(u,n7)+ red(u,n1)* red(v,u)* red(v,n1)* red(v,n7) red(w,n7) red(w,n1)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1995[53:Res:1665.0,334.0] || green(n4,n3)*+ green(u,n4) green(u,n3)* green(u,n12) green(v,n12) green(v,n3)* green(v,n4) green(v,u)* -> red(n3,n12). % 0.92/1.17 1997[28:Res:808.0,334.0] || green(n8,n3)*+ green(u,n8) green(u,n3)* green(u,n12) green(v,n12) green(v,n3)* green(v,n8) green(v,u)* -> red(n3,n12). % 0.92/1.17 1998[0:Obv:1996.8] || green(n3,n3)*+ green(u,n3)* green(u,n12) green(v,n12) green(v,n3)* green(v,u)* -> red(n3,n12). % 0.92/1.17 334[0:Res:332.0,19.0] || green(u,n12)+ green(u,n3)* green(v,u)* green(v,n3)* green(v,n12) green(w,n12) green(w,n3)* green(w,u)* green(w,v)* -> red(n3,n12). % 0.92/1.17 1988[43:Res:382.0,1189.0] || red(n6,n2)*+ red(u,n6) red(u,n2)* red(u,n7) red(v,n7) red(v,n2)* red(v,n6) red(v,u)* -> . % 0.92/1.17 1993[44:MRR:1992.0,1057.0] || red(u,n1)*+ red(u,n2) red(u,n7) red(v,n7) red(v,n2) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1189[43:Res:1185.0,20.0] || red(u,n7)+ red(u,n2)* red(v,u)* red(v,n2)* red(v,n7) red(w,n7) red(w,n2)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1960[57:MRR:1772.9,1953.0] || green(n1,n3)*+ green(u,n1)* green(u,n3) green(u,n11) green(v,n11) green(v,n3) green(v,n1)* green(v,u)* -> red(n1,n11). % 0.92/1.17 1961[57:MRR:319.9,1953.0] || green(u,n11)+ green(u,n3)* green(v,u)* green(v,n3)* green(v,n11) green(w,n11) green(w,n3)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1958[57:MRR:1769.8,1953.0] || green(n4,n3)*+ green(u,n4) green(u,n3)* green(u,n11) green(v,n11) green(v,n3)* green(v,n4) green(v,u)* -> . % 0.92/1.17 1981[56:MRR:1979.0,700.0] || red(n3,n12)*+ red(u,n12) red(u,n6) red(u,n5) red(u,n3)* -> . % 0.92/1.17 1865[56:MRR:1849.0,386.0] || red(u,n5)*+ red(u,n6) red(u,n12) red(v,n12) red(v,n6) red(v,n5)* red(v,u)* -> . % 0.92/1.17 1959[57:MRR:1681.8,1953.0] || green(n3,n4)*+ green(u,n3)* green(u,n4) green(u,n11) green(v,n11) green(v,n4) green(v,n3)* green(v,u)* -> . % 0.92/1.17 1977[56:Res:374.0,1969.0] || red(n11,n7)+ red(n11,n5) red(n11,n2)* -> . % 0.92/1.17 1969[56:MRR:1968.0,1968.1,1185.0,1169.0] || red(u,n12)+ red(u,n7) red(u,n5) red(u,n2)* -> . % 0.92/1.17 1864[56:MRR:1853.0,511.0] || red(u,n5)*+ red(u,n7) red(u,n12) red(v,n12) red(v,n7) red(v,n5)* red(v,u)* -> . % 0.92/1.17 1957[57:MRR:1007.7,1953.0] || green(u,n3)*+ green(u,n7) green(u,n11) green(v,n11) green(v,n7) green(v,n3)* green(v,u)* -> . % 0.92/1.17 1956[57:MRR:1773.6,1953.0] || green(n3,n3)*+ green(u,n3)* green(u,n11) green(v,n11) green(v,n3)* green(v,u)* -> . % 0.92/1.17 1922[56:MRR:1920.0,1735.0] || red(n3,n12)*+ red(u,n12) red(u,n10) red(u,n5) red(u,n3)* -> . % 0.92/1.17 1953[57:Spt:1948.0,1771.9,1923.0] || red(n3,n11)*+ -> . % 0.92/1.17 1955[57:MRR:317.1,1953.0] || -> green(n3,n11)*. % 0.92/1.17 1863[56:MRR:1859.0,1242.0] || red(u,n5)*+ red(u,n10) red(u,n12) red(v,n12) red(v,n10) red(v,n5)* red(v,u)* -> . % 0.92/1.17 1862[56:MRR:1860.0,1356.0] || red(u,n5)*+ red(u,n11) red(u,n12) red(v,n12) red(v,n11) red(v,n5)* red(v,u)* -> . % 0.92/1.17 1880[56:MRR:1783.9,1875.0] || green(n1,n2)*+ green(u,n1)* green(u,n2) green(u,n10) green(v,n10) green(v,n2) green(v,n1)* green(v,u)* -> red(n1,n10). % 0.92/1.17 1914[56:Res:374.0,1846.0] || red(n11,n7)+ red(n11,n6) red(n11,n5)* -> . % 0.92/1.17 1846[56:MRR:1698.0,1842.0] || red(u,n12)+ red(u,n7) red(u,n6) red(u,n5)* -> . % 0.92/1.17 1905[56:Res:374.0,1845.0] || red(n11,n11)+ red(n11,n6) red(n11,n5)* -> . % 0.92/1.17 1906[56:MRR:1898.0,368.0] || red(n10,n6)+ red(n10,n5)* -> . % 0.92/1.17 1879[56:MRR:1784.6,1875.0] || green(n2,n2)*+ green(u,n2)* green(u,n10) green(v,n10) green(v,n2)* green(v,u)* -> . % 0.92/1.17 1845[56:MRR:1574.0,1842.0] || red(u,n12)+ red(u,n11) red(u,n6) red(u,n5)* -> . % 0.92/1.17 1891[56:Res:374.0,1844.0] || red(n11,n11)+ red(n11,n10) red(n11,n5)* -> . % 0.92/1.17 1892[56:MRR:1884.0,368.0] || red(n10,n10)+ red(n10,n5)* -> . % 0.92/1.17 1893[56:MRR:1885.0,1885.1,440.0,366.0] || red(n9,n5)*+ -> . % 0.92/1.17 1878[56:MRR:324.9,1875.0] || green(u,n10)+ green(u,n2)* green(v,u)* green(v,n2)* green(v,n10) green(w,n10) green(w,n2)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1844[56:MRR:1358.0,1842.0] || red(u,n12)+ red(u,n11) red(u,n10) red(u,n5)* -> . % 0.92/1.17 1873[56:Res:374.0,1843.0] || red(n11,n10)+ red(n11,n7) red(n11,n5)* -> . % 0.92/1.17 1877[56:MRR:1047.7,1875.0] || green(u,n2)*+ green(u,n6) green(u,n10) green(v,n10) green(v,n6) green(v,n2)* green(v,u)* -> . % 0.92/1.17 1875[56:MRR:1871.1,1871.2,1185.0,713.0] || red(n2,n10)*+ -> . % 0.92/1.17 1876[56:MRR:322.1,1875.0] || -> green(n2,n10)*. % 0.92/1.17 1843[56:MRR:1245.0,1842.0] || red(u,n12)+ red(u,n10) red(u,n7) red(u,n5)* -> . % 0.92/1.17 1861[56:MRR:1851.0,1851.1,511.0,386.0] || red(n5,n1)*+ -> . % 0.92/1.17 1842[56:Spt:1537.9] || -> red(n5,n12)*. % 0.92/1.17 1837[52:Res:502.0,1513.0] || red(n6,n2)*+ red(u,n6) red(u,n2)* red(u,n8) red(v,n8) red(v,n2)* red(v,n6) red(v,u)* -> . % 0.92/1.17 1828[42:Res:413.0,1178.0] || red(n10,n1)*+ red(u,n10) red(u,n1)* red(u,n12) red(v,n12) red(v,n1)* red(v,n10) red(v,u)* -> . % 0.92/1.17 1829[42:Res:587.0,1178.0] || red(n9,n1)*+ red(u,n9) red(u,n1)* red(u,n12) red(v,n12) red(v,n1)* red(v,n9) red(v,u)* -> . % 0.92/1.17 1834[42:Res:374.0,1178.0] || red(n11,n1)*+ red(u,n11) red(u,n1)* red(u,n12) red(v,n12) red(v,n1)* red(v,n11) red(v,u)* -> . % 0.92/1.17 1513[52:Res:1506.0,20.0] || red(u,n8)+ red(u,n2)* red(v,u)* red(v,n2)* red(v,n8) red(w,n8) red(w,n2)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1178[42:Res:1177.0,20.0] || red(u,n12)+ red(u,n1)* red(v,u)* red(v,n1)* red(v,n12) red(w,n12) red(w,n1)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1811[50:Res:464.0,1450.0] || red(n8,n4)*+ red(u,n8) red(u,n4)* red(u,n10) red(v,n10) red(v,n4)* red(v,n8) red(v,u)* -> . % 0.92/1.17 1801[49:Res:413.0,1419.0] || red(n10,n6)*+ red(u,n10) red(u,n6)* red(u,n12) red(v,n12) red(v,n6)* red(v,n10) red(v,u)* -> . % 0.92/1.17 1484[51:Res:1478.0,20.0] || red(u,n9)+ red(u,n3)* red(v,u)* red(v,n3)* red(v,n9) red(w,n9) red(w,n3)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1792[41:Res:413.0,1170.0] || red(n10,n2)*+ red(u,n10) red(u,n2)* red(u,n12) red(v,n12) red(v,n2)* red(v,n10) red(v,u)* -> . % 0.92/1.17 1820[55:MRR:1819.0,980.0] || red(n1,n10)*+ red(u,n10) red(u,n4) red(u,n3) red(u,n1)* -> . % 0.92/1.17 1816[55:MRR:1815.0,394.0] || red(u,n3)*+ red(u,n4) red(u,n10) red(v,n10) red(v,n4) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1450[50:Res:1443.0,20.0] || red(u,n10)+ red(u,n4)* red(v,u)* red(v,n4)* red(v,n10) red(w,n10) red(w,n4)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1793[41:Res:587.0,1170.0] || red(n9,n2)*+ red(u,n9) red(u,n2)* red(u,n12) red(v,n12) red(v,n2)* red(v,n9) red(v,u)* -> . % 0.92/1.17 1795[49:Res:1416.0,1170.0] || red(n6,n2)*+ red(u,n6) red(u,n2)* red(u,n12) red(v,n12) red(v,n2)* red(v,n6) red(v,u)* -> . % 0.92/1.17 1808[49:MRR:1806.0,1375.0] || red(u,n1)*+ red(u,n6) red(u,n12) red(v,n12) red(v,n6) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1419[49:Res:1416.0,20.0] || red(u,n12)+ red(u,n6)* red(v,u)* red(v,n6)* red(v,n12) red(w,n12) red(w,n6)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1799[42:MRR:1797.0,1057.0] || red(u,n1)*+ red(u,n2) red(u,n12) red(v,n12) red(v,n2) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1170[41:Res:1169.0,20.0] || red(u,n12)+ red(u,n2)* red(v,u)* red(v,n2)* red(v,n12) red(w,n12) red(w,n2)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1790[55:Res:1018.0,1753.0] || red(n1,n8)*+ red(n1,n10) red(u,n10) red(u,n8) red(u,n3) red(u,n1)* -> . % 0.92/1.17 1753[55:MRR:1749.0,1151.0] || red(u,n3)*+ red(u,n8) red(u,n10) red(v,n10) red(v,n8) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1752[55:MRR:1751.0,1478.0] || red(u,n3)*+ red(u,n9) red(u,n10) red(v,n10) red(v,n9) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1786[52:MRR:1785.0,1018.0] || red(n1,n8)*+ red(u,n8) red(u,n3) red(u,n2) red(u,n1)* -> . % 0.92/1.17 1733[52:MRR:1732.0,398.0] || red(u,n2)*+ red(u,n3) red(u,n8) red(v,n8) red(v,n3) red(v,n2)* red(v,u)* -> . % 0.92/1.17 1741[55:MRR:1488.0,1735.0] || red(n3,n12)*+ red(u,n12) red(u,n10) red(u,n9) red(u,n3)* -> . % 0.92/1.17 1780[55:MRR:1775.0,362.0] || red(n8,n4)+ red(n8,n3)* -> . % 0.92/1.17 1742[55:MRR:1584.0,1735.0] || red(u,n10)+ red(u,n9) red(u,n4) red(u,n3)* -> . % 0.92/1.17 1767[55:MRR:1763.0,1763.1,485.0,378.0] || red(n7,n3)*+ -> . % 0.92/1.17 1739[55:MRR:1481.0,1735.0] || red(u,n10)+ red(u,n9) red(u,n8) red(u,n3)* -> . % 0.92/1.17 1737[55:MRR:1275.0,1735.0] || red(u,n10)+ red(u,n8) red(u,n5) red(u,n3)* -> . % 0.92/1.17 1735[55:Spt:1548.9] || -> red(n3,n10)*. % 0.92/1.17 1154[40:Res:1151.0,20.0] || red(u,n8)+ red(u,n3)* red(v,u)* red(v,n3)* red(v,n8) red(w,n8) red(w,n3)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1711[39:Res:368.0,1135.0] || red(n10,n6)*+ red(u,n10) red(u,n6)* red(u,n11) red(v,n11) red(v,n6)* red(v,n10) red(v,u)* -> . % 0.92/1.17 1716[47:MRR:1715.0,386.0] || red(u,n5)*+ red(u,n6) red(u,n11) red(v,n11) red(v,n6) red(v,n5)* red(v,u)* -> . % 0.92/1.17 1673[54:Res:1672.0,19.0] || green(u,n11)+ green(u,n4)* green(v,u)* green(v,n4)* green(v,n11) green(w,n11) green(w,n4)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1135[39:Res:1132.0,20.0] || red(u,n11)+ red(u,n6)* red(v,u)* red(v,n6)* red(v,n11) red(w,n11) red(w,n6)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1708[53:Res:332.0,1667.0] || green(n3,n4)*+ green(u,n3)* green(u,n4) green(u,n12) green(v,n12) green(v,n4) green(v,n3)* green(v,u)* -> red(n3,n12). % 0.92/1.17 1710[53:Obv:1707.5] || green(n4,n4)*+ green(u,n4)* green(u,n12) green(v,n12) green(v,n4)* green(v,u)* -> . % 0.92/1.17 1667[53:MRR:314.9,1663.0] || green(u,n12)+ green(u,n4)* green(v,u)* green(v,n4)* green(v,n12) green(w,n12) green(w,n4)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1679[54:MRR:1544.9,1674.0] || green(n1,n4)*+ green(u,n1)* green(u,n4) green(u,n11) green(v,n11) green(v,n4) green(v,n1)* green(v,u)* -> red(n1,n11). % 0.92/1.17 1627[38:Res:374.0,1099.0] || red(n11,n7)*+ red(u,n11) red(u,n7)* red(u,n12) red(v,n12) red(v,n7)* red(v,n11) red(v,u)* -> . % 0.92/1.17 1678[54:MRR:1540.8,1674.0] || green(n7,n4)*+ green(u,n7) green(u,n4)* green(u,n11) green(v,n11) green(v,n4)* green(v,n7) green(v,u)* -> . % 0.92/1.17 1705[49:Res:374.0,1697.0] || red(n11,n7)+ red(n11,n6) red(n11,n1)* -> . % 0.92/1.17 1700[49:Res:587.0,1697.0] || red(n9,n7)+ red(n9,n6) red(n9,n1)* -> . % 0.92/1.17 1699[49:Res:413.0,1697.0] || red(n10,n7)+ red(n10,n6) red(n10,n1)* -> . % 0.92/1.17 1675[54:Res:1672.0,854.0] || green(n4,n7)*+ green(u,n4)* green(u,n7) green(u,n11) green(v,n11) green(v,n7) green(v,n4)* green(v,u)* -> . % 0.92/1.17 1697[49:MRR:1696.0,1696.1,1215.0,1177.0] || red(u,n12)+ red(u,n7) red(u,n6) red(u,n1)* -> . % 0.92/1.17 1630[49:MRR:1624.0,382.0] || red(u,n6)*+ red(u,n7) red(u,n12) red(v,n12) red(v,n7) red(v,n6)* red(v,u)* -> . % 0.92/1.17 1691[44:Res:374.0,1684.0] || red(n11,n7)+ red(n11,n2) red(n11,n1)* -> . % 0.92/1.17 1686[44:Res:587.0,1684.0] || red(n9,n7)+ red(n9,n2) red(n9,n1)* -> . % 0.92/1.17 1666[53:MRR:967.7,1663.0] || green(u,n4)*+ green(u,n8) green(u,n12) green(v,n12) green(v,n8) green(v,n4)* green(v,u)* -> . % 0.92/1.17 1685[44:Res:413.0,1684.0] || red(n10,n7)+ red(n10,n2) red(n10,n1)* -> . % 0.92/1.17 1692[49:MRR:1688.0,382.0] || red(n6,n2)+ red(n6,n1)* -> . % 0.92/1.17 1684[44:MRR:1683.0,1683.1,1215.0,1177.0] || red(u,n12)+ red(u,n7) red(u,n2) red(u,n1)* -> . % 0.92/1.17 1629[43:MRR:1625.0,1185.0] || red(u,n2)*+ red(u,n7) red(u,n12) red(v,n12) red(v,n7) red(v,n2)* red(v,u)* -> . % 0.92/1.17 1676[54:MRR:1545.6,1674.0] || green(n4,n4)*+ green(u,n4)* green(u,n11) green(v,n11) green(v,n4)* green(v,u)* -> . % 0.92/1.17 1674[54:Res:1672.0,18.0] || red(n4,n11)*+ -> . % 0.92/1.17 1672[54:Spt:292.0] || -> green(n4,n11)*. % 0.92/1.17 1663[53:Spt:1659.0,1536.8,1632.0] || red(n4,n12)*+ -> . % 0.92/1.17 1665[53:MRR:312.1,1663.0] || -> green(n4,n12)*. % 0.92/1.17 1628[44:MRR:1626.0,1215.0] || red(u,n1)*+ red(u,n7) red(u,n12) red(v,n12) red(v,n7) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1099[38:Res:1097.0,20.0] || red(u,n12)+ red(u,n7)* red(v,u)* red(v,n7)* red(v,n12) red(w,n12) red(w,n7)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1618[49:Res:302.0,1437.0] || green(n2,n1)*+ green(u,n2) green(u,n1)* green(u,n9) green(v,n9) green(v,n1)* green(v,n2) green(v,u)* -> red(n2,n9). % 0.92/1.17 1620[49:Obv:1619.5] || green(n1,n1)*+ green(u,n1)* green(u,n9) green(v,n9) green(v,n1)* green(v,u)* -> . % 0.92/1.17 1437[49:MRR:329.9,1434.0] || green(u,n9)+ green(u,n1)* green(v,u)* green(v,n1)* green(v,n9) green(w,n9) green(w,n1)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1060[37:Res:1057.0,20.0] || red(u,n2)+ red(u,n1)* red(v,u)* red(v,n1)* red(v,n2) red(w,n2) red(w,n1)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1605[46:Res:362.0,1304.0] || red(n8,n4)*+ red(u,n8) red(u,n4)* red(u,n9) red(v,n9) red(v,n4)* red(v,n8) red(v,u)* -> . % 0.92/1.17 1614[51:MRR:1612.0,532.0] || red(n2,n9)*+ red(u,n9) red(u,n4) red(u,n3) red(u,n2)* -> . % 0.92/1.17 1610[51:MRR:1609.0,394.0] || red(u,n3)*+ red(u,n4) red(u,n9) red(v,n9) red(v,n4) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1304[46:Res:1299.0,20.0] || red(u,n9)+ red(u,n4)* red(v,u)* red(v,n4)* red(v,n9) red(w,n9) red(w,n4)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1020[35:Res:1018.0,20.0] || red(u,n3)+ red(u,n1)* red(v,u)* red(v,n1)* red(v,n3) red(w,n3) red(w,n1)* red(w,u)* red(w,v)* -> . % 0.92/1.17 981[33:Res:980.0,20.0] || red(u,n4)+ red(u,n1)* red(v,u)* red(v,n1)* red(v,n4) red(w,n4) red(w,n1)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1555[32:Res:966.0,309.0] || green(n4,n1)*+ green(u,n4) green(u,n1)* green(u,n8) green(v,n8) green(v,n1)* green(v,n4) green(v,u)* -> red(n1,n8). % 0.92/1.17 1523[52:MRR:1514.0,713.0] || red(u,n2)*+ red(u,n5) red(u,n8) red(v,n8) red(v,n5) red(v,n2)* red(v,u)* -> . % 0.92/1.17 1551[31:Res:929.0,304.0] || green(n5,n2)*+ green(u,n5) green(u,n2)* green(u,n9) green(v,n9) green(v,n2)* green(v,n5) green(v,u)* -> red(n2,n9). % 0.92/1.17 1596[52:MRR:1595.0,1215.0] || red(n1,n8)*+ red(u,n8) red(u,n7) red(u,n2) red(u,n1)* -> . % 0.92/1.17 1522[52:MRR:1521.0,1185.0] || red(u,n2)*+ red(u,n7) red(u,n8) red(v,n8) red(v,n7) red(v,n2)* red(v,u)* -> . % 0.92/1.17 1494[51:MRR:1486.0,700.0] || red(u,n3)*+ red(u,n6) red(u,n9) red(v,n9) red(v,n6) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1592[52:MRR:1590.0,1506.0] || red(n2,n9)*+ red(u,n9) red(u,n8) red(u,n3) red(u,n2)* -> . % 0.92/1.17 1553[49:Res:1435.0,304.0] || green(n1,n2)*+ green(u,n1)* green(u,n2) green(u,n9) green(v,n9) green(v,n2) green(v,n1)* green(v,u)* -> red(n2,n9). % 0.92/1.17 1493[51:MRR:1492.0,1151.0] || red(u,n3)*+ red(u,n8) red(u,n9) red(v,n9) red(v,n8) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1588[50:MRR:1587.0,1215.0] || red(n1,n10)*+ red(u,n10) red(u,n7) red(u,n4) red(u,n1)* -> . % 0.92/1.17 1458[50:MRR:1452.0,687.0] || red(u,n4)*+ red(u,n7) red(u,n10) red(v,n10) red(v,n7) red(v,n4)* red(v,u)* -> . % 0.92/1.17 1457[50:MRR:1456.0,1299.0] || red(u,n4)*+ red(u,n9) red(u,n10) red(v,n10) red(v,n9) red(v,n4)* red(v,u)* -> . % 0.92/1.17 1579[51:MRR:1577.0,1478.0] || red(n3,n12)*+ red(u,n12) red(u,n9) red(u,n6) red(u,n3)* -> . % 0.92/1.17 1426[49:MRR:1421.0,658.0] || red(u,n6)*+ red(u,n9) red(u,n12) red(v,n12) red(v,n9) red(v,n6)* red(v,u)* -> . % 0.92/1.17 1573[49:MRR:1572.1,1177.0] || red(n1,n11)*+ red(u,n12) red(u,n11) red(u,n6) red(u,n1)* -> . % 0.92/1.17 1425[49:MRR:1424.0,1132.0] || red(u,n6)*+ red(u,n11) red(u,n12) red(v,n12) red(v,n11) red(v,n6)* red(v,u)* -> . % 0.92/1.17 1561[48:Res:1375.0,1410.0] || red(n1,n8)*+ red(n1,n11) red(u,n11) red(u,n8) red(u,n6) red(u,n1)* -> . % 0.92/1.17 1436[49:MRR:1234.7,1434.0] || green(u,n1)*+ green(u,n5) green(u,n9) green(v,n9) green(v,n5) green(v,n1)* green(v,u)* -> . % 0.92/1.17 1563[47:MRR:1558.0,1558.1,673.0,1356.0] || red(u,n11)+ red(u,n8) red(u,n6) red(u,n5)* -> . % 0.92/1.17 1410[39:MRR:1407.0,502.0] || red(u,n6)*+ red(u,n8) red(u,n11) red(v,n11) red(v,n8) red(v,n6)* red(v,u)* -> . % 0.92/1.17 1557[0:Obv:1556.8] || green(n1,n1)*+ green(u,n1)* green(u,n8) green(v,n8) green(v,n1)* green(v,u)* -> red(n1,n8). % 0.92/1.17 1554[0:Obv:1552.8] || green(n2,n2)*+ green(u,n2)* green(u,n9) green(v,n9) green(v,n2)* green(v,u)* -> red(n2,n9). % 0.92/1.17 309[0:Res:307.0,19.0] || green(u,n8)+ green(u,n1)* green(v,u)* green(v,n1)* green(v,n8) green(w,n8) green(w,n1)* green(w,u)* green(w,v)* -> red(n1,n8). % 0.92/1.17 304[0:Res:302.0,19.0] || green(u,n9)+ green(u,n2)* green(v,u)* green(v,n2)* green(v,n9) green(w,n9) green(w,n2)* green(w,u)* green(w,v)* -> red(n2,n9). % 0.92/1.17 1508[52:MRR:1196.0,1506.0] || red(n2,n9)*+ red(u,n9) red(u,n8) red(u,n7) red(u,n2)* -> . % 0.92/1.17 1511[52:MRR:1287.0,1506.0] || red(u,n8)+ red(u,n5) red(u,n3) red(u,n2)* -> . % 0.92/1.17 1529[52:MRR:1525.0,382.0] || red(n6,n5)+ red(n6,n2)* -> . % 0.92/1.17 1507[52:MRR:1186.0,1506.0] || red(u,n8)+ red(u,n7) red(u,n5) red(u,n2)* -> . % 0.92/1.17 1506[52:Spt:1354.9] || -> red(n2,n8)*. % 0.92/1.17 1483[51:MRR:1351.0,1478.0] || red(u,n9)+ red(u,n6) red(u,n4) red(u,n3)* -> . % 0.92/1.17 1480[51:MRR:1152.0,1478.0] || red(u,n9)+ red(u,n8) red(u,n6) red(u,n3)* -> . % 0.92/1.17 1478[51:Spt:1345.9] || -> red(n3,n9)*. % 0.92/1.17 1445[50:MRR:1284.0,1443.0] || red(u,n10)+ red(u,n7) red(u,n5) red(u,n4)* -> . % 0.92/1.17 1472[50:MRR:1468.0,362.0] || red(n8,n7)+ red(n8,n4)* -> . % 0.92/1.17 1446[50:MRR:1300.0,1443.0] || red(u,n10)+ red(u,n9) red(u,n7) red(u,n4)* -> . % 0.92/1.17 1465[49:Res:374.0,1418.0] || red(n11,n11)+ red(n11,n9) red(n11,n6)* -> . % 0.92/1.17 1466[49:MRR:1459.0,368.0] || red(n10,n9)+ red(n10,n6)* -> . % 0.92/1.17 1418[49:MRR:1133.0,1416.0] || red(u,n12)+ red(u,n11) red(u,n9) red(u,n6)* -> . % 0.92/1.17 1433[49:Res:374.0,1417.0] || red(n11,n9)+ red(n11,n7) red(n11,n6)* -> . % 0.92/1.17 1443[50:Spt:1334.9] || -> red(n4,n10)*. % 0.92/1.17 1434[49:MRR:1432.1,1432.2,1215.0,1375.0] || red(n1,n9)*+ -> . % 0.92/1.17 1435[49:MRR:327.1,1434.0] || -> green(n1,n9)*. % 0.92/1.17 1417[49:MRR:1127.0,1416.0] || red(u,n12)+ red(u,n9) red(u,n7) red(u,n6)* -> . % 0.92/1.17 1416[49:Spt:1319.9] || -> red(n6,n12)*. % 0.92/1.17 1409[47:MRR:1408.0,673.0] || red(u,n5)*+ red(u,n8) red(u,n11) red(v,n11) red(v,n8) red(v,n5)* red(v,u)* -> . % 0.92/1.17 630[21:Res:626.0,20.0] || red(u,n11)+ red(u,n8)* red(v,u)* red(v,n8)* red(v,n11) red(w,n11) red(w,n8)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1393[48:MRR:1382.0,1018.0] || red(u,n1)*+ red(u,n3) red(u,n6) red(v,n6) red(v,n3) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1392[48:MRR:1387.0,980.0] || red(u,n1)*+ red(u,n4) red(u,n6) red(v,n6) red(v,n4) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1379[48:MRR:1229.0,1375.0] || red(u,n1)*+ red(u,n6) red(u,n7) red(v,n7) red(v,n6) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1390[48:MRR:1388.0,1215.0] || red(n1,n8)*+ red(u,n8) red(u,n7) red(u,n6) red(u,n1)* -> . % 0.92/1.17 1377[48:MRR:1167.0,1375.0] || red(n1,n8)*+ red(u,n8) red(u,n6) red(u,n3) red(u,n1)* -> . % 0.92/1.17 1378[48:MRR:1216.0,1375.0] || red(u,n7)+ red(u,n6) red(u,n4) red(u,n1)* -> . % 0.92/1.17 1376[48:MRR:1026.0,1375.0] || red(u,n6)+ red(u,n4) red(u,n3) red(u,n1)* -> . % 0.92/1.17 970[32:MRR:768.9,964.0] || green(n1,n4)*+ green(u,n1)* green(u,n4) green(u,n8) green(v,n8) green(v,n4) green(v,n1)* green(v,u)* -> red(n1,n8). % 0.92/1.17 1375[48:Spt:1374.7] || -> red(n1,n6)*. % 0.92/1.17 892[30:MRR:748.9,885.0] || green(n1,n6)*+ green(u,n1)* green(u,n6) green(u,n10) green(v,n10) green(v,n6) green(v,n1)* green(v,u)* -> red(n1,n10). % 0.92/1.17 932[31:MRR:758.9,927.0] || green(n2,n5)*+ green(u,n2)* green(u,n5) green(u,n9) green(v,n9) green(v,n5) green(v,n2)* green(v,u)* -> red(n2,n9). % 0.92/1.17 1364[47:MRR:1363.0,1242.0] || red(u,n5)*+ red(u,n10) red(u,n11) red(v,n11) red(v,n10) red(v,n5)* red(v,u)* -> . % 0.92/1.17 1357[47:MRR:1243.0,1356.0] || red(u,n11)+ red(u,n10) red(u,n8) red(u,n5)* -> . % 0.92/1.17 1356[47:Spt:1330.8] || -> red(n5,n11)*. % 0.92/1.17 1313[46:MRR:1305.0,518.0] || red(u,n4)*+ red(u,n6) red(u,n9) red(v,n9) red(v,n6) red(v,n4)* red(v,u)* -> . % 0.92/1.17 1342[46:MRR:1339.0,1185.0] || red(n2,n9)*+ red(u,n9) red(u,n7) red(u,n4) red(u,n2)* -> . % 0.92/1.17 1312[46:MRR:1309.0,687.0] || red(u,n4)*+ red(u,n7) red(u,n9) red(v,n9) red(v,n7) red(v,n4)* red(v,u)* -> . % 0.92/1.17 1301[46:MRR:791.0,1299.0] || red(u,n9)+ red(u,n7) red(u,n6) red(u,n4)* -> . % 0.92/1.17 1299[46:Spt:1112.9] || -> red(n4,n9)*. % 0.92/1.17 1293[44:MRR:1292.0,1292.1,980.0,1215.0] || red(u,n7)+ red(u,n4) red(u,n2) red(u,n1)* -> . % 0.92/1.17 1270[43:MRR:1267.0,532.0] || red(u,n2)*+ red(u,n4) red(u,n7) red(v,n7) red(v,n4) red(v,n2)* red(v,u)* -> . % 0.92/1.17 1269[44:MRR:1268.0,980.0] || red(u,n1)*+ red(u,n4) red(u,n7) red(v,n7) red(v,n4) red(v,n1)* red(v,u)* -> . % 0.92/1.17 716[27:Res:713.0,20.0] || red(u,n5)+ red(u,n2)* red(v,u)* red(v,n2)* red(v,n5) red(w,n5) red(w,n2)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1258[40:MRR:1257.0,525.0] || red(u,n3)*+ red(u,n5) red(u,n8) red(v,n8) red(v,n5) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1253[45:MRR:1247.0,511.0] || red(u,n5)*+ red(u,n7) red(u,n10) red(v,n10) red(v,n7) red(v,n5)* red(v,u)* -> . % 0.92/1.17 703[26:Res:700.0,20.0] || red(u,n6)+ red(u,n3)* red(v,u)* red(v,n3)* red(v,n6) red(w,n6) red(w,n3)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1252[45:MRR:1249.0,673.0] || red(u,n5)*+ red(u,n8) red(u,n10) red(v,n10) red(v,n8) red(v,n5)* red(v,u)* -> . % 0.92/1.17 690[25:Res:687.0,20.0] || red(u,n7)+ red(u,n4)* red(v,u)* red(v,n4)* red(v,n7) red(w,n7) red(w,n4)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1244[45:MRR:773.0,1242.0] || red(u,n10)+ red(u,n8) red(u,n7) red(u,n5)* -> . % 0.92/1.17 676[24:Res:673.0,20.0] || red(u,n8)+ red(u,n5)* red(v,u)* red(v,n5)* red(v,n8) red(w,n8) red(w,n5)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1242[45:Spt:1235.8] || -> red(n5,n10)*. % 0.92/1.17 1224[44:Res:1215.0,653.0] || red(n1,n8)*+ red(n1,n10) red(u,n10) red(u,n8) red(u,n7) red(u,n1)* -> . % 0.92/1.17 1233[44:MRR:787.6,1230.0] || green(n1,n1)*+ green(u,n1)* green(u,n5) green(v,n5) green(v,n1)* green(v,u)* -> . % 0.92/1.17 1236[44:MRR:1223.1,1177.0] || red(n1,n10)*+ red(u,n12) red(u,n10) red(u,n7) red(u,n1)* -> . % 0.92/1.17 1232[44:MRR:191.9,1230.0] || green(u,n5)+ green(u,n1)* green(v,u)* green(v,n1)* green(v,n5) green(w,n5) green(w,n1)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1230[44:MRR:1221.1,1221.2,980.0,1057.0] || red(n1,n5)*+ -> . % 0.92/1.17 1231[44:MRR:189.1,1230.0] || -> green(n1,n5)*. % 0.92/1.17 1215[44:Spt:1210.7] || -> red(n1,n7)*. % 0.92/1.17 661[23:Res:658.0,20.0] || red(u,n9)+ red(u,n6)* red(v,u)* red(v,n6)* red(v,n9) red(w,n9) red(w,n6)* red(w,u)* red(w,v)* -> . % 0.92/1.17 853[29:MRR:741.9,845.0] || green(n1,n7)*+ green(u,n1)* green(u,n7) green(u,n11) green(v,n11) green(v,n7) green(v,n1)* green(v,u)* -> red(n1,n11). % 0.92/1.17 1200[43:MRR:1195.0,713.0] || red(u,n2)*+ red(u,n5) red(u,n7) red(v,n7) red(v,n5) red(v,n2)* red(v,u)* -> . % 0.92/1.17 648[22:Res:643.0,20.0] || red(u,n10)+ red(u,n7)* red(v,u)* red(v,n7)* red(v,n10) red(w,n10) red(w,n7)* red(w,u)* red(w,v)* -> . % 0.92/1.17 1199[43:MRR:1190.1,1169.0] || red(n2,n9)*+ red(u,n12) red(u,n9) red(u,n7) red(u,n2)* -> . % 0.92/1.17 1187[43:MRR:908.0,1185.0] || red(u,n7)+ red(u,n5) red(u,n4) red(u,n2)* -> . % 0.92/1.17 1185[43:Spt:1184.7] || -> red(n2,n7)*. % 0.92/1.17 1182[42:Res:1177.0,414.0] || red(n1,n10)*+ red(u,n1)* red(u,n10) red(u,n12) red(v,n12) red(v,n10) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1183[42:Res:1177.0,375.0] || red(n1,n11)*+ red(u,n1)* red(u,n11) red(u,n12) red(v,n12) red(v,n11) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1177[42:Spt:1176.8] || -> red(n1,n12)*. % 0.92/1.17 1172[41:Res:1169.0,589.0] || red(n2,n9)*+ red(u,n2)* red(u,n9) red(u,n12) red(v,n12) red(v,n9) red(v,n2)* red(v,u)* -> . % 0.92/1.17 1169[41:Spt:1168.8] || -> red(n2,n12)*. % 0.92/1.17 1161[40:MRR:1158.0,700.0] || red(u,n3)*+ red(u,n6) red(u,n8) red(v,n8) red(v,n6) red(v,n3)* red(v,u)* -> . % 0.92/1.17 1153[40:MRR:868.0,1151.0] || red(u,n8)+ red(u,n6) red(u,n5) red(u,n3)* -> . % 0.92/1.17 1151[40:Spt:1150.7] || -> red(n3,n8)*. % 0.92/1.17 813[28:MRR:731.9,806.0] || green(n3,n8)*+ green(u,n3)* green(u,n8) green(u,n12) green(v,n12) green(v,n8) green(v,n3)* green(v,u)* -> red(n3,n12). % 0.92/1.17 1139[39:MRR:1137.0,658.0] || red(u,n6)*+ red(u,n9) red(u,n11) red(v,n11) red(v,n9) red(v,n6)* red(v,u)* -> . % 0.92/1.17 1134[39:MRR:753.0,1132.0] || red(u,n11)+ red(u,n9) red(u,n8) red(u,n6)* -> . % 0.92/1.17 1132[39:Spt:1088.8] || -> red(n6,n11)*. % 0.92/1.17 1105[38:MRR:1100.0,485.0] || red(u,n7)*+ red(u,n9) red(u,n12) red(v,n12) red(v,n9) red(v,n7)* red(v,u)* -> . % 0.92/1.17 1104[38:MRR:1102.0,643.0] || red(u,n7)*+ red(u,n10) red(u,n12) red(v,n12) red(v,n10) red(v,n7)* red(v,u)* -> . % 0.92/1.17 1109[38:Res:374.0,1098.0] || red(n11,n10)+ red(n11,n9) red(n11,n7)* -> . % 0.92/1.17 1098[38:MRR:646.0,1097.0] || red(u,n12)+ red(u,n10) red(u,n9) red(u,n7)* -> . % 0.92/1.17 1097[38:Spt:1075.8] || -> red(n7,n12)*. % 0.92/1.17 1059[37:MRR:1024.0,1057.0] || red(u,n1)*+ red(u,n2) red(u,n3) red(v,n3) red(v,n2) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1058[37:MRR:984.0,1057.0] || red(u,n1)*+ red(u,n2) red(u,n4) red(v,n4) red(v,n2) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1080[37:MRR:1079.0,1079.1,1018.0,1057.0] || red(n1,n1)*+ -> . % 0.92/1.17 1064[37:MRR:1063.0,1063.1,1018.0,980.0] || red(u,n4)+ red(u,n3) red(u,n2) red(u,n1)* -> . % 0.92/1.17 1057[37:Spt:1056.6] || -> red(n1,n2)*. % 0.92/1.17 1019[35:MRR:986.0,1018.0] || red(u,n1)*+ red(u,n3) red(u,n4) red(v,n4) red(v,n3) red(v,n1)* red(v,u)* -> . % 0.92/1.17 1048[36:MRR:781.6,1044.0] || green(n2,n2)*+ green(u,n2)* green(u,n6) green(v,n6) green(v,n2)* green(v,u)* -> . % 0.92/1.17 1049[36:MRR:187.9,1044.0] || green(u,n6)+ green(u,n2)* green(v,u)* green(v,n2)* green(v,n6) green(w,n6) green(w,n2)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1044[36:Spt:1041.0,780.9,1027.0] || red(n2,n6)*+ -> . % 0.92/1.17 1046[36:MRR:180.1,1044.0] || -> green(n2,n6)*. % 0.92/1.17 1018[35:Spt:1017.6] || -> red(n1,n3)*. % 0.92/1.17 1008[34:MRR:778.6,1004.0] || green(n3,n3)*+ green(u,n3)* green(u,n7) green(v,n7) green(v,n3)* green(v,u)* -> . % 0.92/1.17 1010[34:MRR:178.9,1004.0] || green(u,n7)+ green(u,n3)* green(v,u)* green(v,n3)* green(v,n7) green(w,n7) green(w,n3)* green(w,u)* green(w,v)* -> . % 0.92/1.17 1004[34:Spt:1001.0,776.9,987.0] || red(n3,n7)*+ -> . % 0.92/1.17 1006[34:MRR:176.1,1004.0] || -> green(n3,n7)*. % 0.92/1.17 980[33:Spt:979.6] || -> red(n1,n4)*. % 0.92/1.17 721[27:MRR:717.0,398.0] || red(u,n2)*+ red(u,n3) red(u,n5) red(v,n5) red(v,n3) red(v,n2)* red(v,u)* -> . % 0.92/1.17 971[32:MRR:174.9,964.0] || green(u,n8)+ green(u,n4)* green(v,u)* green(v,n4)* green(v,n8) green(w,n8) green(w,n4)* green(w,u)* green(w,v)* -> . % 0.92/1.17 720[27:MRR:719.0,532.0] || red(u,n2)*+ red(u,n4) red(u,n5) red(v,n5) red(v,n4) red(v,n2)* red(v,u)* -> . % 0.92/1.17 968[32:MRR:769.6,964.0] || green(n4,n4)*+ green(u,n4)* green(u,n8) green(v,n8) green(v,n4)* green(v,u)* -> . % 0.92/1.17 964[32:Spt:961.0,766.9,947.0] || red(n4,n8)*+ -> . % 0.92/1.17 966[32:MRR:167.1,964.0] || -> green(n4,n8)*. % 0.92/1.17 708[26:MRR:704.0,394.0] || red(u,n3)*+ red(u,n4) red(u,n6) red(v,n6) red(v,n4) red(v,n3)* red(v,u)* -> . % 0.92/1.17 707[26:MRR:706.0,525.0] || red(u,n3)*+ red(u,n5) red(u,n6) red(v,n6) red(v,n5) red(v,n3)* red(v,u)* -> . % 0.92/1.17 934[31:MRR:164.9,927.0] || green(u,n9)+ green(u,n5)* green(v,u)* green(v,n5)* green(v,n9) green(w,n9) green(w,n5)* green(w,u)* green(w,v)* -> . % 0.92/1.17 930[31:MRR:760.6,927.0] || green(n5,n5)*+ green(u,n5)* green(u,n9) green(v,n9) green(v,n5)* green(v,u)* -> . % 0.92/1.17 927[31:Spt:924.0,756.9,910.0] || red(n5,n9)*+ -> . % 0.92/1.17 929[31:MRR:162.1,927.0] || -> green(n5,n9)*. % 0.92/1.17 695[25:MRR:691.0,388.0] || red(u,n4)*+ red(u,n5) red(u,n7) red(v,n7) red(v,n5) red(v,n4)* red(v,u)* -> . % 0.92/1.17 893[30:MRR:159.9,885.0] || green(u,n10)+ green(u,n6)* green(v,u)* green(v,n6)* green(v,n10) green(w,n10) green(w,n6)* green(w,u)* green(w,v)* -> . % 0.92/1.17 694[25:MRR:693.0,518.0] || red(u,n4)*+ red(u,n6) red(u,n7) red(v,n7) red(v,n6) red(v,n4)* red(v,u)* -> . % 0.92/1.17 888[30:MRR:749.6,885.0] || green(n6,n6)*+ green(u,n6)* green(u,n10) green(v,n10) green(v,n6)* green(v,u)* -> . % 0.92/1.17 885[30:Spt:882.0,744.9,870.0] || red(n6,n10)*+ -> . % 0.92/1.17 887[30:MRR:153.1,885.0] || -> green(n6,n10)*. % 0.92/1.17 682[24:MRR:678.0,386.0] || red(u,n5)*+ red(u,n6) red(u,n8) red(v,n8) red(v,n6) red(v,n5)* red(v,u)* -> . % 0.92/1.17 854[29:MRR:151.9,845.0] || green(u,n11)+ green(u,n7)* green(v,u)* green(v,n7)* green(v,n11) green(w,n11) green(w,n7)* green(w,u)* green(w,v)* -> . % 0.92/1.17 848[29:MRR:742.6,845.0] || green(n7,n7)*+ green(u,n7)* green(u,n11) green(v,n11) green(v,n7)* green(v,u)* -> . % 0.92/1.17 845[29:Spt:842.0,736.9,832.0] || red(n7,n11)*+ -> . % 0.92/1.17 847[29:MRR:149.1,845.0] || -> green(n7,n11)*. % 0.92/1.17 681[24:MRR:680.0,511.0] || red(u,n5)*+ red(u,n7) red(u,n8) red(v,n8) red(v,n7) red(v,n5)* red(v,u)* -> . % 0.92/1.17 809[28:MRR:734.6,806.0] || green(n8,n8)*+ green(u,n8)* green(u,n12) green(v,n12) green(v,n8)* green(v,u)* -> . % 0.92/1.17 816[28:MRR:147.9,806.0] || green(u,n12)+ green(u,n8)* green(v,u)* green(v,n8)* green(v,n12) green(w,n12) green(w,n8)* green(w,u)* green(w,v)* -> . % 0.92/1.17 806[28:Spt:802.0,727.9,793.0] || red(n8,n12)*+ -> . % 0.92/1.17 808[28:MRR:141.1,806.0] || -> green(n8,n12)*. % 0.92/1.17 668[23:MRR:664.0,382.0] || red(u,n6)*+ red(u,n7) red(u,n9) red(v,n9) red(v,n7) red(v,n6)* red(v,u)* -> . % 0.92/1.17 667[23:MRR:666.0,502.0] || red(u,n6)*+ red(u,n8) red(u,n9) red(v,n9) red(v,n8) red(v,n6)* red(v,u)* -> . % 0.92/1.17 653[22:MRR:649.0,378.0] || red(u,n7)*+ red(u,n8) red(u,n10) red(v,n10) red(v,n8) red(v,n7)* red(v,u)* -> . % 0.92/1.17 652[22:MRR:651.0,485.0] || red(u,n7)*+ red(u,n9) red(u,n10) red(v,n10) red(v,n9) red(v,n7)* red(v,u)* -> . % 0.92/1.17 634[21:MRR:631.0,362.0] || red(u,n8)*+ red(u,n9) red(u,n11) red(v,n11) red(v,n9) red(v,n8)* red(v,u)* -> . % 0.92/1.17 725[27:MRR:724.0,724.1,532.0,398.0] || red(n2,n2)*+ -> . % 0.92/1.17 714[27:MRR:533.0,713.0] || red(u,n5)+ red(u,n4) red(u,n3) red(u,n2)* -> . % 0.92/1.17 713[27:Spt:624.9] || -> red(n2,n5)*. % 0.92/1.17 712[26:MRR:711.0,711.1,525.0,394.0] || red(n3,n3)*+ -> . % 0.92/1.17 701[26:MRR:526.0,700.0] || red(u,n6)+ red(u,n5) red(u,n4) red(u,n3)* -> . % 0.92/1.17 700[26:Spt:616.9] || -> red(n3,n6)*. % 0.92/1.17 699[25:MRR:698.0,698.1,518.0,388.0] || red(n4,n4)*+ -> . % 0.92/1.17 688[25:MRR:519.0,687.0] || red(u,n7)+ red(u,n6) red(u,n5) red(u,n4)* -> . % 0.92/1.17 687[25:Spt:608.9] || -> red(n4,n7)*. % 0.92/1.17 686[24:MRR:685.0,685.1,511.0,386.0] || red(n5,n5)*+ -> . % 0.92/1.17 674[24:MRR:512.0,673.0] || red(u,n8)+ red(u,n7) red(u,n6) red(u,n5)* -> . % 0.92/1.17 673[24:Spt:600.9] || -> red(n5,n8)*. % 0.92/1.17 672[23:MRR:671.0,671.1,502.0,382.0] || red(n6,n6)*+ -> . % 0.92/1.17 659[23:MRR:503.0,658.0] || red(u,n9)+ red(u,n8) red(u,n7) red(u,n6)* -> . % 0.92/1.17 658[23:Spt:581.9] || -> red(n6,n9)*. % 0.92/1.17 657[22:MRR:656.0,656.1,485.0,378.0] || red(n7,n7)*+ -> . % 0.92/1.17 644[22:MRR:486.0,643.0] || red(u,n10)+ red(u,n9) red(u,n8) red(u,n7)* -> . % 0.92/1.17 643[22:Spt:570.9] || -> red(n7,n10)*. % 0.92/1.17 633[21:MRR:632.0,464.0] || red(u,n8)*+ red(u,n10) red(u,n11) red(v,n11) red(v,n10) red(v,n8)* red(v,u)* -> . % 0.92/1.17 638[21:MRR:637.0,637.1,464.0,362.0] || red(n8,n8)*+ -> . % 0.92/1.17 627[21:MRR:465.0,626.0] || red(u,n11)+ red(u,n10) red(u,n9) red(u,n8)* -> . % 0.92/1.17 626[21:Spt:561.9] || -> red(n8,n11)*. % 0.92/1.17 589[20:Res:587.0,20.0] || red(u,n12)+ red(u,n9)* red(v,u)* red(v,n9)* red(v,n12) red(w,n12) red(w,n9)* red(w,u)* red(w,v)* -> . % 0.92/1.17 593[20:MRR:590.0,366.0] || red(u,n9)*+ red(u,n10) red(u,n12) red(v,n12) red(v,n10) red(v,n9)* red(v,u)* -> . % 0.92/1.17 592[20:MRR:591.0,440.0] || red(u,n9)*+ red(u,n11) red(u,n12) red(v,n12) red(v,n11) red(v,n9)* red(v,u)* -> . % 0.92/1.17 596[20:Res:374.0,588.0] || red(n11,n11)+ red(n11,n10) red(n11,n9)* -> . % 0.92/1.17 597[20:MRR:594.0,368.0] || red(n10,n10)+ red(n10,n9)* -> . % 0.92/1.17 598[20:MRR:595.0,595.1,440.0,366.0] || red(n9,n9)*+ -> . % 0.92/1.17 588[20:MRR:441.0,587.0] || red(u,n12)+ red(u,n11) red(u,n10) red(u,n9)* -> . % 0.92/1.17 587[20:Spt:549.9] || -> red(n9,n12)*. % 0.92/1.17 534[19:Res:532.0,20.0] || red(u,n4)+ red(u,n2)* red(v,u)* red(v,n2)* red(v,n4) red(w,n4) red(w,n2)* red(w,u)* red(w,v)* -> . % 0.92/1.17 527[18:Res:525.0,20.0] || red(u,n5)+ red(u,n3)* red(v,u)* red(v,n3)* red(v,n5) red(w,n5) red(w,n3)* red(w,u)* red(w,v)* -> . % 0.92/1.17 520[17:Res:518.0,20.0] || red(u,n6)+ red(u,n4)* red(v,u)* red(v,n4)* red(v,n6) red(w,n6) red(w,n4)* red(w,u)* red(w,v)* -> . % 0.92/1.17 513[16:Res:511.0,20.0] || red(u,n7)+ red(u,n5)* red(v,u)* red(v,n5)* red(v,n7) red(w,n7) red(w,n5)* red(w,u)* red(w,v)* -> . % 0.92/1.17 504[15:Res:502.0,20.0] || red(u,n8)+ red(u,n6)* red(v,u)* red(v,n6)* red(v,n8) red(w,n8) red(w,n6)* red(w,u)* red(w,v)* -> . % 0.92/1.17 537[19:MRR:536.0,398.0] || red(u,n2)*+ red(u,n3) red(u,n4) red(v,n4) red(v,n3) red(v,n2)* red(v,u)* -> . % 0.92/1.17 532[19:Spt:497.9] || -> red(n2,n4)*. % 0.92/1.17 530[18:MRR:529.0,394.0] || red(u,n3)*+ red(u,n4) red(u,n5) red(v,n5) red(v,n4) red(v,n3)* red(v,u)* -> . % 0.92/1.17 525[18:Spt:492.9] || -> red(n3,n5)*. % 0.92/1.17 523[17:MRR:522.0,388.0] || red(u,n4)*+ red(u,n5) red(u,n6) red(v,n6) red(v,n5) red(v,n4)* red(v,u)* -> . % 0.92/1.17 518[17:Spt:481.9] || -> red(n4,n6)*. % 0.92/1.17 516[16:MRR:515.0,386.0] || red(u,n5)*+ red(u,n6) red(u,n7) red(v,n7) red(v,n6) red(v,n5)* red(v,u)* -> . % 0.92/1.17 511[16:Spt:471.9] || -> red(n5,n7)*. % 0.92/1.17 507[15:MRR:506.0,382.0] || red(u,n6)*+ red(u,n7) red(u,n8) red(v,n8) red(v,n7) red(v,n6)* red(v,u)* -> . % 0.92/1.17 502[15:Spt:462.9] || -> red(n6,n8)*. % 0.92/1.17 487[14:Res:485.0,20.0] || red(u,n9)+ red(u,n7)* red(v,u)* red(v,n7)* red(v,n9) red(w,n9) red(w,n7)* red(w,u)* red(w,v)* -> . % 0.92/1.17 490[14:MRR:489.0,378.0] || red(u,n7)*+ red(u,n8) red(u,n9) red(v,n9) red(v,n8) red(v,n7)* red(v,u)* -> . % 0.92/1.17 485[14:Spt:452.9] || -> red(n7,n9)*. % 0.92/1.17 466[13:Res:464.0,20.0] || red(u,n10)+ red(u,n8)* red(v,u)* red(v,n8)* red(v,n10) red(w,n10) red(w,n8)* red(w,u)* red(w,v)* -> . % 0.92/1.17 469[13:MRR:468.0,362.0] || red(u,n8)*+ red(u,n9) red(u,n10) red(v,n10) red(v,n9) red(v,n8)* red(v,u)* -> . % 0.92/1.17 464[13:Spt:438.9] || -> red(n8,n10)*. % 0.92/1.17 442[12:Res:440.0,20.0] || red(u,n11)+ red(u,n9)* red(v,u)* red(v,n9)* red(v,n11) red(w,n11) red(w,n9)* red(w,u)* red(w,v)* -> . % 0.92/1.17 444[12:MRR:443.0,366.0] || red(u,n9)*+ red(u,n10) red(u,n11) red(v,n11) red(v,n10) red(v,n9)* red(v,u)* -> . % 0.92/1.17 440[12:Spt:426.9] || -> red(n9,n11)*. % 0.92/1.17 430[11:Obv:428.5] || red(n10,n10)*+ red(u,n10)* red(u,n12) red(v,n12) red(v,n10)* red(v,u)* -> . % 0.92/1.17 414[11:Res:413.0,20.0] || red(u,n12)+ red(u,n10)* red(v,u)* red(v,n10)* red(v,n12) red(w,n12) red(w,n10)* red(w,u)* red(w,v)* -> . % 0.92/1.17 416[11:MRR:415.0,368.0] || red(u,n10)*+ red(u,n11) red(u,n12) red(v,n12) red(v,n11) red(v,n10)* red(v,u)* -> . % 0.92/1.17 413[11:Spt:411.9] || -> red(n10,n12)*. % 0.92/1.17 399[10:Res:398.0,20.0] || red(u,n3)+ red(u,n2)* red(v,u)* red(v,n2)* red(v,n3) red(w,n3) red(w,n2)* red(w,u)* red(w,v)* -> . % 0.92/1.17 398[10:Spt:265.9] || -> red(n2,n3)*. % 0.92/1.17 395[9:Res:394.0,20.0] || red(u,n4)+ red(u,n3)* red(v,u)* red(v,n3)* red(v,n4) red(w,n4) red(w,n3)* red(w,u)* red(w,v)* -> . % 0.92/1.17 394[9:Spt:251.9] || -> red(n3,n4)*. % 0.92/1.17 389[8:Res:388.0,20.0] || red(u,n5)+ red(u,n4)* red(v,u)* red(v,n4)* red(v,n5) red(w,n5) red(w,n4)* red(w,u)* red(w,v)* -> . % 0.92/1.17 387[7:Res:386.0,20.0] || red(u,n6)+ red(u,n5)* red(v,u)* red(v,n5)* red(v,n6) red(w,n6) red(w,n5)* red(w,u)* red(w,v)* -> . % 0.92/1.17 388[8:Spt:239.9] || -> red(n4,n5)*. % 0.92/1.17 386[7:Spt:226.9] || -> red(n5,n6)*. % 0.92/1.17 383[6:Res:382.0,20.0] || red(u,n7)+ red(u,n6)* red(v,u)* red(v,n6)* red(v,n7) red(w,n7) red(w,n6)* red(w,u)* red(w,v)* -> . % 0.92/1.17 382[6:Spt:209.9] || -> red(n6,n7)*. % 0.92/1.17 379[5:Res:378.0,20.0] || red(u,n8)+ red(u,n7)* red(v,u)* red(v,n7)* red(v,n8) red(w,n8) red(w,n7)* red(w,u)* red(w,v)* -> . % 0.92/1.17 378[5:Spt:196.9] || -> red(n7,n8)*. % 0.92/1.17 377[4:Obv:376.5] || red(n11,n11)*+ red(u,n11)* red(u,n12) red(v,n12) red(v,n11)* red(v,u)* -> . % 0.92/1.17 375[4:Res:374.0,20.0] || red(u,n12)+ red(u,n11)* red(v,u)* red(v,n11)* red(v,n12) red(w,n12) red(w,n11)* red(w,u)* red(w,v)* -> . % 0.92/1.17 374[4:Spt:183.9] || -> red(n11,n12)*. % 0.92/1.17 373[3:Obv:372.5] || red(n10,n10)*+ red(u,n10)* red(u,n11) red(v,n11) red(v,n10)* red(v,u)* -> . % 0.92/1.17 369[3:Res:368.0,20.0] || red(u,n11)+ red(u,n10)* red(v,u)* red(v,n10)* red(v,n11) red(w,n11) red(w,n10)* red(w,u)* red(w,v)* -> . % 0.92/1.17 367[2:Res:366.0,20.0] || red(u,n10)+ red(u,n9)* red(v,u)* red(v,n9)* red(v,n10) red(w,n10) red(w,n9)* red(w,u)* red(w,v)* -> . % 0.92/1.17 368[3:Spt:170.9] || -> red(n10,n11)*. % 0.92/1.17 366[2:Spt:157.9] || -> red(n9,n10)*. % 0.92/1.17 363[1:Res:362.0,20.0] || red(u,n9)+ red(u,n8)* red(v,u)* red(v,n8)* red(v,n9) red(w,n9) red(w,n8)* red(w,u)* red(w,v)* -> . % 0.92/1.17 362[1:Spt:145.9] || -> red(n8,n9)*. % 0.92/1.17 358[0:NCh:15.2,15.0,353.0,12.0] || less_than(n12,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 353[0:NCh:15.2,15.0,343.0,11.0] || less_than(n11,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 348[0:NCh:15.2,15.0,338.0,12.0] || less_than(n12,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 352[0:Res:11.0,343.0] || -> green(n1,n11)* red(n1,n11). % 0.92/1.17 343[0:NCh:15.2,15.0,328.0,10.0] || less_than(n10,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 338[0:NCh:15.2,15.0,323.0,11.0] || less_than(n11,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 333[0:NCh:15.2,15.0,318.0,12.0] || less_than(n12,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.17 342[0:Res:10.0,328.0] || -> green(n1,n10)* red(n1,n10). % 0.92/1.17 328[0:NCh:15.2,15.0,308.0,9.0] || less_than(n9,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 323[0:NCh:15.2,15.0,303.0,10.0] || less_than(n10,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 332[0:Res:12.0,318.0] || -> green(n3,n12)* red(n3,n12). % 0.92/1.17 318[0:NCh:15.2,15.0,298.0,11.0] || less_than(n11,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.17 313[0:NCh:15.2,15.0,293.0,12.0] || less_than(n12,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.17 308[0:NCh:15.2,15.0,283.0,8.0] || less_than(n8,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 303[0:NCh:15.2,15.0,276.0,9.0] || less_than(n9,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 298[0:NCh:15.2,15.0,271.0,10.0] || less_than(n10,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.17 293[0:NCh:15.2,15.0,263.0,11.0] || less_than(n11,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.17 288[0:NCh:15.2,15.0,258.0,12.0] || less_than(n12,u)+ -> green(n5,u)* red(n5,u). % 0.92/1.17 307[0:Res:8.0,283.0] || -> green(n1,n8)* red(n1,n8). % 0.92/1.17 283[0:NCh:15.2,15.0,244.0,7.0] || less_than(n7,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 302[0:Res:9.0,276.0] || -> green(n2,n9)* red(n2,n9). % 0.92/1.17 276[0:NCh:15.2,15.0,234.0,8.0] || less_than(n8,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 271[0:NCh:15.2,15.0,229.0,9.0] || less_than(n9,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.17 263[0:NCh:15.2,15.0,219.0,10.0] || less_than(n10,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.17 258[0:NCh:15.2,15.0,214.0,11.0] || less_than(n11,u)+ -> green(n5,u)* red(n5,u). % 0.92/1.17 249[0:NCh:15.2,15.0,204.0,12.0] || less_than(n12,u)+ -> green(n6,u)* red(n6,u). % 0.92/1.17 244[0:NCh:15.2,15.0,190.0,6.0] || less_than(n6,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 234[0:NCh:15.2,15.0,181.0,7.0] || less_than(n7,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 229[0:NCh:15.2,15.0,177.0,8.0] || less_than(n8,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.17 219[0:NCh:15.2,15.0,168.0,9.0] || less_than(n9,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.17 214[0:NCh:15.2,15.0,163.0,10.0] || less_than(n10,u)+ -> green(n5,u)* red(n5,u). % 0.92/1.17 204[0:NCh:15.2,15.0,154.0,11.0] || less_than(n11,u)+ -> green(n6,u)* red(n6,u). % 0.92/1.17 199[0:NCh:15.2,15.0,150.0,12.0] || less_than(n12,u)+ -> green(n7,u)* red(n7,u). % 0.92/1.17 190[0:NCh:15.2,15.0,136.0,5.0] || less_than(n5,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 181[0:NCh:15.2,15.0,134.0,6.0] || less_than(n6,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 177[0:NCh:15.2,15.0,130.0,7.0] || less_than(n7,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.17 168[0:NCh:15.2,15.0,126.0,8.0] || less_than(n8,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.17 163[0:NCh:15.2,15.0,122.0,9.0] || less_than(n9,u)+ -> green(n5,u)* red(n5,u). % 0.92/1.17 154[0:NCh:15.2,15.0,116.0,10.0] || less_than(n10,u)+ -> green(n6,u)* red(n6,u). % 0.92/1.17 150[0:NCh:15.2,15.0,114.0,11.0] || less_than(n11,u)+ -> green(n7,u)* red(n7,u). % 0.92/1.17 142[0:NCh:15.2,15.0,110.0,12.0] || less_than(n12,u)+ -> green(n8,u)* red(n8,u). % 0.92/1.17 136[0:NCh:15.2,15.0,102.0,4.0] || less_than(n4,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.17 134[0:NCh:15.2,15.0,98.0,5.0] || less_than(n5,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.17 130[0:NCh:15.2,15.0,94.0,6.0] || less_than(n6,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.17 126[0:NCh:15.2,15.0,88.0,7.0] || less_than(n7,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.17 122[0:NCh:15.2,15.0,86.0,8.0] || less_than(n8,u)+ -> green(n5,u)* red(n5,u). % 0.92/1.17 116[0:NCh:15.2,15.0,82.0,9.0] || less_than(n9,u)+ -> green(n6,u)* red(n6,u). % 0.92/1.17 114[0:NCh:15.2,15.0,78.0,10.0] || less_than(n10,u)+ -> green(n7,u)* red(n7,u). % 0.92/1.17 110[0:NCh:15.2,15.0,74.0,11.0] || less_than(n11,u)+ -> green(n8,u)* red(n8,u). % 0.92/1.18 106[0:NCh:15.2,15.0,68.0,12.0] || less_than(n12,u)+ -> green(n9,u)* red(n9,u). % 0.92/1.18 102[0:NCh:15.2,15.0,42.0,3.0] || less_than(n3,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.18 98[0:NCh:15.2,15.0,41.0,4.0] || less_than(n4,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.18 94[0:NCh:15.2,15.0,40.0,5.0] || less_than(n5,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.18 88[0:NCh:15.2,15.0,39.0,6.0] || less_than(n6,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.18 86[0:NCh:15.2,15.0,38.0,7.0] || less_than(n7,u)+ -> green(n5,u)* red(n5,u). % 0.92/1.18 82[0:NCh:15.2,15.0,37.0,8.0] || less_than(n8,u)+ -> green(n6,u)* red(n6,u). % 0.92/1.18 78[0:NCh:15.2,15.0,36.0,9.0] || less_than(n9,u)+ -> green(n7,u)* red(n7,u). % 0.92/1.18 74[0:NCh:15.2,15.0,35.0,10.0] || less_than(n10,u)+ -> green(n8,u)* red(n8,u). % 0.92/1.18 68[0:NCh:15.2,15.0,34.0,11.0] || less_than(n11,u)+ -> green(n9,u)* red(n9,u). % 0.92/1.18 66[0:NCh:15.2,15.0,33.0,12.0] || less_than(n12,u)+ -> green(n10,u)* red(n10,u). % 0.92/1.18 42[0:NCh:15.2,15.0,14.0,2.0] || less_than(n2,u)+ -> green(n1,u)* red(n1,u). % 0.92/1.18 41[0:NCh:15.2,15.0,14.0,3.0] || less_than(n3,u)+ -> green(n2,u)* red(n2,u). % 0.92/1.18 40[0:NCh:15.2,15.0,14.0,4.0] || less_than(n4,u)+ -> green(n3,u)* red(n3,u). % 0.92/1.18 39[0:NCh:15.2,15.0,14.0,5.0] || less_than(n5,u)+ -> green(n4,u)* red(n4,u). % 0.92/1.18 38[0:NCh:15.2,15.0,14.0,6.0] || less_than(n6,u)+ -> green(n5,u)* red(n5,u). % 0.92/1.18 37[0:NCh:15.2,15.0,14.0,7.0] || less_than(n7,u)+ -> green(n6,u)* red(n6,u). % 0.92/1.18 36[0:NCh:15.2,15.0,14.0,8.0] || less_than(n8,u)+ -> green(n7,u)* red(n7,u). % 0.92/1.18 35[0:NCh:15.2,15.0,14.0,9.0] || less_than(n9,u)+ -> green(n8,u)* red(n8,u). % 0.92/1.18 34[0:NCh:15.2,15.0,14.0,10.0] || less_than(n10,u)+ -> green(n9,u)* red(n9,u). % 0.92/1.18 33[0:NCh:15.2,15.0,14.0,11.0] || less_than(n11,u)+ -> green(n10,u)* red(n10,u). % 0.92/1.18 32[0:NCh:15.2,15.0,14.0,12.0] || less_than(n12,u)+ -> green(n11,u)* red(n11,u). % 0.92/1.18 19[0:MRR:16.10,1.0] || green(u,v)*+ green(w,v)* green(w,u)* green(x,w)* green(x,u)* green(x,v)* green(y,v)* green(y,u)* green(y,w)* green(y,x)* -> . % 0.92/1.18 20[0:MRR:17.10,1.0] || red(u,v)*+ red(w,v)* red(w,u)* red(x,w)* red(x,u)* red(x,v)* red(y,v)* red(y,u)* red(y,w)* red(y,x)* -> . % 0.92/1.18 14[0:Inp] || less_than(u,v)+ -> green(u,v)* red(u,v). % 0.92/1.18 18[0:MRR:13.2,1.0] || green(u,v)*+ red(u,v) -> . % 0.92/1.18 2[0:Inp] || -> less_than(n1,n2)*l. % 0.92/1.18 3[0:Inp] || -> less_than(n2,n3)*l. % 0.92/1.18 4[0:Inp] || -> less_than(n3,n4)*l. % 0.92/1.18 5[0:Inp] || -> less_than(n4,n5)*l. % 0.92/1.18 6[0:Inp] || -> less_than(n5,n6)*l. % 0.92/1.18 7[0:Inp] || -> less_than(n6,n7)*l. % 0.92/1.18 8[0:Inp] || -> less_than(n7,n8)*l. % 0.92/1.18 9[0:Inp] || -> less_than(n8,n9)*l. % 0.92/1.18 10[0:Inp] || -> less_than(n9,n10)*l. % 0.92/1.18 11[0:Inp] || -> less_than(n10,n11)*l. % 0.92/1.18 12[0:Inp] || -> less_than(n11,n12)*l. % 0.92/1.18 1[0:Inp] || goal*+ -> . % 0.92/1.18 % SZS output end Saturation %------------------------------------------------------------------------------