FORMULAS
➀   forall t, u (t <->* u & NF(u) => t ->* u)
➁   forall t, u (t <->* u & NF(u) => t ->* u)
➂   forall s, t, u (s -> t & s ->! u => t ->* u)
➃   forall s, t, u (s -> t & s ->! u => t ->* u)
➄   forall t (WN(t) => CR(t))
➅   forall t (WN(t) => CR(t))

➀➁ ➂➃ ➄➅
version   fort-2.1 fort-h ✔ fort-2.1 fort-h ✔ fort-2.1 fort-h ✔
total   122 122 51 122 122 96 122 122 87
yes   59 59 31 59 59 46 59 59 42
⌀ yes time   0.23 0.70 0.22 0.03 0.31 0.05
total yes time   13.42 41.25 13.19 1.90 18.41 3.03
no   63 63 20 63 63 50 62 62 45
⌀ no time   0.39 0.07 0.30 0.01 0.64 0.12
total no time   24.74 4.37 18.64 0.65 39.45 7.48
maybe   0 0 0 0 0 0
timeout   (60s) 0 (60s) 0 (600s) 71 (60s) 0 (60s) 0 (600s) 26 (60s) 1 (60s) 1 (600s) 34
⌀ time   0.31 0.37 0.26 0.02 0.97 0.58
total time   38.16 45.62 52650.06 31.83 2.55 22654.34 117.86 70.51 30820.59
 
