[runlim] version: 1.7 [runlim] time limit: 3600 seconds [runlim] real time limit: 311040000 seconds [runlim] space limit: 4294967069 MB [runlim] argv[0]: ./armc [runlim] argv[1]: Motor50R.armc [runlim] start: Sat Nov 29 18:15:05 2014 [runlim] main pid: 26157 ARMC3: Abstraction Refinement Model Checker, v. 3.20.05 (May-21-2008) rybal@mpi-sws.mpg.de cmd line: [Motor50R.armc] reading input from Motor50R.armc...done. -------------------------------------------------- abstraction refinement iteration 0: predicates: pc(_6243): #0: lfp iteration 0 1 2 abstract_check at refinement step 0 completed in 1630 msec counterexample is spurious refining abstraction... cex: 55 53 52 0 Refining 52 Pivot Node : 2 RevSuffix [2-53-3,1-52-2] LI at pc(v_1):x_1-x_2>=5 preds(p(_,data(A,B,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1)]). -------------------------------------------------- abstraction refinement iteration 1: predicates: _1408238: #1: x_1-x_2>=5 lfp iteration 0 1 2 3 abstract_check at refinement step 1 completed in 3120 msec counterexample is spurious refining abstraction... cex: 55 53 1 52 0 Refining 101 Pivot Node : 52 RevSuffix [52-55-101,3-53-52] [runlim] sample: 10.0 seconds, 28.8 MB LI at pc(v_2):x_1-x_2>=2 preds(p(_,data(A,B,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 2: predicates: _884868: #2: x_1-x_2>=5, x_1-x_2>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 2 completed in 3580 msec counterexample is spurious refining abstraction... cex: 58 56 1 52 0 Refining 101 Pivot Node : 53 RevSuffix [53-58-101,3-56-53] [runlim] sample: 20.0 seconds, 42.2 MB LI at pc(v_3):x_2-x_3>=2 preds(p(_,data(A,B,C,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 3: predicates: _2532632: #3: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 3 completed in 3820 msec counterexample is spurious refining abstraction... cex: 61 59 1 52 0 Refining 101 Pivot Node : 54 RevSuffix [54-61-101,3-59-54] [runlim] sample: 30.0 seconds, 42.2 MB LI at pc(v_4):x_3-x_4>=2 preds(p(_,data(A,B,C,D,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 4: predicates: _2581328: #4: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 4 completed in 4020 msec counterexample is spurious refining abstraction... cex: 64 62 1 52 0 Refining 102 Pivot Node : 55 RevSuffix [55-64-102,3-62-55] [runlim] sample: 40.0 seconds, 42.2 MB LI at pc(v_5):x_4-x_5>=2 preds(p(_,data(A,B,C,D,E,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 5: predicates: _2629474: #5: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 5 completed in 4230 msec counterexample is spurious refining abstraction... cex: 67 65 1 52 0 Refining 103 Pivot Node : 56 RevSuffix [56-67-103,3-65-56] [runlim] sample: 50.0 seconds, 42.2 MB LI at pc(v_6):x_5-x_6>=2 preds(p(_,data(A,B,C,D,E,F,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 6: predicates: _2684691: #6: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 6 completed in 4410 msec counterexample is spurious refining abstraction... cex: 70 68 1 52 0 Refining 104 Pivot Node : 57 RevSuffix [57-70-104,3-68-57] [runlim] sample: 59.9 seconds, 42.2 MB LI at pc(v_7):x_6-x_7>=2 preds(p(_,data(A,B,C,D,E,F,G,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 7: predicates: _3037021: #7: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2 lfp iteration 0 1 2 3 [runlim] sample: 69.9 seconds, 42.2 MB abstract_check at refinement step 7 completed in 4620 msec counterexample is spurious refining abstraction... cex: 73 71 1 52 0 Refining 105 Pivot Node : 58 RevSuffix [58-73-105,3-71-58] LI at pc(v_8):x_7-x_8>=2 preds(p(_,data(A,B,C,D,E,F,G,H,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 8: predicates: _3080705: #8: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2 lfp iteration 0 1 2 3 [runlim] sample: 79.9 seconds, 42.2 MB abstract_check at refinement step 8 completed in 4790 msec counterexample is spurious refining abstraction... cex: 76 74 1 52 0 Refining 106 Pivot Node : 59 RevSuffix [59-76-106,3-74-59] LI at pc(v_9):x_8-x_9>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 9: predicates: _2075094: #9: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2 lfp iteration 0 1 2 3 [runlim] sample: 89.9 seconds, 42.2 MB abstract_check at refinement step 9 completed in 4970 msec counterexample is spurious refining abstraction... cex: 79 77 1 52 0 Refining 107 Pivot Node : 60 RevSuffix [60-79-107,3-77-60] LI at pc(v_10):x_9-x_10>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 10: predicates: _2150700: #10: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2 lfp iteration 0 1 2 3 [runlim] sample: 99.9 seconds, 42.2 MB abstract_check at refinement step 10 completed in 5160 msec counterexample is spurious refining abstraction... cex: 82 80 1 52 0 Refining 108 Pivot Node : 61 RevSuffix [61-82-108,3-80-61] LI at pc(v_11):x_10-x_11>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 11: predicates: _2688201: #11: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2 lfp iteration 0 1 2 3 [runlim] sample: 109.9 seconds, 42.2 MB abstract_check at refinement step 11 completed in 5290 msec counterexample is spurious refining abstraction... cex: 85 83 1 52 0 Refining 109 Pivot Node : 62 RevSuffix [62-85-109,3-83-62] LI at pc(v_12):x_11-x_12>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 12: predicates: _2552716: #12: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2 lfp iteration 0 1 2 3 [runlim] sample: 119.9 seconds, 42.2 MB abstract_check at refinement step 12 completed in 5450 msec counterexample is spurious refining abstraction... cex: 88 86 1 52 0 Refining 110 Pivot Node : 63 RevSuffix [63-88-110,3-86-63] LI at pc(v_13):x_12-x_13>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 13: predicates: _2626613: #13: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2 lfp iteration 0 1 2 [runlim] sample: 129.9 seconds, 42.2 MB 3 abstract_check at refinement step 13 completed in 5600 msec counterexample is spurious refining abstraction... cex: 91 89 1 52 0 Refining 111 Pivot Node : 64 RevSuffix [64-91-111,3-89-64] LI at pc(v_14):x_13-x_14>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 14: predicates: _2824846: #14: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2 lfp iteration 0 1 2 [runlim] sample: 139.9 seconds, 42.2 MB 3 abstract_check at refinement step 14 completed in 5760 msec counterexample is spurious refining abstraction... cex: 94 92 1 52 0 Refining 112 Pivot Node : 65 RevSuffix [65-94-112,3-92-65] LI at pc(v_15):x_14-x_15>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 15: predicates: _1888163: #15: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2 lfp iteration 0 1 [runlim] sample: 149.8 seconds, 42.2 MB 2 3 abstract_check at refinement step 15 completed in 5890 msec counterexample is spurious refining abstraction... cex: 97 95 1 52 0 Refining 113 Pivot Node : 66 RevSuffix [66-97-113,3-95-66] LI at pc(v_16):x_15-x_16>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 16: predicates: _2465957: #16: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2 lfp iteration 0 1 [runlim] sample: 159.8 seconds, 42.2 MB 2 3 abstract_check at refinement step 16 completed in 6050 msec counterexample is spurious refining abstraction... cex: 100 98 1 52 0 Refining 114 Pivot Node : 67 RevSuffix [67-100-114,3-98-67] [runlim] sample: 169.8 seconds, 42.2 MB LI at pc(v_17):x_16-x_17>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 17: predicates: _2958762: #17: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 17 completed in 6160 msec counterexample is spurious refining abstraction... cex: 103 101 1 52 0 Refining 115 Pivot Node : 68 RevSuffix [68-103-115,3-101-68] [runlim] sample: 179.8 seconds, 42.2 MB LI at pc(v_18):x_17-x_18>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 18: predicates: _2945779: #18: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 18 completed in 6300 msec counterexample is spurious refining abstraction... cex: 106 104 1 52 0 Refining 116 Pivot Node : 69 RevSuffix [69-106-116,3-104-69] [runlim] sample: 189.8 seconds, 42.2 MB LI at pc(v_19):x_18-x_19>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 19: predicates: _3035376: #19: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 19 completed in 6500 msec counterexample is spurious refining abstraction... cex: 109 107 1 52 0 Refining 117 Pivot Node : 70 RevSuffix [70-109-117,3-107-70] [runlim] sample: 199.8 seconds, 42.2 MB LI at pc(v_20):x_19-x_20>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 20: predicates: _2696663: #20: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2 lfp iteration 0 1 2 3 [runlim] sample: 209.8 seconds, 42.2 MB abstract_check at refinement step 20 completed in 6520 msec counterexample is spurious refining abstraction... cex: 112 110 1 52 0 Refining 118 Pivot Node : 71 RevSuffix [71-112-118,3-110-71] LI at pc(v_21):x_20-x_21>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 21: predicates: _2933389: #21: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2 lfp iteration 0 1 2 3 [runlim] sample: 219.8 seconds, 42.2 MB abstract_check at refinement step 21 completed in 6670 msec counterexample is spurious refining abstraction... cex: 115 113 1 52 0 Refining 119 Pivot Node : 72 RevSuffix [72-115-119,3-113-72] LI at pc(v_22):x_21-x_22>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 22: predicates: _2449949: #22: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2 lfp iteration 0 1 2 3 [runlim] sample: 229.8 seconds, 42.2 MB abstract_check at refinement step 22 completed in 6780 msec counterexample is spurious refining abstraction... cex: 118 116 1 52 0 Refining 120 Pivot Node : 73 RevSuffix [73-118-120,3-116-73] LI at pc(v_23):x_22-x_23>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 23: predicates: _2254469: #23: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2 lfp iteration 0 1 2 3 [runlim] sample: 239.8 seconds, 42.2 MB abstract_check at refinement step 23 completed in 6930 msec counterexample is spurious refining abstraction... cex: 121 119 1 52 0 Refining 121 Pivot Node : 74 RevSuffix [74-121-121,3-119-74] LI at pc(v_24):x_23-x_24>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 24: predicates: _2672693: #24: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2 lfp iteration 0 1 [runlim] sample: 249.8 seconds, 42.2 MB 2 3 abstract_check at refinement step 24 completed in 7000 msec counterexample is spurious refining abstraction... cex: 124 122 1 52 0 Refining 122 Pivot Node : 75 RevSuffix [75-124-122,3-122-75] [runlim] sample: 259.7 seconds, 42.2 MB LI at pc(v_25):x_24-x_25>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 25: predicates: _2468675: #25: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 25 completed in 7130 msec counterexample is spurious refining abstraction... cex: 127 125 1 52 0 Refining 123 Pivot Node : 76 RevSuffix [76-127-123,3-125-76] [runlim] sample: 269.7 seconds, 42.2 MB LI at pc(v_26):x_25-x_26>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 26: predicates: _2252036: #26: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2 lfp iteration 0 1 2 3 [runlim] sample: 279.7 seconds, 42.2 MB abstract_check at refinement step 26 completed in 7250 msec counterexample is spurious refining abstraction... cex: 130 128 1 52 0 Refining 124 Pivot Node : 77 RevSuffix [77-130-124,3-128-77] LI at pc(v_27):x_26-x_27>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 27: predicates: _2558992: #27: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2 lfp iteration 0 1 2 3 [runlim] sample: 289.7 seconds, 42.2 MB abstract_check at refinement step 27 completed in 7310 msec counterexample is spurious refining abstraction... cex: 133 131 1 52 0 Refining 125 Pivot Node : 78 RevSuffix [78-133-125,3-131-78] LI at pc(v_28):x_27-x_28>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 28: predicates: _2983921: #28: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2 lfp iteration 0 1 2 [runlim] sample: 299.7 seconds, 42.2 MB 3 abstract_check at refinement step 28 completed in 7450 msec counterexample is spurious refining abstraction... cex: 136 134 1 52 0 Refining 126 Pivot Node : 79 RevSuffix [79-136-126,3-134-79] [runlim] sample: 309.7 seconds, 42.2 MB LI at pc(v_29):x_28-x_29>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 29: predicates: _3055042: #29: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 29 completed in 7540 msec counterexample is spurious refining abstraction... cex: 139 137 1 52 0 Refining 127 [runlim] sample: 319.7 seconds, 42.2 MB Pivot Node : 80 RevSuffix [80-139-127,3-137-80] LI at pc(v_30):x_29-x_30>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 30: predicates: _2869771: #30: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2 lfp iteration 0 1 2 3 [runlim] sample: 329.7 seconds, 42.2 MB abstract_check at refinement step 30 completed in 7610 msec counterexample is spurious refining abstraction... cex: 142 140 1 52 0 Refining 128 Pivot Node : 81 RevSuffix [81-142-128,3-140-81] [runlim] sample: 339.6 seconds, 42.2 MB LI at pc(v_31):x_30-x_31>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 31: predicates: _2876428: #31: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 31 completed in 7690 msec counterexample is spurious refining abstraction... cex: 145 143 1 52 0 Refining 129 Pivot Node : 82 RevSuffix [82-145-129,3-143-82] [runlim] sample: 349.6 seconds, 64.1 MB LI at pc(v_32):x_31-x_32>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 32: predicates: _2969199: #32: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2 lfp iteration 0 1 2 3 [runlim] sample: 359.6 seconds, 64.1 MB abstract_check at refinement step 32 completed in 7740 msec counterexample is spurious refining abstraction... cex: 148 146 1 52 0 Refining 130 Pivot Node : 83 RevSuffix [83-148-130,3-146-83] LI at pc(v_33):x_32-x_33>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 33: predicates: _4303483: #33: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2 lfp iteration 0 1 2 3 [runlim] sample: 369.6 seconds, 64.1 MB abstract_check at refinement step 33 completed in 7840 msec counterexample is spurious refining abstraction... cex: 151 149 1 52 0 Refining 131 Pivot Node : 84 RevSuffix [84-151-131,3-149-84] LI at pc(v_34):x_33-x_34>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 34: predicates: _4671943: #34: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2 lfp iteration 0 1 2 [runlim] sample: 379.6 seconds, 64.1 MB 3 abstract_check at refinement step 34 completed in 7900 msec counterexample is spurious refining abstraction... cex: 154 152 1 52 0 Refining 132 Pivot Node : 85 RevSuffix [85-154-132,3-152-85] [runlim] sample: 389.6 seconds, 64.1 MB LI at pc(v_35):x_34-x_35>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 35: predicates: _5041055: #35: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 35 completed in 7970 msec counterexample is spurious refining abstraction... cex: 157 155 1 52 0 Refining 133 Pivot Node : 86 RevSuffix [86-157-133,3-155-86] [runlim] sample: 399.6 seconds, 64.1 MB LI at pc(v_36):x_35-x_36>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 36: predicates: _4787702: #36: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2 lfp iteration 0 1 2 3 [runlim] sample: 409.6 seconds, 64.1 MB abstract_check at refinement step 36 completed in 8040 msec counterexample is spurious refining abstraction... cex: 160 158 1 52 0 Refining 134 Pivot Node : 87 RevSuffix [87-160-134,3-158-87] LI at pc(v_37):x_36-x_37>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,_,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 37: predicates: _5160011: #37: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2 lfp iteration 0 1 2 3 [runlim] sample: 419.6 seconds, 64.1 MB abstract_check at refinement step 37 completed in 8090 msec counterexample is spurious refining abstraction... cex: 163 161 1 52 0 Refining 135 Pivot Node : 88 RevSuffix [88-163-135,3-161-88] [runlim] sample: 429.6 seconds, 64.1 MB LI at pc(v_38):x_37-x_38>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,_,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 38: predicates: _3210848: #38: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2 lfp iteration 0 1 2 3 abstract_check at refinement step 38 completed in 8150 msec counterexample is spurious refining abstraction... cex: 166 164 1 52 0 Refining 136 Pivot Node : 89 RevSuffix [89-166-136,3-164-89] [runlim] sample: 439.6 seconds, 64.1 MB LI at pc(v_39):x_38-x_39>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,_,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 39: predicates: _4139677: #39: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2 lfp iteration 0 1 2 3 [runlim] sample: 449.6 seconds, 64.1 MB abstract_check at refinement step 39 completed in 8230 msec counterexample is spurious refining abstraction... cex: 169 167 1 52 0 Refining 137 Pivot Node : 90 RevSuffix [90-169-137,3-167-90] LI at pc(v_40):x_39-x_40>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,_,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 40: predicates: _4697719: #40: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2 lfp iteration 0 1 2 3 [runlim] sample: 459.6 seconds, 64.1 MB abstract_check at refinement step 40 completed in 8240 msec counterexample is spurious refining abstraction... cex: 172 170 1 52 0 Refining 138 Pivot Node : 91 RevSuffix [91-172-138,3-170-91] LI at pc(v_41):x_40-x_41>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,_,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 41: predicates: _4684548: #41: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2 lfp iteration 0 1 [runlim] sample: 469.5 seconds, 64.1 MB 2 3 abstract_check at refinement step 41 completed in 8290 msec counterexample is spurious refining abstraction... cex: 175 173 1 52 0 Refining 139 Pivot Node : 92 RevSuffix [92-175-139,3-173-92] [runlim] sample: 479.5 seconds, 64.1 MB LI at pc(v_42):x_41-x_42>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,_,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 42: predicates: _4005409: #42: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2 lfp iteration 0 1 2 3 [runlim] sample: 489.5 seconds, 64.1 MB abstract_check at refinement step 42 completed in 8350 msec counterexample is spurious refining abstraction... cex: 178 176 1 52 0 Refining 140 Pivot Node : 93 RevSuffix [93-178-140,3-176-93] LI at pc(v_43):x_42-x_43>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,_,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 43: predicates: _4653930: #43: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2 lfp iteration 0 1 2 3 [runlim] sample: 499.5 seconds, 64.1 MB abstract_check at refinement step 43 completed in 8350 msec counterexample is spurious refining abstraction... cex: 181 179 1 52 0 Refining 141 Pivot Node : 94 RevSuffix [94-181-141,3-179-94] LI at pc(v_44):x_43-x_44>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,_,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 44: predicates: _5042142: #44: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2 lfp iteration 0 1 2 [runlim] sample: 509.5 seconds, 64.1 MB 3 abstract_check at refinement step 44 completed in 8400 msec counterexample is spurious refining abstraction... cex: 184 182 1 52 0 Refining 142 Pivot Node : 95 RevSuffix [95-184-142,3-182-95] [runlim] sample: 519.5 seconds, 64.1 MB LI at pc(v_45):x_44-x_45>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,_,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1),R1-S1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 45: predicates: _5057493: #45: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2 lfp iteration 0 1 2 3 [runlim] sample: 529.5 seconds, 64.1 MB abstract_check at refinement step 45 completed in 8430 msec counterexample is spurious refining abstraction... cex: 187 185 1 52 0 Refining 143 Pivot Node : 96 RevSuffix [96-187-143,3-185-96] LI at pc(v_46):x_45-x_46>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,_,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1),R1-S1>=rat(2,1),S1-T1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 46: predicates: _4639200: #46: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2 lfp iteration 0 1 2 3 [runlim] sample: 539.5 seconds, 64.1 MB abstract_check at refinement step 46 completed in 8430 msec counterexample is spurious refining abstraction... cex: 190 188 1 52 0 Refining 144 Pivot Node : 97 RevSuffix [97-190-144,3-188-97] LI at pc(v_47):x_46-x_47>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,_,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1),R1-S1>=rat(2,1),S1-T1>=rat(2,1),T1-U1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 47: predicates: _5036325: #47: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2 lfp iteration 0 1 2 [runlim] sample: 549.5 seconds, 64.1 MB 3 abstract_check at refinement step 47 completed in 8450 msec counterexample is spurious refining abstraction... cex: 193 191 1 52 0 Refining 145 Pivot Node : 98 RevSuffix [98-193-145,3-191-98] [runlim] sample: 559.5 seconds, 64.1 MB LI at pc(v_48):x_47-x_48>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,_,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1),R1-S1>=rat(2,1),S1-T1>=rat(2,1),T1-U1>=rat(2,1),U1-V1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 48: predicates: _4510215: #48: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2 lfp iteration 0 1 2 3 [runlim] sample: 569.5 seconds, 64.1 MB abstract_check at refinement step 48 completed in 8450 msec counterexample is spurious refining abstraction... cex: 196 194 1 52 0 Refining 146 Pivot Node : 99 RevSuffix [99-196-146,3-194-99] LI at pc(v_49):x_48-x_49>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,_,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1),R1-S1>=rat(2,1),S1-T1>=rat(2,1),T1-U1>=rat(2,1),U1-V1>=rat(2,1),V1-W1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 49: predicates: _4987790: #49: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2, x_48-x_49>=2 lfp iteration 0 1 2 3 [runlim] sample: 579.4 seconds, 64.1 MB abstract_check at refinement step 49 completed in 8460 msec counterexample is spurious refining abstraction... cex: 199 197 1 52 0 Refining 147 Pivot Node : 100 RevSuffix [100-199-147,3-197-100] LI at pc(v_50):x_49-x_50>=2 preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1),R1-S1>=rat(2,1),S1-T1>=rat(2,1),T1-U1>=rat(2,1),U1-V1>=rat(2,1),V1-W1>=rat(2,1),W1-X1>=rat(2,1)]). -------------------------------------------------- abstraction refinement iteration 50: predicates: _4912299: #50: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2, x_48-x_49>=2, x_49-x_50>=2 lfp iteration 0 1 [runlim] sample: 589.4 seconds, 64.1 MB 2 3 4 [runlim] sample: 599.4 seconds, 99.2 MB [runlim] sample: 609.4 seconds, 99.2 MB [runlim] sample: 619.4 seconds, 99.2 MB 5 Number of interpolation queries: 50. Number of entailment checks during fixpoint checking: 0. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 219,175. abstract_check at refinement step 50 completed in 30680 msec ================================================== ARMC: program is correct abstract fixpoint abstract_state(1, pc(v_0), []). abstract_state(3, pc(v_1), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50]). abstract_state(99, pc(v_49), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50]). abstract_state(100, pc(v_50), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50]). abstract_state(101, pc(v_2), [2,3]). abstract_state(102, pc(v_3), [2,3,4]). abstract_state(103, pc(v_4), [2,3,4,5]). abstract_state(104, pc(v_5), [2,3,4,5,6]). abstract_state(105, pc(v_6), [2,3,4,5,6,7]). abstract_state(106, pc(v_7), [2,3,4,5,6,7,8]). abstract_state(107, pc(v_8), [2,3,4,5,6,7,8,9]). abstract_state(108, pc(v_9), [2,3,4,5,6,7,8,9,10]). abstract_state(109, pc(v_10), [2,3,4,5,6,7,8,9,10,11]). abstract_state(110, pc(v_11), [2,3,4,5,6,7,8,9,10,11,12]). abstract_state(111, pc(v_12), [2,3,4,5,6,7,8,9,10,11,12,13]). abstract_state(112, pc(v_13), [2,3,4,5,6,7,8,9,10,11,12,13,14]). abstract_state(113, pc(v_14), [2,3,4,5,6,7,8,9,10,11,12,13,14,15]). abstract_state(114, pc(v_15), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]). abstract_state(115, pc(v_16), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17]). abstract_state(116, pc(v_17), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18]). abstract_state(117, pc(v_18), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19]). abstract_state(118, pc(v_19), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]). abstract_state(119, pc(v_20), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]). abstract_state(120, pc(v_21), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22]). abstract_state(121, pc(v_22), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23]). abstract_state(122, pc(v_23), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24]). abstract_state(123, pc(v_24), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]). abstract_state(124, pc(v_25), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]). abstract_state(125, pc(v_26), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27]). abstract_state(126, pc(v_27), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28]). abstract_state(127, pc(v_28), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29]). abstract_state(128, pc(v_29), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]). abstract_state(129, pc(v_30), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31]). abstract_state(130, pc(v_31), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32]). abstract_state(131, pc(v_32), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33]). abstract_state(132, pc(v_33), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34]). abstract_state(133, pc(v_34), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35]). abstract_state(134, pc(v_35), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36]). abstract_state(135, pc(v_36), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37]). abstract_state(136, pc(v_37), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38]). abstract_state(137, pc(v_38), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39]). abstract_state(138, pc(v_39), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40]). abstract_state(139, pc(v_40), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41]). abstract_state(140, pc(v_41), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42]). abstract_state(141, pc(v_42), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43]). abstract_state(142, pc(v_43), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44]). abstract_state(143, pc(v_44), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45]). abstract_state(144, pc(v_45), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46]). abstract_state(145, pc(v_46), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47]). abstract_state(146, pc(v_47), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48]). abstract_state(147, pc(v_48), [2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49]). frontier 0: 1 pc(v_0) from 0 by appying 0: T frontier 2: 3 pc(v_1) from 2 by appying 1: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2, x_48-x_49>=2, x_49-x_50>=2 frontier 3: 99 pc(v_49) from 3 by appying 194: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2, x_48-x_49>=2, x_49-x_50>=2 frontier 3: 100 pc(v_50) from 3 by appying 197: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2, x_48-x_49>=2, x_49-x_50>=2 frontier 4: 101 pc(v_2) from 52 by appying 2: x_1-x_2>=2, x_2-x_3>=2 frontier 4: 102 pc(v_3) from 53 by appying 3: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2 frontier 4: 103 pc(v_4) from 54 by appying 4: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2 frontier 4: 104 pc(v_5) from 55 by appying 5: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2 frontier 4: 105 pc(v_6) from 56 by appying 6: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2 frontier 4: 106 pc(v_7) from 57 by appying 7: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2 frontier 4: 107 pc(v_8) from 58 by appying 8: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2 frontier 4: 108 pc(v_9) from 59 by appying 9: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2 frontier 4: 109 pc(v_10) from 60 by appying 10: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2 frontier 4: 110 pc(v_11) from 61 by appying 11: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2 frontier 4: 111 pc(v_12) from 62 by appying 12: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2 frontier 4: 112 pc(v_13) from 63 by appying 13: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2 frontier 4: 113 pc(v_14) from 64 by appying 14: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2 frontier 4: 114 pc(v_15) from 65 by appying 15: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2 frontier 4: 115 pc(v_16) from 66 by appying 16: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2 frontier 4: 116 pc(v_17) from 67 by appying 17: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2 frontier 4: 117 pc(v_18) from 68 by appying 18: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2 frontier 4: 118 pc(v_19) from 69 by appying 19: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2 frontier 4: 119 pc(v_20) from 70 by appying 20: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2 frontier 4: 120 pc(v_21) from 71 by appying 21: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2 frontier 4: 121 pc(v_22) from 72 by appying 22: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2 frontier 4: 122 pc(v_23) from 73 by appying 23: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2 frontier 4: 123 pc(v_24) from 74 by appying 24: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2 frontier 4: 124 pc(v_25) from 75 by appying 25: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2 frontier 4: 125 pc(v_26) from 76 by appying 26: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2 frontier 4: 126 pc(v_27) from 77 by appying 27: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2 frontier 4: 127 pc(v_28) from 78 by appying 28: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2 frontier 4: 128 pc(v_29) from 79 by appying 29: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2 frontier 4: 129 pc(v_30) from 80 by appying 30: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2 frontier 4: 130 pc(v_31) from 81 by appying 31: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2 frontier 4: 131 pc(v_32) from 82 by appying 32: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2 frontier 4: 132 pc(v_33) from 83 by appying 33: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2 frontier 4: 133 pc(v_34) from 84 by appying 34: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2 frontier 4: 134 pc(v_35) from 85 by appying 35: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2 frontier 4: 135 pc(v_36) from 86 by appying 36: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2 frontier 4: 136 pc(v_37) from 87 by appying 37: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2 frontier 4: 137 pc(v_38) from 88 by appying 38: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2 frontier 4: 138 pc(v_39) from 89 by appying 39: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2 frontier 4: 139 pc(v_40) from 90 by appying 40: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2 frontier 4: 140 pc(v_41) from 91 by appying 41: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2 frontier 4: 141 pc(v_42) from 92 by appying 42: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2 frontier 4: 142 pc(v_43) from 93 by appying 43: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2 frontier 4: 143 pc(v_44) from 94 by appying 44: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2 frontier 4: 144 pc(v_45) from 95 by appying 45: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2 frontier 4: 145 pc(v_46) from 96 by appying 46: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2 frontier 4: 146 pc(v_47) from 97 by appying 47: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2 frontier 4: 147 pc(v_48) from 98 by appying 48: x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2, x_48-x_49>=2 _3948261: #50: x_1-x_2>=5, x_1-x_2>=2, x_2-x_3>=2, x_3-x_4>=2, x_4-x_5>=2, x_5-x_6>=2, x_6-x_7>=2, x_7-x_8>=2, x_8-x_9>=2, x_9-x_10>=2, x_10-x_11>=2, x_11-x_12>=2, x_12-x_13>=2, x_13-x_14>=2, x_14-x_15>=2, x_15-x_16>=2, x_16-x_17>=2, x_17-x_18>=2, x_18-x_19>=2, x_19-x_20>=2, x_20-x_21>=2, x_21-x_22>=2, x_22-x_23>=2, x_23-x_24>=2, x_24-x_25>=2, x_25-x_26>=2, x_26-x_27>=2, x_27-x_28>=2, x_28-x_29>=2, x_29-x_30>=2, x_30-x_31>=2, x_31-x_32>=2, x_32-x_33>=2, x_33-x_34>=2, x_34-x_35>=2, x_35-x_36>=2, x_36-x_37>=2, x_37-x_38>=2, x_38-x_39>=2, x_39-x_40>=2, x_40-x_41>=2, x_41-x_42>=2, x_42-x_43>=2, x_43-x_44>=2, x_44-x_45>=2, x_45-x_46>=2, x_46-x_47>=2, x_47-x_48>=2, x_48-x_49>=2, x_49-x_50>=2 ================================================== verifying fixpoint...done. pc(v_0): [[]] pc(v_1): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50]] pc(v_10): [[2,3,4,5,6,7,8,9,10,11]] pc(v_11): [[2,3,4,5,6,7,8,9,10,11,12]] pc(v_12): [[2,3,4,5,6,7,8,9,10,11,12,13]] pc(v_13): [[2,3,4,5,6,7,8,9,10,11,12,13,14]] pc(v_14): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15]] pc(v_15): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]] pc(v_16): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17]] pc(v_17): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18]] pc(v_18): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19]] pc(v_19): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]] pc(v_2): [[2,3]] pc(v_20): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]] pc(v_21): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22]] pc(v_22): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23]] pc(v_23): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24]] pc(v_24): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25]] pc(v_25): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26]] pc(v_26): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27]] pc(v_27): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28]] pc(v_28): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29]] pc(v_29): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]] pc(v_3): [[2,3,4]] pc(v_30): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31]] pc(v_31): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32]] pc(v_32): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33]] pc(v_33): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34]] pc(v_34): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35]] pc(v_35): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36]] pc(v_36): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37]] pc(v_37): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38]] pc(v_38): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39]] pc(v_39): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40]] pc(v_4): [[2,3,4,5]] pc(v_40): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41]] pc(v_41): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42]] pc(v_42): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43]] pc(v_43): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44]] pc(v_44): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45]] pc(v_45): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46]] pc(v_46): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47]] pc(v_47): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48]] pc(v_48): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49]] pc(v_49): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50]] pc(v_5): [[2,3,4,5,6]] pc(v_50): [[2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50]] pc(v_6): [[2,3,4,5,6,7]] pc(v_7): [[2,3,4,5,6,7,8]] pc(v_8): [[2,3,4,5,6,7,8,9]] pc(v_9): [[2,3,4,5,6,7,8,9,10]] Time on instantiating uf axioms: run 0.00, wall 0.00 s. Time on cli constraint solving: run 126.91, wall 237.35 s. Time on cli constraint preparation: run 0.33, wall 0.28 s. Time on cli matrix parsing: run 0.00, wall 0.00 s. Time on cli preprocessing: run 0.00, wall 0.00 s. Time on computing the subsumer subtree: run 0.00, wall 0.00 s. Time on finding the location of subsumer in queue: run 0.00, wall 0.00 s. Time on asserting thick transitions: run 0.00, wall 0.00 s. Time on path invariant generation: run 0.00, wall 0.00 s. Time on new predicate selection: run 0.10, wall 0.08 s. Time on refinement preprocessing cut: run 6.03, wall 6.07 s. Time on refinement cutting trace: run 133.39, wall 243.81 s. Time on refinement finding unsat subtrace: run 3.14, wall 3.25 s. Time on refinement: run 136.62, wall 247.16 s. Time on concrete postcondition operator: run 0.00, wall 0.00 s. Time on fixpoint abstraction: run 131.74, wall 131.74 s. Time on fixpoint test: run 0.33, wall 0.34 s. Time on abstract check: run 332.29, wall 341.47 s. Time on total including result checking: run 506.31, wall 627.48 s. Time on check result: run 6.36, wall 6.71 s. Time on total: run 499.95, wall 620.77 s. Number of interpolation queries: 50. Number of entailment checks during fixpoint checking: 51. Number of entailment checks that could be saved: 0. Number of entailment checks for abstraction: 219,175. ================================================== ARMC: program is correct preds(p(_,data(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,_)), [A-B>=rat(5,1),A-B>=rat(2,1),B-C>=rat(2,1),C-D>=rat(2,1),D-E>=rat(2,1),E-F>=rat(2,1),F-G>=rat(2,1),G-H>=rat(2,1),H-I>=rat(2,1),I-J>=rat(2,1),J-K>=rat(2,1),K-L>=rat(2,1),L-M>=rat(2,1),M-N>=rat(2,1),N-O>=rat(2,1),O-P>=rat(2,1),P-Q>=rat(2,1),Q-R>=rat(2,1),R-S>=rat(2,1),S-T>=rat(2,1),T-U>=rat(2,1),U-V>=rat(2,1),V-W>=rat(2,1),W-X>=rat(2,1),X-Y>=rat(2,1),Y-Z>=rat(2,1),Z-A1>=rat(2,1),A1-B1>=rat(2,1),B1-C1>=rat(2,1),C1-D1>=rat(2,1),D1-E1>=rat(2,1),E1-F1>=rat(2,1),F1-G1>=rat(2,1),G1-H1>=rat(2,1),H1-I1>=rat(2,1),I1-J1>=rat(2,1),J1-K1>=rat(2,1),K1-L1>=rat(2,1),L1-M1>=rat(2,1),M1-N1>=rat(2,1),N1-O1>=rat(2,1),O1-P1>=rat(2,1),P1-Q1>=rat(2,1),Q1-R1>=rat(2,1),R1-S1>=rat(2,1),S1-T1>=rat(2,1),T1-U1>=rat(2,1),U1-V1>=rat(2,1),V1-W1>=rat(2,1),W1-X1>=rat(2,1)]). System information Variables: 51 Transitions: 199 Locations: 52 Analysis information Predicates: 50 Reachable abstract states: 147 Abstraction refinement iterations: 50 [runlim] end: Sat Nov 29 18:25:33 2014 [runlim] status: ok [runlim] result: 0 [runlim] children: 0 [runlim] real: 628.74 seconds [runlim] time: 627.59 seconds [runlim] space: 99.2 MB [runlim] samples: 6282