Features
Processor
Intel(R) Core(TM) i5-7300U CPU @ 2.60GHz 2.71GHz
RAM
8.00 GB
OS
Linux 4.4.0-17134-Microsoft
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
muTerm, version 5.0
Database
TermComp (TRS Context-Sensitive)
Timeout
120s
Date
11.11.21
Examples
confident-1.3.4
confident-noECPs
Ex14_AEGL02.trs
0.001
0.003
Ex14_Luc06.trs
0.001
0.001
Ex15_Luc06.trs
0.001
0.001
Ex15_Luc98.trs
0.001
0.001
Ex16_Luc06.trs
0.001
0.002
Ex18_Luc06.trs
0.001
0.001
Ex1_2_AEL03.trs
0.001
0.003
Ex1_2_Luc02c.trs
0.001
0.002
Ex1_GL02a.trs
0.001
0.001
Ex1_GM03.trs
0.014
0.014
Ex1_GM99.trs
0.001
0.001
Ex1_Luc02b.trs
0.001
0.002
Ex1_Luc04b.trs
0.001
0.001
Ex1_Zan97.trs
0.001
0.001
Ex23_Luc06.trs
0.001
0.001
Ex24_GM04.trs
0.001
0.001
Ex24_Luc06.trs
0.001
0.002
Ex25_Luc06.trs
0.001
0.001
Ex26_Luc03b.trs
0.002
0.002
Ex2_Luc02a.trs
0.001
0.002
Ex2_Luc03b.trs
0.002
0.002
Ex3_12_Luc96a.trs
0.001
0.002
Ex3_2_Luc97.trs
0.001
0.001
Ex3_3_25_Bor03.trs
0.002
0.002
Ex49_GM04.trs
0.001
0.006
Ex4_4_Luc96b.trs
0.001
0.002
Ex4_7_15_Bor03.trs
0.001
0.001
Ex4_7_37_Bor03.trs
0.002
0.003
Ex4_7_56_Bor03.trs
0.001
0.002
Ex4_7_77_Bor03.trs
0.001
0.001
Ex4_DLMMU04.trs
0.001
0.001
Ex4_Zan97.trs
0.001
0.002
Ex5_7_Luc97.trs
0.001
0.001
Ex5_DLMMU04.trs
0.002
0.002
Ex5_Zan97.trs
0.001
0.001
Ex6_15_AEL02.trs
0.004
0.084
Ex6_9_Luc02c.trs
0.001
0.002
Ex6_GM04.trs
0.001
0.001
Ex6_Luc98.trs
0.001
0.002
Ex7_BLR02.trs
0.001
0.002
Ex8_BLR02.trs
0.001
0.002
Ex9_BLR02.trs
0.002
0.002
Ex9_Luc04.trs
0.001
0.001
Ex9_Luc06.trs
0.001
0.01
ExAppendixB_AEL03.trs
0.002
0.002
ExConc_Zan97.trs
0.001
0.002
ExIntrod_GM01.trs
0.001
0.001
ExIntrod_GM04.trs
0.001
0.001
ExIntrod_GM99.trs
0.002
0.002
ExIntrod_Zan97.trs
0.025
4.034
ExProp7_Luc06.trs
0.001
0.001
ExSec11_1_Luc02a.trs
0.002
0.039
ExSec4_2_DLMMU04.trs
0.002
0.002
LISTUTILITIES_complete-noand.trs
0.019
5.097
LISTUTILITIES_complete.trs
0.016
30.003
LISTUTILITIES_nokinds-noand.trs
0.008
0.055
LISTUTILITIES_nokinds.trs
0.008
30.002
LISTUTILITIES_nosorts-noand.trs
0.019
0.004
LISTUTILITIES_nosorts.trs
0.002
0.002
LengthOfFiniteLists_complete-noand.trs
0.002
0.002
LengthOfFiniteLists_complete.trs
0.002
0.002
LengthOfFiniteLists_nokinds-noand.trs
0.001
0.001
LengthOfFiniteLists_nokinds.trs
0.001
0.001
LengthOfFiniteLists_nosorts-noand.trs
0.001
0.001
LengthOfFiniteLists_nosorts.trs
0.001
0.001
MYNAT_complete-noand-peanoSimple.trs
0.002
0.009
MYNAT_complete-noand.trs
0.003
0.031
MYNAT_complete-peanoSimple.trs
0.002
0.025
MYNAT_complete.trs
0.002
11
MYNAT_nokinds-noand-peanoSimple.trs
0.001
0.002
MYNAT_nokinds-noand.trs
0.002
0.003
MYNAT_nokinds-peanoSimple.trs
0.001
0.005
MYNAT_nokinds.trs
0.002
1.078
MYNAT_nosorts-noand-peanoSimple.trs
0.015
0.002
MYNAT_nosorts-noand.trs
3.018
0.002
MYNAT_nosorts-peanoSimple.trs
0.001
0.001
MYNAT_nosorts.trs
0.001
0.001
OvConsOS_complete-noand.trs
0.002
0.003
OvConsOS_complete.trs
0.002
0.002
OvConsOS_nokinds-noand.trs
0.001
0.001
OvConsOS_nokinds.trs
0.001
0.001
OvConsOS_nosorts-noand.trs
0.001
0.05
OvConsOS_nosorts.trs
0.001
0.011
PALINDROME_complete-noand.trs
0.002
0.002
PALINDROME_complete.trs
0.002
0.002
PALINDROME_nokinds-noand.trs
0.002
0.001
PALINDROME_nokinds.trs
0.001
0.001
PALINDROME_nosorts-noand.trs
0.004
0.001
PALINDROME_nosorts.trs
0.001
0.001
cariboo_ex1.trs
0.001
0.001
cariboo_ex2.trs
3.052
0.039
cariboo_ex3.trs
0.001
0.001
cariboo_ex4.trs
0.001
0.001
cariboo_ex5.trs
0.001
0.001
cariboo_ex6.trs
0.001
0.001
csrdiv.trs
0.001
0.014
emmes.trs
0.001
1.001
ex5.3.trs
0.001
0.001
ex5.4.trs
0.001
0.002
ex5.5.trs
10.036
4.017
ex5.6.trs
0.001
0.001
ex5.7.trs
0.001
0.001
ex5.8.trs
0.001
0.001
f20.trs
0.004
0.003
f30.trs
0.009
0.008
f4.trs
0.001
0.001
f40.trs
0.017
0.017
morse.trs
0.002
0.002
confident-1.3.4
confident-noECPs
Time
16.386
86.781
#YES
27
25
#MAYBE
2
53
#NO
79
30
Avg.YES
0.11
0
Avg.NO
0
0
Examples (using canonical replacemnt map)
confident-1.3.4
Ex14_AEGL02-canonical.trs
0.001
Ex14_Luc06-canonical.trs
0.001
Ex15_Luc06-canonical.trs
0.001
Ex15_Luc98-canonical.trs
0.001
Ex16_Luc06-canonical.trs
0.005
Ex18_Luc06-canonical.trs
0.001
Ex1_2_AEL03-canonical.trs
0.001
Ex1_2_Luc02c-canonical.trs
0.001
Ex1_GL02a-canonical.trs
0.001
Ex1_GM03-canonical.trs
0.001
Ex1_GM99-canonical.trs
0.001
Ex1_Luc02b-canonical.trs
0.001
Ex1_Luc04b-canonical.trs
0.001
Ex1_Zan97-canonical.trs
0.001
Ex23_Luc06-canonical.trs
0.001
Ex24_GM04-canonical.trs
0.001
Ex24_Luc06-canonical.trs
0.001
Ex25_Luc06-canonical.trs
0.001
Ex26_Luc03b-canonical.trs
0.001
Ex2_Luc02a-canonical.trs
0.001
Ex2_Luc03b-canonical.trs
0.001
Ex3_12_Luc96a-canonical.trs
0.001
Ex3_2_Luc97-canonical.trs
0.001
Ex3_3_25_Bor03-canonical.trs
0.001
Ex49_GM04-canonical.trs
0.001
Ex4_4_Luc96b-canonical.trs
0.001
Ex4_7_15_Bor03-canonical.trs
0.001
Ex4_7_37_Bor03-canonical.trs
0.001
Ex4_7_56_Bor03-canonical.trs
0.001
Ex4_7_77_Bor03-canonical.trs
0.001
Ex4_DLMMU04-canonical.trs
0.002
Ex4_Zan97-canonical.trs
0.001
Ex5_7_Luc97-canonical.trs
0.001
Ex5_DLMMU04-canonical.trs
0.001
Ex5_Zan97-canonical.trs
0.001
Ex6_15_AEL02-canonical.trs
0.002
Ex6_9_Luc02c-canonical.trs
0.001
Ex6_GM04-canonical.trs
0.001
Ex6_Luc98-canonical.trs
0.001
Ex7_BLR02-canonical.trs
0.001
Ex8_BLR02-canonical.trs
0.001
Ex9_BLR02-canonical.trs
0.001
Ex9_Luc04-canonical.trs
0.001
Ex9_Luc06-canonical.trs
0.018
ExAppendixB_AEL03-canonical.trs
0.001
ExConc_Zan97-canonical.trs
0.001
ExIntrod_GM01-canonical.trs
0.001
ExIntrod_GM04-canonical.trs
0.001
ExIntrod_GM99-canonical.trs
0.002
ExIntrod_Zan97-canonical.trs
0.001
ExProp7_Luc06-canonical.trs
0.001
ExSec11_1_Luc02a-canonical.trs
0.001
ExSec4_2_DLMMU04-canonical.trs
0.001
LISTUTILITIES_complete-noand-canonical.trs
0.008
LISTUTILITIES_complete-canonical.trs
0.003
LISTUTILITIES_nokinds-noand-canonical.trs
0.002
LISTUTILITIES_nokinds-canonical.trs
0.002
LISTUTILITIES_nosorts-noand-canonical.trs
0.002
LISTUTILITIES_nosorts-canonical.trs
0.002
LengthOfFiniteLists_complete-noand-canonical.trs
0.002
LengthOfFiniteLists_complete-canonical.trs
0.002
LengthOfFiniteLists_nokinds-noand-canonical.trs
0.001
LengthOfFiniteLists_nokinds-canonical.trs
0.001
LengthOfFiniteLists_nosorts-noand-canonical.trs
0.001
LengthOfFiniteLists_nosorts-canonical.trs
0.001
MYNAT_complete-noand-peanoSimple-canonical.trs
0.002
MYNAT_complete-noand-canonical.trs
0.002
MYNAT_complete-peanoSimple-canonical.trs
0.001
MYNAT_complete-canonical.trs
0.001
MYNAT_nokinds-noand-peanoSimple-canonical.trs
0.001
MYNAT_nokinds-noand-canonical.trs
0.001
MYNAT_nokinds-peanoSimple-canonical.trs
0.001
MYNAT_nokinds-canonical.trs
0.001
MYNAT_nosorts-noand-peanoSimple-canonical.trs
0.001
MYNAT_nosorts-noand-canonical.trs
0.001
MYNAT_nosorts-peanoSimple-canonical.trs
0.001
MYNAT_nosorts-canonical.trs
0.001
OvConsOS_complete-noand-canonical.trs
0.003
OvConsOS_complete-canonical.trs
0.002
OvConsOS_nokinds-noand-canonical.trs
0.002
OvConsOS_nokinds-canonical.trs
0.001
OvConsOS_nosorts-noand-canonical.trs
0.001
OvConsOS_nosorts-canonical.trs
0.001
PALINDROME_complete-noand-canonical.trs
0.003
PALINDROME_complete-canonical.trs
0.003
PALINDROME_nokinds-noand-canonical.trs
0.002
PALINDROME_nokinds-canonical.trs
0.002
PALINDROME_nosorts-noand-canonical.trs
0.009
PALINDROME_nosorts-canonical.trs
0.001
cariboo_ex1-canonical.trs
0.002
cariboo_ex2-canonical.trs
0.001
cariboo_ex3-canonical.trs
0.005
cariboo_ex4-canonical.trs
0.023
cariboo_ex5-canonical.trs
0.001
cariboo_ex6-canonical.trs
24.012
csrdiv-canonical.trs
0.004
emmes-canonical.trs
0.001
ex5.3-canonical.trs
0.001
ex5.4-canonical.trs
0.01
ex5.5-canonical.trs
60
ex5.6-canonical.trs
0.001
ex5.7-canonical.trs
0.001
ex5.8-canonical.trs
0.001
f20-canonical.trs
60.004
f30-canonical.trs
60.002
f4-canonical.trs
0.002
f40-canonical.trs
1.099
morse-canonical.trs
0.003
confident-1.3.4
Time
25.315
#YES
52
#MAYBE
6
#NO
50
Avg.YES
0.02
Avg.NO
0