Features
Processor13th Gen Intel(R) Core(TM) i5-1335U 1.30 GHz
RAM16.00 GB
OSLinux 6.6.87.2-microsoft-standard-WSL2
Program Versions
Mace4 (64) version 2009-11A, November 2009
Prover9 (64) version 2009-11A, November 2009
AGES, version 1.0
Barcelogic 2016
infChecker, version 1.0
MU-TERM, version 6.0
MU-TERM GTRS, version 1.0
DatabaseCSR + CTRSs from TPDB
Timeout240s
Date02.2026


Examples MU-TERM TERM MU-TERM GTRS
TRS_GTRS/COPS/262.xml 29.75 106.92
TRS_GTRS/COPS/263.xml 0.93 37.93
TRS_GTRS/COPS/264.xml 1.24 0.01
TRS_GTRS/COPS/266.xml 30.53 0.05
TRS_GTRS/COPS/267.xml 29.92 37.74
TRS_GTRS/COPS/268.xml 29.85 18.89
TRS_GTRS/COPS/271.xml 30.15 0.07
TRS_GTRS/COPS/272.xml 29.83 134.28
TRS_GTRS/COPS/286.xml 30.06 198.62
TRS_GTRS/COPS/288.xml 0.48 0.01
TRS_GTRS/COPS/289.xml 240 215.50
TRS_GTRS/COPS/292.xml 3.99 57.55
TRS_GTRS/COPS/293.xml 0.15 0.01
TRS_GTRS/COPS/294.xml 0.35 19.92
TRS_GTRS/COPS/307.xml 29.99 79.80
TRS_GTRS/COPS/308.xml 0.92 0.01
TRS_GTRS/COPS/310.xml 30.38 100.40
TRS_GTRS/COPS/311.xml 240 219.26
TRS_GTRS/COPS/312.xml 240 231.30
TRS_GTRS/COPS/315.xml 8.78 9.51
TRS_GTRS/COPS/316.xml 1.85 0.03
TRS_GTRS/COPS/317.xml 0.18 0.01
TRS_GTRS/COPS/319.xml 1.19 0.02
TRS_GTRS/COPS/321.xml 14.09 25.24
TRS_GTRS/COPS/322.xml 29.99 230.31
TRS_GTRS/COPS/323.xml 1.09 0.01
TRS_GTRS/COPS/324.xml 30.01 0.06
TRS_GTRS/COPS/325.xml 4.05 19.87
TRS_GTRS/COPS/326.xml 30.01 47.77
TRS_GTRS/COPS/329.xml 240 217.30
TRS_GTRS/COPS/330.xml 0.74 57.50
TRS_GTRS/COPS/332.xml 1.62 77.23
TRS_GTRS/COPS/333.xml 2.89 19.82
TRS_GTRS/COPS/334.xml 0.43 39.86
TRS_GTRS/COPS/337.xml 240 165.93
TRS_GTRS/COPS/339.xml 7.29 0.07
TRS_GTRS/COPS/340.xml 3.06 0.02
TRS_GTRS/COPS/341.xml 0.59 19.90
TRS_GTRS/COPS/342.xml 187.55 227.47
TRS_GTRS/COPS/343.xml 29.96 44.03
TRS_GTRS/COPS/344.xml 1.08 50.63
TRS_GTRS/COPS/351.xml 29.96 222.99
TRS_GTRS/COPS/353.xml 240 224.11
TRS_GTRS/COPS/354.xml 0.68 37.88
TRS_GTRS/COPS/355.xml 0.08 0.02
TRS_GTRS/COPS/356.xml 0.26 0.04
TRS_GTRS/COPS/358.xml 0.41 19.92
TRS_GTRS/COPS/359.xml 0.73 0.02
TRS_GTRS/COPS/361.xml 240 66.74
TRS_GTRS/COPS/364.xml 0.88 38.58
TRS_GTRS/COPS/365.xml 0.70 38.08
TRS_GTRS/COPS/366.xml 0.50 0.01
TRS_GTRS/COPS/367.xml 0.28 0.01
TRS_GTRS/COPS/368.xml 0.38 19.96
TRS_GTRS/COPS/369.xml 2.76 19.49
TRS_GTRS/COPS/370.xml 6.15 19.39
TRS_GTRS/COPS/371.xml 0.53 19.91
TRS_GTRS/COPS/372.xml 3.53 19.44
TRS_GTRS/COPS/373.xml 1.37 59.48
TRS_GTRS/COPS/374.xml 0.58 0.01
TRS_GTRS/COPS/375.xml 1.16 19.91
TRS_GTRS/COPS/376.xml 0.36 19.95
TRS_GTRS/COPS/377.xml 2.18 19.93
TRS_GTRS/COPS/378.xml 179.22 159.90
TRS_GTRS/COPS/379.xml 29.92 8.58
TRS_GTRS/COPS/380.xml 0.79 0.01
TRS_GTRS/COPS/381.xml 1.87 19.92
TRS_GTRS/COPS/382.xml 2.90 59.54
TRS_GTRS/COPS/383.xml 0.88 19.87
TRS_GTRS/COPS/384.xml 2.39 39.62
TRS_GTRS/COPS/385.xml 0.67 19.34
TRS_GTRS/COPS/387.xml 0.40 19.94
TRS_GTRS/COPS/388.xml 29.89 94.99
TRS_GTRS/COPS/389.xml 29.85 0.01
TRS_GTRS/COPS/390.xml 0.31 0.00
TRS_GTRS/COPS/391.xml 0.55 39.99
TRS_GTRS/COPS/403.xml 0.62 39.79
TRS_GTRS/COPS/404.xml 0.44 79.76
TRS_GTRS/COPS/405.xml 240 218.61
TRS_GTRS/COPS/406.xml 2.45 37.00
TRS_GTRS/COPS/407.xml 29.90 36.00
TRS_GTRS/COPS/408.xml 1.90 38.21
TRS_GTRS/COPS/409.xml 29.89 36.96
TRS_GTRS/COPS/410.xml 3.08 39.86
TRS_GTRS/COPS/411.xml 29.82 39.88
TRS_GTRS/CSR_04/Ex14_AEGL02.xml 0.01 73.20
TRS_GTRS/CSR_04/Ex14_Luc06.xml 0.90 59.51
TRS_GTRS/CSR_04/Ex15_Luc06.xml 0.01 0.02
TRS_GTRS/CSR_04/Ex15_Luc98.xml 0.02 218.64
TRS_GTRS/CSR_04/Ex16_Luc06.xml 0.01 0.01
TRS_GTRS/CSR_04/Ex18_Luc06.xml 0.01 0.05
TRS_GTRS/CSR_04/Ex1_2_AEL03.xml 0.03 200.85
TRS_GTRS/CSR_04/Ex1_2_Luc02c.xml 0.00 0.03
TRS_GTRS/CSR_04/Ex1_GL02a.xml 0.06 35.73
TRS_GTRS/CSR_04/Ex1_GM03.xml 0.15 78.84
TRS_GTRS/CSR_04/Ex1_GM99.xml 0.00 0.00
TRS_GTRS/CSR_04/Ex1_Luc02b.xml 0.00 57.33
TRS_GTRS/CSR_04/Ex1_Luc04b.xml 0.00 0.00
TRS_GTRS/CSR_04/Ex1_Zan97.xml 0.02 39.84
Examples 99% muterm-term muterm-gtrs
TRS_GTRS/CSR_04/Ex23_Luc06.xml 0.01 0.00
TRS_GTRS/CSR_04/Ex24_GM04.xml 0.01 0.03
TRS_GTRS/CSR_04/Ex24_Luc06.xml 0.00 0.03
TRS_GTRS/CSR_04/Ex25_Luc06.xml 0.00 0.02
TRS_GTRS/CSR_04/Ex26_Luc03b.xml 0.00 0.01
TRS_GTRS/CSR_04/Ex2_Luc02a.xml 0.01 195.18
TRS_GTRS/CSR_04/Ex2_Luc03b.xml 0.00 0.02
TRS_GTRS/CSR_04/Ex3_12_Luc96a.xml 0.00 31.76
TRS_GTRS/CSR_04/Ex3_2_Luc97.xml 4.87 215.69
TRS_GTRS/CSR_04/Ex3_3_25_Bor03.xml 0.01 0.04
TRS_GTRS/CSR_04/Ex49_GM04.xml 0.05 76.04
TRS_GTRS/CSR_04/Ex4_4_Luc96b.xml 0.00 18.46
TRS_GTRS/CSR_04/Ex4_7_15_Bor03.xml 0.02 0.03
TRS_GTRS/CSR_04/Ex4_7_37_Bor03.xml 0.03 114.56
TRS_GTRS/CSR_04/Ex4_7_56_Bor03.xml 0.01 32.11
TRS_GTRS/CSR_04/Ex4_7_77_Bor03.xml 0.00 0.00
TRS_GTRS/CSR_04/Ex4_DLMMU04.xml 1.44 215.23
TRS_GTRS/CSR_04/Ex4_Zan97.xml 0.01 79.25
TRS_GTRS/CSR_04/Ex5_7_Luc97.xml 2.89 218.82
TRS_GTRS/CSR_04/Ex5_DLMMU04.xml 0.01 0.00
TRS_GTRS/CSR_04/Ex5_Zan97.xml 0.10 0.01
TRS_GTRS/CSR_04/Ex6_15_AEL02.xml 1.45 203.59
TRS_GTRS/CSR_04/Ex6_9_Luc02c.xml 0.00 0.00
TRS_GTRS/CSR_04/Ex6_GM04.xml 0.01 0.00
TRS_GTRS/CSR_04/Ex6_Luc98.xml 0.03 0.04
TRS_GTRS/CSR_04/Ex7_BLR02.xml 0.02 55.64
TRS_GTRS/CSR_04/Ex8_BLR02.xml 0.02 124.38
TRS_GTRS/CSR_04/Ex9_BLR02.xml 0.00 0.02
TRS_GTRS/CSR_04/Ex9_Luc04.xml 0.12 0.04
TRS_GTRS/CSR_04/Ex9_Luc06.xml 0.19 10.19
TRS_GTRS/CSR_04/ExAppendixB_AEL03.xml 0.01 202.12
TRS_GTRS/CSR_04/ExConc_Zan97.xml 0.00 0.00
TRS_GTRS/CSR_04/ExIntrod_GM01.xml 0.00 0.03
TRS_GTRS/CSR_04/ExIntrod_GM04.xml 0.02 0.00
TRS_GTRS/CSR_04/ExIntrod_GM99.xml 0.00 0.01
TRS_GTRS/CSR_04/ExIntrod_Zan97.xml 2.81 150.70
TRS_GTRS/CSR_04/ExProp7_Luc06.xml 0.07 0.02
TRS_GTRS/CSR_04/ExSec11_1_Luc02a.xml 0.00 208.80
TRS_GTRS/CSR_04/ExSec4_2_DLMMU04.xml 0.03 133.99
TRS_GTRS/Maude_06/csrdiv.xml 0.27 154.54
TRS_GTRS/Maude_06/emmes.xml 1.11 0.00
TRS_GTRS/Maude_06/LengthOfFiniteLists_complete-noand.xml 0.39 204.11
TRS_GTRS/Maude_06/LengthOfFiniteLists_complete.xml 17.54 204.78
TRS_GTRS/Maude_06/LengthOfFiniteLists_nokinds-noand.xml 0.13 197.65
TRS_GTRS/Maude_06/LengthOfFiniteLists_nokinds.xml 4.01 211.97
TRS_GTRS/Maude_06/LengthOfFiniteLists_nosorts-noand.xml 0.51 121.95
TRS_GTRS/Maude_06/LengthOfFiniteLists_nosorts.xml 0.16 53.88
TRS_GTRS/Maude_06/LISTUTILITIES_complete-noand.xml 7.49 213.28
TRS_GTRS/Maude_06/LISTUTILITIES_complete.xml 221.67 212.36
TRS_GTRS/Maude_06/LISTUTILITIES_nokinds-noand.xml 0.51 209.18
TRS_GTRS/Maude_06/LISTUTILITIES_nokinds.xml 147.97 212.52
TRS_GTRS/Maude_06/LISTUTILITIES_nosorts-noand.xml 0.02 202.88
TRS_GTRS/Maude_06/LISTUTILITIES_nosorts.xml 0.03 130.24
TRS_GTRS/Maude_06/MYNAT_complete-noand-peanoSimple.xml 0.08 207.61
TRS_GTRS/Maude_06/MYNAT_complete-noand.xml 0.23 207.43
TRS_GTRS/Maude_06/MYNAT_complete-peanoSimple.xml 0.26 224.42
TRS_GTRS/Maude_06/MYNAT_complete.xml 10.77 211.86
TRS_GTRS/Maude_06/MYNAT_nokinds-noand-peanoSimple.xml 0.00 209.62
TRS_GTRS/Maude_06/MYNAT_nokinds-noand.xml 0.01 211.33
TRS_GTRS/Maude_06/MYNAT_nokinds-peanoSimple.xml 0.03 232.36
TRS_GTRS/Maude_06/MYNAT_nokinds.xml 1.83 220.63
TRS_GTRS/Maude_06/MYNAT_nosorts-noand-peanoSimple.xml 0.00 54.87
TRS_GTRS/Maude_06/MYNAT_nosorts-noand.xml 0.01 147.56
TRS_GTRS/Maude_06/MYNAT_nosorts-peanoSimple.xml 0.00 18.61
TRS_GTRS/Maude_06/MYNAT_nosorts.xml 0.00 49.62
TRS_GTRS/Maude_06/OvConsOS_complete-noand.xml 0.93 209.70
TRS_GTRS/Maude_06/OvConsOS_complete.xml 225.64 209.43
TRS_GTRS/Maude_06/OvConsOS_nokinds-noand.xml 0.14 204.52
TRS_GTRS/Maude_06/OvConsOS_nokinds.xml 88.32 212.57
TRS_GTRS/Maude_06/OvConsOS_nosorts-noand.xml 0.74 204.12
TRS_GTRS/Maude_06/OvConsOS_nosorts.xml 0.18 71.29
TRS_GTRS/Maude_06/PALINDROME_complete-noand.xml 0.24 205.54
TRS_GTRS/Maude_06/PALINDROME_complete.xml 0.35 200.15
TRS_GTRS/Maude_06/PALINDROME_nokinds-noand.xml 0.03 197.49
TRS_GTRS/Maude_06/PALINDROME_nokinds.xml 0.11 213.21
TRS_GTRS/Maude_06/PALINDROME_nosorts-noand.xml 0.02 79.15
TRS_GTRS/Maude_06/PALINDROME_nosorts.xml 0.01 62.96
TRS_GTRS/Mixed_CTRS/AAECC-ring-cond.xml 240 214.78
TRS_GTRS/Mixed_CTRS/AAECCcond.xml 240 204.59
TRS_GTRS/Mixed_CTRS/fib.xml 65.20 228.66
TRS_GTRS/Mixed_CTRS/gcd.xml 30.11 209.18
TRS_GTRS/Mixed_CTRS/quick.xml 0.04 227.35
TRS_GTRS/Mixed_CTRS/quicksort.xml 31.30 62.00
TRS_GTRS/Mixed_CTRS/quotrem.xml 30.13 35.35
TRS_GTRS/Mixed_CTRS_2014/ex1-lucmes-wrla14.xml 240 38.33
TRS_GTRS/Mixed_CTRS_2014/ex1-muterm14.xml 0.12 0.01
TRS_GTRS/Mixed_CTRS_2014/ex2-lucmes-wrla14.xml 240 20.01
TRS_GTRS/Mixed_CTRS_2014/ex2-muterm14.xml 0.12 0.01
TRS_GTRS/Mixed_CTRS_2014/ex3-muterm14.xml 29.99 159.30
TRS_GTRS/Mixed_CTRS_2014/hosc08-ex5-aecc-p46.xml 30.09 0.01
TRS_GTRS/Mixed_CTRS_2014/jlap09-ex16.xml 30.20 0.02
TRS_GTRS/Mixed_CTRS_2014/jlap09-ex17.xml 236.21 19.96
TRS_GTRS/Mixed_CTRS_2014/logic.xml 240 109.30
TRS_GTRS/Mixed_CTRS_2014/lucMarMes.xml 0.28 0.03
TRS_GTRS/Mixed_CTRS_2014/mar.xml 240 120.12
TRS_GTRS/Mixed_CTRS_2014/mar_simple1.xml 240 121.29
TRS_GTRS/Mixed_CTRS_2014/mar_simple2.xml 240 119.47
TRS_GTRS/Mixed_CTRS_2014/minus1.xml 0.70 58.80
TRS_GTRS/Mixed_CTRS_2014/ohl.xml 164.40 0.06
TRS_GTRS/Mixed_CTRS_2014/ohl190.xml 0.44 19.97
TRS_GTRS/Mixed_CTRS_2014/ohl194.xml 30.39 129.30
TRS_GTRS/Mixed_CTRS_2014/ohl196.xml 0.44 39.86
TRS_GTRS/Mixed_CTRS_2014/ohl206.xml 29.94 38.23
TRS_GTRS/Mixed_CTRS_2014/ohl211.xml 0.51 0.04
TRS_GTRS/Mixed_CTRS_2014/ohl216.xml 0.84 79.13
TRS_GTRS/Mixed_CTRS_2014/ohl228.xml 167.23 57.21
TRS_GTRS/Mixed_CTRS_2014/ohl230.xml 30.04 159.40
TRS_GTRS/Mixed_CTRS_2014/plus1.xml 29.87 44.20
TRS_GTRS/Mixed_CTRS_2014/sche128.xml 0.74 0.02
TRS_GTRS/Transformed_outermost_08/cariboo_ex1.xml 0.04 0.02
TRS_GTRS/Transformed_outermost_08/cariboo_ex2.xml 0.81 215.71
TRS_GTRS/Transformed_outermost_08/cariboo_ex3.xml 0.05 146.87
TRS_GTRS/Transformed_outermost_08/cariboo_ex4.xml 0.01 39.62
TRS_GTRS/Transformed_outermost_08/cariboo_ex5.xml 0.04 0.01
TRS_GTRS/Transformed_outermost_08/cariboo_ex6.xml 0.03 216.84
TRS_GTRS/Transformed_outermost_08/ex5.3.xml 0.01 0.03
TRS_GTRS/Transformed_outermost_08/ex5.4.xml 0.70 209.20
TRS_GTRS/Transformed_outermost_08/ex5.5.xml 0.20 224.35
TRS_GTRS/Transformed_outermost_08/ex5.6.xml 0.01 216.71
TRS_GTRS/Transformed_outermost_08/ex5.7.xml 0.06 209.01
TRS_GTRS/Transformed_outermost_08/ex5.8.xml 0.06 77.29
TRS_GTRS/Transformed_outermost_08/f20.xml 2.17 216.38
TRS_GTRS/Transformed_outermost_08/f30.xml 0.09 195.29
TRS_GTRS/Transformed_outermost_08/f4.xml 0.15 70.52
TRS_GTRS/Transformed_outermost_08/f40.xml 0.17 199.67
TRS_GTRS/Transformed_outermost_08/morse.xml 1.14 212.19
MU-TERM TERM MU-TERM GTRS
Time 2758.47 19036.51
#YES 186 133
#MAYBE 24 85
#NO 15 7
Avg. YES 7.58 30.98
Avg. NO 31.21 20.05