main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() br label %bb4 bb4: %.03 = phi i32 [0, %bb], [%tmp13, %bb12] %.01 = phi i32 [%tmp, %bb], [%.02, %bb12] %tmp5 = icmp sgt i32 %.01, 1 br i1 %tmp5, label %bb6, label %bb14 bb6: br label %bb7 bb7: %.02 = phi i32 [%.01, %bb6], [%tmp10, %bb9] %.0 = phi i32 [0, %bb6], [%tmp11, %bb9] %tmp8 = icmp sgt i32 %.02, 1 br i1 %tmp8, label %bb9, label %bb12 bb9: %tmp10 = sub i32 %.02, 2 %tmp11 = add i32 %.0, 1 br label %bb7 bb12: %tmp13 = add i32 %.03, 1 br label %bb4 bb14: ret i32 0 } 2.1 54 64 main bb7 3 tmp v1 .03 v2 .01 v3 tmp5 v4 .02 v6 .0 v7 tmp8 v8 v2 0 v3 v1 v4 1 v6 v3 v7 0 v8 1 v3 1 65 main bb9 0 tmp v1 .03 v2 .01 v3 tmp5 v4 .02 v6 .0 v7 tmp8 v8 v2 0 v3 v1 v4 1 v6 v3 v7 0 v8 1 v3 1 v6 1 66 main bb9 1 tmp v1 .03 v2 .01 v3 tmp5 v4 .02 v6 .0 v7 tmp8 v8 tmp10 v9 v2 0 v3 v1 v4 1 v6 v3 v7 0 v8 1 v9 v6 -1 2 v3 1 v6 1 67 main bb9 2 tmp v1 .03 v2 .01 v3 tmp5 v4 .02 v6 .0 v7 tmp8 v8 tmp10 v9 tmp11 v10 v2 0 v3 v1 v4 1 v6 v3 v7 0 v8 1 v9 v6 -1 2 v10 v7 1 v3 1 v6 1 68 main bb7 2 tmp v1 .03 v2 .01 v3 tmp5 v4 .02 v11 .0 v12 tmp8 v8 tmp10 v9 tmp11 v10 v2 0 v3 v1 v4 1 v6 v3 v7 0 v8 1 v9 v6 -1 2 v10 v7 1 v11 v9 v12 v10 v3 1 v6 1 80 main bb7 2 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v28 tmp10 v29 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 81 main bb7 2 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v28 tmp10 v29 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v24 1 v6 1 v26 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 82 main bb7 2 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v28 tmp10 v29 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 v26 1 83 main bb7 3 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v31 tmp10 v29 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v31 1 v24 1 v6 1 v26 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 84 main bb7 3 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v32 tmp10 v29 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v32 0 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 v26 1 85 main bb9 0 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v31 tmp10 v29 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v31 1 v24 1 v6 1 v26 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 86 main bb12 0 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v32 tmp10 v29 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v32 0 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 v26 1 87 main bb9 1 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v31 tmp10 v33 tmp11 v30 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v31 1 v33 v26 -1 2 v24 1 v6 1 v26 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 88 main bb12 1 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v32 tmp10 v29 tmp11 v30 tmp13 v34 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v32 0 v34 v23 1 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 v26 1 89 main bb9 2 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v26 .0 v27 tmp8 v31 tmp10 v33 tmp11 v35 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v31 1 v33 v26 -1 2 v35 v27 1 v24 1 v6 1 v26 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 90 main bb4 2 tmp v22 .03 v36 .01 v37 tmp5 v25 .02 v26 .0 v27 tmp8 v32 tmp10 v29 tmp11 v30 tmp13 v34 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v32 0 v34 v23 1 v36 v34 v37 v26 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 v26 1 91 main bb7 2 tmp v22 .03 v23 .01 v24 tmp5 v25 .02 v38 .0 v39 tmp8 v31 tmp10 v33 tmp11 v35 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v31 1 v33 v26 -1 2 v35 v27 1 v38 v33 v39 v35 v24 1 v6 1 v26 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 92 main bb4 3 tmp v22 .03 v36 .01 v37 tmp5 v49 .02 v26 .0 v27 tmp8 v32 tmp10 v29 tmp11 v30 tmp13 v34 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v32 0 v34 v23 1 v36 v34 v37 v26 v49 0 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 v26 1 93 main bb14 0 tmp v22 .03 v36 .01 v37 tmp5 v49 .02 v26 .0 v27 tmp8 v32 tmp10 v29 tmp11 v30 tmp13 v34 v23 0 v24 v22 v25 1 v6 v24 v7 0 v28 1 v26 v29 v27 v30 v32 0 v34 v23 1 v36 v34 v37 v26 v49 0 v24 1 v6 1 v23 0 0 v23 v24 v22 v22 v24 v25 1 1 v25 v6 v24 v24 v6 v7 0 0 v7 v28 1 1 v28 v26 v29 v29 v26 v27 v30 v30 v27 v26 1 v37 1 54 main bb 0 55 main bb 1 tmp v1 56 main bb4 2 tmp v1 .03 v2 .01 v3 v2 0 v3 v1 57 main bb4 2 tmp v1 .03 v2 .01 v3 v2 0 v3 v1 v3 1 58 main bb4 2 tmp v1 .03 v2 .01 v3 v2 0 v3 v1 v3 1 59 main bb4 3 tmp v1 .03 v2 .01 v3 tmp5 v4 v2 0 v3 v1 v4 1 v3 1 60 main bb4 3 tmp v1 .03 v2 .01 v3 tmp5 v5 v2 0 v3 v1 v5 0 v3 1 61 main bb6 0 tmp v1 .03 v2 .01 v3 tmp5 v4 v2 0 v3 v1 v4 1 v3 1 62 main bb14 0 tmp v1 .03 v2 .01 v3 tmp5 v5 v2 0 v3 v1 v5 0 v3 1 63 main bb7 2 tmp v1 .03 v2 .01 v3 tmp5 v4 .02 v6 .0 v7 v2 0 v3 v1 v4 1 v6 v3 v7 0 v3 1 64 65 65 66 v9 66 67 v10 67
68 v11 v9 v12 v10
68 80 v22 v1 v23 v2 v24 v3 v25 v4 v26 v11 v27 v12 v28 v8 v29 v9 v30 v10 80 81 82 v26 1 81 83 v31 82 84 v32 83 85 84 86 85 87 v33 86 88 v34 87 89 v35 88
90 v36 v34 v37 v26
89
91 v38 v33 v39 v35
90 92 v49 91 80 v22 v22 v23 v23 v24 v24 v25 v25 v26 v38 v27 v39 v28 v31 v29 v33 v30 v35 92 93 93 54 55 v1 55
56 v2 0 v3 v1
56 57 58 v3 1 57 59 v4 58 60 v5 59 61 60 62 61
63 v6 v3 v7 0
62 63 64 v8 68 81 89 60 64 85 67 80 86 65 58 59 87 83 66 91 92 61 54 88 57 82 56 63 84 90 55 1 68 80 pp1 v12 pp2 v3 pp3 v11 pp4 v2 pp5 v1 pp6 v9 pp7 v10 pp8 v4 pp9 v8 pp1 v12 pp2 v3 pp3 v11 pp4 v2 pp5 v1 pp6 v9 pp7 v10 pp8 v4 pp9 v8 v4 1 v9 v6 -1 2 v2 0 v8 1 v12 v10 v3 v1 v6 v3 v10 v7 1 v11 v9 1 v6 1 v3 v7 0 v3 v1 v3 v1 v1 v3 v4 1 1 v6 v4 1 1 v4 v7 0 0 v7 v7 0 v6 v3 v3 v6 v6 v3 v8 1 v8 1 1 v8 v12 v10 v12 v10 v10 v12 v11 v9 v9 v11 1 v3 v2 0 v2 0 0 v2 v11 v9 2 54 55 pp1 v1 3 58 60 pp1 v3 pp2 v2 pp3 v1 pp1 v3 pp2 v2 pp3 v1 pp4 v5 v2 0 v3 1 v3 v1 v5 0 v2 0 v3 1 v3 v1 4 55 56 pp1 v1 pp1 v3 pp2 v2 pp3 v1 v2 0 v3 v1 5 84 86 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v32 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v32 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 6 67 68 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v9 pp7 v10 pp8 v4 pp9 v8 pp1 v12 pp2 v3 pp3 v11 pp4 v2 pp5 v1 pp6 v9 pp7 v10 pp8 v4 pp9 v8 v4 1 v9 v6 -1 2 v2 0 v8 1 v3 v1 v6 v3 v10 v7 1 1 v6 1 v3 v7 0 v4 1 v9 v6 -1 2 v2 0 v8 1 v12 v10 v3 v1 v6 v3 v10 v7 1 v11 v9 1 v6 1 v3 v7 0 7 59 61 pp1 v3 pp2 v2 pp3 v1 pp4 v4 pp1 v3 pp2 v2 pp3 v1 pp4 v4 v4 1 v2 0 v3 v1 1 v3 v4 1 v2 0 v3 v1 1 v3 8 65 66 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 pp7 v8 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v9 pp7 v4 pp8 v8 v4 1 v2 0 v8 1 v3 v1 v6 v3 1 v6 1 v3 v7 0 v4 1 v9 v6 -1 2 v2 0 v8 1 v3 v1 v6 v3 1 v6 1 v3 v7 0 9 83 85 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v31 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v31 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 10 60 62 pp1 v3 pp2 v2 pp3 v1 pp4 v5 pp1 v3 pp2 v2 pp3 v1 pp4 v5 v5 0 v2 0 v3 1 v3 v1 v5 0 v2 0 v3 1 v3 v1 11 87 89 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v33 pp7 v30 pp8 v25 pp9 v31 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v33 pp7 v35 pp8 v25 pp9 v31 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 v33 v26 -1 2 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v35 v27 1 v26 v29 v29 v26 v33 v26 -1 2 1 v24 v23 0 v23 0 0 v23 v26 v29 12 61 63 pp1 v3 pp2 v2 pp3 v1 pp4 v4 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 v4 1 v2 0 v3 v1 1 v3 v4 1 v2 0 v3 v1 v6 v3 1 v3 v7 0 13 64 65 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 pp7 v8 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 pp7 v8 v4 1 v2 0 v8 1 v3 v1 v6 v3 1 v6 1 v3 v7 0 v4 1 v2 0 v8 1 v3 v1 v6 v3 1 v6 1 v3 v7 0 14 92 93 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v49 pp10 v32 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v49 pp10 v32 v37 1 v24 v22 v24 v22 v22 v24 v25 1 v37 v26 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v49 0 v26 v29 v29 v26 1 v24 v36 v34 v23 0 v34 v23 1 v23 0 0 v23 v26 v29 v37 1 v24 v22 v24 v22 v22 v24 v25 1 v37 v26 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v49 0 v26 v29 v29 v26 1 v24 v36 v34 v23 0 v34 v23 1 v23 0 0 v23 v26 v29 15 66 67 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v9 pp7 v4 pp8 v8 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v9 pp7 v10 pp8 v4 pp9 v8 v4 1 v9 v6 -1 2 v2 0 v8 1 v3 v1 v6 v3 1 v6 1 v3 v7 0 v4 1 v9 v6 -1 2 v2 0 v8 1 v3 v1 v6 v3 v10 v7 1 1 v6 1 v3 v7 0 16 86 88 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v32 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v25 pp10 v32 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v34 v23 1 v23 0 0 v23 v26 v29 17 82 84 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v32 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 18 56 58 pp1 v3 pp2 v2 pp3 v1 pp1 v3 pp2 v2 pp3 v1 v2 0 v3 v1 v2 0 v3 1 v3 v1 19 80 82 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 20 91 80 pp1 v39 pp2 v24 pp3 v38 pp4 v23 pp5 v22 pp6 v33 pp7 v35 pp8 v25 pp9 v31 pp1 v39 pp2 v24 pp3 v38 pp4 v23 pp5 v22 pp6 v33 pp7 v35 pp8 v25 pp9 v31 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v38 v33 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v35 v27 1 v39 v35 v26 v29 v29 v26 v33 v26 -1 2 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v31 1 v31 1 1 v31 v39 v35 v39 v35 v35 v39 v38 v33 v33 v38 1 v24 v23 0 v23 0 0 v23 v38 v33 21 57 59 pp1 v3 pp2 v2 pp3 v1 pp1 v3 pp2 v2 pp3 v1 pp4 v4 v2 0 v3 v1 1 v3 v4 1 v2 0 v3 v1 1 v3 22 85 87 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v31 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v33 pp7 v30 pp8 v25 pp9 v31 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 v33 v26 -1 2 1 v24 v23 0 v23 0 0 v23 v26 v29 23 81 83 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v31 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 24 63 64 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 pp7 v8 v4 1 v2 0 v3 v1 v6 v3 1 v3 v7 0 v4 1 v2 0 v8 1 v3 v1 v6 v3 1 v6 1 v3 v7 0 25 89 91 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v33 pp7 v35 pp8 v25 pp9 v31 pp1 v39 pp2 v24 pp3 v38 pp4 v23 pp5 v22 pp6 v33 pp7 v35 pp8 v25 pp9 v31 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v35 v27 1 v26 v29 v29 v26 v33 v26 -1 2 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v38 v33 v6 v24 v28 1 v28 1 1 v28 v31 1 1 v26 v27 v30 v27 v30 v30 v27 v35 v27 1 v39 v35 v26 v29 v29 v26 v33 v26 -1 2 1 v24 v23 0 v23 0 0 v23 v26 v29 26 90 92 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v25 pp10 v32 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v49 pp10 v32 v24 v22 v24 v22 v22 v24 v25 1 v37 v26 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v36 v34 v23 0 v34 v23 1 v23 0 0 v23 v26 v29 v37 1 v24 v22 v24 v22 v22 v24 v25 1 v37 v26 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v49 0 v26 v29 v29 v26 1 v24 v36 v34 v23 0 v34 v23 1 v23 0 0 v23 v26 v29 27 56 57 pp1 v3 pp2 v2 pp3 v1 pp1 v3 pp2 v2 pp3 v1 v2 0 v3 v1 v2 0 v3 v1 1 v3 28 88 90 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v25 pp10 v32 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v25 pp10 v32 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v34 v23 1 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 v37 v26 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v26 1 v32 0 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v36 v34 v23 0 v34 v23 1 v23 0 0 v23 v26 v29 29 80 81 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 v24 v22 v24 v22 v22 v24 v25 1 1 v6 v25 1 1 v25 v7 0 0 v7 v7 0 v6 v24 v24 v6 v6 v24 v28 1 v28 1 1 v28 1 v26 v27 v30 v27 v30 v30 v27 v26 v29 v29 v26 1 v24 v23 0 v23 0 0 v23 v26 v29 64 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 pp7 v8 65 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 pp7 v8 66 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v9 pp7 v4 pp8 v8 67 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v9 pp7 v10 pp8 v4 pp9 v8 68 pp1 v12 pp2 v3 pp3 v11 pp4 v2 pp5 v1 pp6 v9 pp7 v10 pp8 v4 pp9 v8 80 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 81 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 82 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v28 83 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v31 84 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v32 85 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v31 86 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v25 pp9 v32 87 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v33 pp7 v30 pp8 v25 pp9 v31 88 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v25 pp10 v32 89 pp1 v27 pp2 v24 pp3 v26 pp4 v23 pp5 v22 pp6 v33 pp7 v35 pp8 v25 pp9 v31 90 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v25 pp10 v32 91 pp1 v39 pp2 v24 pp3 v38 pp4 v23 pp5 v22 pp6 v33 pp7 v35 pp8 v25 pp9 v31 92 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v49 pp10 v32 93 pp1 v27 pp2 v37 pp3 v26 pp4 v36 pp5 v22 pp6 v29 pp7 v30 pp8 v34 pp9 v49 pp10 v32 54 55 pp1 v1 56 pp1 v3 pp2 v2 pp3 v1 57 pp1 v3 pp2 v2 pp3 v1 58 pp1 v3 pp2 v2 pp3 v1 59 pp1 v3 pp2 v2 pp3 v1 pp4 v4 60 pp1 v3 pp2 v2 pp3 v1 pp4 v5 61 pp1 v3 pp2 v2 pp3 v1 pp4 v4 62 pp1 v3 pp2 v2 pp3 v1 pp4 v5 63 pp1 v7 pp2 v3 pp3 v6 pp4 v2 pp5 v1 pp6 v4 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