%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL642+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:07:51 PM UTC 2026 % Result : Theorem 11.36s 11.67s % Output : Refutation 15.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL642+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.35 % Computer : n017.cluster.edu % 0.11/0.35 % Model : x86_64 x86_64 % 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.35 % Memory : 8046.5625MB % 0.11/0.35 % OS : Linux 6.8.0-71-generic % 0.11/0.35 % CPULimit : 300 % 0.11/0.35 % WCLimit : 300 % 0.11/0.35 % DateTime : Sat Sep 5 11:59:06 UTC 2026 % 0.14/0.36 % CPUTime : % 11.36/11.67 % 11.36/11.67 SPASS V 3.9 % 11.36/11.67 SPASS beiseite: Proof found. % 11.36/11.67 % SZS status Theorem % 11.36/11.67 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 11.36/11.67 SPASS derived 21703 clauses, backtracked 6394 clauses, performed 370 splits and kept 12080 clauses. % 11.36/11.67 SPASS allocated 117163 KBytes. % 11.36/11.67 SPASS spent 0:0:11.27 on the problem. % 11.36/11.67 0:00:00.06 for the input. % 11.36/11.67 0:00:00.15 for the FLOTTER CNF translation. % 11.36/11.67 0:00:00.80 for inferences. % 11.36/11.67 0:00:00.26 for the backtracking. % 11.36/11.67 0:00:09.69 for the reduction. % 11.36/11.67 % 11.36/11.67 % 11.36/11.67 Here is a proof with depth 8, length 787 : % 11.36/11.67 % SZS output start Refutation % 11.36/11.67 2[0:Inp] || -> r1(skc5,skc8)*. % 11.36/11.67 3[0:Inp] || -> r1(skc5,skc6)*. % 11.36/11.67 5[0:Inp] || p2(skc8)* -> . % 11.36/11.67 7[0:Inp] || p2(skf34(u))* -> . % 11.36/11.67 8[0:Inp] || p2(skf32(u))* -> . % 11.36/11.67 9[0:Inp] || p2(skf30(u))* -> . % 11.36/11.67 10[0:Inp] || p2(skf26(u))* -> . % 11.36/11.67 11[0:Inp] || p2(skf25(u))* -> . % 11.36/11.67 12[0:Inp] || p2(skf23(u))* -> . % 11.36/11.67 14[0:Inp] || p2(skf19(u))* -> . % 11.36/11.67 16[0:Inp] || -> r1(skf33(u),skf34(u))*. % 11.36/11.67 17[0:Inp] || -> r1(skf31(u),skf32(u))*. % 11.36/11.67 18[0:Inp] || -> r1(skf24(u),skf25(u))*. % 11.36/11.67 20[0:Inp] || -> r1(skf18(u),skf19(u))*. % 11.36/11.67 22[0:Inp] || -> SkP1(skc5) r1(skc5,skc12)*. % 11.36/11.67 23[0:Inp] || SkP1(skc12) -> SkP1(skc5)*. % 11.36/11.67 24[0:Inp] SkP1(u) || -> SkP0(u)*. % 11.36/11.67 25[0:Inp] || -> SkP0(u) r1(u,skf29(u))*. % 11.36/11.67 26[0:Inp] || -> SkP0(u)* r1(skf29(v),skf30(v))*. % 11.36/11.67 27[0:Inp] SkP1(u) || -> p2(u) p2(skf33(u))*. % 11.36/11.67 28[0:Inp] SkP0(u) p2(u) || -> SkP1(u)*. % 11.36/11.67 30[0:Inp] || r1(skc5,u) -> p2(u) p2(skf18(u))*. % 11.36/11.67 32[0:Inp] SkP1(u) || -> p2(u) r1(u,skf33(u))*. % 11.36/11.67 33[0:Inp] SkP2(u) || r1(u,v)* -> SkP1(v). % 11.36/11.67 34[0:Inp] || r1(skc5,u) -> p3(u) r1(u,skf16(u))*. % 11.36/11.67 35[0:Inp] || r1(skc5,u) -> p2(u) r1(u,skf18(u))*. % 11.36/11.67 36[0:Inp] || r1(skc5,u) -> p1(u) r1(u,skf20(u))*. % 11.36/11.67 37[0:Inp] || r1(skc5,u) -> p2(u) r1(u,skf23(u))*. % 11.36/11.67 38[0:Inp] SkP1(u) || r1(skc12,u)* -> SkP2(u) SkP1(skc5). % 11.36/11.67 39[0:Inp] || r1(u,v)*+ -> SkP0(u) p2(v) p2(skf31(v))*. % 11.36/11.67 40[0:Inp] || r1(u,v)*+ -> SkP0(u) p2(v) r1(v,skf31(v))*. % 11.36/11.67 41[0:Inp] p2(u) || r1(u,v)* r1(skf30(w),u)*+ -> SkP0(x)* p2(v). % 11.36/11.67 42[0:Inp] SkP0(u) p2(v) || r1(v,w)*+ r1(u,v)* -> SkP1(u) p2(w). % 11.36/11.67 43[0:Inp] SkP0(u) || r1(v,w)*+ r1(u,v)* -> p2(w) p2(skf24(w))* r1(u,skf26(u))*. % 11.36/11.67 44[0:Inp] p2(u) || r1(u,v)* r1(skc5,w) r1(skf23(w),u)*+ -> p2(w) p2(v). % 11.36/11.67 45[0:Inp] SkP0(u) || r1(v,w)*+ r1(u,v)* -> p2(w) r1(w,skf24(w))* r1(u,skf26(u))*. % 11.36/11.67 46[0:Inp] SkP0(u) p2(v) || r1(w,x)* r1(u,w)* r1(v,y)* r1(skf26(u),v)*+ -> p2(x) p2(y) p2(skf24(x))*. % 11.36/11.67 47[0:Inp] SkP0(u) p2(v) || r1(w,x)* r1(u,w)* r1(v,y)* r1(skf26(u),v)*+ -> p2(x) p2(y) r1(x,skf24(x))*. % 11.36/11.67 89[1:Spt:41.0,41.1,41.2,41.4] p2(u) || r1(u,v)* r1(skf30(w),u)*+ -> p2(v). % 11.36/11.67 90[2:Spt:26.0] || -> SkP0(u)*. % 11.36/11.67 92[2:MRR:42.0,90.0] p2(u) || r1(u,v)*+ r1(w,u)* -> SkP1(w) p2(v). % 11.36/11.67 93[2:MRR:43.0,90.0] || r1(u,v)*+ r1(w,u)* -> p2(v) p2(skf24(v))* r1(w,skf26(w))*. % 11.36/11.67 94[2:MRR:45.0,90.0] || r1(u,v)*+ r1(w,u)* -> p2(v) r1(v,skf24(v))* r1(w,skf26(w))*. % 11.36/11.67 95[2:MRR:46.0,90.0] p2(u) || r1(v,w)* r1(x,v)* r1(u,y)* r1(skf26(x),u)*+ -> p2(w) p2(y) p2(skf24(w))*. % 11.36/11.67 96[2:MRR:47.0,90.0] p2(u) || r1(v,w)* r1(x,v)* r1(u,y)* r1(skf26(x),u)*+ -> p2(w) p2(y) r1(w,skf24(w))*. % 11.36/11.67 98[1:Res:32.2,89.2] SkP1(skf30(u)) p2(skf33(skf30(u))) || r1(skf33(skf30(u)),v)* -> p2(skf30(u)) p2(v). % 11.36/11.67 100[1:MRR:98.1,98.3,27.2,9.0] SkP1(skf30(u)) || r1(skf33(skf30(u)),v)* -> p2(v). % 11.36/11.67 139[2:Res:18.0,92.1] p2(skf24(u)) || r1(v,skf24(u))* -> SkP1(v) p2(skf25(u)). % 11.36/11.67 144[2:MRR:139.3,11.0] p2(skf24(u)) || r1(v,skf24(u))* -> SkP1(v). % 11.36/11.67 152[2:Res:37.2,93.0] || r1(skc5,u) r1(v,u)* -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))* r1(v,skf26(v))*. % 11.36/11.67 169[2:MRR:152.3,12.0] || r1(skc5,u)+ r1(v,u)* -> p2(u) p2(skf24(skf23(u)))* r1(v,skf26(v))*. % 11.36/11.67 184[2:Res:37.2,94.0] || r1(skc5,u) r1(v,u)* -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))* r1(v,skf26(v))*. % 11.36/11.67 202[2:MRR:184.3,12.0] || r1(skc5,u)+ r1(v,u)* -> p2(u) r1(skf23(u),skf24(skf23(u)))* r1(v,skf26(v))*. % 11.36/11.67 205[0:Res:32.2,44.3] SkP1(skf23(u)) p2(skf33(skf23(u))) || r1(skf33(skf23(u)),v)* r1(skc5,u) -> p2(skf23(u)) p2(u) p2(v). % 11.36/11.67 211[0:MRR:205.1,205.4,27.2,12.0] SkP1(skf23(u)) || r1(skf33(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.67 220[2:Res:35.2,95.4] p2(skf18(skf26(u))) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)* -> p2(skf26(u)) p2(w) p2(x) p2(skf24(w))*. % 11.36/11.67 223[2:MRR:220.0,220.5,30.2,10.0] || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)*+ -> p2(w) p2(x) p2(skf24(w))*. % 11.36/11.67 233[2:Res:35.2,96.4] p2(skf18(skf26(u))) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)* -> p2(skf26(u)) p2(w) p2(x) r1(w,skf24(w))*. % 11.36/11.67 236[2:MRR:233.0,233.5,30.2,10.0] || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)*+ -> p2(w) p2(x) r1(w,skf24(w))*. % 11.36/11.67 406[2:Res:2.0,169.0] || r1(u,skc8) -> p2(skc8) p2(skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.67 408[2:MRR:406.1,5.0] || r1(u,skc8)+ -> p2(skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.67 410[3:Spt:408.0,408.2] || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.67 493[2:Res:2.0,202.0] || r1(u,skc8) -> p2(skc8) r1(skf23(skc8),skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.67 657[2:Res:20.0,223.3] || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* -> p2(w) p2(skf19(skf26(u)))* p2(skf24(w))*. % 11.36/11.67 658[2:MRR:657.4,14.0] || r1(skc5,skf26(u))*+ r1(v,w)* r1(u,v)* -> p2(w) p2(skf24(w))*. % 11.36/11.67 699[2:Res:20.0,236.3] || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* -> p2(w) p2(skf19(skf26(u)))* r1(w,skf24(w))*. % 11.36/11.67 700[2:MRR:699.4,14.0] || r1(skc5,skf26(u))*+ r1(v,w)* r1(u,v)* -> p2(w) r1(w,skf24(w))*. % 11.36/11.67 772[3:Res:410.1,658.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.67 857[3:Res:410.1,700.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.67 1718[3:MRR:772.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.67 1719[3:MRR:857.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.67 1853[3:Res:37.2,1718.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.67 1883[3:Obv:1853.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.67 1884[3:MRR:1883.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.67 1938[3:SoR:144.0,1884.2] || r1(u,skf24(skf23(v)))* r1(skc5,v) -> SkP1(u) p2(v). % 11.36/11.67 2059[3:Res:37.2,1719.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.67 2091[3:Obv:2059.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.67 2092[3:MRR:2091.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.67 2242[3:Res:2092.2,1938.0] || r1(skc5,u) r1(skc5,u) -> p2(u) SkP1(skf23(u))* p2(u). % 11.36/11.67 2244[3:Obv:2242.2] || r1(skc5,u) -> SkP1(skf23(u))* p2(u). % 11.36/11.67 2245[3:MRR:211.0,2244.1] || r1(skf33(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.67 2261[3:Res:16.0,2245.0] || r1(skc5,u) -> p2(u) p2(skf34(skf23(u)))*. % 11.36/11.67 2262[3:MRR:2261.2,7.0] || r1(skc5,u)* -> p2(u). % 11.36/11.67 2274[3:Res:410.1,2262.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.67 2282[3:MRR:2274.0,2274.1,2.0,10.0] || -> . % 11.36/11.67 2284[3:Spt:2282.0,408.1] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.67 2286[2:MRR:493.1,5.0] || r1(u,skc8)+ -> r1(skf23(skc8),skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.67 2922[4:Spt:2286.0,2286.2] || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.67 2936[4:Res:2922.1,700.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.67 2937[4:Res:2922.1,658.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.67 2941[4:MRR:2937.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.67 2942[4:MRR:2936.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.67 2998[4:Res:37.2,2941.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.67 3022[4:Obv:2998.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.67 3023[4:MRR:3022.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.67 3049[4:SoR:144.0,3023.2] || r1(u,skf24(skf23(v)))* r1(skc5,v) -> SkP1(u) p2(v). % 11.36/11.67 3228[4:Res:37.2,2942.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.67 3256[4:Obv:3228.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.67 3257[4:MRR:3256.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.67 3378[4:Res:3257.2,3049.0] || r1(skc5,u) r1(skc5,u) -> p2(u) SkP1(skf23(u))* p2(u). % 11.36/11.67 3381[4:Obv:3378.2] || r1(skc5,u) -> SkP1(skf23(u))* p2(u). % 11.36/11.67 3382[4:MRR:211.0,3381.1] || r1(skf33(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.67 3399[4:Res:16.0,3382.0] || r1(skc5,u) -> p2(u) p2(skf34(skf23(u)))*. % 11.36/11.67 3400[4:MRR:3399.2,7.0] || r1(skc5,u)* -> p2(u). % 11.36/11.67 3410[4:Res:2922.1,3400.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.67 3419[4:MRR:3410.0,3410.1,2.0,10.0] || -> . % 11.36/11.67 3421[4:Spt:3419.0,2286.1] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.67 3501[4:Res:3421.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.67 3502[4:SSi:3501.0,2284.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.67 3503[4:MRR:3502.1,3502.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.67 3514[4:Res:18.0,3503.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.67 3515[4:MRR:3514.0,11.0] || -> . % 11.36/11.67 3517[2:Spt:3515.0,26.1] || -> r1(skf29(u),skf30(u))*. % 11.36/11.67 3518[2:Res:3517.0,33.1] SkP2(skf29(u)) || -> SkP1(skf30(u))*. % 11.36/11.67 3519[3:Spt:38.0,38.1,38.2] SkP1(u) || r1(skc12,u)* -> SkP2(u). % 11.36/11.67 3525[4:Spt:22.0] || -> SkP1(skc5)*. % 11.36/11.67 3528[0:Res:25.1,44.3] p2(skf29(skf23(u))) || r1(skf29(skf23(u)),v)* r1(skc5,u) -> SkP0(skf23(u)) p2(u) p2(v). % 11.36/11.67 3529[3:Res:25.1,3519.1] SkP1(skf29(skc12)) || -> SkP0(skc12) SkP2(skf29(skc12))*. % 11.36/11.67 3533[3:SoR:3529.0,28.2] p2(skf29(skc12)) SkP0(skf29(skc12)) || -> SkP0(skc12) SkP2(skf29(skc12))*. % 11.36/11.67 3539[0:Res:37.2,39.0] || r1(skc5,u) -> p2(u) SkP0(u) p2(skf23(u)) p2(skf31(skf23(u)))*. % 11.36/11.67 3540[0:Res:25.1,39.0] || -> SkP0(u) SkP0(u) p2(skf29(u)) p2(skf31(skf29(u)))*. % 11.36/11.67 3542[0:Res:2.0,39.0] || -> SkP0(skc5) p2(skc8) p2(skf31(skc8))*. % 11.36/11.67 3550[2:Res:3517.0,39.0] || -> SkP0(skf29(u)) p2(skf30(u)) p2(skf31(skf30(u)))*. % 11.36/11.67 3551[0:MRR:3542.1,5.0] || -> SkP0(skc5) p2(skf31(skc8))*. % 11.36/11.67 3556[2:MRR:3550.1,9.0] || -> SkP0(skf29(u)) p2(skf31(skf30(u)))*. % 11.36/11.67 3557[0:Obv:3540.0] || -> SkP0(u) p2(skf29(u)) p2(skf31(skf29(u)))*. % 11.36/11.67 3558[0:MRR:3539.3,12.0] || r1(skc5,u) -> p2(u) SkP0(u) p2(skf31(skf23(u)))*. % 11.36/11.67 3559[5:Spt:3551.0] || -> SkP0(skc5)*. % 11.36/11.67 3564[0:Res:37.2,40.0] || r1(skc5,u) -> p2(u) SkP0(u) p2(skf23(u)) r1(skf23(u),skf31(skf23(u)))*. % 11.36/11.67 3565[0:Res:25.1,40.0] || -> SkP0(u) SkP0(u) p2(skf29(u)) r1(skf29(u),skf31(skf29(u)))*. % 11.36/11.67 3575[2:Res:3517.0,40.0] || -> SkP0(skf29(u)) p2(skf30(u)) r1(skf30(u),skf31(skf30(u)))*. % 11.36/11.67 3580[2:MRR:3575.1,9.0] || -> SkP0(skf29(u)) r1(skf30(u),skf31(skf30(u)))*. % 11.36/11.67 3581[0:Obv:3565.0] || -> SkP0(u) p2(skf29(u)) r1(skf29(u),skf31(skf29(u)))*. % 11.36/11.67 3582[0:MRR:3564.3,12.0] || r1(skc5,u) -> p2(u) SkP0(u) r1(skf23(u),skf31(skf23(u)))*. % 11.36/11.67 3593[0:Res:20.0,42.2] SkP0(u) p2(skf18(v)) || r1(u,skf18(v))* -> SkP1(u) p2(skf19(v)). % 11.36/11.67 3595[0:Res:18.0,42.2] SkP0(u) p2(skf24(v)) || r1(u,skf24(v))* -> SkP1(u) p2(skf25(v)). % 11.36/11.67 3596[0:Res:17.0,42.2] SkP0(u) p2(skf31(v)) || r1(u,skf31(v))* -> SkP1(u) p2(skf32(v)). % 11.36/11.67 3600[0:MRR:3593.4,14.0] SkP0(u) p2(skf18(v)) || r1(u,skf18(v))* -> SkP1(u). % 11.36/11.67 3601[0:MRR:3595.4,11.0] SkP0(u) p2(skf24(v)) || r1(u,skf24(v))* -> SkP1(u). % 11.36/11.67 3602[0:MRR:3596.4,8.0] SkP0(u) p2(skf31(v)) || r1(u,skf31(v))* -> SkP1(u). % 11.36/11.67 3625[0:Res:37.2,43.1] SkP0(u) || r1(skc5,v) r1(u,v)* -> p2(v) p2(skf23(v)) p2(skf24(skf23(v)))* r1(u,skf26(u))*. % 11.36/11.67 3626[0:Res:25.1,43.1] SkP0(u) || r1(u,v)*+ -> SkP0(v) p2(skf29(v)) p2(skf24(skf29(v)))* r1(u,skf26(u))*. % 11.36/11.67 3647[0:MRR:3625.4,12.0] SkP0(u) || r1(skc5,v)+ r1(u,v)* -> p2(v) p2(skf24(skf23(v)))* r1(u,skf26(u))*. % 11.36/11.67 3651[2:Res:3580.1,89.2] p2(skf31(skf30(u))) || r1(skf31(skf30(u)),v)* -> SkP0(skf29(u)) p2(v). % 11.36/11.67 3654[2:MRR:3651.0,3556.1] || r1(skf31(skf30(u)),v)* -> SkP0(skf29(u)) p2(v). % 11.36/11.67 3659[0:Res:37.2,45.1] SkP0(u) || r1(skc5,v) r1(u,v)* -> p2(v) p2(skf23(v)) r1(skf23(v),skf24(skf23(v)))* r1(u,skf26(u))*. % 11.36/11.67 3660[0:Res:25.1,45.1] SkP0(u) || r1(u,v)*+ -> SkP0(v) p2(skf29(v)) r1(skf29(v),skf24(skf29(v)))* r1(u,skf26(u))*. % 11.36/11.68 3682[0:MRR:3659.4,12.0] SkP0(u) || r1(skc5,v)+ r1(u,v)* -> p2(v) r1(skf23(v),skf24(skf23(v)))* r1(u,skf26(u))*. % 11.36/11.68 3686[0:Res:35.2,46.5] SkP0(u) p2(skf18(skf26(u))) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)* -> p2(skf26(u)) p2(w) p2(x) p2(skf24(w))*. % 11.36/11.68 3691[0:MRR:3686.1,3686.6,30.2,10.0] SkP0(u) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)*+ -> p2(w) p2(x) p2(skf24(w))*. % 11.36/11.68 3704[2:Res:17.0,3654.0] || -> SkP0(skf29(u)) p2(skf32(skf30(u)))*. % 11.36/11.68 3705[2:MRR:3704.1,8.0] || -> SkP0(skf29(u))*. % 11.36/11.68 3706[3:MRR:3533.1,3705.0] p2(skf29(skc12)) || -> SkP0(skc12) SkP2(skf29(skc12))*. % 11.36/11.68 3710[0:Res:35.2,47.5] SkP0(u) p2(skf18(skf26(u))) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)* -> p2(skf26(u)) p2(w) p2(x) r1(w,skf24(w))*. % 11.36/11.68 3715[0:MRR:3710.1,3710.6,30.2,10.0] SkP0(u) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* r1(skf18(skf26(u)),x)*+ -> p2(w) p2(x) r1(w,skf24(w))*. % 11.36/11.68 3758[0:Res:3582.3,44.3] p2(skf31(skf23(u))) || r1(skc5,u) r1(skf31(skf23(u)),v)* r1(skc5,u) -> p2(u) SkP0(u) p2(u) p2(v). % 11.36/11.68 3762[0:Obv:3758.4] p2(skf31(skf23(u))) || r1(skf31(skf23(u)),v)* r1(skc5,u) -> SkP0(u) p2(u) p2(v). % 11.36/11.68 3763[0:MRR:3762.0,3558.3] || r1(skf31(skf23(u)),v)* r1(skc5,u) -> SkP0(u) p2(u) p2(v). % 11.36/11.68 3766[0:SoR:3600.1,30.2] SkP0(u) || r1(u,skf18(v))* r1(skc5,v) -> SkP1(u) p2(v). % 11.36/11.68 3777[0:SoR:3602.1,3557.2] SkP0(u) || r1(u,skf31(skf29(v)))* -> SkP1(u) p2(skf29(v)) SkP0(v). % 11.36/11.68 3858[0:Res:17.0,3763.0] || r1(skc5,u) -> SkP0(u) p2(u) p2(skf32(skf23(u)))*. % 11.36/11.68 3859[0:MRR:3858.3,8.0] || r1(skc5,u)* -> SkP0(u) p2(u). % 11.36/11.68 3959[0:Res:35.2,3766.1] SkP0(u) || r1(skc5,u)* r1(skc5,u)* -> p2(u) SkP1(u) p2(u). % 11.36/11.68 3960[0:Obv:3959.3] SkP0(u) || r1(skc5,u)* -> SkP1(u) p2(u). % 11.36/11.68 3961[0:MRR:3960.0,3859.1] || r1(skc5,u)* -> SkP1(u) p2(u). % 11.36/11.68 3963[0:Res:36.2,3961.0] || r1(skc5,skc5) -> p1(skc5) SkP1(skf20(skc5))* p2(skf20(skc5)). % 11.36/11.68 3964[0:Res:34.2,3961.0] || r1(skc5,skc5) -> p3(skc5) SkP1(skf16(skc5))* p2(skf16(skc5)). % 11.36/11.68 3980[6:Spt:3963.1] || -> p1(skc5)*. % 11.36/11.68 3981[7:Spt:3964.1] || -> p3(skc5)*. % 11.36/11.68 3991[0:Res:3581.2,3777.1] SkP0(skf29(u)) || -> SkP0(u) p2(skf29(u)) SkP1(skf29(u))* p2(skf29(u)) SkP0(u). % 11.36/11.68 3992[0:Obv:3991.2] SkP0(skf29(u)) || -> SkP1(skf29(u))* p2(skf29(u)) SkP0(u). % 11.36/11.68 3993[2:SSi:3992.0,3705.0] || -> SkP1(skf29(u))* p2(skf29(u)) SkP0(u). % 11.36/11.68 4004[3:SoR:3529.0,3993.0] || -> SkP0(skc12) SkP2(skf29(skc12))* SkP0(skc12) p2(skf29(skc12)). % 11.36/11.68 4005[3:Obv:4004.0] || -> SkP2(skf29(skc12))* SkP0(skc12) p2(skf29(skc12)). % 11.36/11.68 4006[3:MRR:4005.2,3706.0] || -> SkP2(skf29(skc12))* SkP0(skc12). % 11.36/11.68 4008[3:SoR:3518.0,4006.0] || -> SkP1(skf30(skc12))* SkP0(skc12). % 11.36/11.68 4053[0:Res:37.2,3626.1] SkP0(u) || r1(skc5,u) -> p2(u) SkP0(skf23(u)) p2(skf29(skf23(u))) p2(skf24(skf29(skf23(u))))* r1(u,skf26(u))*. % 11.36/11.68 4084[0:MRR:4053.0,3859.1] || r1(skc5,u)+ -> p2(u) SkP0(skf23(u)) p2(skf29(skf23(u))) p2(skf24(skf29(skf23(u))))* r1(u,skf26(u))*. % 11.36/11.68 4139[0:Res:2.0,3647.1] SkP0(u) || r1(u,skc8) -> p2(skc8) p2(skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.68 4141[0:MRR:4139.2,5.0] SkP0(u) || r1(u,skc8)+ -> p2(skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.68 4144[8:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 4218[0:Res:3.0,3660.1] SkP0(skc5) || -> SkP0(skc6) p2(skf29(skc6)) r1(skf29(skc6),skf24(skf29(skc6)))* r1(skc5,skf26(skc5)). % 11.36/11.68 4240[7:SSi:4218.0,3525.0,3559.0,3980.0,3981.0] || -> SkP0(skc6) p2(skf29(skc6)) r1(skf29(skc6),skf24(skf29(skc6)))* r1(skc5,skf26(skc5)). % 11.36/11.68 4249[9:Spt:4240.3] || -> r1(skc5,skf26(skc5))*. % 11.36/11.68 4290[0:Res:2.0,3682.1] SkP0(u) || r1(u,skc8) -> p2(skc8) r1(skf23(skc8),skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.68 4514[0:Res:20.0,3691.4] SkP0(u) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* -> p2(w) p2(skf19(skf26(u)))* p2(skf24(w))*. % 11.36/11.68 4515[0:MRR:4514.5,14.0] SkP0(u) || r1(skc5,skf26(u))*+ r1(v,w)* r1(u,v)* -> p2(w) p2(skf24(w))*. % 11.36/11.68 4587[0:Res:20.0,3715.4] SkP0(u) || r1(skc5,skf26(u)) r1(v,w)* r1(u,v)* -> p2(w) p2(skf19(skf26(u)))* r1(w,skf24(w))*. % 11.36/11.68 4588[0:MRR:4587.5,14.0] SkP0(u) || r1(skc5,skf26(u))*+ r1(v,w)* r1(u,v)* -> p2(w) r1(w,skf24(w))*. % 11.36/11.68 4663[9:Res:4249.0,4515.1] SkP0(skc5) || r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 4664[9:SSi:4663.0,3525.0,3559.0,3980.0,3981.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 4674[9:Res:37.2,4664.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 4722[9:Obv:4674.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 4723[9:MRR:4722.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 4792[0:Res:2.0,4084.0] || -> p2(skc8) SkP0(skf23(skc8)) p2(skf29(skf23(skc8))) p2(skf24(skf29(skf23(skc8))))* r1(skc8,skf26(skc8)). % 11.36/11.68 4885[9:Res:4249.0,4588.1] SkP0(skc5) || r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 4886[9:SSi:4885.0,3525.0,3559.0,3980.0,3981.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 4895[9:Res:37.2,4886.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 4943[9:Obv:4895.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 4944[9:MRR:4943.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 5123[9:Res:4944.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 5129[9:Obv:5123.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 5130[9:MRR:5129.0,4723.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 5222[9:Res:18.0,5130.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 5223[9:MRR:5222.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 5234[9:Res:4144.2,5223.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 5246[9:SSi:5234.0,3525.0,3559.0,3980.0,3981.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 5247[9:MRR:5246.0,5246.1,2.0,10.0] || -> . % 11.36/11.68 5250[9:Spt:5247.0,4240.3,4249.0] || r1(skc5,skf26(skc5))* -> . % 11.36/11.68 5251[9:Spt:5247.0,4240.0,4240.1,4240.2] || -> SkP0(skc6) p2(skf29(skc6)) r1(skf29(skc6),skf24(skf29(skc6)))*. % 11.36/11.68 5255[0:MRR:4792.0,5.0] || -> SkP0(skf23(skc8)) p2(skf29(skf23(skc8))) p2(skf24(skf29(skf23(skc8))))* r1(skc8,skf26(skc8)). % 11.36/11.68 5276[9:Res:4144.2,5250.0] SkP0(skc5) || r1(skc5,skc8)* -> . % 11.36/11.68 5278[9:SSi:5276.0,3525.0,3559.0,3980.0,3981.0] || r1(skc5,skc8)* -> . % 11.36/11.68 5279[9:MRR:5278.0,2.0] || -> . % 11.36/11.68 5281[8:Spt:5279.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 5282[0:MRR:4290.2,5.0] SkP0(u) || r1(u,skc8)+ -> r1(skf23(skc8),skf24(skf23(skc8)))* r1(u,skf26(u))*. % 11.36/11.68 7881[9:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 7905[9:Res:7881.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 7906[9:Res:7881.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 7915[9:Obv:7906.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 7916[9:SSi:7915.0,3525.0,3559.0,3980.0,3981.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 7917[9:MRR:7916.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 7919[9:Obv:7905.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 7920[9:SSi:7919.0,3525.0,3559.0,3980.0,3981.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 7921[9:MRR:7920.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 7980[9:Res:37.2,7917.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 8021[9:Obv:7980.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 8022[9:MRR:8021.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 8092[9:Res:37.2,7921.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 8136[9:Obv:8092.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 8137[9:MRR:8136.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 8424[9:Res:8137.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 8430[9:Obv:8424.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 8431[9:MRR:8430.0,8022.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 8604[9:Res:18.0,8431.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 8605[9:MRR:8604.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 8637[9:Res:7881.2,8605.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 8647[9:SSi:8637.0,3525.0,3559.0,3980.0,3981.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 8648[9:MRR:8647.0,8647.1,2.0,10.0] || -> . % 11.36/11.68 8653[9:Spt:8648.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 8747[9:Res:8653.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 8748[9:SSi:8747.0,5281.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 8749[9:MRR:8748.1,8748.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 8759[9:Res:18.0,8749.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 8760[9:MRR:8759.0,11.0] || -> . % 11.36/11.68 8762[7:Spt:8760.0,3964.1,3981.0] || p3(skc5)* -> . % 11.36/11.68 8763[7:Spt:8760.0,3964.0,3964.2,3964.3] || r1(skc5,skc5) -> SkP1(skf16(skc5))* p2(skf16(skc5)). % 11.36/11.68 8821[8:Spt:4006.0] || -> SkP2(skf29(skc12))*. % 11.36/11.68 8825[8:SoR:3518.0,8821.0] || -> SkP1(skf30(skc12))*. % 11.36/11.68 8828[8:SoR:100.0,8825.0] || r1(skf33(skf30(skc12)),u)* -> p2(u). % 11.36/11.68 8841[8:Res:16.0,8828.0] || -> p2(skf34(skf30(skc12)))*. % 11.36/11.68 8842[8:MRR:8841.0,7.0] || -> . % 11.36/11.68 8847[8:Spt:8842.0,4006.0,8821.0] || SkP2(skf29(skc12))* -> . % 11.36/11.68 8848[8:Spt:8842.0,4006.1] || -> SkP0(skc12)*. % 11.36/11.68 8990[9:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 9019[9:Res:8990.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 9020[9:Res:8990.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 9029[9:Obv:9020.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 9030[9:SSi:9029.0,3525.0,3559.0,3980.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 9031[9:MRR:9030.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 9033[9:Obv:9019.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 9034[9:SSi:9033.0,3525.0,3559.0,3980.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 9035[9:MRR:9034.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 9099[9:Res:37.2,9031.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 9139[9:Obv:9099.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 9140[9:MRR:9139.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 9327[9:Res:37.2,9035.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 9368[9:Obv:9327.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 9369[9:MRR:9368.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 9521[9:Res:9369.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 9525[9:Obv:9521.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 9526[9:MRR:9525.0,9140.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 9611[9:Res:18.0,9526.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 9612[9:MRR:9611.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 9623[9:Res:8990.2,9612.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 9635[9:SSi:9623.0,3525.0,3559.0,3980.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 9636[9:MRR:9635.0,9635.1,2.0,10.0] || -> . % 11.36/11.68 9639[9:Spt:9636.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 9646[0:Res:34.2,3859.0] || r1(skc5,skc5) -> p3(skc5) SkP0(skf16(skc5))* p2(skf16(skc5)). % 11.36/11.68 10531[10:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 10556[10:Res:10531.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 10557[10:Res:10531.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 10566[10:Obv:10557.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 10567[10:SSi:10566.0,3525.0,3559.0,3980.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 10568[10:MRR:10567.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 10570[10:Obv:10556.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 10571[10:SSi:10570.0,3525.0,3559.0,3980.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 10572[10:MRR:10571.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 10629[10:Res:37.2,10568.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 10669[10:Obv:10629.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 10670[10:MRR:10669.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 10741[10:Res:37.2,10572.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 10782[10:Obv:10741.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 10783[10:MRR:10782.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 11017[10:Res:10783.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 11023[10:Obv:11017.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 11024[10:MRR:11023.0,10670.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 11123[10:Res:18.0,11024.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 11124[10:MRR:11123.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 11157[10:Res:10531.2,11124.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 11169[10:SSi:11157.0,3525.0,3559.0,3980.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 11170[10:MRR:11169.0,11169.1,2.0,10.0] || -> . % 11.36/11.68 11173[10:Spt:11170.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 11265[10:Res:11173.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 11266[10:SSi:11265.0,9639.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 11267[10:MRR:11266.1,11266.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 11277[10:Res:18.0,11267.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 11278[10:MRR:11277.0,11.0] || -> . % 11.36/11.68 11280[6:Spt:11278.0,3963.1,3980.0] || p1(skc5)* -> . % 11.36/11.68 11281[6:Spt:11278.0,3963.0,3963.2,3963.3] || r1(skc5,skc5) -> SkP1(skf20(skc5))* p2(skf20(skc5)). % 11.36/11.68 11332[7:Spt:4008.0] || -> SkP1(skf30(skc12))*. % 11.36/11.68 11335[7:SoR:100.0,11332.0] || r1(skf33(skf30(skc12)),u)* -> p2(u). % 11.36/11.68 11353[7:Res:16.0,11335.0] || -> p2(skf34(skf30(skc12)))*. % 11.36/11.68 11354[7:MRR:11353.0,7.0] || -> . % 11.36/11.68 11359[7:Spt:11354.0,4008.0,11332.0] || SkP1(skf30(skc12))* -> . % 11.36/11.68 11360[7:Spt:11354.0,4008.1] || -> SkP0(skc12)*. % 11.36/11.68 11394[8:Spt:9646.1] || -> p3(skc5)*. % 11.36/11.68 11495[9:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 11523[9:Res:11495.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 11524[9:Res:11495.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 11533[9:Obv:11524.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 11534[9:SSi:11533.0,3525.0,3559.0,11394.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 11535[9:MRR:11534.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 11537[9:Obv:11523.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 11538[9:SSi:11537.0,3525.0,3559.0,11394.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 11539[9:MRR:11538.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 11615[9:Res:37.2,11535.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 11655[9:Obv:11615.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 11656[9:MRR:11655.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 11827[9:Res:37.2,11539.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 11868[9:Obv:11827.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 11869[9:MRR:11868.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 12035[9:Res:11869.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 12039[9:Obv:12035.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 12040[9:MRR:12039.0,11656.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 12114[9:Res:18.0,12040.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 12115[9:MRR:12114.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 12126[9:Res:11495.2,12115.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 12138[9:SSi:12126.0,3525.0,3559.0,11394.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 12139[9:MRR:12138.0,12138.1,2.0,10.0] || -> . % 11.36/11.68 12142[9:Spt:12139.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 12165[0:Res:36.2,3859.0] || r1(skc5,skc5) -> p1(skc5) SkP0(skf20(skc5))* p2(skf20(skc5)). % 11.36/11.68 13021[10:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 13045[10:Res:13021.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13046[10:Res:13021.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13055[10:Obv:13046.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13056[10:SSi:13055.0,3525.0,3559.0,11394.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13057[10:MRR:13056.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13059[10:Obv:13045.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13060[10:SSi:13059.0,3525.0,3559.0,11394.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13061[10:MRR:13060.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13134[10:Res:37.2,13057.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 13174[10:Obv:13134.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 13175[10:MRR:13174.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 13246[10:Res:37.2,13061.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 13287[10:Obv:13246.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 13288[10:MRR:13287.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 13506[10:Res:13288.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 13512[10:Obv:13506.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 13513[10:MRR:13512.0,13175.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 13628[10:Res:18.0,13513.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 13629[10:MRR:13628.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 13640[10:Res:13021.2,13629.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 13652[10:SSi:13640.0,3525.0,3559.0,11394.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 13653[10:MRR:13652.0,13652.1,2.0,10.0] || -> . % 11.36/11.68 13656[10:Spt:13653.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 13752[10:Res:13656.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 13753[10:SSi:13752.0,12142.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 13754[10:MRR:13753.1,13753.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 13764[10:Res:18.0,13754.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 13765[10:MRR:13764.0,11.0] || -> . % 11.36/11.68 13767[8:Spt:13765.0,9646.1,11394.0] || p3(skc5)* -> . % 11.36/11.68 13768[8:Spt:13765.0,9646.0,9646.2,9646.3] || r1(skc5,skc5) -> SkP0(skf16(skc5))* p2(skf16(skc5)). % 11.36/11.68 13884[9:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 13910[9:Res:13884.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13911[9:Res:13884.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13920[9:Obv:13911.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13921[9:SSi:13920.0,3525.0,3559.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13922[9:MRR:13921.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 13924[9:Obv:13910.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13925[9:SSi:13924.0,3525.0,3559.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13926[9:MRR:13925.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 13998[9:Res:37.2,13922.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 14038[9:Obv:13998.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 14039[9:MRR:14038.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 14113[9:Res:37.2,13926.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 14154[9:Obv:14113.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 14155[9:MRR:14154.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 14389[9:Res:14155.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 14393[9:Obv:14389.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 14394[9:MRR:14393.0,14039.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 14492[9:Res:18.0,14394.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 14493[9:MRR:14492.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 14504[9:Res:13884.2,14493.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 14518[9:SSi:14504.0,3525.0,3559.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 14519[9:MRR:14518.0,14518.1,2.0,10.0] || -> . % 11.36/11.68 14522[9:Spt:14519.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 14555[0:Res:34.2,3961.0] || r1(skc5,skc5) -> p3(skc5) SkP1(skf16(skc5))* p2(skf16(skc5)). % 11.36/11.68 15403[10:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 15427[10:Res:15403.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 15428[10:Res:15403.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 15437[10:Obv:15428.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 15438[10:SSi:15437.0,3525.0,3559.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 15439[10:MRR:15438.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 15441[10:Obv:15427.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 15442[10:SSi:15441.0,3525.0,3559.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 15443[10:MRR:15442.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 15516[10:Res:37.2,15439.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 15556[10:Obv:15516.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 15557[10:MRR:15556.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 15628[10:Res:37.2,15443.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 15669[10:Obv:15628.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 15670[10:MRR:15669.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 15904[10:Res:15670.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 15910[10:Obv:15904.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 15911[10:MRR:15910.0,15557.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 16010[10:Res:18.0,15911.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 16011[10:MRR:16010.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 16022[10:Res:15403.2,16011.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 16036[10:SSi:16022.0,3525.0,3559.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 16037[10:MRR:16036.0,16036.1,2.0,10.0] || -> . % 11.36/11.68 16040[10:Spt:16037.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 16134[10:Res:16040.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 16135[10:SSi:16134.0,14522.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 16136[10:MRR:16135.1,16135.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 16146[10:Res:18.0,16136.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 16147[10:MRR:16146.0,11.0] || -> . % 11.36/11.68 16149[5:Spt:16147.0,3551.0,3559.0] || SkP0(skc5)* -> . % 11.36/11.68 16150[5:Spt:16147.0,3551.1] || -> p2(skf31(skc8))*. % 11.36/11.68 16190[5:Res:24.1,16149.0] SkP1(skc5) || -> . % 11.36/11.68 16191[5:SSi:16190.0,3525.0] || -> . % 11.36/11.68 16192[4:Spt:16191.0,22.0,3525.0] || SkP1(skc5)* -> . % 11.36/11.68 16193[4:Spt:16191.0,22.1] || -> r1(skc5,skc12)*. % 11.36/11.68 16204[4:MRR:23.1,16192.0] || SkP1(skc12)* -> . % 11.36/11.68 16219[4:Res:16193.0,3961.0] || -> SkP1(skc12)* p2(skc12). % 11.36/11.68 16228[4:MRR:16219.0,16204.0] || -> p2(skc12)*. % 11.36/11.68 16231[4:Res:28.2,16204.0] SkP0(skc12) p2(skc12) || -> . % 11.36/11.68 16232[4:SSi:16231.1,16228.0] SkP0(skc12) || -> . % 11.36/11.68 16234[4:MRR:4008.1,16232.0] || -> SkP1(skf30(skc12))*. % 11.36/11.68 16244[4:SoR:100.0,16234.0] || r1(skf33(skf30(skc12)),u)* -> p2(u). % 11.36/11.68 16332[4:Res:16.0,16244.0] || -> p2(skf34(skf30(skc12)))*. % 11.36/11.68 16333[4:MRR:16332.0,7.0] || -> . % 11.36/11.68 16338[3:Spt:16333.0,38.3] || -> SkP1(skc5)*. % 11.36/11.68 16353[4:Spt:3551.0] || -> SkP0(skc5)*. % 11.36/11.68 16360[5:Spt:14555.1] || -> p3(skc5)*. % 11.36/11.68 16361[6:Spt:12165.1] || -> p1(skc5)*. % 11.36/11.68 16497[7:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 16523[7:Res:16497.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 16524[7:Res:16497.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 16532[7:Obv:16524.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 16533[7:SSi:16532.0,16338.0,16353.0,16360.0,16361.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 16534[7:MRR:16533.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 16536[7:Obv:16523.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 16537[7:SSi:16536.0,16338.0,16353.0,16360.0,16361.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 16538[7:MRR:16537.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 16594[7:Res:37.2,16534.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 16632[7:Obv:16594.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 16633[7:MRR:16632.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 16708[7:Res:37.2,16538.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 16747[7:Obv:16708.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 16748[7:MRR:16747.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 16945[7:Res:16748.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 16949[7:Obv:16945.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 16950[7:MRR:16949.0,16633.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 17094[7:Res:18.0,16950.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 17095[7:MRR:17094.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 17106[7:Res:16497.2,17095.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 17116[7:SSi:17106.0,16338.0,16353.0,16360.0,16361.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 17117[7:MRR:17116.0,17116.1,2.0,10.0] || -> . % 11.36/11.68 17120[7:Spt:17117.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 17245[8:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 17268[8:Res:17245.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 17269[8:Res:17245.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 17277[8:Obv:17269.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 17278[8:SSi:17277.0,16338.0,16353.0,16360.0,16361.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 17279[8:MRR:17278.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 17281[8:Obv:17268.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 17282[8:SSi:17281.0,16338.0,16353.0,16360.0,16361.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 17283[8:MRR:17282.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 17334[8:Res:37.2,17279.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 17373[8:Obv:17334.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 17374[8:MRR:17373.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 17445[8:Res:37.2,17283.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 17484[8:Obv:17445.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 17485[8:MRR:17484.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 17730[8:Res:17485.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 17736[8:Obv:17730.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 17737[8:MRR:17736.0,17374.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 17845[8:Res:18.0,17737.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 17846[8:MRR:17845.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 17857[8:Res:17245.2,17846.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 17867[8:SSi:17857.0,16338.0,16353.0,16360.0,16361.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 17868[8:MRR:17867.0,17867.1,2.0,10.0] || -> . % 11.36/11.68 17871[8:Spt:17868.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 17976[8:Res:17871.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 17977[8:SSi:17976.0,17120.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 17978[8:MRR:17977.1,17977.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 17988[8:Res:18.0,17978.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 17989[8:MRR:17988.0,11.0] || -> . % 11.36/11.68 17991[6:Spt:17989.0,12165.1,16361.0] || p1(skc5)* -> . % 11.36/11.68 17992[6:Spt:17989.0,12165.0,12165.2,12165.3] || r1(skc5,skc5) -> SkP0(skf20(skc5))* p2(skf20(skc5)). % 11.36/11.68 18138[7:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 18163[7:Res:18138.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 18164[7:Res:18138.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 18172[7:Obv:18164.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 18173[7:SSi:18172.0,16338.0,16353.0,16360.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 18174[7:MRR:18173.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 18176[7:Obv:18163.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 18177[7:SSi:18176.0,16338.0,16353.0,16360.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 18178[7:MRR:18177.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 18219[7:Res:37.2,18174.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 18257[7:Obv:18219.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 18258[7:MRR:18257.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 18346[7:Res:37.2,18178.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 18385[7:Obv:18346.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 18386[7:MRR:18385.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 18585[7:Res:18386.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 18589[7:Obv:18585.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 18590[7:MRR:18589.0,18258.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 18710[7:Res:18.0,18590.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 18711[7:MRR:18710.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 18722[7:Res:18138.2,18711.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 18734[7:SSi:18722.0,16338.0,16353.0,16360.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 18735[7:MRR:18734.0,18734.1,2.0,10.0] || -> . % 11.36/11.68 18738[7:Spt:18735.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 18739[7:SoR:3601.1,18738.0] SkP0(u) || r1(u,skf24(skf23(skc8)))* -> SkP1(u). % 11.36/11.68 18769[0:Res:36.2,3961.0] || r1(skc5,skc5) -> p1(skc5) SkP1(skf20(skc5))* p2(skf20(skc5)). % 11.36/11.68 18829[8:Spt:5255.0] || -> SkP0(skf23(skc8))*. % 11.36/11.68 18863[9:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 18886[9:Res:18863.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 18899[9:Obv:18886.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 18900[9:SSi:18899.0,16338.0,16353.0,16360.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 18901[9:MRR:18900.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 19063[9:Res:37.2,18901.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 19102[9:Obv:19063.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 19103[9:MRR:19102.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 19368[9:Res:19103.2,18739.1] SkP0(skf23(skc8)) || r1(skc5,skc8) -> p2(skc8) SkP1(skf23(skc8))*. % 11.36/11.68 19369[9:SSi:19368.0,18829.0] || r1(skc5,skc8) -> p2(skc8) SkP1(skf23(skc8))*. % 11.36/11.68 19370[9:MRR:19369.0,19369.1,2.0,5.0] || -> SkP1(skf23(skc8))*. % 11.36/11.68 19374[9:SoR:211.0,19370.0] || r1(skf33(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 19375[9:MRR:19374.1,19374.2,2.0,5.0] || r1(skf33(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 19388[9:Res:16.0,19375.0] || -> p2(skf34(skf23(skc8)))*. % 11.36/11.68 19389[9:MRR:19388.0,7.0] || -> . % 11.36/11.68 19397[9:Spt:19389.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 19406[9:Res:19397.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 19414[9:SSi:19406.0,18738.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 19415[9:MRR:19414.1,19414.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 19452[9:Res:18.0,19415.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 19453[9:MRR:19452.0,11.0] || -> . % 11.36/11.68 19455[8:Spt:19453.0,5255.0,18829.0] || SkP0(skf23(skc8))* -> . % 11.36/11.68 19456[8:Spt:19453.0,5255.1,5255.2,5255.3] || -> p2(skf29(skf23(skc8))) p2(skf24(skf29(skf23(skc8))))* r1(skc8,skf26(skc8)). % 11.36/11.68 19458[9:Spt:19456.0] || -> p2(skf29(skf23(skc8)))*. % 11.36/11.68 19460[9:SoR:3528.0,19458.0] || r1(skf29(skf23(skc8)),u)* r1(skc5,skc8) -> SkP0(skf23(skc8)) p2(skc8) p2(u). % 11.36/11.68 19461[9:MRR:19460.1,19460.3,2.0,5.0] || r1(skf29(skf23(skc8)),u)* -> SkP0(skf23(skc8)) p2(u). % 11.36/11.68 19462[9:MRR:19461.1,19455.0] || r1(skf29(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 19486[9:Res:3517.0,19462.0] || -> p2(skf30(skf23(skc8)))*. % 11.36/11.68 19491[9:MRR:19486.0,9.0] || -> . % 11.36/11.68 19495[9:Spt:19491.0,19456.0,19458.0] || p2(skf29(skf23(skc8)))* -> . % 11.36/11.68 19496[9:Spt:19491.0,19456.1,19456.2] || -> p2(skf24(skf29(skf23(skc8))))* r1(skc8,skf26(skc8)). % 11.36/11.68 19513[10:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 19543[10:Res:19513.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 19544[10:Res:19513.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 19552[10:Obv:19544.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 19553[10:SSi:19552.0,16338.0,16353.0,16360.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 19554[10:MRR:19553.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 19556[10:Obv:19543.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 19557[10:SSi:19556.0,16338.0,16353.0,16360.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 19558[10:MRR:19557.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 19620[10:Res:37.2,19554.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 19659[10:Obv:19620.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 19660[10:MRR:19659.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 19795[10:Res:37.2,19558.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 19834[10:Obv:19795.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 19835[10:MRR:19834.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 20021[10:Res:19835.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 20027[10:Obv:20021.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 20028[10:MRR:20027.0,19660.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 20132[10:Res:18.0,20028.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 20133[10:MRR:20132.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 20145[10:Res:19513.2,20133.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 20157[10:SSi:20145.0,16338.0,16353.0,16360.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 20158[10:MRR:20157.0,20157.1,2.0,10.0] || -> . % 11.36/11.68 20163[10:Spt:20158.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 20267[10:Res:20163.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 20268[10:SSi:20267.0,18738.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 20269[10:MRR:20268.1,20268.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 20279[10:Res:18.0,20269.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 20280[10:MRR:20279.0,11.0] || -> . % 11.36/11.68 20282[5:Spt:20280.0,14555.1,16360.0] || p3(skc5)* -> . % 11.36/11.68 20283[5:Spt:20280.0,14555.0,14555.2,14555.3] || r1(skc5,skc5) -> SkP1(skf16(skc5))* p2(skf16(skc5)). % 11.36/11.68 20358[6:Spt:18769.1] || -> p1(skc5)*. % 11.36/11.68 20431[7:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 20456[7:Res:20431.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 20457[7:Res:20431.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 20465[7:Obv:20457.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 20466[7:SSi:20465.0,16338.0,16353.0,20358.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 20467[7:MRR:20466.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 20469[7:Obv:20456.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 20470[7:SSi:20469.0,16338.0,16353.0,20358.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 20471[7:MRR:20470.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 20527[7:Res:37.2,20467.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 20565[7:Obv:20527.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 20566[7:MRR:20565.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 20639[7:Res:37.2,20471.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 20678[7:Obv:20639.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 20679[7:MRR:20678.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 20878[7:Res:20679.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 20882[7:Obv:20878.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 20883[7:MRR:20882.0,20566.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 21003[7:Res:18.0,20883.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 21004[7:MRR:21003.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 21015[7:Res:20431.2,21004.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 21027[7:SSi:21015.0,16338.0,16353.0,20358.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 21028[7:MRR:21027.0,21027.1,2.0,10.0] || -> . % 11.36/11.68 21031[7:Spt:21028.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 21159[8:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 21182[8:Res:21159.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 21183[8:Res:21159.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 21191[8:Obv:21183.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 21192[8:SSi:21191.0,16338.0,16353.0,20358.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 21193[8:MRR:21192.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 21195[8:Obv:21182.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 21196[8:SSi:21195.0,16338.0,16353.0,20358.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 21197[8:MRR:21196.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 21262[8:Res:37.2,21193.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 21301[8:Obv:21262.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 21302[8:MRR:21301.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 21360[8:Res:37.2,21197.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 21399[8:Obv:21360.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 21400[8:MRR:21399.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 21661[8:Res:21400.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 21667[8:Obv:21661.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 21668[8:MRR:21667.0,21302.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 21751[8:Res:18.0,21668.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 21752[8:MRR:21751.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 21763[8:Res:21159.2,21752.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 21775[8:SSi:21763.0,16338.0,16353.0,20358.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 21776[8:MRR:21775.0,21775.1,2.0,10.0] || -> . % 11.36/11.68 21779[8:Spt:21776.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 21869[8:Res:21779.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 21870[8:SSi:21869.0,21031.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 21871[8:MRR:21870.1,21870.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 21881[8:Res:18.0,21871.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 21882[8:MRR:21881.0,11.0] || -> . % 11.36/11.68 21884[6:Spt:21882.0,18769.1,20358.0] || p1(skc5)* -> . % 11.36/11.68 21885[6:Spt:21882.0,18769.0,18769.2,18769.3] || r1(skc5,skc5) -> SkP1(skf20(skc5))* p2(skf20(skc5)). % 11.36/11.68 21999[7:Spt:4141.0,4141.1,4141.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 22024[7:Res:21999.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22025[7:Res:21999.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 22033[7:Obv:22025.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 22034[7:SSi:22033.0,16338.0,16353.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 22035[7:MRR:22034.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 11.36/11.68 22037[7:Obv:22024.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22038[7:SSi:22037.0,16338.0,16353.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22039[7:MRR:22038.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22091[7:Res:37.2,22035.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 22129[7:Obv:22091.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 11.36/11.68 22130[7:MRR:22129.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 11.36/11.68 22203[7:Res:37.2,22039.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 22242[7:Obv:22203.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 22243[7:MRR:22242.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 22440[7:Res:22243.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 11.36/11.68 22444[7:Obv:22440.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 22445[7:MRR:22444.0,22130.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 11.36/11.68 22563[7:Res:18.0,22445.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 11.36/11.68 22564[7:MRR:22563.2,11.0] || r1(skc5,u)* -> p2(u). % 11.36/11.68 22575[7:Res:21999.2,22564.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 22589[7:SSi:22575.0,16338.0,16353.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 11.36/11.68 22590[7:MRR:22589.0,22589.1,2.0,10.0] || -> . % 11.36/11.68 22593[7:Spt:22590.0,4141.2] || -> p2(skf24(skf23(skc8)))*. % 11.36/11.68 22594[7:SoR:3601.1,22593.0] SkP0(u) || r1(u,skf24(skf23(skc8)))* -> SkP1(u). % 11.36/11.68 22684[8:Spt:5255.0] || -> SkP0(skf23(skc8))*. % 11.36/11.68 22718[9:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 22741[9:Res:22718.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22754[9:Obv:22741.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22755[9:SSi:22754.0,16338.0,16353.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22756[9:MRR:22755.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 22918[9:Res:37.2,22756.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 22957[9:Obv:22918.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 22958[9:MRR:22957.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 11.36/11.68 23223[9:Res:22958.2,22594.1] SkP0(skf23(skc8)) || r1(skc5,skc8) -> p2(skc8) SkP1(skf23(skc8))*. % 11.36/11.68 23224[9:SSi:23223.0,22684.0] || r1(skc5,skc8) -> p2(skc8) SkP1(skf23(skc8))*. % 11.36/11.68 23225[9:MRR:23224.0,23224.1,2.0,5.0] || -> SkP1(skf23(skc8))*. % 11.36/11.68 23229[9:SoR:211.0,23225.0] || r1(skf33(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 23230[9:MRR:23229.1,23229.2,2.0,5.0] || r1(skf33(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 23243[9:Res:16.0,23230.0] || -> p2(skf34(skf23(skc8)))*. % 11.36/11.68 23244[9:MRR:23243.0,7.0] || -> . % 11.36/11.68 23252[9:Spt:23244.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 11.36/11.68 23261[9:Res:23252.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 23269[9:SSi:23261.0,22593.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 11.36/11.68 23270[9:MRR:23269.1,23269.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 23307[9:Res:18.0,23270.0] || -> p2(skf25(skf23(skc8)))*. % 11.36/11.68 23308[9:MRR:23307.0,11.0] || -> . % 11.36/11.68 23310[8:Spt:23308.0,5255.0,22684.0] || SkP0(skf23(skc8))* -> . % 11.36/11.68 23311[8:Spt:23308.0,5255.1,5255.2,5255.3] || -> p2(skf29(skf23(skc8))) p2(skf24(skf29(skf23(skc8))))* r1(skc8,skf26(skc8)). % 11.36/11.68 23313[9:Spt:23311.0] || -> p2(skf29(skf23(skc8)))*. % 11.36/11.68 23315[9:SoR:3528.0,23313.0] || r1(skf29(skf23(skc8)),u)* r1(skc5,skc8) -> SkP0(skf23(skc8)) p2(skc8) p2(u). % 11.36/11.68 23316[9:MRR:23315.1,23315.3,2.0,5.0] || r1(skf29(skf23(skc8)),u)* -> SkP0(skf23(skc8)) p2(u). % 11.36/11.68 23317[9:MRR:23316.1,23310.0] || r1(skf29(skf23(skc8)),u)* -> p2(u). % 11.36/11.68 23341[9:Res:3517.0,23317.0] || -> p2(skf30(skf23(skc8)))*. % 11.36/11.68 23346[9:MRR:23341.0,9.0] || -> . % 11.36/11.68 23350[9:Spt:23346.0,23311.0,23313.0] || p2(skf29(skf23(skc8)))* -> . % 11.36/11.68 23351[9:Spt:23346.0,23311.1,23311.2] || -> p2(skf24(skf29(skf23(skc8))))* r1(skc8,skf26(skc8)). % 11.36/11.68 23368[10:Spt:5282.0,5282.1,5282.3] SkP0(u) || r1(u,skc8) -> r1(u,skf26(u))*. % 11.36/11.68 23398[10:Res:23368.2,4588.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 11.36/11.68 23399[10:Res:23368.2,4515.1] SkP0(skc5) SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 23407[10:Obv:23399.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 23408[10:SSi:23407.0,16338.0,16353.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 23409[10:MRR:23408.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 23411[10:Obv:23398.0] SkP0(skc5) || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 15.66/15.91 23412[10:SSi:23411.0,16338.0,16353.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 15.66/15.91 23413[10:MRR:23412.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 15.66/15.91 23475[10:Res:37.2,23409.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 15.66/15.91 23514[10:Obv:23475.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 15.66/15.91 23515[10:MRR:23514.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 15.66/15.91 23650[10:Res:37.2,23413.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 23689[10:Obv:23650.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 23690[10:MRR:23689.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 23853[10:Res:23690.2,44.3] p2(skf24(skf23(u))) || r1(skc5,u) r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(u) p2(v). % 15.66/15.91 23859[10:Obv:23853.4] p2(skf24(skf23(u))) || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 15.66/15.91 23860[10:MRR:23859.0,23515.2] || r1(skf24(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 15.66/15.91 23987[10:Res:18.0,23860.0] || r1(skc5,u) -> p2(u) p2(skf25(skf23(u)))*. % 15.66/15.91 23988[10:MRR:23987.2,11.0] || r1(skc5,u)* -> p2(u). % 15.66/15.91 24000[10:Res:23368.2,23988.0] SkP0(skc5) || r1(skc5,skc8) -> p2(skf26(skc5))*. % 15.66/15.91 24014[10:SSi:24000.0,16338.0,16353.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 15.66/15.91 24015[10:MRR:24014.0,24014.1,2.0,10.0] || -> . % 15.66/15.91 24020[10:Spt:24015.0,5282.2] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 15.66/15.91 24113[10:Res:24020.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 15.66/15.91 24114[10:SSi:24113.0,22593.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 15.66/15.91 24115[10:MRR:24114.1,24114.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 15.66/15.91 24125[10:Res:18.0,24115.0] || -> p2(skf25(skf23(skc8)))*. % 15.66/15.91 24126[10:MRR:24125.0,11.0] || -> . % 15.66/15.91 24128[4:Spt:24126.0,3551.0,16353.0] || SkP0(skc5)* -> . % 15.66/15.91 24129[4:Spt:24126.0,3551.1] || -> p2(skf31(skc8))*. % 15.66/15.91 24150[4:Res:24.1,24128.0] SkP1(skc5) || -> . % 15.66/15.91 24151[4:SSi:24150.0,16338.0] || -> . % 15.66/15.91 24152[1:Spt:24151.0,41.3] || -> SkP0(u)*. % 15.66/15.91 24160[1:MRR:3601.0,24152.0] p2(skf24(u)) || r1(v,skf24(u))* -> SkP1(v). % 15.66/15.91 24183[1:MRR:4515.0,24152.0] || r1(skc5,skf26(u))*+ r1(v,w)* r1(u,v)* -> p2(w) p2(skf24(w))*. % 15.66/15.91 24186[1:MRR:4588.0,24152.0] || r1(skc5,skf26(u))*+ r1(v,w)* r1(u,v)* -> p2(w) r1(w,skf24(w))*. % 15.66/15.91 24231[1:MRR:4141.0,24152.0] || r1(u,skc8)+ -> p2(skf24(skf23(skc8)))* r1(u,skf26(u))*. % 15.66/15.91 24234[1:MRR:5282.0,24152.0] || r1(u,skc8)+ -> r1(skf23(skc8),skf24(skf23(skc8)))* r1(u,skf26(u))*. % 15.66/15.91 24436[2:Spt:24231.0,24231.2] || r1(u,skc8) -> r1(u,skf26(u))*. % 15.66/15.91 24717[2:Res:24436.1,24183.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 24874[2:Res:24436.1,24186.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 15.66/15.91 25649[2:MRR:24717.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 25651[2:MRR:24874.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 15.66/15.91 25730[2:Res:37.2,25649.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 15.66/15.91 25754[2:Obv:25730.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 15.66/15.91 25755[2:MRR:25754.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 15.66/15.91 25795[2:SoR:24160.0,25755.2] || r1(u,skf24(skf23(v)))* r1(skc5,v) -> SkP1(u) p2(v). % 15.66/15.91 25959[2:Res:37.2,25651.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 25987[2:Obv:25959.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 25988[2:MRR:25987.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 26107[2:Res:25988.2,25795.0] || r1(skc5,u) r1(skc5,u) -> p2(u) SkP1(skf23(u))* p2(u). % 15.66/15.91 26109[2:Obv:26107.2] || r1(skc5,u) -> SkP1(skf23(u))* p2(u). % 15.66/15.91 26110[2:MRR:211.0,26109.1] || r1(skf33(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 15.66/15.91 26130[2:Res:16.0,26110.0] || r1(skc5,u) -> p2(u) p2(skf34(skf23(u)))*. % 15.66/15.91 26131[2:MRR:26130.2,7.0] || r1(skc5,u)* -> p2(u). % 15.66/15.91 26142[2:Res:24436.1,26131.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 15.66/15.91 26150[2:MRR:26142.0,26142.1,2.0,10.0] || -> . % 15.66/15.91 26152[2:Spt:26150.0,24231.1] || -> p2(skf24(skf23(skc8)))*. % 15.66/15.91 26812[3:Spt:24234.0,24234.2] || r1(u,skc8) -> r1(u,skf26(u))*. % 15.66/15.91 26825[3:Res:26812.1,24186.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 15.66/15.91 26826[3:Res:26812.1,24183.0] || r1(skc5,skc8) r1(u,v)* r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 26830[3:MRR:26826.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) p2(skf24(v))*. % 15.66/15.91 26831[3:MRR:26825.0,2.0] || r1(u,v)*+ r1(skc5,u)* -> p2(v) r1(v,skf24(v))*. % 15.66/15.91 26888[3:Res:37.2,26830.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 15.66/15.91 26913[3:Obv:26888.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) p2(skf24(skf23(u)))*. % 15.66/15.91 26914[3:MRR:26913.2,12.0] || r1(skc5,u) -> p2(u) p2(skf24(skf23(u)))*. % 15.66/15.91 26954[3:SoR:24160.0,26914.2] || r1(u,skf24(skf23(v)))* r1(skc5,v) -> SkP1(u) p2(v). % 15.66/15.91 27120[3:Res:37.2,26831.0] || r1(skc5,u) r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 27149[3:Obv:27120.0] || r1(skc5,u) -> p2(u) p2(skf23(u)) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 27150[3:MRR:27149.2,12.0] || r1(skc5,u) -> p2(u) r1(skf23(u),skf24(skf23(u)))*. % 15.66/15.91 27272[3:Res:27150.2,26954.0] || r1(skc5,u) r1(skc5,u) -> p2(u) SkP1(skf23(u))* p2(u). % 15.66/15.91 27275[3:Obv:27272.2] || r1(skc5,u) -> SkP1(skf23(u))* p2(u). % 15.66/15.91 27276[3:MRR:211.0,27275.1] || r1(skf33(skf23(u)),v)* r1(skc5,u) -> p2(u) p2(v). % 15.66/15.91 27293[3:Res:16.0,27276.0] || r1(skc5,u) -> p2(u) p2(skf34(skf23(u)))*. % 15.66/15.91 27294[3:MRR:27293.2,7.0] || r1(skc5,u)* -> p2(u). % 15.66/15.91 27304[3:Res:26812.1,27294.0] || r1(skc5,skc8) -> p2(skf26(skc5))*. % 15.66/15.91 27313[3:MRR:27304.0,27304.1,2.0,10.0] || -> . % 15.66/15.91 27315[3:Spt:27313.0,24234.1] || -> r1(skf23(skc8),skf24(skf23(skc8)))*. % 15.66/15.91 27377[3:Res:27315.0,44.3] p2(skf24(skf23(skc8))) || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 15.66/15.91 27379[3:SSi:27377.0,26152.0] || r1(skf24(skf23(skc8)),u)* r1(skc5,skc8) -> p2(skc8) p2(u). % 15.66/15.91 27380[3:MRR:27379.1,27379.2,2.0,5.0] || r1(skf24(skf23(skc8)),u)* -> p2(u). % 15.66/15.91 27390[3:Res:18.0,27380.0] || -> p2(skf25(skf23(skc8)))*. % 15.66/15.91 27391[3:MRR:27390.0,11.0] || -> . % 15.66/15.91 % SZS output end Refutation % 15.66/15.91 Formulae used in the proof : main % 15.66/15.91 %------------------------------------------------------------------------------