%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRA014+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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:10 EDT 2022 % Result : Theorem 0.38s 0.61s % Output : Refutation 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRA014+1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n022.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 03:54:07 EDT 2022 % 0.14/0.34 % CPUTime : % 0.38/0.61 % 0.38/0.61 SPASS V 3.9 % 0.38/0.61 SPASS beiseite: Proof found. % 0.38/0.61 % SZS status Theorem % 0.38/0.61 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.38/0.61 SPASS derived 2429 clauses, backtracked 2999 clauses, performed 346 splits and kept 4575 clauses. % 0.38/0.61 SPASS allocated 86319 KBytes. % 0.38/0.61 SPASS spent 0:00:00.26 on the problem. % 0.38/0.61 0:00:00.04 for the input. % 0.38/0.61 0:00:00.03 for the FLOTTER CNF translation. % 0.38/0.61 0:00:00.02 for inferences. % 0.38/0.61 0:00:00.01 for the backtracking. % 0.38/0.61 0:00:00.13 for the reduction. % 0.38/0.61 % 0.38/0.61 % 0.38/0.61 Here is a proof with depth 9, length 1069 : % 0.38/0.61 % SZS output start Refutation % 0.38/0.61 1[0:Inp] || goal*+ -> . % 0.38/0.61 2[0:Inp] || -> less_than(n1,n2)*l. % 0.38/0.61 3[0:Inp] || -> less_than(n2,n3)*l. % 0.38/0.61 4[0:Inp] || -> less_than(n3,n4)*l. % 0.38/0.61 5[0:Inp] || -> less_than(n4,n5)*l. % 0.38/0.61 6[0:Inp] || -> less_than(n5,n6)*l. % 0.38/0.61 7[0:Inp] || less_than(u,v)+ -> green(u,v) red(u,v)*. % 0.38/0.61 8[0:Inp] || less_than(u,v)* less_than(v,w)* -> less_than(u,w)*. % 0.38/0.61 9[0:Inp] || red(u,v)* red(u,w)* red(v,w)* -> goal. % 0.38/0.61 10[0:Inp] || green(u,v)* green(u,w)* green(v,w)* -> goal. % 0.38/0.61 11[0:MRR:10.3,1.0] || green(u,v)*+ green(w,v)* green(w,u)* -> . % 0.38/0.61 12[0:MRR:9.3,1.0] || red(u,v)*+ red(w,v)* red(w,u)* -> . % 0.38/0.61 13[0:Res:6.0,7.0] || -> green(n5,n6) red(n5,n6)*. % 0.38/0.61 14[0:Res:5.0,7.0] || -> green(n4,n5) red(n4,n5)*. % 0.38/0.61 15[0:Res:4.0,7.0] || -> green(n3,n4) red(n3,n4)*. % 0.38/0.61 16[0:Res:3.0,7.0] || -> green(n2,n3) red(n2,n3)*. % 0.38/0.61 17[0:Res:2.0,7.0] || -> green(n1,n2) red(n1,n2)*. % 0.38/0.61 19[0:NCh:8.2,8.0,7.0,5.0] || less_than(n5,u)+ -> green(n4,u) red(n4,u)*. % 0.38/0.61 20[0:NCh:8.2,8.0,7.0,4.0] || less_than(n4,u)+ -> green(n3,u) red(n3,u)*. % 0.38/0.61 21[0:NCh:8.2,8.0,7.0,3.0] || less_than(n3,u)+ -> green(n2,u) red(n2,u)*. % 0.38/0.61 22[0:NCh:8.2,8.0,7.0,2.0] || less_than(n2,u)+ -> green(n1,u) red(n1,u)*. % 0.38/0.61 23[0:Res:13.1,12.0] || red(u,n6)+ red(u,n5)* -> green(n5,n6). % 0.38/0.61 24[0:Res:14.1,12.0] || red(u,n5)+ red(u,n4)* -> green(n4,n5). % 0.38/0.61 25[0:Res:15.1,12.0] || red(u,n4)+ red(u,n3)* -> green(n3,n4). % 0.38/0.61 26[0:Res:16.1,12.0] || red(u,n3)+ red(u,n2)* -> green(n2,n3). % 0.38/0.61 32[0:Res:6.0,19.0] || -> green(n4,n6) red(n4,n6)*. % 0.38/0.61 34[0:Res:32.1,12.0] || red(u,n6)+ red(u,n4)* -> green(n4,n6). % 0.38/0.61 35[0:Res:32.1,23.0] || red(n4,n5)*+ -> green(n4,n6) green(n5,n6). % 0.38/0.61 36[1:Spt:35.2] || -> green(n5,n6)*. % 0.38/0.61 37[1:Res:36.0,11.0] || green(u,n6)+ green(u,n5)* -> . % 0.38/0.61 39[0:Res:5.0,20.0] || -> green(n3,n5) red(n3,n5)*. % 0.38/0.61 40[0:NCh:8.2,8.0,20.0,5.0] || less_than(n5,u)+ -> green(n3,u) red(n3,u)*. % 0.38/0.61 41[0:Res:39.1,12.0] || red(u,n5)+ red(u,n3)* -> green(n3,n5). % 0.38/0.61 42[0:Res:39.1,24.0] || red(n3,n4)*+ -> green(n3,n5) green(n4,n5). % 0.38/0.61 43[2:Spt:42.2] || -> green(n4,n5)*. % 0.38/0.61 44[2:Res:43.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.61 46[0:Res:4.0,21.0] || -> green(n2,n4) red(n2,n4)*. % 0.38/0.61 47[0:NCh:8.2,8.0,21.0,4.0] || less_than(n4,u)+ -> green(n2,u) red(n2,u)*. % 0.38/0.61 48[0:Res:46.1,12.0] || red(u,n4)+ red(u,n2)* -> green(n2,n4). % 0.38/0.61 50[0:Res:46.1,25.0] || red(n2,n3)*+ -> green(n2,n4) green(n3,n4). % 0.38/0.61 52[3:Spt:50.2] || -> green(n3,n4)*. % 0.38/0.61 53[3:Res:52.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 54[0:Res:3.0,22.0] || -> green(n1,n3) red(n1,n3)*. % 0.38/0.61 55[0:NCh:8.2,8.0,22.0,3.0] || less_than(n3,u)+ -> green(n1,u) red(n1,u)*. % 0.38/0.61 59[0:Res:54.1,26.0] || red(n1,n2)*+ -> green(n1,n3) green(n2,n3). % 0.38/0.61 63[4:Spt:59.2] || -> green(n2,n3)*. % 0.38/0.61 64[4:Res:63.0,11.0] || green(u,n3)+ green(u,n2)* -> . % 0.38/0.61 70[0:Res:6.0,40.0] || -> green(n3,n6) red(n3,n6)*. % 0.38/0.61 72[0:Res:70.1,12.0] || red(u,n6)+ red(u,n3)* -> green(n3,n6). % 0.38/0.61 73[0:Res:70.1,34.0] || red(n3,n4)*+ -> green(n3,n6) green(n4,n6). % 0.38/0.61 74[5:Spt:73.2] || -> green(n4,n6)*. % 0.38/0.61 76[5:Res:74.0,37.0] || green(n4,n5)* -> . % 0.38/0.61 77[5:MRR:76.0,43.0] || -> . % 0.38/0.61 78[5:Spt:77.0,73.2,74.0] || green(n4,n6)*+ -> . % 0.38/0.61 79[5:Spt:77.0,73.0,73.1] || red(n3,n4)*+ -> green(n3,n6). % 0.38/0.61 82[5:MRR:34.2,78.0] || red(u,n6)+ red(u,n4)* -> . % 0.38/0.61 88[0:Res:5.0,47.0] || -> green(n2,n5) red(n2,n5)*. % 0.38/0.61 89[0:NCh:8.2,8.0,47.0,5.0] || less_than(n5,u)+ -> green(n2,u) red(n2,u)*. % 0.38/0.61 90[0:Res:88.1,12.0] || red(u,n5)+ red(u,n2)* -> green(n2,n5). % 0.38/0.61 91[0:Res:88.1,41.0] || red(n2,n3)*+ -> green(n2,n5) green(n3,n5). % 0.38/0.61 92[6:Spt:91.2] || -> green(n3,n5)*. % 0.38/0.61 94[6:Res:92.0,44.0] || green(n3,n4)* -> . % 0.38/0.61 95[6:MRR:94.0,52.0] || -> . % 0.38/0.61 96[6:Spt:95.0,91.2,92.0] || green(n3,n5)*+ -> . % 0.38/0.61 97[6:Spt:95.0,91.0,91.1] || red(n2,n3)*+ -> green(n2,n5). % 0.38/0.61 100[6:MRR:41.2,96.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.61 102[0:Res:4.0,55.0] || -> green(n1,n4) red(n1,n4)*. % 0.38/0.61 103[0:NCh:8.2,8.0,55.0,4.0] || less_than(n4,u)+ -> green(n1,u) red(n1,u)*. % 0.38/0.61 105[0:Res:102.1,48.0] || red(n1,n2)*+ -> green(n1,n4) green(n2,n4). % 0.38/0.61 108[7:Spt:105.2] || -> green(n2,n4)*. % 0.38/0.61 110[7:Res:108.0,53.0] || green(n2,n3)* -> . % 0.38/0.61 111[7:MRR:110.0,63.0] || -> . % 0.38/0.61 112[7:Spt:111.0,105.2,108.0] || green(n2,n4)*+ -> . % 0.38/0.61 113[7:Spt:111.0,105.0,105.1] || red(n1,n2)*+ -> green(n1,n4). % 0.38/0.61 114[7:MRR:46.0,112.0] || -> red(n2,n4)*. % 0.38/0.61 117[7:Res:17.1,113.0] || -> green(n1,n2)* green(n1,n4). % 0.38/0.61 119[8:Spt:117.0] || -> green(n1,n2)*. % 0.38/0.61 135[0:Res:6.0,89.0] || -> green(n2,n6) red(n2,n6)*. % 0.38/0.61 137[0:Res:135.1,12.0] || red(u,n6) red(u,n2)* -> green(n2,n6). % 0.38/0.61 138[0:Res:135.1,72.0] || red(n2,n3)* -> green(n2,n6) green(n3,n6). % 0.38/0.61 139[5:Res:135.1,82.0] || red(n2,n4)* -> green(n2,n6). % 0.38/0.61 140[7:MRR:139.0,114.0] || -> green(n2,n6)*. % 0.38/0.61 142[7:Res:140.0,37.0] || green(n2,n5)*+ -> . % 0.38/0.61 145[7:MRR:90.2,142.0] || red(u,n5)+ red(u,n2)* -> . % 0.38/0.61 149[0:Res:5.0,103.0] || -> green(n1,n5) red(n1,n5)*. % 0.38/0.61 150[0:NCh:8.2,8.0,103.0,5.0] || less_than(n5,u)+ -> green(n1,u) red(n1,u)*. % 0.38/0.61 152[6:Res:149.1,100.0] || red(n1,n3)*+ -> green(n1,n5). % 0.38/0.61 154[7:Res:149.1,145.0] || red(n1,n2)* -> green(n1,n5). % 0.38/0.61 156[6:Res:54.1,152.0] || -> green(n1,n3)* green(n1,n5). % 0.38/0.61 157[9:Spt:156.0] || -> green(n1,n3)*. % 0.38/0.61 159[9:Res:157.0,64.0] || green(n1,n2)* -> . % 0.38/0.61 160[9:MRR:159.0,119.0] || -> . % 0.38/0.61 161[9:Spt:160.0,156.0,157.0] || green(n1,n3)*+ -> . % 0.38/0.61 162[9:Spt:160.0,156.1] || -> green(n1,n5)*. % 0.38/0.61 167[9:Res:162.0,44.0] || green(n1,n4)*+ -> . % 0.38/0.61 168[9:MRR:102.0,167.0] || -> red(n1,n4)*. % 0.38/0.61 182[0:Res:6.0,150.0] || -> green(n1,n6) red(n1,n6)*. % 0.38/0.61 185[0:Res:182.1,72.0] || red(n1,n3)* -> green(n1,n6) green(n3,n6). % 0.38/0.61 186[5:Res:182.1,82.0] || red(n1,n4)* -> green(n1,n6). % 0.38/0.61 187[9:MRR:186.0,168.0] || -> green(n1,n6)*. % 0.38/0.61 190[9:Res:187.0,37.0] || green(n1,n5)* -> . % 0.38/0.61 192[9:MRR:190.0,162.0] || -> . % 0.38/0.61 193[8:Spt:192.0,117.0,119.0] || green(n1,n2)* -> . % 0.38/0.61 194[8:Spt:192.0,117.1] || -> green(n1,n4)*. % 0.38/0.61 195[8:MRR:17.0,193.0] || -> red(n1,n2)*. % 0.38/0.61 196[8:MRR:154.0,195.0] || -> green(n1,n5)*. % 0.38/0.61 206[8:Res:196.0,44.0] || green(n1,n4)* -> . % 0.38/0.61 207[8:MRR:206.0,194.0] || -> . % 0.38/0.61 208[4:Spt:207.0,59.2,63.0] || green(n2,n3)*+ -> . % 0.38/0.61 209[4:Spt:207.0,59.0,59.1] || red(n1,n2)*+ -> green(n1,n3). % 0.38/0.61 210[4:MRR:16.0,208.0] || -> red(n2,n3)*. % 0.38/0.61 212[4:MRR:138.0,210.0] || -> green(n2,n6)* green(n3,n6). % 0.38/0.61 213[4:MRR:91.0,210.0] || -> green(n2,n5)* green(n3,n5). % 0.38/0.61 216[5:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 218[5:Res:216.0,37.0] || green(n1,n5)*+ -> . % 0.38/0.61 219[5:MRR:149.0,218.0] || -> red(n1,n5)*. % 0.38/0.61 222[6:Spt:17.1] || -> red(n1,n2)*. % 0.38/0.61 223[6:MRR:209.0,222.0] || -> green(n1,n3)*. % 0.38/0.61 224[6:MRR:105.0,222.0] || -> green(n1,n4)* green(n2,n4). % 0.38/0.61 227[7:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.61 229[7:Res:227.0,53.0] || green(n1,n3)* -> . % 0.38/0.61 230[7:MRR:229.0,223.0] || -> . % 0.38/0.61 231[7:Spt:230.0,102.0,227.0] || green(n1,n4)*+ -> . % 0.38/0.61 232[7:Spt:230.0,102.1] || -> red(n1,n4)*. % 0.38/0.61 233[7:MRR:224.0,231.0] || -> green(n2,n4)*. % 0.38/0.61 239[8:Spt:39.0] || -> green(n3,n5)*. % 0.38/0.61 241[8:Res:239.0,44.0] || green(n3,n4)* -> . % 0.38/0.61 242[8:MRR:241.0,52.0] || -> . % 0.38/0.61 243[8:Spt:242.0,39.0,239.0] || green(n3,n5)* -> . % 0.38/0.61 244[8:Spt:242.0,39.1] || -> red(n3,n5)*. % 0.38/0.61 245[8:MRR:213.1,243.0] || -> green(n2,n5)*. % 0.38/0.61 250[8:Res:245.0,44.0] || green(n2,n4)* -> . % 0.38/0.61 251[8:MRR:250.0,233.0] || -> . % 0.38/0.61 252[6:Spt:251.0,17.1,222.0] || red(n1,n2)*+ -> . % 0.38/0.61 253[6:Spt:251.0,17.0] || -> green(n1,n2)*. % 0.38/0.61 255[7:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.61 257[7:Res:255.0,37.0] || green(n2,n5)* -> . % 0.38/0.61 258[7:MRR:213.0,257.0] || -> green(n3,n5)*. % 0.38/0.61 262[7:Res:258.0,44.0] || green(n3,n4)* -> . % 0.38/0.61 263[7:MRR:262.0,52.0] || -> . % 0.38/0.61 264[7:Spt:263.0,135.0,255.0] || green(n2,n6)*+ -> . % 0.38/0.61 265[7:Spt:263.0,135.1] || -> red(n2,n6)*. % 0.38/0.61 266[7:MRR:212.0,264.0] || -> green(n3,n6)*. % 0.38/0.61 269[7:Res:266.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.61 270[7:Res:266.0,37.0] || green(n3,n5)*+ -> . % 0.38/0.61 274[7:MRR:41.2,270.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.61 281[8:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 283[8:Res:281.0,37.0] || green(n4,n5)* -> . % 0.38/0.61 284[8:MRR:283.0,43.0] || -> . % 0.38/0.61 285[8:Spt:284.0,32.0,281.0] || green(n4,n6)*+ -> . % 0.38/0.61 286[8:Spt:284.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 290[9:Spt:54.0] || -> green(n1,n3)*. % 0.38/0.61 310[7:Res:219.0,274.0] || red(n1,n3)*+ -> . % 0.38/0.61 314[7:Res:216.0,269.0] || green(n1,n3)* -> . % 0.38/0.61 315[9:MRR:314.0,290.0] || -> . % 0.38/0.61 316[9:Spt:315.0,54.0,290.0] || green(n1,n3)* -> . % 0.38/0.61 317[9:Spt:315.0,54.1] || -> red(n1,n3)*. % 0.38/0.61 318[9:MRR:317.0,310.0] || -> . % 0.38/0.61 320[5:Spt:318.0,182.0,216.0] || green(n1,n6)*+ -> . % 0.38/0.61 321[5:Spt:318.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 322[5:MRR:185.1,320.0] || red(n1,n3)* -> green(n3,n6). % 0.38/0.61 325[6:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.61 327[6:Res:325.0,53.0] || green(n1,n3)*+ -> . % 0.38/0.61 328[6:MRR:54.0,327.0] || -> red(n1,n3)*. % 0.38/0.61 332[6:MRR:322.0,328.0] || -> green(n3,n6)*. % 0.38/0.61 338[6:Res:332.0,37.0] || green(n3,n5)*+ -> . % 0.38/0.61 342[6:MRR:41.2,338.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.61 368[6:Res:149.1,342.0] || red(n1,n3)* -> green(n1,n5). % 0.38/0.61 370[6:MRR:368.0,328.0] || -> green(n1,n5)*. % 0.38/0.61 372[6:Res:370.0,44.0] || green(n1,n4)* -> . % 0.38/0.61 373[6:MRR:372.0,325.0] || -> . % 0.38/0.61 374[6:Spt:373.0,102.0,325.0] || green(n1,n4)*+ -> . % 0.38/0.61 375[6:Spt:373.0,102.1] || -> red(n1,n4)*. % 0.38/0.61 379[7:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 381[7:Res:379.0,37.0] || green(n4,n5)* -> . % 0.38/0.61 382[7:MRR:381.0,43.0] || -> . % 0.38/0.61 383[7:Spt:382.0,32.0,379.0] || green(n4,n6)*+ -> . % 0.38/0.61 384[7:Spt:382.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 387[7:MRR:34.2,383.0] || red(u,n6)+ red(u,n4)* -> . % 0.38/0.61 428[7:Res:321.0,387.0] || red(n1,n4)* -> . % 0.38/0.61 430[7:MRR:428.0,375.0] || -> . % 0.38/0.61 431[3:Spt:430.0,50.2,52.0] || green(n3,n4)*+ -> . % 0.38/0.61 432[3:Spt:430.0,50.0,50.1] || red(n2,n3)*+ -> green(n2,n4). % 0.38/0.61 433[3:MRR:15.0,431.0] || -> red(n3,n4)*. % 0.38/0.61 435[3:MRR:73.0,433.0] || -> green(n3,n6)* green(n4,n6). % 0.38/0.61 436[3:MRR:25.2,431.0] || red(u,n4)+ red(u,n3)* -> . % 0.38/0.61 439[4:Spt:17.0] || -> green(n1,n2)*. % 0.38/0.61 441[5:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.61 443[5:Res:441.0,37.0] || green(n3,n5)*+ -> . % 0.38/0.61 445[5:MRR:91.2,443.0] || red(n2,n3)* -> green(n2,n5). % 0.38/0.61 446[5:MRR:41.2,443.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.61 449[6:Spt:16.1] || -> red(n2,n3)*. % 0.38/0.61 450[6:MRR:432.0,449.0] || -> green(n2,n4)*. % 0.38/0.61 451[6:MRR:445.0,449.0] || -> green(n2,n5)*. % 0.38/0.61 455[6:Res:451.0,44.0] || green(n2,n4)* -> . % 0.38/0.61 456[6:MRR:455.0,450.0] || -> . % 0.38/0.61 457[6:Spt:456.0,16.1,449.0] || red(n2,n3)*+ -> . % 0.38/0.61 458[6:Spt:456.0,16.0] || -> green(n2,n3)*. % 0.38/0.61 459[6:Res:458.0,11.0] || green(u,n3)+ green(u,n2)* -> . % 0.38/0.61 460[7:Spt:54.0] || -> green(n1,n3)*. % 0.38/0.61 491[5:Res:149.1,446.0] || red(n1,n3)*+ -> green(n1,n5). % 0.38/0.61 493[7:Res:460.0,459.0] || green(n1,n2)* -> . % 0.38/0.61 494[7:MRR:493.0,439.0] || -> . % 0.38/0.61 495[7:Spt:494.0,54.0,460.0] || green(n1,n3)* -> . % 0.38/0.61 496[7:Spt:494.0,54.1] || -> red(n1,n3)*. % 0.38/0.61 497[7:MRR:491.0,496.0] || -> green(n1,n5)*. % 0.38/0.61 502[7:Res:497.0,44.0] || green(n1,n4)* -> . % 0.38/0.61 503[7:MRR:102.0,502.0] || -> red(n1,n4)*. % 0.38/0.61 507[7:Res:503.0,436.0] || red(n1,n3)* -> . % 0.38/0.61 508[7:MRR:507.0,496.0] || -> . % 0.38/0.61 509[5:Spt:508.0,70.0,441.0] || green(n3,n6)*+ -> . % 0.38/0.61 510[5:Spt:508.0,70.1] || -> red(n3,n6)*. % 0.38/0.61 511[5:MRR:435.0,509.0] || -> green(n4,n6)*. % 0.38/0.61 517[5:Res:511.0,37.0] || green(n4,n5)* -> . % 0.38/0.61 518[5:MRR:517.0,43.0] || -> . % 0.38/0.61 519[4:Spt:518.0,17.0,439.0] || green(n1,n2)*+ -> . % 0.38/0.61 520[4:Spt:518.0,17.1] || -> red(n1,n2)*. % 0.38/0.61 526[5:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.61 528[5:Res:526.0,44.0] || green(n2,n4)*+ -> . % 0.38/0.61 529[5:MRR:46.0,528.0] || -> red(n2,n4)*. % 0.38/0.61 549[6:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 551[6:Res:549.0,37.0] || green(n4,n5)* -> . % 0.38/0.61 552[6:MRR:551.0,43.0] || -> . % 0.38/0.61 553[6:Spt:552.0,32.0,549.0] || green(n4,n6)*+ -> . % 0.38/0.61 554[6:Spt:552.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 556[6:MRR:34.2,553.0] || red(u,n6)+ red(u,n4)* -> . % 0.38/0.61 573[6:Res:135.1,556.0] || red(n2,n4)* -> green(n2,n6). % 0.38/0.61 575[6:MRR:573.0,529.0] || -> green(n2,n6)*. % 0.38/0.61 578[6:Res:575.0,37.0] || green(n2,n5)* -> . % 0.38/0.61 580[6:MRR:578.0,526.0] || -> . % 0.38/0.61 581[5:Spt:580.0,88.0,526.0] || green(n2,n5)*+ -> . % 0.38/0.61 582[5:Spt:580.0,88.1] || -> red(n2,n5)*. % 0.38/0.61 585[5:MRR:90.2,581.0] || red(u,n5)+ red(u,n2)* -> . % 0.38/0.61 592[6:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 594[6:Res:592.0,37.0] || green(n4,n5)* -> . % 0.38/0.61 595[6:MRR:594.0,43.0] || -> . % 0.38/0.61 596[6:Spt:595.0,32.0,592.0] || green(n4,n6)*+ -> . % 0.38/0.61 597[6:Spt:595.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 600[6:MRR:34.2,596.0] || red(u,n6)+ red(u,n4)* -> . % 0.38/0.61 614[5:Res:149.1,585.0] || red(n1,n2)* -> green(n1,n5). % 0.38/0.61 616[5:MRR:614.0,520.0] || -> green(n1,n5)*. % 0.38/0.61 618[5:Res:616.0,44.0] || green(n1,n4)*+ -> . % 0.38/0.61 622[5:MRR:102.0,618.0] || -> red(n1,n4)*. % 0.38/0.61 632[6:Res:182.1,600.0] || red(n1,n4)* -> green(n1,n6). % 0.38/0.61 633[6:MRR:632.0,622.0] || -> green(n1,n6)*. % 0.38/0.61 635[6:Res:633.0,37.0] || green(n1,n5)* -> . % 0.38/0.61 636[6:MRR:635.0,616.0] || -> . % 0.38/0.61 637[2:Spt:636.0,42.2,43.0] || green(n4,n5)*+ -> . % 0.38/0.61 638[2:Spt:636.0,42.0,42.1] || red(n3,n4)*+ -> green(n3,n5). % 0.38/0.61 641[2:MRR:24.2,637.0] || red(u,n5)+ red(u,n4)* -> . % 0.38/0.61 643[3:Spt:16.0] || -> green(n2,n3)*. % 0.38/0.61 644[3:Res:643.0,11.0] || green(u,n3)+ green(u,n2)* -> . % 0.38/0.61 645[4:Spt:46.0] || -> green(n2,n4)*. % 0.38/0.61 646[4:Res:645.0,11.0] || green(u,n4)+ green(u,n2)* -> . % 0.38/0.61 647[5:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.61 649[5:Res:647.0,37.0] || green(n3,n5)*+ -> . % 0.38/0.61 650[5:MRR:638.1,649.0] || red(n3,n4)*+ -> . % 0.38/0.61 655[5:MRR:15.1,650.0] || -> green(n3,n4)*. % 0.38/0.61 657[5:Res:655.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 670[2:Res:149.1,641.0] || red(n1,n4)*+ -> green(n1,n5). % 0.38/0.61 698[5:Res:645.0,657.0] || green(n2,n3)* -> . % 0.38/0.61 699[5:MRR:698.0,643.0] || -> . % 0.38/0.61 700[5:Spt:699.0,70.0,647.0] || green(n3,n6)*+ -> . % 0.38/0.61 701[5:Spt:699.0,70.1] || -> red(n3,n6)*. % 0.38/0.61 703[5:MRR:185.2,700.0] || red(n1,n3)*+ -> green(n1,n6). % 0.38/0.61 708[6:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.61 728[5:Res:54.1,703.0] || -> green(n1,n3)* green(n1,n6). % 0.38/0.61 746[7:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.61 747[7:Res:746.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 773[7:Res:645.0,747.0] || green(n2,n3)* -> . % 0.38/0.61 774[7:MRR:773.0,643.0] || -> . % 0.38/0.61 775[7:Spt:774.0,15.0,746.0] || green(n3,n4)*+ -> . % 0.38/0.61 776[7:Spt:774.0,15.1] || -> red(n3,n4)*. % 0.38/0.61 778[7:MRR:638.0,776.0] || -> green(n3,n5)*. % 0.38/0.61 783[7:Res:778.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.61 808[7:Res:708.0,783.0] || green(n2,n3)* -> . % 0.38/0.61 810[7:MRR:808.0,643.0] || -> . % 0.38/0.61 812[6:Spt:810.0,88.0,708.0] || green(n2,n5)*+ -> . % 0.38/0.61 813[6:Spt:810.0,88.1] || -> red(n2,n5)*. % 0.38/0.61 816[6:MRR:90.2,812.0] || red(u,n5)+ red(u,n2)* -> . % 0.38/0.61 819[7:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.61 820[7:Res:819.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 874[7:Res:645.0,820.0] || green(n2,n3)* -> . % 0.38/0.61 875[7:MRR:874.0,643.0] || -> . % 0.38/0.61 876[7:Spt:875.0,15.0,819.0] || green(n3,n4)*+ -> . % 0.38/0.61 877[7:Spt:875.0,15.1] || -> red(n3,n4)*. % 0.38/0.61 879[7:MRR:638.0,877.0] || -> green(n3,n5)*. % 0.38/0.61 884[7:Res:879.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.61 885[8:Spt:149.0] || -> green(n1,n5)*. % 0.38/0.61 887[9:Spt:728.0] || -> green(n1,n3)*. % 0.38/0.61 913[8:Res:885.0,884.0] || green(n1,n3)* -> . % 0.38/0.61 914[9:MRR:913.0,887.0] || -> . % 0.38/0.61 915[9:Spt:914.0,728.0,887.0] || green(n1,n3)* -> . % 0.38/0.61 916[9:Spt:914.0,728.1] || -> green(n1,n6)*. % 0.38/0.61 923[9:Res:916.0,37.0] || green(n1,n5)* -> . % 0.38/0.61 925[9:MRR:923.0,885.0] || -> . % 0.38/0.61 926[8:Spt:925.0,149.0,885.0] || green(n1,n5)* -> . % 0.38/0.61 927[8:Spt:925.0,149.1] || -> red(n1,n5)*. % 0.38/0.61 928[8:MRR:670.1,926.0] || red(n1,n4)* -> . % 0.38/0.61 929[8:MRR:102.1,928.0] || -> green(n1,n4)*. % 0.38/0.61 932[8:Res:927.0,816.0] || red(n1,n2)* -> . % 0.38/0.61 934[8:MRR:17.1,932.0] || -> green(n1,n2)*. % 0.38/0.61 936[8:Res:929.0,646.0] || green(n1,n2)* -> . % 0.38/0.61 937[8:MRR:936.0,934.0] || -> . % 0.38/0.61 938[4:Spt:937.0,46.0,645.0] || green(n2,n4)*+ -> . % 0.38/0.61 939[4:Spt:937.0,46.1] || -> red(n2,n4)*. % 0.38/0.61 941[4:MRR:105.2,938.0] || red(n1,n2)* -> green(n1,n4). % 0.38/0.61 945[5:Spt:17.0] || -> green(n1,n2)*. % 0.38/0.61 947[6:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 949[6:Res:947.0,37.0] || green(n1,n5)*+ -> . % 0.38/0.61 951[6:MRR:670.1,949.0] || red(n1,n4)*+ -> . % 0.38/0.61 953[6:MRR:102.1,951.0] || -> green(n1,n4)*. % 0.38/0.61 959[7:Spt:54.0] || -> green(n1,n3)*. % 0.38/0.61 961[7:Res:959.0,644.0] || green(n1,n2)* -> . % 0.38/0.61 962[7:MRR:961.0,945.0] || -> . % 0.38/0.61 963[7:Spt:962.0,54.0,959.0] || green(n1,n3)*+ -> . % 0.38/0.61 964[7:Spt:962.0,54.1] || -> red(n1,n3)*. % 0.38/0.61 968[8:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 969[8:Res:968.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.61 974[2:Res:88.1,641.0] || red(n2,n4)* -> green(n2,n5). % 0.38/0.61 975[4:MRR:974.0,939.0] || -> green(n2,n5)*. % 0.38/0.61 976[4:Res:975.0,11.0] || green(u,n5)+ green(u,n2)* -> . % 0.38/0.61 1001[8:Res:947.0,969.0] || green(n1,n4)* -> . % 0.38/0.61 1002[8:MRR:1001.0,953.0] || -> . % 0.38/0.61 1003[8:Spt:1002.0,32.0,968.0] || green(n4,n6)*+ -> . % 0.38/0.61 1004[8:Spt:1002.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 1006[8:MRR:34.2,1003.0] || red(u,n6)+ red(u,n4)* -> . % 0.38/0.61 1020[8:Res:135.1,1006.0] || red(n2,n4)* -> green(n2,n6). % 0.38/0.61 1021[8:MRR:1020.0,939.0] || -> green(n2,n6)*. % 0.38/0.61 1024[8:Res:1021.0,37.0] || green(n2,n5)* -> . % 0.38/0.61 1025[8:MRR:1024.0,975.0] || -> . % 0.38/0.61 1026[6:Spt:1025.0,182.0,947.0] || green(n1,n6)*+ -> . % 0.38/0.61 1027[6:Spt:1025.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 1028[6:MRR:185.1,1026.0] || red(n1,n3)* -> green(n3,n6). % 0.38/0.61 1031[7:Spt:39.0] || -> green(n3,n5)*. % 0.38/0.61 1033[8:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.61 1035[8:Res:1033.0,37.0] || green(n3,n5)* -> . % 0.38/0.61 1036[8:MRR:1035.0,1031.0] || -> . % 0.38/0.61 1037[8:Spt:1036.0,70.0,1033.0] || green(n3,n6)*+ -> . % 0.38/0.61 1038[8:Spt:1036.0,70.1] || -> red(n3,n6)*. % 0.38/0.61 1040[8:MRR:1028.1,1037.0] || red(n1,n3)* -> . % 0.38/0.61 1041[8:MRR:54.1,1040.0] || -> green(n1,n3)*. % 0.38/0.61 1047[8:Res:1041.0,644.0] || green(n1,n2)* -> . % 0.38/0.61 1048[8:MRR:1047.0,945.0] || -> . % 0.38/0.61 1049[7:Spt:1048.0,39.0,1031.0] || green(n3,n5)*+ -> . % 0.38/0.61 1050[7:Spt:1048.0,39.1] || -> red(n3,n5)*. % 0.38/0.61 1052[7:MRR:638.1,1049.0] || red(n3,n4)*+ -> . % 0.38/0.61 1053[7:MRR:15.1,1052.0] || -> green(n3,n4)*. % 0.38/0.61 1054[7:MRR:41.2,1049.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.61 1057[7:Res:1053.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 1059[8:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.61 1061[8:Res:1059.0,37.0] || green(n2,n5)* -> . % 0.38/0.61 1062[8:MRR:1061.0,975.0] || -> . % 0.38/0.61 1063[8:Spt:1062.0,135.0,1059.0] || green(n2,n6)*+ -> . % 0.38/0.61 1064[8:Spt:1062.0,135.1] || -> red(n2,n6)*. % 0.38/0.61 1068[9:Spt:149.0] || -> green(n1,n5)*. % 0.38/0.61 1087[9:Res:1068.0,976.0] || green(n1,n2)* -> . % 0.38/0.61 1088[9:MRR:1087.0,945.0] || -> . % 0.38/0.61 1089[9:Spt:1088.0,149.0,1068.0] || green(n1,n5)*+ -> . % 0.38/0.61 1090[9:Spt:1088.0,149.1] || -> red(n1,n5)*. % 0.38/0.61 1091[9:MRR:670.1,1089.0] || red(n1,n4)*+ -> . % 0.38/0.61 1092[9:MRR:102.1,1091.0] || -> green(n1,n4)*. % 0.38/0.61 1097[9:Res:1092.0,1057.0] || green(n1,n3)*+ -> . % 0.38/0.61 1098[9:MRR:54.0,1097.0] || -> red(n1,n3)*. % 0.38/0.61 1107[9:Res:1090.0,1054.0] || red(n1,n3)* -> . % 0.38/0.61 1108[9:MRR:1107.0,1098.0] || -> . % 0.38/0.61 1109[5:Spt:1108.0,17.0,945.0] || green(n1,n2)*+ -> . % 0.38/0.61 1110[5:Spt:1108.0,17.1] || -> red(n1,n2)*. % 0.38/0.61 1111[5:MRR:941.0,1110.0] || -> green(n1,n4)*. % 0.38/0.61 1116[6:Spt:54.0] || -> green(n1,n3)*. % 0.38/0.61 1119[7:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.61 1120[7:Res:1119.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 1137[7:Res:1111.0,1120.0] || green(n1,n3)* -> . % 0.38/0.61 1138[7:MRR:1137.0,1116.0] || -> . % 0.38/0.61 1139[7:Spt:1138.0,15.0,1119.0] || green(n3,n4)*+ -> . % 0.38/0.61 1140[7:Spt:1138.0,15.1] || -> red(n3,n4)*. % 0.38/0.61 1141[7:MRR:638.0,1140.0] || -> green(n3,n5)*. % 0.38/0.61 1148[7:Res:1141.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.61 1171[7:Res:975.0,1148.0] || green(n2,n3)* -> . % 0.38/0.61 1173[7:MRR:1171.0,643.0] || -> . % 0.38/0.61 1175[6:Spt:1173.0,54.0,1116.0] || green(n1,n3)*+ -> . % 0.38/0.61 1176[6:Spt:1173.0,54.1] || -> red(n1,n3)*. % 0.38/0.61 1177[6:MRR:185.0,1176.0] || -> green(n1,n6)* green(n3,n6). % 0.38/0.61 1180[7:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 1181[7:Res:1180.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.61 1183[8:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.61 1186[9:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.61 1201[9:Res:1186.0,1181.0] || green(n3,n4)* -> . % 0.38/0.61 1202[9:MRR:1201.0,1183.0] || -> . % 0.38/0.61 1203[9:Spt:1202.0,70.0,1186.0] || green(n3,n6)*+ -> . % 0.38/0.61 1204[9:Spt:1202.0,70.1] || -> red(n3,n6)*. % 0.38/0.61 1205[9:MRR:1177.1,1203.0] || -> green(n1,n6)*. % 0.38/0.61 1211[9:Res:1205.0,1181.0] || green(n1,n4)* -> . % 0.38/0.61 1213[9:MRR:1211.0,1111.0] || -> . % 0.38/0.61 1217[8:Spt:1213.0,15.0,1183.0] || green(n3,n4)*+ -> . % 0.38/0.61 1218[8:Spt:1213.0,15.1] || -> red(n3,n4)*. % 0.38/0.61 1219[8:MRR:638.0,1218.0] || -> green(n3,n5)*. % 0.38/0.61 1229[9:Spt:1177.0] || -> green(n1,n6)*. % 0.38/0.61 1231[9:Res:1229.0,1181.0] || green(n1,n4)* -> . % 0.38/0.61 1233[9:MRR:1231.0,1111.0] || -> . % 0.38/0.61 1237[9:Spt:1233.0,1177.0,1229.0] || green(n1,n6)* -> . % 0.38/0.61 1238[9:Spt:1233.0,1177.1] || -> green(n3,n6)*. % 0.38/0.61 1243[9:Res:1238.0,37.0] || green(n3,n5)* -> . % 0.38/0.61 1244[9:MRR:1243.0,1219.0] || -> . % 0.38/0.61 1245[7:Spt:1244.0,32.0,1180.0] || green(n4,n6)*+ -> . % 0.38/0.61 1246[7:Spt:1244.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 1248[7:MRR:34.2,1245.0] || red(u,n6)+ red(u,n4)* -> . % 0.38/0.61 1269[7:Res:135.1,1248.0] || red(n2,n4)* -> green(n2,n6). % 0.38/0.61 1271[7:MRR:1269.0,939.0] || -> green(n2,n6)*. % 0.38/0.61 1275[7:Res:1271.0,37.0] || green(n2,n5)* -> . % 0.38/0.61 1276[7:MRR:1275.0,975.0] || -> . % 0.38/0.61 1277[3:Spt:1276.0,16.0,643.0] || green(n2,n3)*+ -> . % 0.38/0.61 1278[3:Spt:1276.0,16.1] || -> red(n2,n3)*. % 0.38/0.61 1280[3:MRR:138.0,1278.0] || -> green(n2,n6)* green(n3,n6). % 0.38/0.61 1281[3:MRR:50.0,1278.0] || -> green(n2,n4)* green(n3,n4). % 0.38/0.61 1282[3:MRR:91.0,1278.0] || -> green(n2,n5)* green(n3,n5). % 0.38/0.61 1283[3:MRR:59.2,1277.0] || red(n1,n2)* -> green(n1,n3). % 0.38/0.61 1286[4:Spt:39.0] || -> green(n3,n5)*. % 0.38/0.61 1287[4:Res:1286.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.61 1288[5:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.61 1289[5:Res:1288.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 1290[6:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.61 1292[6:Res:1290.0,37.0] || green(n3,n5)* -> . % 0.38/0.61 1293[6:MRR:1292.0,1286.0] || -> . % 0.38/0.61 1294[6:Spt:1293.0,70.0,1290.0] || green(n3,n6)*+ -> . % 0.38/0.61 1295[6:Spt:1293.0,70.1] || -> red(n3,n6)*. % 0.38/0.61 1296[6:MRR:1280.1,1294.0] || -> green(n2,n6)*. % 0.38/0.61 1299[6:MRR:185.2,1294.0] || red(n1,n3)*+ -> green(n1,n6). % 0.38/0.61 1302[6:Res:1296.0,11.0] || green(u,n6)+ green(u,n2)* -> . % 0.38/0.61 1311[7:Spt:149.0] || -> green(n1,n5)*. % 0.38/0.61 1318[8:Spt:54.0] || -> green(n1,n3)*. % 0.38/0.61 1324[7:Res:1311.0,1287.0] || green(n1,n3)* -> . % 0.38/0.61 1325[8:MRR:1324.0,1318.0] || -> . % 0.38/0.61 1326[8:Spt:1325.0,54.0,1318.0] || green(n1,n3)* -> . % 0.38/0.61 1327[8:Spt:1325.0,54.1] || -> red(n1,n3)*. % 0.38/0.61 1328[8:MRR:1299.0,1327.0] || -> green(n1,n6)*. % 0.38/0.61 1335[8:Res:1328.0,37.0] || green(n1,n5)* -> . % 0.38/0.61 1336[8:MRR:1335.0,1311.0] || -> . % 0.38/0.61 1337[7:Spt:1336.0,149.0,1311.0] || green(n1,n5)*+ -> . % 0.38/0.61 1338[7:Spt:1336.0,149.1] || -> red(n1,n5)*. % 0.38/0.61 1339[7:MRR:670.1,1337.0] || red(n1,n4)*+ -> . % 0.38/0.61 1340[7:MRR:102.1,1339.0] || -> green(n1,n4)*. % 0.38/0.61 1345[8:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 1357[7:Res:1340.0,1289.0] || green(n1,n3)*+ -> . % 0.38/0.61 1362[7:MRR:1283.1,1357.0] || red(n1,n2)*+ -> . % 0.38/0.61 1363[7:MRR:17.1,1362.0] || -> green(n1,n2)*. % 0.38/0.61 1375[8:Res:1345.0,1302.0] || green(n1,n2)* -> . % 0.38/0.61 1376[8:MRR:1375.0,1363.0] || -> . % 0.38/0.61 1377[8:Spt:1376.0,182.0,1345.0] || green(n1,n6)* -> . % 0.38/0.61 1378[8:Spt:1376.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 1379[7:MRR:54.0,1357.0] || -> red(n1,n3)*. % 0.38/0.61 1380[8:MRR:1299.0,1299.1,1379.0,1377.0] || -> . % 0.38/0.61 1382[5:Spt:1380.0,15.0,1288.0] || green(n3,n4)*+ -> . % 0.38/0.61 1383[5:Spt:1380.0,15.1] || -> red(n3,n4)*. % 0.38/0.61 1384[5:MRR:1281.1,1382.0] || -> green(n2,n4)*. % 0.38/0.61 1386[5:MRR:73.0,1383.0] || -> green(n3,n6)* green(n4,n6). % 0.38/0.61 1390[6:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 1391[6:Res:1390.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.61 1393[7:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 1395[7:Res:1393.0,37.0] || green(n1,n5)*+ -> . % 0.38/0.61 1397[7:MRR:670.1,1395.0] || red(n1,n4)*+ -> . % 0.38/0.61 1399[7:MRR:102.1,1397.0] || -> green(n1,n4)*. % 0.38/0.61 1439[7:Res:1393.0,1391.0] || green(n1,n4)* -> . % 0.38/0.61 1441[7:MRR:1439.0,1399.0] || -> . % 0.38/0.61 1442[7:Spt:1441.0,182.0,1393.0] || green(n1,n6)*+ -> . % 0.38/0.61 1443[7:Spt:1441.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 1449[8:Spt:1280.1] || -> green(n3,n6)*. % 0.38/0.61 1452[8:Res:1449.0,37.0] || green(n3,n5)* -> . % 0.38/0.61 1453[8:MRR:1452.0,1286.0] || -> . % 0.38/0.61 1454[8:Spt:1453.0,1280.1,1449.0] || green(n3,n6)* -> . % 0.38/0.61 1455[8:Spt:1453.0,1280.0] || -> green(n2,n6)*. % 0.38/0.61 1461[8:Res:1455.0,1391.0] || green(n2,n4)* -> . % 0.38/0.61 1463[8:MRR:1461.0,1384.0] || -> . % 0.38/0.61 1467[6:Spt:1463.0,32.0,1390.0] || green(n4,n6)* -> . % 0.38/0.61 1468[6:Spt:1463.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 1469[6:MRR:1386.1,1467.0] || -> green(n3,n6)*. % 0.38/0.61 1473[6:Res:1469.0,37.0] || green(n3,n5)* -> . % 0.38/0.61 1474[6:MRR:1473.0,1286.0] || -> . % 0.38/0.61 1475[4:Spt:1474.0,39.0,1286.0] || green(n3,n5)*+ -> . % 0.38/0.61 1476[4:Spt:1474.0,39.1] || -> red(n3,n5)*. % 0.38/0.61 1477[4:MRR:1282.1,1475.0] || -> green(n2,n5)*. % 0.38/0.61 1479[4:MRR:638.1,1475.0] || red(n3,n4)*+ -> . % 0.38/0.61 1480[4:MRR:15.1,1479.0] || -> green(n3,n4)*. % 0.38/0.61 1481[4:MRR:41.2,1475.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.61 1484[4:Res:1477.0,11.0] || green(u,n5)+ green(u,n2)* -> . % 0.38/0.61 1485[4:Res:1480.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.61 1486[5:Spt:149.0] || -> green(n1,n5)*. % 0.38/0.61 1488[6:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.61 1490[7:Spt:17.0] || -> green(n1,n2)*. % 0.38/0.61 1511[6:Res:1488.0,1485.0] || green(n1,n3)*+ -> . % 0.38/0.61 1515[6:MRR:1283.1,1511.0] || red(n1,n2)*+ -> . % 0.38/0.61 1522[5:Res:1486.0,1484.0] || green(n1,n2)*+ -> . % 0.38/0.61 1523[7:MRR:1522.0,1490.0] || -> . % 0.38/0.61 1524[7:Spt:1523.0,17.0,1490.0] || green(n1,n2)* -> . % 0.38/0.61 1525[7:Spt:1523.0,17.1] || -> red(n1,n2)*. % 0.38/0.61 1526[7:MRR:1525.0,1515.0] || -> . % 0.38/0.61 1530[6:Spt:1526.0,102.0,1488.0] || green(n1,n4)*+ -> . % 0.38/0.61 1531[6:Spt:1526.0,102.1] || -> red(n1,n4)*. % 0.38/0.61 1532[5:MRR:17.0,1522.0] || -> red(n1,n2)*. % 0.38/0.61 1543[7:Spt:1280.0] || -> green(n2,n6)*. % 0.38/0.61 1545[7:Res:1543.0,37.0] || green(n2,n5)* -> . % 0.38/0.61 1546[7:MRR:1545.0,1477.0] || -> . % 0.38/0.61 1547[7:Spt:1546.0,1280.0,1543.0] || green(n2,n6)*+ -> . % 0.38/0.61 1548[7:Spt:1546.0,1280.1] || -> green(n3,n6)*. % 0.38/0.61 1550[7:MRR:137.2,1547.0] || red(u,n6)+ red(u,n2)* -> . % 0.38/0.61 1558[0:Res:182.1,34.0] || red(n1,n4)* -> green(n1,n6) green(n4,n6). % 0.38/0.61 1569[7:Res:182.1,1550.0] || red(n1,n2)* -> green(n1,n6). % 0.38/0.61 1570[7:MRR:1569.0,1532.0] || -> green(n1,n6)*. % 0.38/0.61 1572[7:Res:1570.0,37.0] || green(n1,n5)* -> . % 0.38/0.61 1573[7:MRR:1572.0,1486.0] || -> . % 0.38/0.61 1574[5:Spt:1573.0,149.0,1486.0] || green(n1,n5)*+ -> . % 0.38/0.61 1575[5:Spt:1573.0,149.1] || -> red(n1,n5)*. % 0.38/0.61 1576[5:MRR:670.1,1574.0] || red(n1,n4)* -> . % 0.38/0.61 1577[5:MRR:102.1,1576.0] || -> green(n1,n4)*. % 0.38/0.61 1580[5:Res:1575.0,1481.0] || red(n1,n3)* -> . % 0.38/0.61 1582[5:MRR:54.1,1580.0] || -> green(n1,n3)*. % 0.38/0.61 1584[5:Res:1577.0,1485.0] || green(n1,n3)* -> . % 0.38/0.61 1585[5:MRR:1584.0,1582.0] || -> . % 0.38/0.61 1586[1:Spt:1585.0,35.2,36.0] || green(n5,n6)*+ -> . % 0.38/0.61 1587[1:Spt:1585.0,35.0,35.1] || red(n4,n5)*+ -> green(n4,n6). % 0.38/0.61 1590[1:MRR:23.2,1586.0] || red(u,n6)+ red(u,n5)* -> . % 0.38/0.61 1592[2:Spt:17.0] || -> green(n1,n2)*. % 0.38/0.61 1594[3:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.61 1595[3:Res:1594.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.61 1596[4:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.61 1597[4:Res:1596.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.61 1600[5:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.61 1618[1:Res:135.1,1590.0] || red(n2,n5)*+ -> green(n2,n6). % 0.38/0.61 1619[1:Res:182.1,1590.0] || red(n1,n5)*+ -> green(n1,n6). % 0.38/0.61 1621[1:Res:149.1,1619.0] || -> green(n1,n5)* green(n1,n6). % 0.38/0.61 1651[4:Res:1596.0,1595.0] || green(n3,n4)*+ -> . % 0.38/0.61 1654[5:MRR:1651.0,1600.0] || -> . % 0.38/0.61 1657[5:Spt:1654.0,15.0,1600.0] || green(n3,n4)* -> . % 0.38/0.61 1658[5:Spt:1654.0,15.1] || -> red(n3,n4)*. % 0.38/0.61 1660[5:MRR:42.0,1658.0] || -> green(n3,n5)* green(n4,n5). % 0.38/0.61 1661[4:MRR:50.2,1651.0] || red(n2,n3)* -> green(n2,n4). % 0.38/0.61 1662[4:MRR:25.2,1651.0] || red(u,n4)+ red(u,n3)* -> . % 0.38/0.61 1664[6:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.61 1665[6:Res:1664.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.61 1666[7:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.61 1668[7:Res:1666.0,1595.0] || green(n2,n4)*+ -> . % 0.38/0.61 1672[7:MRR:1661.1,1668.0] || red(n2,n3)*+ -> . % 0.38/0.61 1674[7:MRR:16.1,1672.0] || -> green(n2,n3)*. % 0.38/0.61 1692[7:Res:1666.0,1597.0] || green(n2,n3)* -> . % 0.38/0.61 1694[7:MRR:1692.0,1674.0] || -> . % 0.38/0.61 1697[7:Spt:1694.0,135.0,1666.0] || green(n2,n6)*+ -> . % 0.38/0.61 1698[7:Spt:1694.0,135.1] || -> red(n2,n6)*. % 0.38/0.61 1699[7:MRR:1618.1,1697.0] || red(n2,n5)*+ -> . % 0.38/0.61 1700[7:MRR:88.1,1699.0] || -> green(n2,n5)*. % 0.38/0.61 1705[8:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.61 1711[9:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 1714[9:Res:1711.0,1595.0] || green(n1,n4)* -> . % 0.38/0.61 1716[9:MRR:1714.0,1705.0] || -> . % 0.38/0.61 1717[9:Spt:1716.0,182.0,1711.0] || green(n1,n6)*+ -> . % 0.38/0.61 1718[9:Spt:1716.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 1719[9:MRR:1621.1,1717.0] || -> green(n1,n5)*. % 0.38/0.61 1729[7:Res:1700.0,1665.0] || green(n2,n4)*+ -> . % 0.38/0.61 1730[9:Res:1719.0,1665.0] || green(n1,n4)* -> . % 0.38/0.61 1732[9:MRR:1730.0,1705.0] || -> . % 0.38/0.61 1733[8:Spt:1732.0,102.0,1705.0] || green(n1,n4)*+ -> . % 0.38/0.61 1734[8:Spt:1732.0,102.1] || -> red(n1,n4)*. % 0.38/0.61 1736[7:MRR:1661.1,1729.0] || red(n2,n3)*+ -> . % 0.38/0.61 1737[7:MRR:16.1,1736.0] || -> green(n2,n3)*. % 0.38/0.61 1744[8:Res:1734.0,1662.0] || red(n1,n3)* -> . % 0.38/0.61 1745[8:MRR:54.1,1744.0] || -> green(n1,n3)*. % 0.38/0.61 1748[7:Res:1737.0,11.0] || green(u,n3)+ green(u,n2)* -> . % 0.38/0.61 1751[8:Res:1745.0,1748.0] || green(n1,n2)* -> . % 0.38/0.61 1752[8:MRR:1751.0,1592.0] || -> . % 0.38/0.61 1753[6:Spt:1752.0,14.0,1664.0] || green(n4,n5)*+ -> . % 0.38/0.61 1754[6:Spt:1752.0,14.1] || -> red(n4,n5)*. % 0.38/0.61 1755[6:MRR:1660.1,1753.0] || -> green(n3,n5)*. % 0.38/0.61 1759[6:Res:1755.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.61 1760[7:Spt:1621.0] || -> green(n1,n5)*. % 0.38/0.61 1762[8:Spt:16.0] || -> green(n2,n3)*. % 0.38/0.61 1764[9:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 1766[9:Res:1764.0,1597.0] || green(n1,n3)* -> . % 0.38/0.61 1767[9:Res:1764.0,1595.0] || green(n1,n4)* -> . % 0.38/0.61 1768[9:MRR:54.0,1766.0] || -> red(n1,n3)*. % 0.38/0.61 1771[9:MRR:102.0,1767.0] || -> red(n1,n4)*. % 0.38/0.61 1777[9:Res:1771.0,1662.0] || red(n1,n3)* -> . % 0.38/0.61 1778[9:MRR:1777.0,1768.0] || -> . % 0.38/0.61 1779[9:Spt:1778.0,182.0,1764.0] || green(n1,n6)*+ -> . % 0.38/0.61 1780[9:Spt:1778.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 1785[10:Spt:46.0] || -> green(n2,n4)*. % 0.38/0.61 1787[11:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.61 1807[11:Res:1787.0,1759.0] || green(n2,n3)* -> . % 0.38/0.61 1808[7:Res:1760.0,1759.0] || green(n1,n3)*+ -> . % 0.38/0.61 1809[11:MRR:1807.0,1762.0] || -> . % 0.38/0.61 1811[11:Spt:1809.0,88.0,1787.0] || green(n2,n5)*+ -> . % 0.38/0.61 1812[11:Spt:1809.0,88.1] || -> red(n2,n5)*. % 0.38/0.61 1813[7:MRR:54.0,1808.0] || -> red(n1,n3)*. % 0.38/0.61 1815[11:MRR:1618.0,1812.0] || -> green(n2,n6)*. % 0.38/0.61 1824[11:Res:1815.0,1595.0] || green(n2,n4)* -> . % 0.38/0.61 1826[11:MRR:1824.0,1785.0] || -> . % 0.38/0.61 1827[10:Spt:1826.0,46.0,1785.0] || green(n2,n4)*+ -> . % 0.38/0.61 1828[10:Spt:1826.0,46.1] || -> red(n2,n4)*. % 0.38/0.61 1837[11:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.61 1839[11:Res:1837.0,1597.0] || green(n2,n3)* -> . % 0.38/0.61 1841[11:MRR:1839.0,1762.0] || -> . % 0.38/0.61 1842[11:Spt:1841.0,135.0,1837.0] || green(n2,n6)*+ -> . % 0.38/0.61 1843[11:Spt:1841.0,135.1] || -> red(n2,n6)*. % 0.38/0.61 1844[11:MRR:1618.1,1842.0] || red(n2,n5)* -> . % 0.38/0.61 1845[11:MRR:88.1,1844.0] || -> green(n2,n5)*. % 0.38/0.61 1850[11:Res:1845.0,1759.0] || green(n2,n3)* -> . % 0.38/0.61 1851[11:MRR:1850.0,1762.0] || -> . % 0.38/0.61 1852[8:Spt:1851.0,16.0,1762.0] || green(n2,n3)*+ -> . % 0.38/0.61 1853[8:Spt:1851.0,16.1] || -> red(n2,n3)*. % 0.38/0.61 1854[8:MRR:1661.0,1853.0] || -> green(n2,n4)*. % 0.38/0.61 1860[8:Res:1854.0,11.0] || green(u,n4)+ green(u,n2)* -> . % 0.38/0.61 1878[4:Res:102.1,1662.0] || red(n1,n3)* -> green(n1,n4). % 0.38/0.61 1879[7:MRR:1878.0,1813.0] || -> green(n1,n4)*. % 0.38/0.61 1898[8:Res:1879.0,1860.0] || green(n1,n2)* -> . % 0.38/0.61 1899[8:MRR:1898.0,1592.0] || -> . % 0.38/0.61 1900[7:Spt:1899.0,1621.0,1760.0] || green(n1,n5)* -> . % 0.38/0.61 1901[7:Spt:1899.0,1621.1] || -> green(n1,n6)*. % 0.38/0.61 1905[7:Res:1901.0,1597.0] || green(n1,n3)* -> . % 0.38/0.61 1906[7:Res:1901.0,1595.0] || green(n1,n4)* -> . % 0.38/0.61 1907[7:MRR:54.0,1905.0] || -> red(n1,n3)*. % 0.38/0.61 1911[7:MRR:1878.0,1907.0] || -> green(n1,n4)*. % 0.38/0.61 1912[7:MRR:1906.0,1911.0] || -> . % 0.38/0.61 1913[4:Spt:1912.0,70.0,1596.0] || green(n3,n6)*+ -> . % 0.38/0.61 1914[4:Spt:1912.0,70.1] || -> red(n3,n6)*. % 0.38/0.61 1916[4:MRR:185.2,1913.0] || red(n1,n3)* -> green(n1,n6). % 0.38/0.61 1917[4:MRR:138.2,1913.0] || red(n2,n3)* -> green(n2,n6). % 0.38/0.61 1920[4:Res:1914.0,1590.0] || red(n3,n5)*+ -> . % 0.38/0.61 1921[4:MRR:39.1,1920.0] || -> green(n3,n5)*. % 0.38/0.61 1922[4:Res:1921.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.61 1923[5:Spt:16.0] || -> green(n2,n3)*. % 0.38/0.61 1925[6:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.61 1926[6:Res:1925.0,11.0] || green(u,n6)+ green(u,n2)* -> . % 0.38/0.61 1937[7:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 1956[7:Res:1937.0,1926.0] || green(n1,n2)* -> . % 0.38/0.61 1957[7:MRR:1956.0,1592.0] || -> . % 0.38/0.61 1958[7:Spt:1957.0,182.0,1937.0] || green(n1,n6)* -> . % 0.38/0.61 1959[7:Spt:1957.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 1960[7:MRR:1621.1,1958.0] || -> green(n1,n5)*. % 0.38/0.61 1962[7:MRR:1916.1,1958.0] || red(n1,n3)* -> . % 0.38/0.61 1963[7:MRR:54.1,1962.0] || -> green(n1,n3)*. % 0.38/0.61 1969[7:Res:1960.0,1922.0] || green(n1,n3)* -> . % 0.38/0.61 1970[7:MRR:1969.0,1963.0] || -> . % 0.38/0.61 1971[6:Spt:1970.0,135.0,1925.0] || green(n2,n6)* -> . % 0.38/0.61 1972[6:Spt:1970.0,135.1] || -> red(n2,n6)*. % 0.38/0.61 1973[6:MRR:1618.1,1971.0] || red(n2,n5)* -> . % 0.38/0.61 1974[6:MRR:88.1,1973.0] || -> green(n2,n5)*. % 0.38/0.61 1981[6:Res:1974.0,1922.0] || green(n2,n3)* -> . % 0.38/0.61 1982[6:MRR:1981.0,1923.0] || -> . % 0.38/0.61 1983[5:Spt:1982.0,16.0,1923.0] || green(n2,n3)*+ -> . % 0.38/0.61 1984[5:Spt:1982.0,16.1] || -> red(n2,n3)*. % 0.38/0.61 1985[5:MRR:1917.0,1984.0] || -> green(n2,n6)*. % 0.38/0.61 1991[5:Res:1985.0,11.0] || green(u,n6)+ green(u,n2)* -> . % 0.38/0.61 2002[6:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.61 2004[7:Spt:1621.0] || -> green(n1,n5)*. % 0.38/0.61 2006[7:Res:2004.0,1922.0] || green(n1,n3)* -> . % 0.38/0.61 2007[7:MRR:54.0,2006.0] || -> red(n1,n3)*. % 0.38/0.61 2011[7:MRR:1916.0,2007.0] || -> green(n1,n6)*. % 0.38/0.61 2014[7:Res:2011.0,1595.0] || green(n1,n4)* -> . % 0.38/0.61 2015[7:MRR:2014.0,2002.0] || -> . % 0.38/0.61 2016[7:Spt:2015.0,1621.0,2004.0] || green(n1,n5)* -> . % 0.38/0.61 2017[7:Spt:2015.0,1621.1] || -> green(n1,n6)*. % 0.38/0.61 2021[7:Res:2017.0,1595.0] || green(n1,n4)* -> . % 0.38/0.61 2022[7:MRR:2021.0,2002.0] || -> . % 0.38/0.61 2023[6:Spt:2022.0,102.0,2002.0] || green(n1,n4)*+ -> . % 0.38/0.61 2024[6:Spt:2022.0,102.1] || -> red(n1,n4)*. % 0.38/0.61 2029[7:Spt:54.0] || -> green(n1,n3)*. % 0.38/0.61 2032[8:Spt:149.0] || -> green(n1,n5)*. % 0.38/0.61 2034[8:Res:2032.0,1922.0] || green(n1,n3)* -> . % 0.38/0.61 2035[8:MRR:2034.0,2029.0] || -> . % 0.38/0.61 2036[8:Spt:2035.0,149.0,2032.0] || green(n1,n5)*+ -> . % 0.38/0.61 2037[8:Spt:2035.0,149.1] || -> red(n1,n5)*. % 0.38/0.61 2038[8:MRR:1619.0,2037.0] || -> green(n1,n6)*. % 0.38/0.61 2046[8:Res:2038.0,1991.0] || green(n1,n2)* -> . % 0.38/0.61 2047[8:MRR:2046.0,1592.0] || -> . % 0.38/0.61 2048[7:Spt:2047.0,54.0,2029.0] || green(n1,n3)* -> . % 0.38/0.61 2049[7:Spt:2047.0,54.1] || -> red(n1,n3)*. % 0.38/0.61 2050[7:MRR:1916.0,2049.0] || -> green(n1,n6)*. % 0.38/0.61 2055[7:Res:2050.0,1991.0] || green(n1,n2)* -> . % 0.38/0.61 2057[7:MRR:2055.0,1592.0] || -> . % 0.38/0.61 2058[3:Spt:2057.0,32.0,1594.0] || green(n4,n6)*+ -> . % 0.38/0.61 2059[3:Spt:2057.0,32.1] || -> red(n4,n6)*. % 0.38/0.61 2060[3:MRR:1587.1,2058.0] || red(n4,n5)*+ -> . % 0.38/0.61 2061[3:MRR:14.1,2060.0] || -> green(n4,n5)*. % 0.38/0.61 2063[3:MRR:1558.2,2058.0] || red(n1,n4)* -> green(n1,n6). % 0.38/0.61 2064[3:MRR:73.2,2058.0] || red(n3,n4)* -> green(n3,n6). % 0.38/0.61 2065[3:MRR:34.2,2058.0] || red(u,n6)+ red(u,n4)* -> . % 0.38/0.61 2068[3:Res:2061.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.61 2069[4:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.61 2071[5:Spt:149.0] || -> green(n1,n5)*. % 0.38/0.61 2073[6:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 2093[5:Res:2071.0,2068.0] || green(n1,n4)*+ -> . % 0.38/0.61 2132[5:MRR:102.0,2093.0] || -> red(n1,n4)*. % 0.38/0.61 2136[7:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.61 2137[7:Res:2136.0,11.0] || green(u,n6)+ green(u,n2)* -> . % 0.38/0.61 2172[7:Res:2073.0,2137.0] || green(n1,n2)* -> . % 0.38/0.61 2173[7:MRR:2172.0,1592.0] || -> . % 0.38/0.61 2174[7:Spt:2173.0,135.0,2136.0] || green(n2,n6)* -> . % 0.38/0.61 2175[7:Spt:2173.0,135.1] || -> red(n2,n6)*. % 0.38/0.61 2176[7:MRR:1618.1,2174.0] || red(n2,n5)* -> . % 0.38/0.61 2177[7:MRR:88.1,2176.0] || -> green(n2,n5)*. % 0.38/0.61 2181[7:Res:2175.0,2065.0] || red(n2,n4)* -> . % 0.38/0.61 2183[7:MRR:46.1,2181.0] || -> green(n2,n4)*. % 0.38/0.61 2186[7:Res:2177.0,2068.0] || green(n2,n4)* -> . % 0.38/0.61 2187[7:MRR:2186.0,2183.0] || -> . % 0.38/0.61 2188[6:Spt:2187.0,182.0,2073.0] || green(n1,n6)* -> . % 0.38/0.61 2189[6:Spt:2187.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 2191[5:MRR:2063.0,2132.0] || -> green(n1,n6)*. % 0.38/0.61 2192[6:MRR:2191.0,2188.0] || -> . % 0.38/0.61 2195[5:Spt:2192.0,149.0,2071.0] || green(n1,n5)*+ -> . % 0.38/0.61 2196[5:Spt:2192.0,149.1] || -> red(n1,n5)*. % 0.38/0.61 2197[5:MRR:1621.0,2195.0] || -> green(n1,n6)*. % 0.38/0.61 2201[6:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.61 2202[6:Res:2201.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.61 2203[7:Spt:39.0] || -> green(n3,n5)*. % 0.38/0.61 2205[7:Res:2203.0,2068.0] || green(n3,n4)* -> . % 0.38/0.61 2206[7:MRR:2205.0,2069.0] || -> . % 0.38/0.61 2207[7:Spt:2206.0,39.0,2203.0] || green(n3,n5)*+ -> . % 0.38/0.61 2208[7:Spt:2206.0,39.1] || -> red(n3,n5)*. % 0.38/0.61 2211[7:MRR:41.2,2207.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.61 2237[7:Res:2196.0,2211.0] || red(n1,n3)*+ -> . % 0.38/0.61 2250[7:MRR:54.1,2237.0] || -> green(n1,n3)*. % 0.38/0.61 2279[6:Res:2197.0,2202.0] || green(n1,n3)* -> . % 0.38/0.61 2280[7:MRR:2279.0,2250.0] || -> . % 0.38/0.61 2281[6:Spt:2280.0,70.0,2201.0] || green(n3,n6)* -> . % 0.38/0.61 2282[6:Spt:2280.0,70.1] || -> red(n3,n6)*. % 0.38/0.61 2289[6:Res:2282.0,1590.0] || red(n3,n5)* -> . % 0.38/0.61 2290[6:MRR:39.1,2289.0] || -> green(n3,n5)*. % 0.38/0.61 2292[6:Res:2290.0,2068.0] || green(n3,n4)* -> . % 0.38/0.61 2293[6:MRR:2292.0,2069.0] || -> . % 0.38/0.61 2294[4:Spt:2293.0,15.0,2069.0] || green(n3,n4)*+ -> . % 0.38/0.61 2295[4:Spt:2293.0,15.1] || -> red(n3,n4)*. % 0.38/0.61 2296[4:MRR:2064.0,2295.0] || -> green(n3,n6)*. % 0.38/0.61 2298[4:MRR:50.2,2294.0] || red(n2,n3)* -> green(n2,n4). % 0.38/0.61 2299[4:MRR:25.2,2294.0] || red(u,n4)+ red(u,n3)* -> . % 0.38/0.61 2301[4:Res:2296.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.61 2302[5:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.61 2303[5:Res:2302.0,11.0] || green(u,n6)+ green(u,n2)* -> . % 0.38/0.61 2304[6:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.61 2306[7:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.61 2308[7:Res:2306.0,2068.0] || green(n2,n4)*+ -> . % 0.38/0.61 2312[7:MRR:2298.1,2308.0] || red(n2,n3)*+ -> . % 0.38/0.61 2313[7:MRR:16.1,2312.0] || -> green(n2,n3)*. % 0.38/0.61 2332[5:Res:2302.0,2301.0] || green(n2,n3)*+ -> . % 0.38/0.61 2334[7:MRR:2332.0,2313.0] || -> . % 0.38/0.61 2336[7:Spt:2334.0,88.0,2306.0] || green(n2,n5)*+ -> . % 0.38/0.61 2337[7:Spt:2334.0,88.1] || -> red(n2,n5)*. % 0.38/0.61 2350[8:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.61 2363[8:Res:2350.0,2303.0] || green(n1,n2)* -> . % 0.38/0.61 2364[8:MRR:2363.0,1592.0] || -> . % 0.38/0.61 2365[8:Spt:2364.0,182.0,2350.0] || green(n1,n6)* -> . % 0.38/0.61 2366[8:Spt:2364.0,182.1] || -> red(n1,n6)*. % 0.38/0.61 2367[8:MRR:1621.1,2365.0] || -> green(n1,n5)*. % 0.38/0.61 2375[8:Res:2367.0,2068.0] || green(n1,n4)* -> . % 0.38/0.61 2376[8:MRR:2375.0,2304.0] || -> . % 0.38/0.61 2377[6:Spt:2376.0,102.0,2304.0] || green(n1,n4)* -> . % 0.38/0.61 2378[6:Spt:2376.0,102.1] || -> red(n1,n4)*. % 0.38/0.62 2379[6:MRR:2063.0,2378.0] || -> green(n1,n6)*. % 0.38/0.62 2384[6:Res:2378.0,2299.0] || red(n1,n3)* -> . % 0.38/0.62 2385[6:MRR:54.1,2384.0] || -> green(n1,n3)*. % 0.38/0.62 2388[6:Res:2379.0,2301.0] || green(n1,n3)* -> . % 0.38/0.62 2390[6:MRR:2388.0,2385.0] || -> . % 0.38/0.62 2391[5:Spt:2390.0,135.0,2302.0] || green(n2,n6)* -> . % 0.38/0.62 2392[5:Spt:2390.0,135.1] || -> red(n2,n6)*. % 0.38/0.62 2393[5:MRR:1618.1,2391.0] || red(n2,n5)* -> . % 0.38/0.62 2394[5:MRR:88.1,2393.0] || -> green(n2,n5)*. % 0.38/0.62 2397[5:Res:2392.0,2065.0] || red(n2,n4)* -> . % 0.38/0.62 2399[5:MRR:46.1,2397.0] || -> green(n2,n4)*. % 0.38/0.62 2401[5:Res:2394.0,2068.0] || green(n2,n4)* -> . % 0.38/0.62 2402[5:MRR:2401.0,2399.0] || -> . % 0.38/0.62 2403[2:Spt:2402.0,17.0,1592.0] || green(n1,n2)*+ -> . % 0.38/0.62 2404[2:Spt:2402.0,17.1] || -> red(n1,n2)*. % 0.38/0.62 2405[2:MRR:59.0,2404.0] || -> green(n1,n3)* green(n2,n3). % 0.38/0.62 2407[2:MRR:105.0,2404.0] || -> green(n1,n4)* green(n2,n4). % 0.38/0.62 2410[3:Spt:149.0] || -> green(n1,n5)*. % 0.38/0.62 2412[4:Spt:39.0] || -> green(n3,n5)*. % 0.38/0.62 2413[4:Res:2412.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.62 2414[5:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.62 2416[6:Spt:16.0] || -> green(n2,n3)*. % 0.38/0.62 2419[7:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.62 2421[8:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.62 2443[8:Res:2421.0,2413.0] || green(n2,n3)* -> . % 0.38/0.62 2444[4:Res:2410.0,2413.0] || green(n1,n3)*+ -> . % 0.38/0.62 2445[8:MRR:2443.0,2416.0] || -> . % 0.38/0.62 2446[4:MRR:54.0,2444.0] || -> red(n1,n3)*. % 0.38/0.62 2448[8:Spt:2445.0,88.0,2421.0] || green(n2,n5)*+ -> . % 0.38/0.62 2449[8:Spt:2445.0,88.1] || -> red(n2,n5)*. % 0.38/0.62 2456[9:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.62 2457[9:Res:2456.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 2481[9:Res:2410.0,2457.0] || green(n1,n4)* -> . % 0.38/0.62 2483[9:MRR:2481.0,2419.0] || -> . % 0.38/0.62 2484[9:Spt:2483.0,14.0,2456.0] || green(n4,n5)*+ -> . % 0.38/0.62 2485[9:Spt:2483.0,14.1] || -> red(n4,n5)*. % 0.38/0.62 2486[9:MRR:1587.0,2485.0] || -> green(n4,n6)*. % 0.38/0.62 2491[9:Res:2486.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.62 2509[9:Res:2414.0,2491.0] || green(n1,n4)* -> . % 0.38/0.62 2512[9:MRR:2509.0,2419.0] || -> . % 0.38/0.62 2513[7:Spt:2512.0,102.0,2419.0] || green(n1,n4)*+ -> . % 0.38/0.62 2514[7:Spt:2512.0,102.1] || -> red(n1,n4)*. % 0.38/0.62 2515[7:MRR:2407.0,2513.0] || -> green(n2,n4)*. % 0.38/0.62 2519[8:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.62 2520[8:Res:2519.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.62 2522[9:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.62 2523[9:Res:2522.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.62 2548[9:Res:2515.0,2523.0] || green(n2,n3)* -> . % 0.38/0.62 2549[9:MRR:2548.0,2416.0] || -> . % 0.38/0.62 2550[9:Spt:2549.0,15.0,2522.0] || green(n3,n4)*+ -> . % 0.38/0.62 2551[9:Spt:2549.0,15.1] || -> red(n3,n4)*. % 0.38/0.62 2556[10:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.62 2558[10:Res:2556.0,2413.0] || green(n2,n3)* -> . % 0.38/0.62 2560[10:MRR:2558.0,2416.0] || -> . % 0.38/0.62 2561[10:Spt:2560.0,88.0,2556.0] || green(n2,n5)*+ -> . % 0.38/0.62 2562[10:Spt:2560.0,88.1] || -> red(n2,n5)*. % 0.38/0.62 2563[10:MRR:1618.0,2562.0] || -> green(n2,n6)*. % 0.38/0.62 2578[10:Res:2563.0,2520.0] || green(n2,n3)* -> . % 0.38/0.62 2580[10:MRR:2578.0,2416.0] || -> . % 0.38/0.62 2581[8:Spt:2580.0,70.0,2519.0] || green(n3,n6)*+ -> . % 0.38/0.62 2582[8:Spt:2580.0,70.1] || -> red(n3,n6)*. % 0.38/0.62 2589[9:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.62 2590[9:Res:2589.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 2615[9:Res:2412.0,2590.0] || green(n3,n4)*+ -> . % 0.38/0.62 2621[9:MRR:25.2,2615.0] || red(u,n4)+ red(u,n3)* -> . % 0.38/0.62 2626[9:Res:2514.0,2621.0] || red(n1,n3)* -> . % 0.38/0.62 2628[9:MRR:2626.0,2446.0] || -> . % 0.38/0.62 2629[9:Spt:2628.0,14.0,2589.0] || green(n4,n5)*+ -> . % 0.38/0.62 2630[9:Spt:2628.0,14.1] || -> red(n4,n5)*. % 0.38/0.62 2631[9:MRR:1587.0,2630.0] || -> green(n4,n6)*. % 0.38/0.62 2635[9:Res:2631.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.62 2639[10:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.62 2641[10:Res:2639.0,2413.0] || green(n2,n3)* -> . % 0.38/0.62 2643[10:MRR:2641.0,2416.0] || -> . % 0.38/0.62 2644[10:Spt:2643.0,88.0,2639.0] || green(n2,n5)*+ -> . % 0.38/0.62 2645[10:Spt:2643.0,88.1] || -> red(n2,n5)*. % 0.38/0.62 2646[10:MRR:1618.0,2645.0] || -> green(n2,n6)*. % 0.38/0.62 2655[10:Res:2646.0,2635.0] || green(n2,n4)* -> . % 0.38/0.62 2657[10:MRR:2655.0,2515.0] || -> . % 0.38/0.62 2658[6:Spt:2657.0,16.0,2416.0] || green(n2,n3)* -> . % 0.38/0.62 2659[6:Spt:2657.0,16.1] || -> red(n2,n3)*. % 0.38/0.62 2660[4:MRR:2405.0,2444.0] || -> green(n2,n3)*. % 0.38/0.62 2661[6:MRR:2660.0,2658.0] || -> . % 0.38/0.62 2666[5:Spt:2661.0,182.0,2414.0] || green(n1,n6)*+ -> . % 0.38/0.62 2667[5:Spt:2661.0,182.1] || -> red(n1,n6)*. % 0.38/0.62 2669[4:MRR:185.0,2446.0] || -> green(n1,n6)* green(n3,n6). % 0.38/0.62 2670[5:MRR:2669.0,2666.0] || -> green(n3,n6)*. % 0.38/0.62 2676[5:Res:2670.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.62 2677[6:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.62 2747[6:Res:2677.0,2676.0] || green(n2,n3)* -> . % 0.38/0.62 2748[6:MRR:2747.0,2660.0] || -> . % 0.38/0.62 2749[6:Spt:2748.0,135.0,2677.0] || green(n2,n6)* -> . % 0.38/0.62 2750[6:Spt:2748.0,135.1] || -> red(n2,n6)*. % 0.38/0.62 2751[6:MRR:1618.1,2749.0] || red(n2,n5)* -> . % 0.38/0.62 2752[6:MRR:88.1,2751.0] || -> green(n2,n5)*. % 0.38/0.62 2758[6:Res:2752.0,2413.0] || green(n2,n3)* -> . % 0.38/0.62 2760[6:MRR:2758.0,2660.0] || -> . % 0.38/0.62 2761[4:Spt:2760.0,39.0,2412.0] || green(n3,n5)*+ -> . % 0.38/0.62 2762[4:Spt:2760.0,39.1] || -> red(n3,n5)*. % 0.38/0.62 2764[4:MRR:91.2,2761.0] || red(n2,n3)* -> green(n2,n5). % 0.38/0.62 2765[4:MRR:42.1,2761.0] || red(n3,n4)* -> green(n4,n5). % 0.38/0.62 2768[5:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.62 2769[5:Res:2768.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.62 2770[6:Spt:2407.0] || -> green(n1,n4)*. % 0.38/0.62 2772[7:Spt:46.0] || -> green(n2,n4)*. % 0.38/0.62 2793[7:Res:2772.0,2769.0] || green(n2,n3)* -> . % 0.38/0.62 2794[6:Res:2770.0,2769.0] || green(n1,n3)*+ -> . % 0.38/0.62 2796[6:MRR:54.0,2794.0] || -> red(n1,n3)*. % 0.38/0.62 2800[7:MRR:2405.0,2405.1,2794.0,2793.0] || -> . % 0.38/0.62 2802[6:MRR:185.0,2796.0] || -> green(n1,n6)* green(n3,n6). % 0.38/0.62 2804[7:Spt:2800.0,46.0,2772.0] || green(n2,n4)*+ -> . % 0.38/0.62 2805[7:Spt:2800.0,46.1] || -> red(n2,n4)*. % 0.38/0.62 2812[8:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.62 2863[9:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.62 2864[9:Res:2863.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 2874[9:Res:2410.0,2864.0] || green(n1,n4)* -> . % 0.38/0.62 2875[9:MRR:2874.0,2770.0] || -> . % 0.38/0.62 2876[9:Spt:2875.0,14.0,2863.0] || green(n4,n5)*+ -> . % 0.38/0.62 2877[9:Spt:2875.0,14.1] || -> red(n4,n5)*. % 0.38/0.62 2878[9:MRR:1587.0,2877.0] || -> green(n4,n6)*. % 0.38/0.62 2884[9:Res:2878.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.62 2895[9:Res:2812.0,2884.0] || green(n1,n4)* -> . % 0.38/0.62 2897[9:MRR:2895.0,2770.0] || -> . % 0.38/0.62 2898[8:Spt:2897.0,182.0,2812.0] || green(n1,n6)*+ -> . % 0.38/0.62 2899[8:Spt:2897.0,182.1] || -> red(n1,n6)*. % 0.38/0.62 2900[8:MRR:2802.0,2898.0] || -> green(n3,n6)*. % 0.38/0.62 2907[9:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.62 2908[9:Res:2907.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 2917[9:Res:2410.0,2908.0] || green(n1,n4)* -> . % 0.38/0.62 2918[9:MRR:2917.0,2770.0] || -> . % 0.38/0.62 2919[9:Spt:2918.0,14.0,2907.0] || green(n4,n5)*+ -> . % 0.38/0.62 2920[9:Spt:2918.0,14.1] || -> red(n4,n5)*. % 0.38/0.62 2921[9:MRR:1587.0,2920.0] || -> green(n4,n6)*. % 0.38/0.62 2927[9:Res:2921.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.62 2936[9:Res:2900.0,2927.0] || green(n3,n4)* -> . % 0.38/0.62 2938[9:MRR:2936.0,2768.0] || -> . % 0.38/0.62 2939[6:Spt:2938.0,2407.0,2770.0] || green(n1,n4)*+ -> . % 0.38/0.62 2940[6:Spt:2938.0,2407.1] || -> green(n2,n4)*. % 0.38/0.62 2945[6:Res:2940.0,2769.0] || green(n2,n3)*+ -> . % 0.38/0.62 2946[6:MRR:2405.1,2945.0] || -> green(n1,n3)*. % 0.38/0.62 2947[6:MRR:16.0,2945.0] || -> red(n2,n3)*. % 0.38/0.62 2950[6:MRR:2764.0,2947.0] || -> green(n2,n5)*. % 0.38/0.62 2957[7:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.62 2959[8:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.62 2960[8:Res:2959.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 2973[8:Res:2950.0,2960.0] || green(n2,n4)* -> . % 0.38/0.62 2975[8:MRR:2973.0,2940.0] || -> . % 0.38/0.62 2976[8:Spt:2975.0,14.0,2959.0] || green(n4,n5)*+ -> . % 0.38/0.62 2977[8:Spt:2975.0,14.1] || -> red(n4,n5)*. % 0.38/0.62 2978[8:MRR:1587.0,2977.0] || -> green(n4,n6)*. % 0.38/0.62 2984[8:Res:2978.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.62 2990[1:Res:70.1,1590.0] || red(n3,n5)* -> green(n3,n6). % 0.38/0.62 2991[4:MRR:2990.0,2762.0] || -> green(n3,n6)*. % 0.38/0.62 2992[4:Res:2991.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.62 3002[8:Res:2957.0,2984.0] || green(n2,n4)* -> . % 0.38/0.62 3005[8:MRR:3002.0,2940.0] || -> . % 0.38/0.62 3006[7:Spt:3005.0,135.0,2957.0] || green(n2,n6)*+ -> . % 0.38/0.62 3007[7:Spt:3005.0,135.1] || -> red(n2,n6)*. % 0.38/0.62 3009[7:MRR:137.2,3006.0] || red(u,n6)+ red(u,n2)* -> . % 0.38/0.62 3012[8:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.62 3035[8:Res:3012.0,2992.0] || green(n1,n3)* -> . % 0.38/0.62 3036[8:MRR:3035.0,2946.0] || -> . % 0.38/0.62 3037[8:Spt:3036.0,182.0,3012.0] || green(n1,n6)*+ -> . % 0.38/0.62 3038[8:Spt:3036.0,182.1] || -> red(n1,n6)*. % 0.38/0.62 3051[8:Res:3038.0,3009.0] || red(n1,n2)* -> . % 0.38/0.62 3053[8:MRR:3051.0,2404.0] || -> . % 0.38/0.62 3054[5:Spt:3053.0,15.0,2768.0] || green(n3,n4)*+ -> . % 0.38/0.62 3055[5:Spt:3053.0,15.1] || -> red(n3,n4)*. % 0.38/0.62 3056[5:MRR:2765.0,3055.0] || -> green(n4,n5)*. % 0.38/0.62 3058[5:MRR:25.2,3054.0] || red(u,n4)+ red(u,n3)* -> . % 0.38/0.62 3060[5:Res:3056.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 3065[6:Spt:16.0] || -> green(n2,n3)*. % 0.38/0.62 3067[7:Spt:182.0] || -> green(n1,n6)*. % 0.38/0.62 3069[7:Res:3067.0,2992.0] || green(n1,n3)*+ -> . % 0.38/0.62 3070[7:MRR:54.0,3069.0] || -> red(n1,n3)*. % 0.38/0.62 3090[5:Res:102.1,3058.0] || red(n1,n3)* -> green(n1,n4). % 0.38/0.62 3091[7:MRR:3090.0,3070.0] || -> green(n1,n4)*. % 0.38/0.62 3095[5:Res:2410.0,3060.0] || green(n1,n4)* -> . % 0.38/0.62 3097[7:MRR:3095.0,3091.0] || -> . % 0.38/0.62 3098[7:Spt:3097.0,182.0,3067.0] || green(n1,n6)*+ -> . % 0.38/0.62 3099[7:Spt:3097.0,182.1] || -> red(n1,n6)*. % 0.38/0.62 3100[5:MRR:2407.0,3095.0] || -> green(n2,n4)*. % 0.38/0.62 3113[8:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.62 3115[8:Res:3113.0,3060.0] || green(n2,n4)* -> . % 0.38/0.62 3117[8:MRR:3115.0,3100.0] || -> . % 0.38/0.62 3118[8:Spt:3117.0,88.0,3113.0] || green(n2,n5)* -> . % 0.38/0.62 3119[8:Spt:3117.0,88.1] || -> red(n2,n5)*. % 0.38/0.62 3120[8:MRR:1618.0,3119.0] || -> green(n2,n6)*. % 0.38/0.62 3127[8:Res:3120.0,2992.0] || green(n2,n3)* -> . % 0.38/0.62 3128[8:MRR:3127.0,3065.0] || -> . % 0.38/0.62 3129[6:Spt:3128.0,16.0,3065.0] || green(n2,n3)* -> . % 0.38/0.62 3130[6:Spt:3128.0,16.1] || -> red(n2,n3)*. % 0.38/0.62 3131[6:MRR:2764.0,3130.0] || -> green(n2,n5)*. % 0.38/0.62 3136[6:Res:3131.0,3060.0] || green(n2,n4)* -> . % 0.38/0.62 3138[6:MRR:3136.0,3100.0] || -> . % 0.38/0.62 3139[3:Spt:3138.0,149.0,2410.0] || green(n1,n5)*+ -> . % 0.38/0.62 3140[3:Spt:3138.0,149.1] || -> red(n1,n5)*. % 0.38/0.62 3141[3:MRR:1619.0,3140.0] || -> green(n1,n6)*. % 0.38/0.62 3145[4:Spt:16.0] || -> green(n2,n3)*. % 0.38/0.62 3147[5:Spt:135.0] || -> green(n2,n6)*. % 0.38/0.62 3151[6:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.62 3152[6:Res:3151.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.62 3210[6:Res:3147.0,3152.0] || green(n2,n4)* -> . % 0.38/0.62 3211[6:Res:3141.0,3152.0] || green(n1,n4)* -> . % 0.38/0.62 3222[6:MRR:2407.0,2407.1,3211.0,3210.0] || -> . % 0.38/0.62 3230[6:Spt:3222.0,32.0,3151.0] || green(n4,n6)*+ -> . % 0.38/0.62 3231[6:Spt:3222.0,32.1] || -> red(n4,n6)*. % 0.38/0.62 3232[6:MRR:1587.1,3230.0] || red(n4,n5)*+ -> . % 0.38/0.62 3233[6:MRR:14.1,3232.0] || -> green(n4,n5)*. % 0.38/0.62 3235[6:MRR:73.2,3230.0] || red(n3,n4)* -> green(n3,n6). % 0.38/0.62 3239[6:Res:3233.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 3241[7:Spt:70.0] || -> green(n3,n6)*. % 0.38/0.62 3242[7:Res:3241.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.62 3280[7:Res:3147.0,3242.0] || green(n2,n3)* -> . % 0.38/0.62 3282[7:MRR:3280.0,3145.0] || -> . % 0.38/0.62 3283[7:Spt:3282.0,70.0,3241.0] || green(n3,n6)* -> . % 0.38/0.62 3284[7:Spt:3282.0,70.1] || -> red(n3,n6)*. % 0.38/0.62 3285[7:MRR:2990.1,3283.0] || red(n3,n5)* -> . % 0.38/0.62 3286[7:MRR:39.1,3285.0] || -> green(n3,n5)*. % 0.38/0.62 3288[7:MRR:3235.1,3283.0] || red(n3,n4)* -> . % 0.38/0.62 3289[7:MRR:15.1,3288.0] || -> green(n3,n4)*. % 0.38/0.62 3295[7:Res:3286.0,3239.0] || green(n3,n4)* -> . % 0.38/0.62 3297[7:MRR:3295.0,3289.0] || -> . % 0.38/0.62 3298[5:Spt:3297.0,135.0,3147.0] || green(n2,n6)*+ -> . % 0.38/0.62 3299[5:Spt:3297.0,135.1] || -> red(n2,n6)*. % 0.38/0.62 3300[5:MRR:1618.1,3298.0] || red(n2,n5)*+ -> . % 0.38/0.62 3301[5:MRR:88.1,3300.0] || -> green(n2,n5)*. % 0.38/0.62 3308[6:Spt:39.0] || -> green(n3,n5)*. % 0.38/0.62 3309[6:Res:3308.0,11.0] || green(u,n5)+ green(u,n3)* -> . % 0.38/0.62 3371[6:Res:3301.0,3309.0] || green(n2,n3)* -> . % 0.38/0.62 3372[6:MRR:3371.0,3145.0] || -> . % 0.38/0.62 3373[6:Spt:3372.0,39.0,3308.0] || green(n3,n5)*+ -> . % 0.38/0.62 3374[6:Spt:3372.0,39.1] || -> red(n3,n5)*. % 0.38/0.62 3375[6:MRR:2990.0,3374.0] || -> green(n3,n6)*. % 0.38/0.62 3378[6:MRR:41.2,3373.0] || red(u,n5)+ red(u,n3)* -> . % 0.38/0.62 3381[6:Res:3375.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.62 3395[6:Res:3140.0,3378.0] || red(n1,n3)*+ -> . % 0.38/0.62 3397[6:MRR:54.1,3395.0] || -> green(n1,n3)*. % 0.38/0.62 3402[6:Res:3141.0,3381.0] || green(n1,n3)* -> . % 0.38/0.62 3403[6:MRR:3402.0,3397.0] || -> . % 0.38/0.62 3404[4:Spt:3403.0,16.0,3145.0] || green(n2,n3)*+ -> . % 0.38/0.62 3405[4:Spt:3403.0,16.1] || -> red(n2,n3)*. % 0.38/0.62 3406[4:MRR:2405.1,3404.0] || -> green(n1,n3)*. % 0.38/0.62 3408[4:MRR:50.0,3405.0] || -> green(n2,n4)* green(n3,n4). % 0.38/0.62 3409[4:MRR:91.0,3405.0] || -> green(n2,n5)* green(n3,n5). % 0.38/0.62 3414[5:Spt:32.0] || -> green(n4,n6)*. % 0.38/0.62 3415[5:Res:3414.0,11.0] || green(u,n6)+ green(u,n4)* -> . % 0.38/0.62 3417[6:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.62 3418[6:Res:3417.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.62 3419[7:Spt:102.0] || -> green(n1,n4)*. % 0.38/0.62 3435[7:Res:3419.0,3418.0] || green(n1,n3)* -> . % 0.38/0.62 3436[7:MRR:3435.0,3406.0] || -> . % 0.38/0.62 3437[7:Spt:3436.0,102.0,3419.0] || green(n1,n4)*+ -> . % 0.38/0.62 3438[7:Spt:3436.0,102.1] || -> red(n1,n4)*. % 0.38/0.62 3439[7:MRR:2407.0,3437.0] || -> green(n2,n4)*. % 0.38/0.62 3447[8:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.62 3448[8:Res:3447.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 3449[9:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.62 3458[9:Res:3449.0,3448.0] || green(n2,n4)* -> . % 0.38/0.62 3460[9:MRR:3458.0,3439.0] || -> . % 0.38/0.62 3461[9:Spt:3460.0,88.0,3449.0] || green(n2,n5)* -> . % 0.38/0.62 3462[9:Spt:3460.0,88.1] || -> red(n2,n5)*. % 0.38/0.62 3463[9:MRR:3409.0,3461.0] || -> green(n3,n5)*. % 0.38/0.62 3468[9:Res:3463.0,3448.0] || green(n3,n4)* -> . % 0.38/0.62 3469[9:MRR:3468.0,3417.0] || -> . % 0.38/0.62 3470[8:Spt:3469.0,14.0,3447.0] || green(n4,n5)*+ -> . % 0.38/0.62 3471[8:Spt:3469.0,14.1] || -> red(n4,n5)*. % 0.38/0.62 3474[8:MRR:24.2,3470.0] || red(u,n5)+ red(u,n4)* -> . % 0.38/0.62 3485[8:Res:3140.0,3474.0] || red(n1,n4)* -> . % 0.38/0.62 3487[8:MRR:3485.0,3438.0] || -> . % 0.38/0.62 3488[6:Spt:3487.0,15.0,3417.0] || green(n3,n4)*+ -> . % 0.38/0.62 3489[6:Spt:3487.0,15.1] || -> red(n3,n4)*. % 0.38/0.62 3490[6:MRR:3408.1,3488.0] || -> green(n2,n4)*. % 0.38/0.62 3499[7:Spt:14.0] || -> green(n4,n5)*. % 0.38/0.62 3500[7:Res:3499.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 3501[8:Spt:3409.0] || -> green(n2,n5)*. % 0.38/0.62 3512[8:Res:3501.0,3500.0] || green(n2,n4)* -> . % 0.38/0.62 3513[8:MRR:3512.0,3490.0] || -> . % 0.38/0.62 3514[8:Spt:3513.0,3409.0,3501.0] || green(n2,n5)*+ -> . % 0.38/0.62 3515[8:Spt:3513.0,3409.1] || -> green(n3,n5)*. % 0.38/0.62 3516[8:MRR:88.0,3514.0] || -> red(n2,n5)*. % 0.38/0.62 3517[8:MRR:1618.0,3516.0] || -> green(n2,n6)*. % 0.38/0.62 3529[8:Res:3517.0,3415.0] || green(n2,n4)* -> . % 0.38/0.62 3530[5:Res:3141.0,3415.0] || green(n1,n4)*+ -> . % 0.38/0.62 3531[8:MRR:3529.0,3490.0] || -> . % 0.38/0.62 3532[5:MRR:102.0,3530.0] || -> red(n1,n4)*. % 0.38/0.62 3535[7:Spt:3531.0,14.0,3499.0] || green(n4,n5)*+ -> . % 0.38/0.62 3536[7:Spt:3531.0,14.1] || -> red(n4,n5)*. % 0.38/0.62 3539[7:MRR:24.2,3535.0] || red(u,n5)+ red(u,n4)* -> . % 0.38/0.62 3546[7:Res:3140.0,3539.0] || red(n1,n4)* -> . % 0.38/0.62 3547[7:MRR:3546.0,3532.0] || -> . % 0.38/0.62 3548[5:Spt:3547.0,32.0,3414.0] || green(n4,n6)*+ -> . % 0.38/0.62 3549[5:Spt:3547.0,32.1] || -> red(n4,n6)*. % 0.38/0.62 3550[5:MRR:1587.1,3548.0] || red(n4,n5)*+ -> . % 0.38/0.62 3551[5:MRR:14.1,3550.0] || -> green(n4,n5)*. % 0.38/0.62 3553[5:MRR:73.2,3548.0] || red(n3,n4)* -> green(n3,n6). % 0.38/0.62 3557[5:Res:3551.0,11.0] || green(u,n5)+ green(u,n4)* -> . % 0.38/0.62 3558[6:Spt:15.0] || -> green(n3,n4)*. % 0.38/0.62 3559[6:Res:3558.0,11.0] || green(u,n4)+ green(u,n3)* -> . % 0.38/0.62 3560[7:Spt:88.0] || -> green(n2,n5)*. % 0.38/0.62 3577[7:Res:3560.0,3557.0] || green(n2,n4)*+ -> . % 0.38/0.62 3582[7:MRR:2407.1,3577.0] || -> green(n1,n4)*. % 0.38/0.62 3596[7:Res:3582.0,3559.0] || green(n1,n3)* -> . % 0.38/0.62 3597[7:MRR:3596.0,3406.0] || -> . % 0.38/0.62 3598[7:Spt:3597.0,88.0,3560.0] || green(n2,n5)* -> . % 0.38/0.62 3599[7:Spt:3597.0,88.1] || -> red(n2,n5)*. % 0.38/0.62 3600[7:MRR:3409.0,3598.0] || -> green(n3,n5)*. % 0.38/0.62 3607[7:Res:3600.0,3557.0] || green(n3,n4)* -> . % 0.38/0.62 3608[7:MRR:3607.0,3558.0] || -> . % 0.38/0.62 3609[6:Spt:3608.0,15.0,3558.0] || green(n3,n4)*+ -> . % 0.38/0.62 3610[6:Spt:3608.0,15.1] || -> red(n3,n4)*. % 0.38/0.62 3611[6:MRR:3553.0,3610.0] || -> green(n3,n6)*. % 0.38/0.62 3616[6:Res:3611.0,11.0] || green(u,n6)+ green(u,n3)* -> . % 0.38/0.62 3640[6:Res:3141.0,3616.0] || green(n1,n3)* -> . % 0.38/0.62 3641[6:MRR:3640.0,3406.0] || -> . % 0.38/0.62 % SZS output end Refutation % 0.38/0.62 Formulae used in the proof : goal_to_be_proved ordering partition less_than_transitive red_clique green_clique % 0.38/0.62 %------------------------------------------------------------------------------