main declare i32 @__VERIFIER_nondet_int() define i32 @main() { bb: %tmp = call i32 @__VERIFIER_nondet_int() %tmp1 = call i32 @__VERIFIER_nondet_int() br label %bb2 bb2: %.0 = phi i32 [%tmp, %bb], [%tmp11, %bb8] %tmp3 = icmp sgt i32 %.0, 0 br i1 %tmp3, label %bb4, label %bb6 bb4: %tmp5 = icmp sgt i32 %tmp1, 0 br label %bb6 bb6: %tmp7 = phi i1 [0, %bb2], [%tmp5, %bb4] br i1 %tmp7, label %bb8, label %bb12 bb8: %tmp9 = mul i32 10, %tmp1 %tmp10 = mul i32 2, %.0 %tmp11 = sub i32 %tmp9, %tmp10 br label %bb2 bb12: ret i32 0 } 2.1 48 64 main bb6 1 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v8 tmp7 v10 v3 v1 v4 1 v8 0 v10 v8 v3 0 v2 0 65 main bb8 0 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v7 tmp7 v9 v3 v1 v4 1 v7 1 v9 v7 v3 0 v2 0 66 main bb12 0 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v8 tmp7 v10 v3 v1 v4 1 v8 0 v10 v8 v3 0 v2 0 67 main bb8 1 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v7 tmp7 v9 tmp9 v17 v3 v1 v4 1 v7 1 v9 v7 v9 1 v17 10 v2 v3 0 v2 0 68 main bb8 2 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v7 tmp7 v9 tmp9 v17 tmp10 v18 v3 v1 v4 1 v7 1 v9 v7 v9 1 v17 10 v2 v18 2 v3 v3 0 v2 0 69 main bb8 3 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v7 tmp7 v9 tmp9 v17 tmp10 v18 tmp11 v19 v3 v1 v4 1 v7 1 v9 v7 v9 1 v17 10 v2 v18 2 v3 v19 v17 -1 v18 v3 0 v2 0 70 main bb2 1 tmp v1 tmp1 v2 .0 v20 tmp3 v4 tmp5 v7 tmp7 v9 tmp9 v17 tmp10 v18 tmp11 v19 v3 v1 v4 1 v7 1 v9 v7 v9 1 v17 10 v2 v18 2 v3 v19 v17 -1 v18 v20 v19 v3 0 v2 0 89 main bb2 1 tmp v39 tmp1 v40 .0 v41 tmp3 v42 tmp5 v43 tmp7 v44 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v3 0 v40 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 90 main bb2 1 tmp v39 tmp1 v40 .0 v41 tmp3 v42 tmp5 v43 tmp7 v44 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 91 main bb2 1 tmp v39 tmp1 v40 .0 v41 tmp3 v42 tmp5 v43 tmp7 v44 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v3 0 v40 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 v41 0 92 main bb2 2 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v43 tmp7 v44 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 93 main bb2 2 tmp v39 tmp1 v40 .0 v41 tmp3 v49 tmp5 v43 tmp7 v44 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v49 0 v3 0 v40 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 v41 0 94 main bb4 0 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v43 tmp7 v44 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 95 main bb6 1 tmp v39 tmp1 v40 .0 v41 tmp3 v49 tmp5 v43 tmp7 v50 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v49 0 v50 0 v3 0 v40 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 v41 0 96 main bb4 1 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v51 tmp7 v44 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v51 1 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 97 main bb12 0 tmp v39 tmp1 v40 .0 v41 tmp3 v49 tmp5 v43 tmp7 v50 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v49 0 v50 0 v3 0 v40 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 v41 0 98 main bb6 1 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v51 tmp7 v52 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v51 1 v52 v51 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 99 main bb8 0 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v51 tmp7 v52 tmp9 v45 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v51 1 v52 v51 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 100 main bb8 1 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v51 tmp7 v52 tmp9 v62 tmp10 v46 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v51 1 v52 v51 v52 1 v62 10 v40 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 101 main bb8 2 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v51 tmp7 v52 tmp9 v62 tmp10 v63 tmp11 v47 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v51 1 v52 v51 v52 1 v62 10 v40 v63 2 v41 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 102 main bb8 3 tmp v39 tmp1 v40 .0 v41 tmp3 v48 tmp5 v51 tmp7 v52 tmp9 v62 tmp10 v63 tmp11 v64 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v51 1 v52 v51 v52 1 v62 10 v40 v63 2 v41 v64 v62 -1 v63 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 103 main bb2 1 tmp v39 tmp1 v40 .0 v65 tmp3 v48 tmp5 v51 tmp7 v52 tmp9 v62 tmp10 v63 tmp11 v64 v3 v39 v43 1 v44 1 v45 10 v40 v47 v45 -1 v46 v41 v47 v44 v43 v48 1 v51 1 v52 v51 v52 1 v62 10 v40 v63 2 v41 v64 v62 -1 v63 v65 v64 v3 0 v40 0 v41 0 v3 v39 v39 v3 v42 1 v43 1 1 v43 v44 v43 v44 1 1 v44 v45 10 v40 10 v40 v45 v47 v45 -1 v46 v45 -1 v46 v47 v41 v47 v47 v41 48 main bb 0 49 main bb 1 tmp v1 50 main bb 2 tmp v1 tmp1 v2 51 main bb2 1 tmp v1 tmp1 v2 .0 v3 v3 v1 52 main bb2 1 tmp v1 tmp1 v2 .0 v3 v3 v1 v3 0 53 main bb2 1 tmp v1 tmp1 v2 .0 v3 v3 v1 v3 0 54 main bb2 2 tmp v1 tmp1 v2 .0 v3 tmp3 v4 v3 v1 v4 1 v3 0 55 main bb2 2 tmp v1 tmp1 v2 .0 v3 tmp3 v5 v3 v1 v5 0 v3 0 56 main bb4 0 tmp v1 tmp1 v2 .0 v3 tmp3 v4 v3 v1 v4 1 v3 0 57 main bb6 1 tmp v1 tmp1 v2 .0 v3 tmp3 v5 tmp7 v6 v3 v1 v5 0 v6 0 v3 0 58 main bb4 0 tmp v1 tmp1 v2 .0 v3 tmp3 v4 v3 v1 v4 1 v3 0 v2 0 59 main bb4 0 tmp v1 tmp1 v2 .0 v3 tmp3 v4 v3 v1 v4 1 v3 0 v2 0 60 main bb12 0 tmp v1 tmp1 v2 .0 v3 tmp3 v5 tmp7 v6 v3 v1 v5 0 v6 0 v3 0 61 main bb4 1 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v7 v3 v1 v4 1 v7 1 v3 0 v2 0 62 main bb4 1 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v8 v3 v1 v4 1 v8 0 v3 0 v2 0 63 main bb6 1 tmp v1 tmp1 v2 .0 v3 tmp3 v4 tmp5 v7 tmp7 v9 v3 v1 v4 1 v7 1 v9 v7 v3 0 v2 0 64 66 65 67 v17 66 67 68 v18 68 69 v19 69
70 v20 v19
70 89 v39 v1 v40 v2 v41 v20 v42 v4 v43 v7 v44 v9 v45 v17 v46 v18 v47 v19 89 90 91 v41 0 90 92 v48 91 93 v49 92 94 93 95 v50 0 94 96 v51 95 97 96
98 v52 v51
97 98 99 99 100 v62 100 101 v63 101 102 v64 102
103 v65 v64
103 89 v39 v39 v40 v40 v41 v65 v42 v48 v43 v51 v44 v52 v45 v62 v46 v63 v47 v64 48 49 v1 49 50 v2 50
51 v3 v1
51 52 53 v3 0 52 54 v4 53 55 v5 54 56 55 57 v6 0 56 58 59 v2 0 57 60 58 61 v7 59 62 v8 60 61
63 v9 v7
62
64 v10 v8
63 65 68 89 98 51 64 101 67 99 65 102 58 59 93 103 94 52 49 70 53 96 91 92 61 95 54 57 50 69 48 100 63 56 90 55 62 1 92 94 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v43 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v43 pp8 v44 pp9 v45 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 2 98 99 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v45 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 3 51 52 pp1 v3 pp2 v1 pp3 v2 pp1 v3 pp2 v1 pp3 v2 v3 v1 0 v3 v3 v1 4 50 51 pp1 v1 pp2 v2 pp1 v3 pp2 v1 pp3 v2 v3 v1 5 89 91 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v45 10 v40 10 v40 v45 v44 1 0 v3 v43 1 v43 1 1 v43 v47 v45 -1 v46 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 0 v40 v44 1 1 v44 v45 10 v40 v44 v43 v41 v47 v44 v43 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v45 10 v40 10 v40 v45 v44 1 0 v3 v43 1 v43 1 1 v43 v47 v45 -1 v46 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 0 v40 v44 1 1 v44 v45 10 v40 v44 v43 v41 0 v41 v47 v44 v43 6 58 61 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 v4 1 0 v3 0 v2 v3 v1 v7 1 v4 1 0 v3 0 v2 v3 v1 7 62 64 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 pp6 v10 v8 0 v4 1 0 v3 v3 v1 v2 0 v8 0 v4 1 v10 v8 0 v3 v3 v1 v2 0 8 49 50 pp1 v1 pp1 v1 pp2 v2 9 51 53 pp1 v3 pp2 v1 pp3 v2 pp1 v3 pp2 v1 pp3 v2 v3 v1 v3 0 v3 v1 10 63 65 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 v7 1 v4 1 v9 v7 0 v3 0 v2 v3 v1 v7 1 v4 1 v9 v7 v9 1 0 v3 0 v2 v3 v1 11 89 90 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v45 10 v40 10 v40 v45 v44 1 0 v3 v43 1 v43 1 1 v43 v47 v45 -1 v46 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 0 v40 v44 1 1 v44 v45 10 v40 v44 v43 v41 v47 v44 v43 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v45 10 v40 10 v40 v45 v44 1 0 v3 v43 1 v43 1 1 v43 v47 v45 -1 v46 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 0 v40 v44 1 1 v44 v45 10 v40 v44 v43 v41 v47 0 v41 v44 v43 12 95 97 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v50 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v50 pp9 v45 v49 0 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 0 v41 v47 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v50 0 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 v49 0 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 0 v41 v47 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v50 0 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 13 56 59 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp1 v3 pp2 v1 pp3 v2 pp4 v4 v4 1 0 v3 v3 v1 v4 1 0 v3 v3 v1 v2 0 14 65 67 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 pp7 v17 v7 1 v4 1 v9 v7 v9 1 0 v3 0 v2 v3 v1 v7 1 v4 1 v9 v7 v9 1 0 v3 v17 10 v2 0 v2 v3 v1 15 54 56 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp1 v3 pp2 v1 pp3 v2 pp4 v4 v4 1 0 v3 v3 v1 v4 1 0 v3 v3 v1 16 94 96 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v43 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v44 pp9 v45 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 17 90 92 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v43 pp8 v44 pp9 v45 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v45 10 v40 10 v40 v45 v44 1 0 v3 v43 1 v43 1 1 v43 v47 v45 -1 v46 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 0 v40 v44 1 1 v44 v45 10 v40 v44 v43 v41 v47 0 v41 v44 v43 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 18 67 68 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 pp7 v17 pp1 v3 pp2 v1 pp3 v2 pp4 v18 pp5 v4 pp6 v7 pp7 v9 pp8 v17 v7 1 v4 1 v9 v7 v9 1 0 v3 v17 10 v2 0 v2 v3 v1 v7 1 v4 1 v9 v7 v18 2 v3 v9 1 0 v3 v17 10 v2 0 v2 v3 v1 19 48 49 pp1 v1 20 93 95 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v50 pp9 v45 v49 0 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 0 v41 v47 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 v49 0 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 0 v41 v47 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v50 0 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 21 103 89 pp1 v65 pp2 v39 pp3 v40 pp4 v63 pp5 v64 pp6 v48 pp7 v51 pp8 v52 pp9 v62 pp1 v65 pp2 v39 pp3 v40 pp4 v63 pp5 v64 pp6 v48 pp7 v51 pp8 v52 pp9 v62 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 v63 2 v41 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v65 v64 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 v64 v62 -1 v63 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 v64 v62 -1 v63 v62 -1 v63 v64 v48 1 v62 10 v40 10 v40 v62 v52 1 0 v3 v51 1 v51 1 1 v51 v64 v62 -1 v63 v3 v39 v39 v3 v65 v64 v64 v65 v3 v39 0 v40 v52 1 1 v52 v62 10 v40 v52 v51 v65 v64 v52 v51 22 64 66 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 pp6 v10 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 pp6 v10 v8 0 v4 1 v10 v8 0 v3 v3 v1 v2 0 v8 0 v4 1 v10 v8 v10 0 0 v3 v3 v1 v2 0 23 70 89 pp1 v20 pp2 v1 pp3 v2 pp4 v18 pp5 v19 pp6 v4 pp7 v7 pp8 v9 pp9 v17 pp1 v20 pp2 v1 pp3 v2 pp4 v18 pp5 v19 pp6 v4 pp7 v7 pp8 v9 pp9 v17 v7 1 v4 1 v9 v7 v18 2 v3 v9 1 v19 v17 -1 v18 0 v3 v17 10 v2 0 v2 v3 v1 v20 v19 v19 v17 -1 v18 v17 -1 v18 v19 v4 1 v17 10 v2 10 v2 v17 v9 1 0 v3 v7 1 v7 1 1 v7 v19 v17 -1 v18 v3 v1 v1 v3 v20 v19 v19 v20 v3 v1 0 v2 v9 1 1 v9 v17 10 v2 v9 v7 v20 v19 v9 v7 24 91 93 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v44 pp9 v45 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v45 10 v40 10 v40 v45 v44 1 0 v3 v43 1 v43 1 1 v43 v47 v45 -1 v46 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 0 v40 v44 1 1 v44 v45 10 v40 v44 v43 v41 0 v41 v47 v44 v43 v49 0 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 0 v41 v47 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v44 v43 25 61 63 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 v7 1 v4 1 0 v3 0 v2 v3 v1 v7 1 v4 1 v9 v7 0 v3 0 v2 v3 v1 26 99 100 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v62 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 27 100 101 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v62 pp1 v41 pp2 v39 pp3 v40 pp4 v63 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v62 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 v63 2 v41 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 28 101 102 pp1 v41 pp2 v39 pp3 v40 pp4 v63 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v62 pp1 v41 pp2 v39 pp3 v40 pp4 v63 pp5 v64 pp6 v48 pp7 v51 pp8 v52 pp9 v62 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 v63 2 v41 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 v63 2 v41 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 v64 v62 -1 v63 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 29 53 55 pp1 v3 pp2 v1 pp3 v2 pp1 v3 pp2 v1 pp3 v2 pp4 v5 v3 0 v3 v1 v5 0 v3 0 v3 v1 30 59 62 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 v4 1 0 v3 v3 v1 v2 0 v8 0 v4 1 0 v3 v3 v1 v2 0 31 68 69 pp1 v3 pp2 v1 pp3 v2 pp4 v18 pp5 v4 pp6 v7 pp7 v9 pp8 v17 pp1 v3 pp2 v1 pp3 v2 pp4 v18 pp5 v19 pp6 v4 pp7 v7 pp8 v9 pp9 v17 v7 1 v4 1 v9 v7 v18 2 v3 v9 1 0 v3 v17 10 v2 0 v2 v3 v1 v7 1 v4 1 v9 v7 v18 2 v3 v9 1 v19 v17 -1 v18 0 v3 v17 10 v2 0 v2 v3 v1 32 57 60 pp1 v3 pp2 v1 pp3 v2 pp4 v5 pp5 v6 pp1 v3 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 0 v3 0 v6 0 v3 v1 v5 0 v3 0 v6 0 v3 v1 33 69 70 pp1 v3 pp2 v1 pp3 v2 pp4 v18 pp5 v19 pp6 v4 pp7 v7 pp8 v9 pp9 v17 pp1 v20 pp2 v1 pp3 v2 pp4 v18 pp5 v19 pp6 v4 pp7 v7 pp8 v9 pp9 v17 v7 1 v4 1 v9 v7 v18 2 v3 v9 1 v19 v17 -1 v18 0 v3 v17 10 v2 0 v2 v3 v1 v7 1 v4 1 v9 v7 v18 2 v3 v9 1 v19 v17 -1 v18 0 v3 v17 10 v2 0 v2 v3 v1 v20 v19 34 56 58 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp1 v3 pp2 v1 pp3 v2 pp4 v4 v4 1 0 v3 v3 v1 v4 1 0 v3 0 v2 v3 v1 35 102 103 pp1 v41 pp2 v39 pp3 v40 pp4 v63 pp5 v64 pp6 v48 pp7 v51 pp8 v52 pp9 v62 pp1 v65 pp2 v39 pp3 v40 pp4 v63 pp5 v64 pp6 v48 pp7 v51 pp8 v52 pp9 v62 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 v63 2 v41 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 v64 v62 -1 v63 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 v62 10 v40 v48 1 v45 10 v40 10 v40 v45 v63 2 v41 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v52 1 v41 v47 v52 v51 0 v41 v65 v64 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 v64 v62 -1 v63 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 36 96 98 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v44 pp9 v45 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v45 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 v48 1 v45 10 v40 10 v40 v45 0 v3 v43 1 v43 1 1 v43 v3 v39 v39 v3 v41 v47 v47 v41 v3 v39 v45 10 v40 v41 v47 v52 v51 0 v41 v47 v45 -1 v46 v45 -1 v46 v47 v42 1 v44 1 v47 v45 -1 v46 0 v40 v44 1 1 v44 v44 v43 v51 1 v44 v43 37 52 54 pp1 v3 pp2 v1 pp3 v2 pp1 v3 pp2 v1 pp3 v2 pp4 v4 0 v3 v3 v1 v4 1 0 v3 v3 v1 38 55 57 pp1 v3 pp2 v1 pp3 v2 pp4 v5 pp1 v3 pp2 v1 pp3 v2 pp4 v5 pp5 v6 v5 0 v3 0 v3 v1 v5 0 v3 0 v6 0 v3 v1 64 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 pp6 v10 65 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 66 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 pp6 v10 67 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 pp7 v17 68 pp1 v3 pp2 v1 pp3 v2 pp4 v18 pp5 v4 pp6 v7 pp7 v9 pp8 v17 69 pp1 v3 pp2 v1 pp3 v2 pp4 v18 pp5 v19 pp6 v4 pp7 v7 pp8 v9 pp9 v17 70 pp1 v20 pp2 v1 pp3 v2 pp4 v18 pp5 v19 pp6 v4 pp7 v7 pp8 v9 pp9 v17 89 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 90 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 91 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v42 pp7 v43 pp8 v44 pp9 v45 92 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v43 pp8 v44 pp9 v45 93 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v44 pp9 v45 94 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v43 pp8 v44 pp9 v45 95 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v50 pp9 v45 96 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v44 pp9 v45 97 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v49 pp7 v43 pp8 v50 pp9 v45 98 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v45 99 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v45 100 pp1 v41 pp2 v39 pp3 v40 pp4 v46 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v62 101 pp1 v41 pp2 v39 pp3 v40 pp4 v63 pp5 v47 pp6 v48 pp7 v51 pp8 v52 pp9 v62 102 pp1 v41 pp2 v39 pp3 v40 pp4 v63 pp5 v64 pp6 v48 pp7 v51 pp8 v52 pp9 v62 103 pp1 v65 pp2 v39 pp3 v40 pp4 v63 pp5 v64 pp6 v48 pp7 v51 pp8 v52 pp9 v62 48 49 pp1 v1 50 pp1 v1 pp2 v2 51 pp1 v3 pp2 v1 pp3 v2 52 pp1 v3 pp2 v1 pp3 v2 53 pp1 v3 pp2 v1 pp3 v2 54 pp1 v3 pp2 v1 pp3 v2 pp4 v4 55 pp1 v3 pp2 v1 pp3 v2 pp4 v5 56 pp1 v3 pp2 v1 pp3 v2 pp4 v4 57 pp1 v3 pp2 v1 pp3 v2 pp4 v5 pp5 v6 58 pp1 v3 pp2 v1 pp3 v2 pp4 v4 59 pp1 v3 pp2 v1 pp3 v2 pp4 v4 60 pp1 v3 pp2 v1 pp3 v2 pp4 v5 pp5 v6 61 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 62 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v8 63 pp1 v3 pp2 v1 pp3 v2 pp4 v4 pp5 v7 pp6 v9 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