COPS/111   0.41 0.16 0.23 0.02 0.27 0.08
COPS/114   0.26 1.70 0.31 0.11 0.35 0.11
COPS/115   0.68 16.74 0.57 0.97 1.80 1.44
COPS/116   0.16 4.26 0.41 0.30 0.42 0.29
COPS/212   0.16 0.02 7.61 0.18 0.00 15.17 0.17 0.00 37.70
COPS/213   0.16 0.04 379.77 0.20 0.01 0.19 0.01
COPS/214   0.17 7.86 0.56 0.07 0.44 0.09
COPS/215   0.18 8.63 0.38 0.15 0.38 0.14
COPS/21   0.17 0.12 242.41 0.20 0.00 465.92 0.20 0.00
COPS/223   0.19 0.01 84.06 0.19 0.00 18.61 0.22 0.02 46.39
COPS/224   0.23 0.03 0.17 0.00 5.44 0.25 0.01 18.18
COPS/225   0.20 0.00 413.90 0.19 0.00 4.27 0.20 0.00 10.72
COPS/33   0.18 0.02 101.46 0.20 0.00 203.61 0.20 0.00 503.22
COPS/34   0.25 0.04 0.23 0.01 436.37 0.28 0.03
COPS/36   0.22 0.02 0.20 0.00 35.99 0.21 0.02 90.07
COPS/38   0.18 0.00 352.19 0.19 0.00 34.32 0.19 0.00 85.59
COPS/39   0.32 0.10 0.22 0.01 0.27 0.03
COPS/40   0.30 0.06 0.20 0.00 63.21 0.22 0.01 161.44
COPS/503   0.22 0.03 342.40 0.20 0.00 38.02 0.26 0.02 109.09
COPS/505   0.21 0.03 330.18 0.19 0.00 1.08 0.21 0.01 2.48
COPS/506   0.38 0.22 0.21 0.01 148.50 0.30 0.06 230.02
COPS/507   0.21 0.02 338.88 0.21 0.01 13.91 0.40 0.25 46.87
COPS/508   0.17 0.02 14.41 0.18 0.00 28.55 0.19 0.00 43.99
COPS/509   0.21 0.01 319.71 0.20 0.00 13.50 0.31 0.05 48.04
COPS/510   0.20 0.02 333.51 0.21 0.00 3.85 2.17 0.15 31.22
COPS/511   0.39 0.15 0.25 0.02 231.77 1.06 0.22
COPS/512   0.24 0.04 0.20 0.00 14.15 0.25 0.05 51.32
COPS/543   0.19 0.00 65.52 0.19 0.00 27.22 0.19 0.00 68.37
COPS/557   0.25 0.05 0.20 0.00 14.46 0.32 0.07 96.92
COPS/647   0.21 0.01 255.50 0.20 0.00 14.92 0.28 0.02 44.27
COPS/648   0.19 0.00 37.41 0.19 0.00 0.85 0.19 0.00 1.31
COPS/649   0.18 0.00 9.59 0.20 0.00 18.67 0.19 0.00 47.45
COPS/650   0.66 0.14 0.52 0.05 1.87 0.69
COPS/651   0.38 0.08 0.43 0.02 1.25 0.40
COPS/652   0.20 0.01 73.42 0.20 0.00 3.48 0.23 0.00 11.49
COPS/653   0.22 0.02 0.20 0.01 20.53 0.26 0.03 54.10
COPS/654   0.65 0.09 0.46 0.05 2.13 0.43
COPS/655   0.30 0.05 0.24 0.01 127.56 0.51 0.05 406.65
COPS/656   0.16 0.00 0.40 0.18 0.00 0.79 0.18 0.00 1.77
COPS/657   0.46 0.42 0.22 0.01 0.36 0.05
COPS/658   0.48 0.27 0.29 0.02 1.31 0.12
COPS/659   0.18 0.06 0.21 0.01 0.20 0.01
COPS/660   0.26 0.06 0.20 0.00 273.00 0.32 0.01
COPS/661   0.24 0.02 0.24 0.01 70.17 0.35 0.04 179.96
COPS/662   0.21 0.01 320.78 0.20 0.00 6.70 0.19 0.00 16.86
COPS/663   0.24 0.03 0.24 0.00 213.66 0.36 0.04 550.67
COPS/664   0.22 0.01 0.21 0.00 28.04 0.29 0.01 76.79
COPS/665   0.26 0.05 0.22 0.01 48.36 0.28 0.04 121.78
COPS/666   0.27 0.05 0.21 0.01 290.48 0.46 0.04
COPS/667   0.31 0.05 0.26 0.01 0.55 0.05
COPS/668   0.27 0.03 0.22 0.01 120.23 0.35 0.03 311.85
COPS/669   0.22 0.02 541.42 0.20 0.00 18.02 0.26 0.01 46.22
COPS/670   0.22 0.03 0.20 0.00 5.23 0.21 0.00 13.21
COPS/671   0.27 0.03 0.26 0.03 89.36 0.30 0.02 195.31
COPS/672   0.19 0.03 37.60 0.19 0.01 72.08 0.20 0.00 224.48
COPS/673   0.23 0.02 0.19 0.00 3.42 0.23 0.01 8.98
COPS/674   0.23 0.02 0.20 0.00 8.77 0.21 0.00 22.12
COPS/675   0.35 0.09 0.27 0.02 198.28 0.50 0.21 475.74
COPS/676   0.26 0.02 0.25 0.01 167.15 0.37 0.08 424.15
COPS/677   0.17 0.06 51.30 0.19 0.00 101.12 0.19 0.00 260.65
COPS/678   0.31 0.11 0.22 0.00 117.86 0.30 0.02 305.43
COPS/679   0.21 0.01 346.17 0.19 0.00 1.16 0.20 0.00 2.90
COPS/680   0.81 0.22 0.67 0.05 5.18 0.50
COPS/681   0.27 0.04 0.27 0.04 179.67 0.32 0.02 293.50
COPS/682   0.24 0.05 0.21 0.00 38.62 0.39 0.05 136.32
COPS/683   0.16 0.03 15.07 0.18 0.00 29.69 0.20 0.00 79.47
COPS/684   0.17 0.00 0.50 0.18 0.00 0.91 0.18 0.00 2.40
COPS/685   0.27 0.05 0.20 0.01 206.19 0.46 0.06 559.75
COPS/686   0.16 0.08 0.21 0.01 0.22 0.01
COPS/687   0.24 0.09 0.20 0.01 75.67 0.30 0.05 200.74
COPS/688   0.25 0.03 0.23 0.01 117.08 0.34 0.03 300.86
COPS/689   0.33 0.05 0.21 0.01 0.71 0.05
COPS/690   0.45 0.08 0.25 0.03 1.10 0.04
COPS/691   0.20 0.00 236.01 0.19 0.00 5.45 0.23 0.00 13.95
COPS/692   0.21 0.01 417.45 0.21 0.01 50.79 0.23 0.01 127.40
COPS/693   0.18 0.01 13.02 0.19 0.00 25.91 0.18 0.00 64.94
COPS/694   0.36 0.06 0.23 0.01 408.31 0.69 0.07
COPS/695   0.28 0.08 0.22 0.01 156.24 0.28 0.04 387.66
COPS/696   0.21 0.01 310.03 0.20 0.00 7.90 0.24 0.01 21.46
COPS/697   0.21 0.01 209.67 0.21 0.00 12.78 0.25 0.01 33.13
COPS/698   0.22 0.01 582.01 0.21 0.00 3.76 0.22 0.00 9.65
COPS/699   0.19 0.24 0.24 0.04 0.24 0.02
COPS/700   0.20 0.00 237.61 0.21 0.00 5.25 0.22 0.00 13.47
COPS/701   0.34 0.03 0.25 0.01 0.48 0.06
COPS/702   0.25 0.03 0.21 0.01 15.74 0.28 0.05 43.36
COPS/703   0.47 0.09 0.64 0.06 1.18 1.12
COPS/704   0.20 0.00 106.75 0.18 0.00 2.37 0.21 0.00 6.60
COPS/705   0.18 0.00 6.73 0.18 0.00 13.53 0.18 0.00 20.32
COPS/706   0.23 0.02 0.20 0.00 45.44 0.31 0.03 127.52
COPS/707   0.22 0.02 334.56 0.18 0.00 1.76 0.20 0.00 4.42
COPS/708   0.49 0.08 0.43 0.06 0.71 0.65
COPS/709   0.18 0.00 9.50 0.19 0.00 0.78 0.20 0.00 1.72
COPS/710   0.19 0.00 36.30 0.18 0.00 0.20 0.20 0.00 0.39
COPS/711   0.23 0.03 0.20 0.00 21.02 0.54 0.07 121.94
COPS/712   0.35 0.05 0.24 0.01 310.06 0.35 0.01
COPS/713   0.22 0.01 517.81 0.21 0.00 11.76 0.24 0.02 29.97
COPS/714   0.19 0.00 142.94 0.21 0.00 2.75 0.20 0.00 6.89
COPS/715   0.27 0.06 0.25 0.01 420.89 0.40 0.04
COPS/716   0.28 0.04 0.27 0.02 0.71 0.10
COPS/717   0.27 0.03 0.22 0.01 211.12 0.33 0.02 542.20
COPS/718   0.24 0.02 0.24 0.01 83.65 0.29 0.01 211.39
COPS/719   0.30 0.06 0.21 0.01 124.60 0.30 0.02 323.59
COPS/720   0.24 0.03 0.20 0.00 36.08 0.25 0.01 92.43
COPS/721   0.21 0.01 298.30 0.20 0.00 4.40 0.24 0.00 11.79
COPS/731   0.22 0.02 329.72 0.21 0.00 16.68 0.31 0.03 56.41
COPS/732   0.27 0.04 0.21 0.01 129.62 3.21 0.67 481.28
COPS/733   0.26 0.08 0.22 0.01 207.57 3.41 0.68
COPS/734   0.20 0.01 92.73 0.20 0.00 1.47 0.41 0.04 7.04
COPS/735   0.21 0.01 331.80 0.20 0.00 6.68 0.22 0.01 16.23
COPS/736   0.19 0.01 48.57 0.20 0.00 1.36 0.28 0.02 6.74
COPS/737   0.20 0.00 36.27 0.19 0.00 0.36 0.26 0.03 4.23
COPS/738   0.21 0.02 0.20 0.00 7.02 0.26 0.04 21.05
COPS/739   0.24 0.05 0.20 0.00 55.55 0.34 0.09 153.66
COPS/740   0.20 0.01 108.00 0.20 0.00 4.95 0.48 0.01 33.72
COPS/741   7.06 1.15 3.47 0.07 ∞ ∞
COPS/74   0.29 0.10 0.23 0.02 0.45 0.07
COPS/761   0.18 0.02 356.20 0.18 0.00 25.36 0.17 0.00 38.23
COPS/800   0.18 0.00 104.96 0.18 0.00 2.14 0.20 0.00 5.44
COPS/80   0.19 0.00 81.12 0.19 0.00 11.16 0.23 0.01 29.30
COPS/81   0.21 0.02 0.19 0.00 90.57 0.23 0.04 228.53
COPS/82   0.19 0.01 81.99 0.19 0.00 12.42 0.21 0.02 31.30
COPS/84   0.20 0.01 0.19 0.00 12.23 0.21 0.00 31.08