main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp2 = call i32 @__VERIFIER_nondet_int() br label %bb3 bb3: %.01 = phi i32 [%tmp, %bb], [%tmp7, %bb5] %.0 = phi i32 [%tmp2, %bb], [%tmp8, %bb5] %tmp4 = icmp sgt i32 %.01, 0 br i1 %tmp4, label %bb5, label %bb9 bb5: %tmp6 = add i32 %.01, %.0 %tmp7 = sub i32 %tmp6, 1 %tmp8 = sub i32 0, %.0 br label %bb3 bb9: ret i32 0 } 2.1 39 64 main bb3 2 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v23 tmp6 v24 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v3 0 v21 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 65 main bb3 2 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v23 tmp6 v24 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v3 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 v21 0 66 main bb3 3 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v27 tmp6 v24 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v27 1 v3 0 v21 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 67 main bb3 3 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v28 tmp6 v24 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v28 0 v3 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 v21 0 68 main bb5 0 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v27 tmp6 v24 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v27 1 v3 0 v21 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 69 main bb9 0 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v28 tmp6 v24 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v28 0 v3 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 v21 0 70 main bb5 1 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v27 tmp6 v29 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v27 1 v29 v21 v22 v3 0 v21 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 71 main bb5 2 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v27 tmp6 v29 tmp7 v30 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v27 1 v29 v21 v22 v30 v29 -1 1 v3 0 v21 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 72 main bb5 3 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v27 tmp6 v29 tmp7 v30 tmp8 v31 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v27 1 v29 v21 v22 v30 v29 -1 1 v31 0 -1 v22 v3 0 v21 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 73 main bb3 2 tmp v19 tmp2 v20 .01 v32 .0 v33 tmp4 v27 tmp6 v29 tmp7 v30 tmp8 v31 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v27 1 v29 v21 v22 v30 v29 -1 1 v31 0 -1 v22 v32 v30 v33 v31 v3 0 v21 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 39 main bb 0 40 main bb 1 tmp v1 41 main bb 2 tmp v1 tmp2 v2 42 main bb3 2 tmp v1 tmp2 v2 .01 v3 .0 v4 v3 v1 v4 v2 43 main bb3 2 tmp v1 tmp2 v2 .01 v3 .0 v4 v3 v1 v4 v2 v3 0 44 main bb3 2 tmp v1 tmp2 v2 .01 v3 .0 v4 v3 v1 v4 v2 v3 0 45 main bb3 3 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 v3 v1 v4 v2 v5 1 v3 0 46 main bb3 3 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v6 v3 v1 v4 v2 v6 0 v3 0 47 main bb5 0 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 v3 v1 v4 v2 v5 1 v3 0 48 main bb9 0 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v6 v3 v1 v4 v2 v6 0 v3 0 49 main bb5 1 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v7 v3 v1 v4 v2 v5 1 v7 v3 v4 v3 0 50 main bb5 2 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v7 tmp7 v8 v3 v1 v4 v2 v5 1 v7 v3 v4 v8 v7 -1 1 v3 0 51 main bb5 3 tmp v1 tmp2 v2 .01 v3 .0 v4 tmp4 v5 tmp6 v7 tmp7 v8 tmp8 v9 v3 v1 v4 v2 v5 1 v7 v3 v4 v8 v7 -1 1 v9 0 -1 v4 v3 0 52 main bb3 2 tmp v1 tmp2 v2 .01 v10 .0 v11 tmp4 v5 tmp6 v7 tmp7 v8 tmp8 v9 v3 v1 v4 v2 v5 1 v7 v3 v4 v8 v7 -1 1 v9 0 -1 v4 v10 v8 v11 v9 v3 0 63 main bb3 2 tmp v19 tmp2 v20 .01 v21 .0 v22 tmp4 v23 tmp6 v24 tmp7 v25 tmp8 v26 v3 v19 v4 v20 v23 1 v25 v24 -1 1 v21 v25 v22 v26 v3 0 v3 v19 v19 v3 v4 v20 v20 v4 v23 1 1 v23 v25 v24 -1 1 v24 -1 1 v25 v21 v25 v25 v21 v22 v26 v26 v22 64 66 v27 65 67 v28 66 68 67 69 68 70 v29 69 70 71 v30 71 72 v31 72
73 v32 v30 v33 v31
73 63 v19 v19 v20 v20 v21 v32 v22 v33 v23 v27 v24 v29 v25 v30 v26 v31 39 40 v1 40 41 v2 41
42 v3 v1 v4 v2
42 43 44 v3 0 43 45 v5 44 46 v6 45 47 46 48 47 49 v7 48 49 50 v8 50 51 v9 51
52 v10 v8 v11 v9
52 63 v19 v1 v20 v2 v21 v10 v22 v11 v23 v5 v24 v7 v25 v8 v26 v9 63 64 65 v21 0 66 49 68 70 72 51 43 40 47 64 71 67 50 39 46 63 44 65 42 73 41 52 45 1 43 45 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 v4 v2 v3 v1 0 v3 v4 v2 v5 1 v3 v1 0 v3 2 39 40 pp1 v1 3 63 65 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v21 0 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 4 73 63 pp1 v33 pp2 v32 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v31 pp1 v33 pp2 v32 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v31 v33 v31 v4 v20 v20 v4 v32 v30 0 v3 v22 v26 v23 1 v30 v29 -1 1 v23 1 1 v23 v31 0 -1 v22 v4 v20 v22 v26 v26 v22 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 v33 v31 v27 1 v27 1 1 v27 v4 v20 v33 v31 v31 v33 v4 v20 v20 v4 v3 v19 v19 v3 v3 v19 v32 v30 v30 v32 0 v3 v30 v29 -1 1 v29 -1 1 v30 v30 v29 -1 1 v32 v30 5 42 43 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 v4 v2 v3 v1 v4 v2 v3 v1 0 v3 6 45 47 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 v4 v2 v5 1 v3 v1 0 v3 v4 v2 v5 1 v3 v1 0 v3 7 64 66 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v24 pp7 v25 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 8 63 64 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 9 67 69 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v28 pp6 v24 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v28 pp6 v24 pp7 v25 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v28 0 v21 0 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v28 0 v21 0 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 10 40 41 pp1 v1 pp1 v1 pp2 v2 11 49 50 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 v4 v2 v7 v3 v4 v5 1 v3 v1 0 v3 v4 v2 v7 v3 v4 v8 v7 -1 1 v5 1 v3 v1 0 v3 12 41 42 pp1 v1 pp2 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 v4 v2 v3 v1 13 51 52 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp8 v9 pp1 v11 pp2 v10 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp8 v9 v4 v2 v7 v3 v4 v8 v7 -1 1 v5 1 v3 v1 v9 0 -1 v4 0 v3 v4 v2 v7 v3 v4 v8 v7 -1 1 v11 v9 v5 1 v3 v1 v9 0 -1 v4 0 v3 v10 v8 14 70 71 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 v22 v26 v23 1 v30 v29 -1 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 15 44 46 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 v4 v2 v3 v1 v3 0 v4 v2 v6 0 v3 v1 v3 0 16 66 68 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v24 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v24 pp7 v25 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 17 46 48 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 v4 v2 v6 0 v3 v1 v3 0 v4 v2 v6 0 v3 v1 v3 0 18 52 63 pp1 v11 pp2 v10 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp8 v9 pp1 v11 pp2 v10 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp8 v9 v4 v2 v7 v3 v4 v8 v7 -1 1 v11 v9 v5 1 v3 v1 v9 0 -1 v4 0 v3 v10 v8 v11 v9 v5 1 v5 1 1 v5 v4 v2 v11 v9 v9 v11 v4 v2 v2 v4 v3 v1 v1 v3 v3 v1 v10 v8 v8 v10 0 v3 v8 v7 -1 1 v7 -1 1 v8 v8 v7 -1 1 v10 v8 19 71 72 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v31 v22 v26 v23 1 v30 v29 -1 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 v22 v26 v23 1 v30 v29 -1 1 v23 1 1 v23 v31 0 -1 v22 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 20 72 73 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v31 pp1 v33 pp2 v32 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v31 v22 v26 v23 1 v30 v29 -1 1 v23 1 1 v23 v31 0 -1 v22 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 v33 v31 v4 v20 v20 v4 v32 v30 0 v3 v22 v26 v23 1 v30 v29 -1 1 v23 1 1 v23 v31 0 -1 v22 v4 v20 v22 v26 v26 v22 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 21 50 51 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp8 v9 v4 v2 v7 v3 v4 v8 v7 -1 1 v5 1 v3 v1 0 v3 v4 v2 v7 v3 v4 v8 v7 -1 1 v5 1 v3 v1 v9 0 -1 v4 0 v3 22 42 44 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp1 v4 pp2 v3 pp3 v1 pp4 v2 v4 v2 v3 v1 v4 v2 v3 v1 v3 0 23 65 67 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v28 pp6 v24 pp7 v25 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v21 0 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v28 0 v21 0 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 24 47 49 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 v4 v2 v5 1 v3 v1 0 v3 v4 v2 v7 v3 v4 v5 1 v3 v1 0 v3 25 68 70 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v24 pp7 v25 pp8 v26 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v25 pp8 v26 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v22 v26 v23 1 v23 1 1 v23 v4 v20 v22 v26 v26 v22 v4 v20 v20 v4 v27 1 0 v21 v3 v19 v19 v3 v3 v19 v21 v25 v25 v21 0 v3 v25 v24 -1 1 v24 -1 1 v25 v25 v24 -1 1 v21 v25 v29 v21 v22 64 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 65 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 66 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v24 pp7 v25 pp8 v26 67 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v28 pp6 v24 pp7 v25 pp8 v26 68 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v24 pp7 v25 pp8 v26 69 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v28 pp6 v24 pp7 v25 pp8 v26 70 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v25 pp8 v26 71 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v26 72 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v31 73 pp1 v33 pp2 v32 pp3 v19 pp4 v20 pp5 v27 pp6 v29 pp7 v30 pp8 v31 39 40 pp1 v1 41 pp1 v1 pp2 v2 42 pp1 v4 pp2 v3 pp3 v1 pp4 v2 43 pp1 v4 pp2 v3 pp3 v1 pp4 v2 44 pp1 v4 pp2 v3 pp3 v1 pp4 v2 45 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 46 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 47 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 48 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v6 49 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 50 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 51 pp1 v4 pp2 v3 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp8 v9 52 pp1 v11 pp2 v10 pp3 v1 pp4 v2 pp5 v5 pp6 v7 pp7 v8 pp8 v9 63 pp1 v22 pp2 v21 pp3 v19 pp4 v20 pp5 v23 pp6 v24 pp7 v25 pp8 v26 AProVE AProVE Commit ID: unknown Statistics for single proof: 75,00 % (3 real / 0 unknown / 1 assumptions / 4 total proof steps) http://aprove.informatik.rwth-aachen.de John Doe