main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp3 = call i32 @__VERIFIER_nondet_int() %tmp4 = call i32 @__VERIFIER_nondet_int() br label %bb5 bb5: %.02 = phi i32 [%tmp3, %bb], [%.0, %bb7] %.01 = phi i32 [%tmp, %bb], [%tmp8, %bb7] %.0 = phi i32 [%tmp4, %bb], [%tmp10, %bb7] %tmp6 = icmp sgt i32 %.01, 0 br i1 %tmp6, label %bb7, label %bb11 bb7: %tmp8 = add i32 %.01, %.02 %tmp9 = sub i32 0, %.0 %tmp10 = sub i32 %tmp9, 1 br label %bb5 bb11: ret i32 0 } 2.1 45 70 main bb5 3 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v29 tmp8 v30 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v5 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 71 main bb5 3 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v29 tmp8 v30 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v5 0 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 72 main bb5 3 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v29 tmp8 v30 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v5 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 v27 0 73 main bb5 4 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v33 tmp8 v30 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v33 1 v5 0 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 74 main bb5 4 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v34 tmp8 v30 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v34 0 v5 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 v27 0 75 main bb7 0 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v33 tmp8 v30 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v33 1 v5 0 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 76 main bb11 0 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v34 tmp8 v30 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v34 0 v5 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 v27 0 77 main bb7 1 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v33 tmp8 v35 tmp9 v31 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v33 1 v35 v27 v26 v5 0 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 78 main bb7 2 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v33 tmp8 v35 tmp9 v36 tmp10 v32 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v33 1 v35 v27 v26 v36 0 -1 v28 v5 0 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 79 main bb7 3 tmp v23 tmp3 v24 tmp4 v25 .02 v26 .01 v27 .0 v28 tmp6 v33 tmp8 v35 tmp9 v36 tmp10 v37 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v33 1 v35 v27 v26 v36 0 -1 v28 v37 v36 -1 1 v5 0 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 80 main bb5 3 tmp v23 tmp3 v24 tmp4 v25 .02 v38 .01 v39 .0 v40 tmp6 v33 tmp8 v35 tmp9 v36 tmp10 v37 v4 v24 v5 v23 v6 v25 v29 1 v32 v31 -1 1 v27 v30 v28 v32 v33 1 v35 v27 v26 v36 0 -1 v28 v37 v36 -1 1 v38 v28 v39 v35 v40 v37 v5 0 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v6 v25 v25 v6 v29 1 1 v29 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v30 v27 v28 v32 v32 v28 45 main bb 0 46 main bb 1 tmp v1 47 main bb 2 tmp v1 tmp3 v2 48 main bb 3 tmp v1 tmp3 v2 tmp4 v3 49 main bb5 3 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 v4 v2 v5 v1 v6 v3 50 main bb5 3 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 v4 v2 v5 v1 v6 v3 v5 0 51 main bb5 3 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 v4 v2 v5 v1 v6 v3 v5 0 52 main bb5 4 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 tmp6 v7 v4 v2 v5 v1 v6 v3 v7 1 v5 0 53 main bb5 4 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 tmp6 v8 v4 v2 v5 v1 v6 v3 v8 0 v5 0 54 main bb7 0 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 tmp6 v7 v4 v2 v5 v1 v6 v3 v7 1 v5 0 55 main bb11 0 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 tmp6 v8 v4 v2 v5 v1 v6 v3 v8 0 v5 0 56 main bb7 1 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 tmp6 v7 tmp8 v9 v4 v2 v5 v1 v6 v3 v7 1 v9 v5 v4 v5 0 57 main bb7 2 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 tmp6 v7 tmp8 v9 tmp9 v10 v4 v2 v5 v1 v6 v3 v7 1 v9 v5 v4 v10 0 -1 v6 v5 0 58 main bb7 3 tmp v1 tmp3 v2 tmp4 v3 .02 v4 .01 v5 .0 v6 tmp6 v7 tmp8 v9 tmp9 v10 tmp10 v11 v4 v2 v5 v1 v6 v3 v7 1 v9 v5 v4 v10 0 -1 v6 v11 v10 -1 1 v5 0 59 main bb5 3 tmp v1 tmp3 v2 tmp4 v3 .02 v12 .01 v13 .0 v14 tmp6 v7 tmp8 v9 tmp9 v10 tmp10 v11 v4 v2 v5 v1 v6 v3 v7 1 v9 v5 v4 v10 0 -1 v6 v11 v10 -1 1 v12 v6 v13 v9 v14 v11 v5 0 70 71 72 v27 0 71 73 v33 72 74 v34 73 75 74 76 75 77 v35 76 77 78 v36 78 79 v37 79
80 v38 v28 v39 v35 v40 v37
80 70 v23 v23 v24 v24 v25 v25 v26 v38 v27 v39 v28 v40 v29 v33 v30 v35 v31 v36 v32 v37 45 46 v1 46 47 v2 47 48 v3 48
49 v4 v2 v5 v1 v6 v3
49 50 51 v5 0 50 52 v7 51 53 v8 52 54 53 55 54 56 v9 55 56 57 v10 57 58 v11 58
59 v12 v6 v13 v9 v14 v11
59 70 v23 v1 v24 v2 v25 v3 v26 v12 v27 v13 v28 v14 v29 v7 v30 v9 v31 v10 v32 v11 49 70 79 53 77 72 51 75 74 47 54 57 78 71 50 80 48 46 56 58 59 73 52 45 1 47 48 pp1 v1 pp2 v2 pp1 v1 pp2 v2 pp3 v3 2 52 54 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 v6 v3 v7 1 v4 v2 v5 v1 0 v5 v6 v3 v7 1 v4 v2 v5 v1 0 v5 3 79 80 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v37 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 pp1 v40 pp2 v39 pp3 v38 pp4 v23 pp5 v37 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 v37 v36 -1 1 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v36 0 -1 v28 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 v37 v36 -1 1 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v39 v35 v29 1 v28 v32 v32 v28 v28 v32 v36 0 -1 v28 v40 v37 0 v27 v4 v24 v5 v23 v38 v28 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 4 50 52 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 v6 v3 v4 v2 v5 v1 0 v5 v6 v3 v7 1 v4 v2 v5 v1 0 v5 5 46 47 pp1 v1 pp1 v1 pp2 v2 6 78 79 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v37 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v36 0 -1 v28 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 v37 v36 -1 1 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v36 0 -1 v28 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 7 54 56 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp8 v9 v6 v3 v7 1 v4 v2 v5 v1 0 v5 v6 v3 v7 1 v4 v2 v5 v1 v9 v5 v4 0 v5 8 74 76 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v34 pp9 v30 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v34 pp9 v30 pp10 v31 v4 v24 v5 v23 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v34 0 v4 v24 v5 v23 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v34 0 9 49 51 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 v6 v3 v4 v2 v5 v1 v6 v3 v4 v2 v5 v1 v5 0 10 59 70 pp1 v14 pp2 v13 pp3 v12 pp4 v1 pp5 v11 pp6 v2 pp7 v3 pp8 v7 pp9 v9 pp10 v10 pp1 v14 pp2 v13 pp3 v12 pp4 v1 pp5 v11 pp6 v2 pp7 v3 pp8 v7 pp9 v9 pp10 v10 v6 v3 v7 1 v4 v2 v5 v1 v12 v6 v10 0 -1 v6 v13 v9 v14 v11 v9 v5 v4 v11 v10 -1 1 0 v5 v4 v2 v5 v1 v4 v2 v2 v4 v5 v1 v1 v5 v11 v10 -1 1 v10 -1 1 v11 v13 v9 v11 v10 -1 1 v13 v9 v9 v13 0 v5 v6 v3 v3 v6 v7 1 1 v7 v6 v3 v7 1 v14 v11 v11 v14 v14 v11 11 70 72 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v4 v24 v5 v23 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 12 49 50 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 v6 v3 v4 v2 v5 v1 v6 v3 v4 v2 v5 v1 0 v5 13 53 55 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v8 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v8 v6 v3 v8 0 v4 v2 v5 v1 v5 0 v6 v3 v8 0 v4 v2 v5 v1 v5 0 14 70 71 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 15 77 78 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v36 0 -1 v28 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 16 80 70 pp1 v40 pp2 v39 pp3 v38 pp4 v23 pp5 v37 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 pp1 v40 pp2 v39 pp3 v38 pp4 v23 pp5 v37 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 v37 v36 -1 1 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v39 v35 v29 1 v28 v32 v32 v28 v28 v32 v36 0 -1 v28 v40 v37 0 v27 v4 v24 v5 v23 v38 v28 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v37 v36 -1 1 v36 -1 1 v37 v39 v35 v37 v36 -1 1 v39 v35 v35 v39 0 v5 v6 v25 v25 v6 v33 1 1 v33 v6 v25 v33 1 v40 v37 v37 v40 v40 v37 17 72 74 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v34 pp9 v30 pp10 v31 v4 v24 v5 v23 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v4 v24 v5 v23 v27 0 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v34 0 18 51 53 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v8 v6 v3 v4 v2 v5 v1 v5 0 v6 v3 v8 0 v4 v2 v5 v1 v5 0 19 71 73 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v30 pp10 v31 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v33 1 20 57 58 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp8 v9 pp9 v10 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v11 pp6 v2 pp7 v3 pp8 v7 pp9 v9 pp10 v10 v6 v3 v7 1 v4 v2 v5 v1 v10 0 -1 v6 v9 v5 v4 0 v5 v6 v3 v7 1 v4 v2 v5 v1 v10 0 -1 v6 v9 v5 v4 v11 v10 -1 1 0 v5 21 58 59 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v11 pp6 v2 pp7 v3 pp8 v7 pp9 v9 pp10 v10 pp1 v14 pp2 v13 pp3 v12 pp4 v1 pp5 v11 pp6 v2 pp7 v3 pp8 v7 pp9 v9 pp10 v10 v6 v3 v7 1 v4 v2 v5 v1 v10 0 -1 v6 v9 v5 v4 v11 v10 -1 1 0 v5 v6 v3 v7 1 v4 v2 v5 v1 v12 v6 v10 0 -1 v6 v13 v9 v14 v11 v9 v5 v4 v11 v10 -1 1 0 v5 22 73 75 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v30 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v30 pp10 v31 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v33 1 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v33 1 23 56 57 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp8 v9 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp8 v9 pp9 v10 v6 v3 v7 1 v4 v2 v5 v1 v9 v5 v4 0 v5 v6 v3 v7 1 v4 v2 v5 v1 v10 0 -1 v6 v9 v5 v4 0 v5 24 45 46 pp1 v1 25 75 77 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v30 pp10 v31 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v31 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 0 v5 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 v33 1 0 v5 v35 v27 v26 v6 v25 v25 v6 v29 1 1 v29 v6 v25 v29 1 v28 v32 v32 v28 v28 v32 0 v27 v4 v24 v5 v23 v4 v24 v24 v4 v5 v23 v23 v5 v32 v31 -1 1 v31 -1 1 v32 v27 v30 v32 v31 -1 1 v27 v30 v30 v27 v33 1 26 48 49 pp1 v1 pp2 v2 pp3 v3 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 v6 v3 v4 v2 v5 v1 70 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 71 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 72 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v29 pp9 v30 pp10 v31 73 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v30 pp10 v31 74 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v34 pp9 v30 pp10 v31 75 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v30 pp10 v31 76 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v34 pp9 v30 pp10 v31 77 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v31 78 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v32 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 79 pp1 v28 pp2 v27 pp3 v26 pp4 v23 pp5 v37 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 80 pp1 v40 pp2 v39 pp3 v38 pp4 v23 pp5 v37 pp6 v24 pp7 v25 pp8 v33 pp9 v35 pp10 v36 45 46 pp1 v1 47 pp1 v1 pp2 v2 48 pp1 v1 pp2 v2 pp3 v3 49 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 50 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 51 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 52 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 53 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v8 54 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 55 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v8 56 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp8 v9 57 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v2 pp6 v3 pp7 v7 pp8 v9 pp9 v10 58 pp1 v6 pp2 v5 pp3 v4 pp4 v1 pp5 v11 pp6 v2 pp7 v3 pp8 v7 pp9 v9 pp10 v10 59 pp1 v14 pp2 v13 pp3 v12 pp4 v1 pp5 v11 pp6 v2 pp7 v3 pp8 v7 pp9 v9 pp10 v10 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