maedmax: Maximal Ordered Completion

MaedMax Experiment : CPF proofs for TPTP UEQ UNSAT

In the following table a few are missiong due to different reasons:
maedmax try to tighten bounds a bit --json
 
10.10
ALG005-1
active equations: 154
iterations: 13
memory: 142 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.836
ground joinability: 0
find TRSs: 1.003
compute CPs: 4.685
main control loop: 7.71
rewriting: 2.58
SMT solver: 0.01
selection: 0.279
success checks: 0.201
proof
0.38
ALG006-1
active equations: 51
iterations: 5
memory: 8 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.029
ground joinability: 0
find TRSs: 0.046
compute CPs: 0.12
main control loop: 0.274
rewriting: 0.102
SMT solver: 0
selection: 0.013
success checks: 0.031
proof
12.75
ALG007-1
active equations: 105
iterations: 9
memory: 130 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.295
ground joinability: 0
find TRSs: 0.38
compute CPs: 7.007
main control loop: 11.076
rewriting: 3.635
SMT solver: 0.004
selection: 0.264
success checks: 0.184
proof
0.04
ALG235-1
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.014
main control loop: 0
rewriting: 0.006
SMT solver: 0
selection: 0.004
success checks: 0
proof
7.47
ALG236-1
active equations: 87
iterations: 8
memory: 63 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.3
ground joinability: 0
find TRSs: 0.356
compute CPs: 2.775
main control loop: 4.861
rewriting: 2.566
SMT solver: 0.003
selection: 0.267
success checks: 0.134
proof
 
 
 
 
 
 
 
 
 
 
0.08
BOO001-1
active equations: 29
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.035
main control loop: 0.044
rewriting: 0.016
SMT solver: 0
selection: 0.003
success checks: 0.002
proof
7.24
BOO002-1
active equations: 100
iterations: 9
memory: 123 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.124
ground joinability: 0
find TRSs: 0.168
compute CPs: 3.362
main control loop: 4.382
rewriting: 2.686
SMT solver: 0.002
selection: 0.228
success checks: 0.096
proof
0.85
BOO002-2
active equations: 53
iterations: 5
memory: 15 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.03
ground joinability: 0
find TRSs: 0.049
compute CPs: 0.357
main control loop: 0.416
rewriting: 0.261
SMT solver: 0.001
selection: 0.033
success checks: 0.015
proof
0.05
BOO003-2
active equations: 42
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.009
main control loop: 0.029
rewriting: 0.004
SMT solver: 0
selection: 0.001
success checks: 0.009
proof
0.05
BOO003-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.015
compute CPs: 0.007
main control loop: 0.024
rewriting: 0.003
SMT solver: 0
selection: 0.001
success checks: 0.008
proof
0.06
BOO004-2
active equations: 42
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.01
main control loop: 0.03
rewriting: 0.004
SMT solver: 0.001
selection: 0.002
success checks: 0.009
proof
0.05
BOO004-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.007
main control loop: 0.024
rewriting: 0.003
SMT solver: 0
selection: 0.001
success checks: 0.008
proof
0.06
BOO005-2
active equations: 42
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.009
main control loop: 0.027
rewriting: 0.004
SMT solver: 0.001
selection: 0.001
success checks: 0.008
proof
0.06
BOO005-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.011
main control loop: 0.025
rewriting: 0.006
SMT solver: 0.001
selection: 0.001
success checks: 0.01
proof
0.04
BOO006-2
active equations: 42
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.007
main control loop: 0.017
rewriting: 0.004
SMT solver: 0
selection: 0.001
success checks: 0.005
proof
0.06
BOO006-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.015
compute CPs: 0.012
main control loop: 0.025
rewriting: 0.006
SMT solver: 0.001
selection: 0.001
success checks: 0.01
proof
39.65
BOO007-2
active equations: 434
iterations: 16
memory: 662 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 7.167
ground joinability: 0
find TRSs: 7.863
compute CPs: 21.137
main control loop: 29.177
rewriting: 4.645
SMT solver: 0.037
selection: 0.544
success checks: 1.578
proof
184.48
BOO007-4
active equations: 791
iterations: 29
memory: 2018 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 50.375
ground joinability: 0
find TRSs: 53.384
compute CPs: 91.728
main control loop: 114.514
rewriting: 15.654
SMT solver: 0.176
selection: 1.289
success checks: 5.614
proof
45.76
BOO008-2
active equations: 490
iterations: 18
memory: 616 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 10.75
ground joinability: 0
find TRSs: 11.578
compute CPs: 20.786
main control loop: 30.814
rewriting: 5.612
SMT solver: 0.05
selection: 0.646
success checks: 2.324
proof
244.35
BOO008-4
active equations: 987
iterations: 36
memory: 2269 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 101.525
ground joinability: 0
find TRSs: 106.662
compute CPs: 82.475
main control loop: 113.951
rewriting: 16.873
SMT solver: 0.335
selection: 1.184
success checks: 11.398
 
0.08
BOO009-2
active equations: 42
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.017
main control loop: 0.029
rewriting: 0.009
SMT solver: 0.001
selection: 0.002
success checks: 0.01
proof
0.05
BOO009-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.009
main control loop: 0.023
rewriting: 0.005
SMT solver: 0.001
selection: 0.002
success checks: 0.008
proof
0.08
BOO010-2
active equations: 42
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.018
main control loop: 0.029
rewriting: 0.009
SMT solver: 0.001
selection: 0.002
success checks: 0.01
proof
0.05
BOO010-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.007
main control loop: 0.021
rewriting: 0.003
SMT solver: 0.001
selection: 0.001
success checks: 0.006
proof
0.03
BOO011-2
active equations: 14
iterations: 1
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.007
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.06
BOO011-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.01
main control loop: 0.022
rewriting: 0.006
SMT solver: 0
selection: 0.002
success checks: 0.008
proof
0.15
BOO012-2
active equations: 70
iterations: 3
memory: 4 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.057
compute CPs: 0.035
main control loop: 0.05
rewriting: 0.014
SMT solver: 0.002
selection: 0.003
success checks: 0.01
proof
0.12
BOO012-4
active equations: 64
iterations: 3
memory: 4 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.024
ground joinability: 0
find TRSs: 0.04
compute CPs: 0.031
main control loop: 0.04
rewriting: 0.011
SMT solver: 0.002
selection: 0.002
success checks: 0.01
proof
0.42
BOO013-2
active equations: 128
iterations: 5
memory: 13 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.128
ground joinability: 0
find TRSs: 0.18
compute CPs: 0.081
main control loop: 0.162
rewriting: 0.039
SMT solver: 0.006
selection: 0.013
success checks: 0.034
proof
0.49
BOO013-4
active equations: 146
iterations: 6
memory: 11 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.212
ground joinability: 0
find TRSs: 0.292
compute CPs: 0.059
main control loop: 0.153
rewriting: 0.025
SMT solver: 0.011
selection: 0.007
success checks: 0.021
proof
210.76
BOO014-2
active equations: 884
iterations: 32
memory: 2330 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 78.144
ground joinability: 0
find TRSs: 82.515
compute CPs: 79.244
main control loop: 118.4
rewriting: 17.139
SMT solver: 0.403
selection: 2.098
success checks: 8.109
proof
154.64
BOO014-4
active equations: 651
iterations: 24
memory: 2026 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 26.299
ground joinability: 0
find TRSs: 28.123
compute CPs: 80.798
main control loop: 121.993
rewriting: 16.773
SMT solver: 0.12
selection: 1.56
success checks: 12.312
proof
220.50
BOO015-2
active equations: 940
iterations: 34
memory: 2351 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 75.923
ground joinability: 0
find TRSs: 81.063
compute CPs: 80.404
main control loop: 121.438
rewriting: 19.956
SMT solver: 0.48
selection: 3.661
success checks: 9.526
proof
70.20
BOO015-4
active equations: 595
iterations: 22
memory: 1286 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 10.746
ground joinability: 0
find TRSs: 11.594
compute CPs: 39.77
main control loop: 56.361
rewriting: 7.186
SMT solver: 0.045
selection: 0.787
success checks: 3.493
proof
0.16
BOO016-2
active equations: 71
iterations: 3
memory: 5 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.037
ground joinability: 0
find TRSs: 0.057
compute CPs: 0.04
main control loop: 0.042
rewriting: 0.014
SMT solver: 0.003
selection: 0.005
success checks: 0.008
proof
0.17
BOO017-2
active equations: 71
iterations: 3
memory: 5 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.06
compute CPs: 0.041
main control loop: 0.045
rewriting: 0.018
SMT solver: 0.003
selection: 0.004
success checks: 0.009
proof
0.03
BOO018-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: boro
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0.004
proof
0.03
BOO021-1
active equations: 30
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.004
main control loop: 0.007
rewriting: 0.004
SMT solver: 0.002
selection: 0
success checks: 0
proof
82.49
BOO022-1
active equations: 573
iterations: 21
memory: 1269 MB
restarts: 1
problem shape: boro
time (sec): 
reducibility constraints: 13.234
ground joinability: 0
find TRSs: 14.657
compute CPs: 44.444
main control loop: 64.546
rewriting: 8.933
SMT solver: 0.074
selection: 0.878
success checks: 4.971
proof
 
0.86
BOO024-1
active equations: 97
iterations: 8
memory: 13 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.215
ground joinability: 0
find TRSs: 0.332
compute CPs: 0.152
main control loop: 0.411
rewriting: 0.125
SMT solver: 0.023
selection: 0.032
success checks: 0.048
proof
0.72
BOO025-1
active equations: 73
iterations: 6
memory: 9 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.174
ground joinability: 0
find TRSs: 0.282
compute CPs: 0.13
main control loop: 0.305
rewriting: 0.099
SMT solver: 0.024
selection: 0.024
success checks: 0.034
proof
49.11
BOO026-1
active equations: 245
iterations: 9
memory: 249 MB
restarts: 3
problem shape: boro
time (sec): 
reducibility constraints: 21.263
ground joinability: 0
find TRSs: 28.119
compute CPs: 6.034
main control loop: 16.85
rewriting: 5.175
SMT solver: 3.354
selection: 1.62
success checks: 1.386
proof
 
1.02
BOO029-1
active equations: 119
iterations: 6
memory: 20 MB
restarts: 1
problem shape: silicio
time (sec): 
reducibility constraints: 0.201
ground joinability: 0
find TRSs: 0.235
compute CPs: 0.156
main control loop: 0.61
rewriting: 0.275
SMT solver: 0.002
selection: 0.025
success checks: 0.079
proof
 
0.17
BOO034-1
active equations: 29
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.065
main control loop: 0.056
rewriting: 0.038
SMT solver: 0.005
selection: 0.005
success checks: 0.013
proof
4.21
BOO067-1
active equations: 39
iterations: 4
memory: 30 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.096
ground joinability: 0
find TRSs: 0.145
compute CPs: 1.457
main control loop: 4.015
rewriting: 1.629
SMT solver: 0.007
selection: 0.142
success checks: 0.022
proof
5.54
BOO068-1
active equations: 59
iterations: 6
memory: 22 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.05
ground joinability: 0
find TRSs: 0.079
compute CPs: 1.846
main control loop: 5.423
rewriting: 2.419
SMT solver: 0.001
selection: 0.187
success checks: 0.013
proof
5.95
BOO069-1
active equations: 47
iterations: 5
memory: 26 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.031
ground joinability: 0
find TRSs: 0.051
compute CPs: 1.967
main control loop: 5.858
rewriting: 2.712
SMT solver: 0.001
selection: 0.192
success checks: 0.012
proof
5.94
BOO070-1
active equations: 83
iterations: 8
memory: 22 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.091
ground joinability: 0
find TRSs: 0.133
compute CPs: 1.929
main control loop: 5.777
rewriting: 2.612
SMT solver: 0.002
selection: 0.197
success checks: 0.012
proof
6.26
BOO071-1
active equations: 47
iterations: 5
memory: 26 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.029
ground joinability: 0
find TRSs: 0.049
compute CPs: 2.111
main control loop: 6.175
rewriting: 2.808
SMT solver: 0.001
selection: 0.187
success checks: 0.011
proof
7.19
BOO072-1
active equations: 96
iterations: 9
memory: 31 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.132
ground joinability: 0
find TRSs: 0.194
compute CPs: 2.103
main control loop: 6.204
rewriting: 3.975
SMT solver: 0.003
selection: 0.314
success checks: 0.029
proof
 
4.06
BOO074-1
active equations: 96
iterations: 9
memory: 34 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.078
ground joinability: 0
find TRSs: 0.117
compute CPs: 1.185
main control loop: 3.699
rewriting: 2.175
SMT solver: 0.001
selection: 0.198
success checks: 0.019
proof
1.28
BOO075-1
active equations: 84
iterations: 7
memory: 16 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.098
ground joinability: 0
find TRSs: 0.13
compute CPs: 0.494
main control loop: 1.097
rewriting: 0.491
SMT solver: 0.001
selection: 0.046
success checks: 0.008
proof
 
0.25
COL001-1
active equations: 26
iterations: 3
memory: 5 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.005
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.079
main control loop: 0.118
rewriting: 0.079
SMT solver: 0
selection: 0.026
success checks: 0.009
proof
0.08
COL001-2
active equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.025
main control loop: 0.023
rewriting: 0.022
SMT solver: 0
selection: 0.007
success checks: 0.004
proof
0.14
COL002-1
active equations: 16
iterations: 2
memory: 4 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.047
main control loop: 0.028
rewriting: 0.036
SMT solver: 0
selection: 0.015
success checks: 0.006
proof
0.03
COL002-4
active equations: 5
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.008
main control loop: 0
rewriting: 0.006
SMT solver: 0
selection: 0.002
success checks: 0
proof
0.03
COL002-5
active equations: 5
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.008
main control loop: 0
rewriting: 0.006
SMT solver: 0
selection: 0.003
success checks: 0
proof
 
1.65
COL003-12
active equations: 63
iterations: 6
memory: 23 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.083
ground joinability: 0
find TRSs: 0.132
compute CPs: 0.426
main control loop: 1.038
rewriting: 0.387
SMT solver: 0.004
selection: 0.084
success checks: 0.119
proof
1.62
COL003-13
active equations: 63
iterations: 6
memory: 17 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.069
ground joinability: 0
find TRSs: 0.111
compute CPs: 0.515
main control loop: 1.023
rewriting: 0.344
SMT solver: 0.004
selection: 0.083
success checks: 0.105
proof
1.75
COL003-14
active equations: 75
iterations: 7
memory: 26 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.127
ground joinability: 0
find TRSs: 0.197
compute CPs: 0.433
main control loop: 1.029
rewriting: 0.362
SMT solver: 0.005
selection: 0.077
success checks: 0.116
proof
1.54
COL003-15
active equations: 63
iterations: 6
memory: 17 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.073
ground joinability: 0
find TRSs: 0.114
compute CPs: 0.44
main control loop: 0.964
rewriting: 0.375
SMT solver: 0.004
selection: 0.078
success checks: 0.095
proof
1.85
COL003-16
active equations: 75
iterations: 7
memory: 26 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.133
ground joinability: 0
find TRSs: 0.206
compute CPs: 0.492
main control loop: 1.037
rewriting: 0.377
SMT solver: 0.006
selection: 0.083
success checks: 0.112
proof
6.62
COL003-17
active equations: 69
iterations: 6
memory: 61 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.406
ground joinability: 0
find TRSs: 0.556
compute CPs: 1.623
main control loop: 5.553
rewriting: 1.784
SMT solver: 0.014
selection: 0.281
success checks: 0.588
proof
7.32
COL003-18
active equations: 69
iterations: 6
memory: 69 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.407
ground joinability: 0
find TRSs: 0.564
compute CPs: 1.887
main control loop: 6.457
rewriting: 2.022
SMT solver: 0.015
selection: 0.295
success checks: 0.466
proof
7.13
COL003-19
active equations: 69
iterations: 6
memory: 59 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.441
ground joinability: 0
find TRSs: 0.599
compute CPs: 1.809
main control loop: 6.014
rewriting: 1.889
SMT solver: 0.013
selection: 0.329
success checks: 0.455
proof
6.70
COL003-20
active equations: 69
iterations: 6
memory: 67 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.41
ground joinability: 0
find TRSs: 0.561
compute CPs: 1.834
main control loop: 5.836
rewriting: 1.849
SMT solver: 0.016
selection: 0.261
success checks: 0.438
proof
 
0.00
COL004-3
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
 
 
 
 
0.01
COL007-1
active equations: 5
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.002
main control loop: 0
rewriting: 0.003
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
COL008-1
active equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.002
main control loop: 0.005
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.19
COL009-1
active equations: 26
iterations: 3
memory: 5 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.015
compute CPs: 0.05
main control loop: 0.108
rewriting: 0.049
SMT solver: 0
selection: 0.015
success checks: 0.007
proof
0.09
COL010-1
active equations: 14
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.03
main control loop: 0.04
rewriting: 0.02
SMT solver: 0
selection: 0.009
success checks: 0.002
proof
 
0.01
COL012-1
active equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
COL013-1
active equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0.003
main control loop: 0.001
rewriting: 0.005
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.02
COL014-1
active equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.005
main control loop: 0
rewriting: 0.004
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.02
COL015-1
active equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.003
main control loop: 0.005
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
COL016-1
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
COL017-1
active equations: 14
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.003
main control loop: 0.008
rewriting: 0.003
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.02
COL018-1
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.006
main control loop: 0
rewriting: 0.003
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.26
COL019-1
active equations: 15
iterations: 2
memory: 6 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.085
main control loop: 0.031
rewriting: 0.076
SMT solver: 0
selection: 0.028
success checks: 0.006
proof
0.23
COL020-1
active equations: 15
iterations: 2
memory: 5 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.073
main control loop: 0.036
rewriting: 0.072
SMT solver: 0
selection: 0.025
success checks: 0.005
proof
0.04
COL021-1
active equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.007
main control loop: 0.013
rewriting: 0.009
SMT solver: 0
selection: 0.002
success checks: 0.001
proof
0.13
COL022-1
active equations: 39
iterations: 4
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.016
ground joinability: 0
find TRSs: 0.035
compute CPs: 0.026
main control loop: 0.047
rewriting: 0.025
SMT solver: 0.002
selection: 0.008
success checks: 0.005
proof
0.14
COL023-1
active equations: 14
iterations: 2
memory: 4 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.047
main control loop: 0.024
rewriting: 0.037
SMT solver: 0
selection: 0.014
success checks: 0.006
proof
0.03
COL024-1
active equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.006
main control loop: 0.014
rewriting: 0.007
SMT solver: 0
selection: 0.002
success checks: 0.001
proof
0.02
COL025-1
active equations: 14
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.005
main control loop: 0.009
rewriting: 0.003
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.07
COL026-1
active equations: 14
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.017
main control loop: 0.013
rewriting: 0.015
SMT solver: 0
selection: 0.006
success checks: 0.002
proof
0.09
COL027-1
active equations: 14
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.03
main control loop: 0.02
rewriting: 0.021
SMT solver: 0
selection: 0.01
success checks: 0.005
proof
0.01
COL029-1
active equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.04
COL030-1
active equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.005
main control loop: 0
rewriting: 0.017
SMT solver: 0
selection: 0.002
success checks: 0
proof
0.07
COL031-1
active equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.016
main control loop: 0
rewriting: 0.017
SMT solver: 0
selection: 0.006
success checks: 0.002
proof
0.02
COL032-1
active equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.003
main control loop: 0.007
rewriting: 0.003
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.23
COL033-1
active equations: 51
iterations: 5
memory: 4 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.04
ground joinability: 0
find TRSs: 0.07
compute CPs: 0.023
main control loop: 0.117
rewriting: 0.053
SMT solver: 0.004
selection: 0.01
success checks: 0.008
proof
 
0.48
COL035-1
active equations: 39
iterations: 4
memory: 11 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.015
ground joinability: 0
find TRSs: 0.034
compute CPs: 0.071
main control loop: 0.218
rewriting: 0.162
SMT solver: 0.003
selection: 0.035
success checks: 0.027
proof
 
1.87
COL037-1
active equations: 39
iterations: 4
memory: 30 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.018
ground joinability: 0
find TRSs: 0.038
compute CPs: 0.345
main control loop: 0.828
rewriting: 0.703
SMT solver: 0.006
selection: 0.143
success checks: 0.094
proof
 
0.57
COL039-1
active equations: 63
iterations: 6
memory: 9 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.059
ground joinability: 0
find TRSs: 0.11
compute CPs: 0.08
main control loop: 0.232
rewriting: 0.164
SMT solver: 0.005
selection: 0.03
success checks: 0.017
proof
 
 
0.26
COL042-6
active equations: 39
iterations: 4
memory: 4 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.018
ground joinability: 0
find TRSs: 0.037
compute CPs: 0.067
main control loop: 0.148
rewriting: 0.056
SMT solver: 0.002
selection: 0.01
success checks: 0.018
proof
1.40
COL042-7
active equations: 63
iterations: 6
memory: 20 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.064
ground joinability: 0
find TRSs: 0.102
compute CPs: 0.385
main control loop: 0.591
rewriting: 0.399
SMT solver: 0.005
selection: 0.072
success checks: 0.068
proof
1.57
COL042-8
active equations: 75
iterations: 7
memory: 23 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.089
ground joinability: 0
find TRSs: 0.139
compute CPs: 0.436
main control loop: 1.06
rewriting: 0.433
SMT solver: 0.006
selection: 0.081
success checks: 0.093
proof
1.97
COL042-9
active equations: 75
iterations: 7
memory: 30 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.115
ground joinability: 0
find TRSs: 0.173
compute CPs: 0.489
main control loop: 0.995
rewriting: 0.498
SMT solver: 0.007
selection: 0.086
success checks: 0.115
proof
 
 
3.63
COL044-1
active equations: 50
iterations: 5
memory: 46 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.034
ground joinability: 0
find TRSs: 0.062
compute CPs: 0.773
main control loop: 1.211
rewriting: 1.347
SMT solver: 0.004
selection: 0.194
success checks: 0.099
proof
0.66
COL044-6
active equations: 39
iterations: 4
memory: 15 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.02
ground joinability: 0
find TRSs: 0.043
compute CPs: 0.219
main control loop: 0.415
rewriting: 0.175
SMT solver: 0.005
selection: 0.048
success checks: 0.052
proof
1.34
COL044-7
active equations: 51
iterations: 5
memory: 20 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.04
ground joinability: 0
find TRSs: 0.075
compute CPs: 0.379
main control loop: 0.842
rewriting: 0.396
SMT solver: 0.009
selection: 0.118
success checks: 0.083
proof
 
 
0.06
COL045-1
active equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.016
main control loop: 0.018
rewriting: 0.014
SMT solver: 0
selection: 0.006
success checks: 0.003
proof
 
0.03
COL048-1
active equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.005
main control loop: 0.012
rewriting: 0.002
SMT solver: 0
selection: 0.002
success checks: 0.002
proof
 
0.01
COL050-1
active equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
COL051-1
active equations: 8
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
COL052-1
active equations: 6
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0
main control loop: 0
rewriting: 0.002
SMT solver: 0.001
selection: 0
success checks: 0
proof
0.00
COL053-1
active equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
COL056-1
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
40.24
COL057-1
active equations: 48
iterations: 4
memory: 286 MB
restarts: 2
problem shape: carbonio
time (sec): 
reducibility constraints: 1.714
ground joinability: 0
find TRSs: 1.967
compute CPs: 8.145
main control loop: 37.808
rewriting: 15.984
SMT solver: 0.02
selection: 1.395
success checks: 3.655
proof
0.04
COL058-1
active equations: 5
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.007
main control loop: 0
rewriting: 0.013
SMT solver: 0
selection: 0.002
success checks: 0
proof
0.01
COL058-2
active equations: 5
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0.001
main control loop: 0.001
rewriting: 0.004
SMT solver: 0
selection: 0
success checks: 0
proof
0.04
COL058-3
active equations: 5
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.006
main control loop: 0
rewriting: 0.011
SMT solver: 0
selection: 0.002
success checks: 0.001
proof
0.09
COL059-1
active equations: 68
iterations: 6
memory: 1 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.034
compute CPs: 0.008
main control loop: 0.021
rewriting: 0.008
SMT solver: 0.004
selection: 0.002
success checks: 0.002
 
6.55
COL060-1
active equations: 2
iterations: 1
memory: 46 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 6.542
 
0.00
COL060-2
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL060-3
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
5.57
COL061-1
active equations: 2
iterations: 1
memory: 46 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 5.57
 
0.00
COL061-2
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL061-3
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
 
0.00
COL062-2
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL062-3
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
 
0.00
COL063-2
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL063-3
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
COL063-4
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL063-5
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL063-6
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
 
0.00
COL064-10
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-11
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-2
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-3
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-4
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-5
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-6
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-7
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-8
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL064-9
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
 
 
0.02
COL066-2
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.006
main control loop: 0
rewriting: 0.004
SMT solver: 0
selection: 0.001
success checks: 0.001
proof
0.01
COL066-3
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.13
COL070-1
active equations: 14
iterations: 2
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.036
main control loop: 0.027
rewriting: 0.036
SMT solver: 0
selection: 0.012
success checks: 0.007
proof
0.10
COL075-2
active equations: 25
iterations: 3
memory: 3 MB
restarts: 0
problem shape: carbonio
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.025
main control loop: 0.056
rewriting: 0.028
SMT solver: 0
selection: 0.006
success checks: 0.005
proof
0.00
COL083-1
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL084-1
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL085-1
active equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
COL086-1
active equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
COM010-2
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.001
selection: 0
success checks: 0
proof
0.01
GRP001-2
active equations: 19
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.001
main control loop: 0.003
rewriting: 0.001
SMT solver: 0.001
selection: 0
success checks: 0
proof
0.03
GRP001-4
active equations: 16
iterations: 2
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.007
main control loop: 0.001
rewriting: 0.007
SMT solver: 0
selection: 0
success checks: 0
proof
0.94
GRP002-2
active equations: 83
iterations: 7
memory: 8 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.09
ground joinability: 0
find TRSs: 0.181
compute CPs: 0.04
main control loop: 0.499
rewriting: 0.601
SMT solver: 0.033
selection: 0.004
success checks: 0.02
proof
2.67
GRP002-3
active equations: 95
iterations: 8
memory: 32 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.264
ground joinability: 0
find TRSs: 0.367
compute CPs: 0.168
main control loop: 1.305
rewriting: 1.403
SMT solver: 0.015
selection: 0.022
success checks: 0.122
proof
1.56
GRP002-4
active equations: 47
iterations: 4
memory: 20 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.166
ground joinability: 0
find TRSs: 0.247
compute CPs: 0.174
main control loop: 1.143
rewriting: 0.682
SMT solver: 0.013
selection: 0.03
success checks: 0.062
proof
0.01
GRP010-4
active equations: 12
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP011-4
active equations: 23
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.005
main control loop: 0.005
rewriting: 0.004
SMT solver: 0.002
selection: 0
success checks: 0
proof
0.03
GRP012-4
active equations: 26
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.01
main control loop: 0.007
rewriting: 0.008
SMT solver: 0
selection: 0.001
success checks: 0
proof
17.34
GRP014-1
active equations: 129
iterations: 11
memory: 220 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 0.642
ground joinability: 0
find TRSs: 0.875
compute CPs: 4.669
main control loop: 16.054
rewriting: 5.038
SMT solver: 0.028
selection: 1.014
success checks: 1.278
proof
0.01
GRP022-2
active equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0.002
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
GRP023-2
active equations: 5
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
 
406.45
GRP114-1
active equations: 762
iterations: 31
memory: 1007 MB
restarts: 4
problem shape: ossigeno
time (sec): 
reducibility constraints: 31.682
ground joinability: 0
find TRSs: 34.324
compute CPs: 24.471
main control loop: 283.031
rewriting: 296.017
SMT solver: 0.145
selection: 1.327
success checks: 2.576
proof
0.13
GRP115-1
active equations: 35
iterations: 3
memory: 3 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.04
main control loop: 0.098
rewriting: 0.034
SMT solver: 0
selection: 0.011
success checks: 0.004
proof
0.16
GRP116-1
active equations: 35
iterations: 3
memory: 3 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.044
main control loop: 0.087
rewriting: 0.059
SMT solver: 0
selection: 0.011
success checks: 0.003
proof
0.06
GRP117-1
active equations: 23
iterations: 2
memory: 3 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.017
main control loop: 0.036
rewriting: 0.01
SMT solver: 0
selection: 0.006
success checks: 0.002
proof
0.17
GRP118-1
active equations: 35
iterations: 3
memory: 4 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.04
main control loop: 0.081
rewriting: 0.077
SMT solver: 0
selection: 0.01
success checks: 0.003
proof
26.99
GRP119-1
active equations: 15
iterations: 1
memory: 137 MB
restarts: 2
problem shape: carbonio
time (sec): 
reducibility constraints: 0.62
ground joinability: 0
find TRSs: 0.727
compute CPs: 3.884
main control loop: 25.998
rewriting: 18.953
SMT solver: 0.004
selection: 0.277
success checks: 0.726
proof
42.22
GRP120-1
active equations: 27
iterations: 2
memory: 176 MB
restarts: 2
problem shape: carbonio
time (sec): 
reducibility constraints: 0.643
ground joinability: 0
find TRSs: 0.752
compute CPs: 3.753
main control loop: 41.24
rewriting: 31.907
SMT solver: 0.004
selection: 0.303
success checks: 1.725
proof
26.66
GRP121-1
active equations: 145
iterations: 12
memory: 158 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.459
ground joinability: 0
find TRSs: 0.548
compute CPs: 2.831
main control loop: 17.678
rewriting: 19.389
SMT solver: 0.003
selection: 0.226
success checks: 0.941
proof
15.34
GRP122-1
active equations: 63
iterations: 5
memory: 85 MB
restarts: 2
problem shape: carbonio
time (sec): 
reducibility constraints: 0.669
ground joinability: 0
find TRSs: 0.802
compute CPs: 3.15
main control loop: 14.238
rewriting: 10.158
SMT solver: 0.007
selection: 0.266
success checks: 0.137
proof
0.03
GRP136-1
active equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.005
main control loop: 0
rewriting: 0.007
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.03
GRP137-1
active equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.004
main control loop: 0
rewriting: 0.006
SMT solver: 0
selection: 0.001
success checks: 0
proof
4.50
GRP138-1
active equations: 147
iterations: 6
memory: 70 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.758
ground joinability: 0
find TRSs: 0.955
compute CPs: 0.987
main control loop: 2.912
rewriting: 0.922
SMT solver: 0.024
selection: 0.102
success checks: 0.321
proof
0.02
GRP139-1
active equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.82
GRP140-1
active equations: 137
iterations: 6
memory: 18 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.185
ground joinability: 0
find TRSs: 0.254
compute CPs: 0.142
main control loop: 0.396
rewriting: 0.14
SMT solver: 0.01
selection: 0.017
success checks: 0.071
proof
0.08
GRP141-1
active equations: 43
iterations: 2
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.015
main control loop: 0.027
rewriting: 0.017
SMT solver: 0.002
selection: 0.003
success checks: 0.003
proof
0.01
GRP142-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP143-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
GRP144-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.04
GRP145-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.006
main control loop: 0
rewriting: 0.011
SMT solver: 0
selection: 0.002
success checks: 0
proof
0.02
GRP146-1
active equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
4.87
GRP147-1
active equations: 147
iterations: 6
memory: 70 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.821
ground joinability: 0
find TRSs: 1.029
compute CPs: 1.063
main control loop: 3.15
rewriting: 0.997
SMT solver: 0.027
selection: 0.114
success checks: 0.357
proof
0.96
GRP148-1
active equations: 137
iterations: 6
memory: 18 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.194
ground joinability: 0
find TRSs: 0.275
compute CPs: 0.175
main control loop: 0.489
rewriting: 0.176
SMT solver: 0.013
selection: 0.022
success checks: 0.089
proof
0.08
GRP149-1
active equations: 43
iterations: 2
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.015
main control loop: 0.029
rewriting: 0.018
SMT solver: 0.003
selection: 0.003
success checks: 0.003
proof
0.02
GRP150-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP151-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP152-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP153-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP154-1
active equations: 18
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP155-1
active equations: 18
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.06
GRP156-1
active equations: 41
iterations: 2
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.008
main control loop: 0.018
rewriting: 0.011
SMT solver: 0.002
selection: 0.002
success checks: 0.002
proof
0.02
GRP157-1
active equations: 18
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP158-1
active equations: 18
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.07
GRP159-1
active equations: 42
iterations: 2
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.012
main control loop: 0.025
rewriting: 0.014
SMT solver: 0.001
selection: 0.002
success checks: 0.003
proof
0.01
GRP160-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP161-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.13
GRP162-1
active equations: 66
iterations: 3
memory: 4 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.027
ground joinability: 0
find TRSs: 0.046
compute CPs: 0.018
main control loop: 0.054
rewriting: 0.022
SMT solver: 0.004
selection: 0.004
success checks: 0.005
proof
0.07
GRP163-1
active equations: 43
iterations: 2
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.01
main control loop: 0.022
rewriting: 0.012
SMT solver: 0.001
selection: 0.002
success checks: 0.004
proof
 
 
0.23
GRP165-1
active equations: 66
iterations: 3
memory: 6 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.03
ground joinability: 0
find TRSs: 0.049
compute CPs: 0.047
main control loop: 0.077
rewriting: 0.064
SMT solver: 0.002
selection: 0.008
success checks: 0.008
proof
0.71
GRP165-2
active equations: 113
iterations: 5
memory: 17 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.119
ground joinability: 0
find TRSs: 0.17
compute CPs: 0.141
main control loop: 0.269
rewriting: 0.147
SMT solver: 0.006
selection: 0.021
success checks: 0.038
proof
5.17
GRP166-1
active equations: 102
iterations: 4
memory: 46 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.682
ground joinability: 0
find TRSs: 0.873
compute CPs: 0.399
main control loop: 3.891
rewriting: 1.95
SMT solver: 0.028
selection: 0.061
success checks: 0.276
proof
7.10
GRP166-2
active equations: 31
iterations: 1
memory: 46 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.591
ground joinability: 0
find TRSs: 0.762
compute CPs: 0.813
main control loop: 5.939
rewriting: 3.572
SMT solver: 0.019
selection: 0.063
success checks: 0.273
proof
0.79
GRP166-3
active equations: 138
iterations: 6
memory: 17 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.162
ground joinability: 0
find TRSs: 0.22
compute CPs: 0.117
main control loop: 0.428
rewriting: 0.16
SMT solver: 0.008
selection: 0.017
success checks: 0.08
proof
0.90
GRP166-4
active equations: 136
iterations: 6
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.176
ground joinability: 0
find TRSs: 0.244
compute CPs: 0.155
main control loop: 0.371
rewriting: 0.169
SMT solver: 0.01
selection: 0.025
success checks: 0.053
proof
99.82
GRP167-1
active equations: 633
iterations: 26
memory: 761 MB
restarts: 2
problem shape: ossigeno
time (sec): 
reducibility constraints: 21.678
ground joinability: 0
find TRSs: 24.222
compute CPs: 9.935
main control loop: 64.913
rewriting: 31.367
SMT solver: 0.332
selection: 1.506
success checks: 4.45
proof
133.24
GRP167-2
active equations: 708
iterations: 29
memory: 876 MB
restarts: 2
problem shape: ossigeno
time (sec): 
reducibility constraints: 31.338
ground joinability: 0
find TRSs: 34.656
compute CPs: 15.868
main control loop: 89.477
rewriting: 45.484
SMT solver: 0.425
selection: 1.792
success checks: 5.015
proof
 
 
0.36
GRP167-5
active equations: 93
iterations: 4
memory: 7 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.067
ground joinability: 0
find TRSs: 0.108
compute CPs: 0.064
main control loop: 0.177
rewriting: 0.087
SMT solver: 0.011
selection: 0.012
success checks: 0.021
proof
0.02
GRP168-1
active equations: 18
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP168-2
active equations: 18
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
2.31
GRP169-1
active equations: 184
iterations: 8
memory: 40 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.462
ground joinability: 0
find TRSs: 0.589
compute CPs: 0.355
main control loop: 1.075
rewriting: 0.532
SMT solver: 0.016
selection: 0.043
success checks: 0.183
proof
3.18
GRP169-2
active equations: 209
iterations: 9
memory: 61 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.604
ground joinability: 0
find TRSs: 0.742
compute CPs: 0.291
main control loop: 1.994
rewriting: 0.631
SMT solver: 0.019
selection: 0.066
success checks: 0.368
proof
5.50
GRP170-1
active equations: 221
iterations: 9
memory: 70 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 1.304
ground joinability: 0
find TRSs: 1.585
compute CPs: 0.676
main control loop: 2.815
rewriting: 0.949
SMT solver: 0.049
selection: 0.089
success checks: 0.462
proof
2.42
GRP170-2
active equations: 210
iterations: 9
memory: 46 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.529
ground joinability: 0
find TRSs: 0.691
compute CPs: 0.321
main control loop: 1.257
rewriting: 0.463
SMT solver: 0.023
selection: 0.051
success checks: 0.162
proof
6.78
GRP170-3
active equations: 222
iterations: 9
memory: 93 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 1.379
ground joinability: 0
find TRSs: 1.674
compute CPs: 1.292
main control loop: 3.878
rewriting: 1.349
SMT solver: 0.044
selection: 0.125
success checks: 0.457
proof
187.30
GRP170-4
active equations: 848
iterations: 35
memory: 1332 MB
restarts: 2
problem shape: ossigeno
time (sec): 
reducibility constraints: 53.973
ground joinability: 0
find TRSs: 58.893
compute CPs: 29.739
main control loop: 100.248
rewriting: 30.3
SMT solver: 0.541
selection: 1.888
success checks: 14.532
 
0.78
GRP171-1
active equations: 138
iterations: 6
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.121
ground joinability: 0
find TRSs: 0.167
compute CPs: 0.106
main control loop: 0.312
rewriting: 0.194
SMT solver: 0.006
selection: 0.016
success checks: 0.067
proof
0.56
GRP171-2
active equations: 113
iterations: 5
memory: 9 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.155
ground joinability: 0
find TRSs: 0.204
compute CPs: 0.091
main control loop: 0.243
rewriting: 0.092
SMT solver: 0.006
selection: 0.013
success checks: 0.042
proof
0.55
GRP172-1
active equations: 114
iterations: 5
memory: 11 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.106
ground joinability: 0
find TRSs: 0.156
compute CPs: 0.074
main control loop: 0.26
rewriting: 0.123
SMT solver: 0.006
selection: 0.012
success checks: 0.032
proof
1.10
GRP172-2
active equations: 137
iterations: 6
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.179
ground joinability: 0
find TRSs: 0.25
compute CPs: 0.178
main control loop: 0.476
rewriting: 0.245
SMT solver: 0.009
selection: 0.026
success checks: 0.122
proof
0.51
GRP173-1
active equations: 114
iterations: 5
memory: 9 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.122
ground joinability: 0
find TRSs: 0.177
compute CPs: 0.087
main control loop: 0.237
rewriting: 0.084
SMT solver: 0.007
selection: 0.012
success checks: 0.03
proof
0.51
GRP174-1
active equations: 113
iterations: 5
memory: 9 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.116
ground joinability: 0
find TRSs: 0.164
compute CPs: 0.088
main control loop: 0.247
rewriting: 0.087
SMT solver: 0.005
selection: 0.012
success checks: 0.022
proof
0.69
GRP175-1
active equations: 113
iterations: 5
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.094
ground joinability: 0
find TRSs: 0.137
compute CPs: 0.127
main control loop: 0.248
rewriting: 0.164
SMT solver: 0.007
selection: 0.017
success checks: 0.039
proof
0.87
GRP175-2
active equations: 138
iterations: 6
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.169
ground joinability: 0
find TRSs: 0.243
compute CPs: 0.111
main control loop: 0.472
rewriting: 0.16
SMT solver: 0.011
selection: 0.019
success checks: 0.108
proof
0.94
GRP175-3
active equations: 137
iterations: 6
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.191
ground joinability: 0
find TRSs: 0.253
compute CPs: 0.187
main control loop: 0.456
rewriting: 0.192
SMT solver: 0.01
selection: 0.022
success checks: 0.059
proof
1.18
GRP175-4
active equations: 114
iterations: 5
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.101
ground joinability: 0
find TRSs: 0.141
compute CPs: 0.097
main control loop: 0.331
rewriting: 0.424
SMT solver: 0.007
selection: 0.024
success checks: 0.13
proof
0.02
GRP176-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP176-2
active equations: 18
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0.001
selection: 0
success checks: 0
proof
3.19
GRP177-2
active equations: 56
iterations: 2
memory: 46 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.543
ground joinability: 0
find TRSs: 0.711
compute CPs: 1.061
main control loop: 2.05
rewriting: 0.432
SMT solver: 0.023
selection: 0.055
success checks: 0.233
proof
4.00
GRP178-1
active equations: 153
iterations: 6
memory: 61 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.838
ground joinability: 0
find TRSs: 1.083
compute CPs: 0.697
main control loop: 1.746
rewriting: 0.601
SMT solver: 0.032
selection: 0.061
success checks: 0.307
proof
5.57
GRP178-2
active equations: 129
iterations: 5
memory: 107 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.811
ground joinability: 0
find TRSs: 1.034
compute CPs: 0.61
main control loop: 3.86
rewriting: 1.273
SMT solver: 0.031
selection: 0.109
success checks: 0.804
proof
 
 
 
 
 
 
 
 
 
0.04
GRP182-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.006
main control loop: 0
rewriting: 0.009
SMT solver: 0
selection: 0.002
success checks: 0
proof
0.04
GRP182-2
active equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.007
main control loop: 0
rewriting: 0.011
SMT solver: 0
selection: 0.002
success checks: 0
proof
0.04
GRP182-3
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.006
main control loop: 0
rewriting: 0.009
SMT solver: 0
selection: 0.002
success checks: 0
proof
0.04
GRP182-4
active equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.007
main control loop: 0
rewriting: 0.011
SMT solver: 0
selection: 0.002
success checks: 0
proof
 
530.29
GRP183-2
active equations: 777
iterations: 32
memory: 2556 MB
restarts: 2
problem shape: ossigeno
time (sec): 
reducibility constraints: 48.331
ground joinability: 0
find TRSs: 52.088
compute CPs: 232.058
main control loop: 433.988
rewriting: 106.822
SMT solver: 0.162
selection: 6.62
success checks: 32.174
 
 
 
2.91
GRP184-1
active equations: 183
iterations: 8
memory: 61 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.426
ground joinability: 0
find TRSs: 0.537
compute CPs: 0.384
main control loop: 1.66
rewriting: 0.621
SMT solver: 0.009
selection: 0.071
success checks: 0.293
proof
80.92
GRP184-2
active equations: 465
iterations: 19
memory: 662 MB
restarts: 2
problem shape: ossigeno
time (sec): 
reducibility constraints: 11.756
ground joinability: 0
find TRSs: 13.107
compute CPs: 21.705
main control loop: 55.076
rewriting: 20.798
SMT solver: 0.086
selection: 1.566
success checks: 4.209
proof
3.05
GRP184-3
active equations: 183
iterations: 8
memory: 61 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.45
ground joinability: 0
find TRSs: 0.572
compute CPs: 0.408
main control loop: 1.75
rewriting: 0.669
SMT solver: 0.011
selection: 0.075
success checks: 0.276
proof
1.38
GRP184-4
active equations: 140
iterations: 6
memory: 20 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.226
ground joinability: 0
find TRSs: 0.315
compute CPs: 0.124
main control loop: 0.788
rewriting: 0.469
SMT solver: 0.024
selection: 0.02
success checks: 0.07
proof
4.16
GRP185-1
active equations: 29
iterations: 1
memory: 70 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.588
ground joinability: 0
find TRSs: 0.71
compute CPs: 0.576
main control loop: 3.085
rewriting: 1.207
SMT solver: 0.014
selection: 0.09
success checks: 0.491
proof
7.82
GRP185-2
active equations: 32
iterations: 1
memory: 81 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.738
ground joinability: 0
find TRSs: 0.903
compute CPs: 0.801
main control loop: 6.272
rewriting: 2.972
SMT solver: 0.017
selection: 0.133
success checks: 0.467
proof
6.58
GRP185-3
active equations: 77
iterations: 3
memory: 81 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.744
ground joinability: 0
find TRSs: 0.915
compute CPs: 0.793
main control loop: 4.985
rewriting: 1.919
SMT solver: 0.018
selection: 0.119
success checks: 0.568
proof
35.64
GRP185-4
active equations: 318
iterations: 13
memory: 286 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 4.204
ground joinability: 0
find TRSs: 4.635
compute CPs: 2.944
main control loop: 27.362
rewriting: 14.9
SMT solver: 0.036
selection: 0.393
success checks: 1.883
proof
 
 
0.21
GRP186-3
active equations: 65
iterations: 3
memory: 5 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.031
ground joinability: 0
find TRSs: 0.048
compute CPs: 0.041
main control loop: 0.108
rewriting: 0.048
SMT solver: 0.003
selection: 0.006
success checks: 0.016
proof
0.12
GRP186-4
active equations: 44
iterations: 2
memory: 4 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.025
main control loop: 0.017
rewriting: 0.034
SMT solver: 0.001
selection: 0.005
success checks: 0.005
proof
 
0.02
GRP188-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.002
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP188-2
active equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.002
main control loop: 0
rewriting: 0.003
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP189-1
active equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP189-2
active equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.006
main control loop: 0
rewriting: 0.009
SMT solver: 0
selection: 0.001
success checks: 0
proof
2.07
GRP190-1
active equations: 186
iterations: 8
memory: 40 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.482
ground joinability: 0
find TRSs: 0.626
compute CPs: 0.251
main control loop: 1.082
rewriting: 0.396
SMT solver: 0.022
selection: 0.038
success checks: 0.134
proof
1.78
GRP190-2
active equations: 186
iterations: 8
memory: 40 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.424
ground joinability: 0
find TRSs: 0.554
compute CPs: 0.23
main control loop: 0.911
rewriting: 0.292
SMT solver: 0.02
selection: 0.036
success checks: 0.235
proof
2.57
GRP191-1
active equations: 99
iterations: 4
memory: 70 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.391
ground joinability: 0
find TRSs: 0.511
compute CPs: 0.378
main control loop: 1.609
rewriting: 0.645
SMT solver: 0.016
selection: 0.056
success checks: 0.144
proof
4.58
GRP191-2
active equations: 122
iterations: 5
memory: 81 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.693
ground joinability: 0
find TRSs: 0.878
compute CPs: 0.621
main control loop: 3.083
rewriting: 1.197
SMT solver: 0.023
selection: 0.11
success checks: 0.52
proof
0.11
GRP192-1
active equations: 66
iterations: 3
memory: 3 MB
restarts: 0
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.025
ground joinability: 0
find TRSs: 0.039
compute CPs: 0.015
main control loop: 0.056
rewriting: 0.019
SMT solver: 0.002
selection: 0.003
success checks: 0.007
proof
3.67
GRP193-1
active equations: 130
iterations: 5
memory: 61 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 0.687
ground joinability: 0
find TRSs: 0.893
compute CPs: 0.518
main control loop: 2.079
rewriting: 0.642
SMT solver: 0.036
selection: 0.061
success checks: 0.411
proof
8.41
GRP193-2
active equations: 225
iterations: 9
memory: 123 MB
restarts: 1
problem shape: ossigeno
time (sec): 
reducibility constraints: 1.29
ground joinability: 0
find TRSs: 1.608
compute CPs: 1.469
main control loop: 5.709
rewriting: 1.855
SMT solver: 0.039
selection: 0.164
success checks: 1.046
proof
0.01
GRP195-1
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0.001
proof
 
proof
proof
119.88
GRP202-1
active equations: 601
iterations: 30
memory: 417 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 18.978
ground joinability: 0
find TRSs: 20.592
compute CPs: 2.772
main control loop: 88.272
rewriting: 54.994
SMT solver: 0.216
selection: 0.692
success checks: 1.424
proof
21.22
GRP203-1
active equations: 203
iterations: 17
memory: 170 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 1.547
ground joinability: 0
find TRSs: 1.846
compute CPs: 5.373
main control loop: 17.797
rewriting: 10.691
SMT solver: 0.021
selection: 0.487
success checks: 0.163
proof
230.69
GRP205-1
active equations: 601
iterations: 30
memory: 325 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 30.758
ground joinability: 0
find TRSs: 33.305
compute CPs: 4.587
main control loop: 173.892
rewriting: 118.54
SMT solver: 0.3
selection: 1.166
success checks: 2.164
proof
0.04
GRP206-1
active equations: 29
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.008
main control loop: 0.003
rewriting: 0.006
SMT solver: 0.004
selection: 0.002
success checks: 0.001
proof
4.79
GRP403-1
active equations: 45
iterations: 5
memory: 45 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.021
ground joinability: 0
find TRSs: 0.036
compute CPs: 1.427
main control loop: 2.606
rewriting: 1.878
SMT solver: 0.001
selection: 0.464
success checks: 0.203
proof
proof
proof
11.56
GRP406-1
active equations: 57
iterations: 6
memory: 78 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.06
compute CPs: 3.457
main control loop: 6.507
rewriting: 4.915
SMT solver: 0.001
selection: 0.92
success checks: 0.243
proof
29.17
GRP407-1
active equations: 93
iterations: 9
memory: 210 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.155
ground joinability: 0
find TRSs: 0.207
compute CPs: 8.176
main control loop: 28.741
rewriting: 11.536
SMT solver: 0.003
selection: 1.597
success checks: 3.045
proof
26.43
GRP408-1
active equations: 43
iterations: 4
memory: 200 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.147
ground joinability: 0
find TRSs: 0.207
compute CPs: 7.556
main control loop: 26.159
rewriting: 10.754
SMT solver: 0.005
selection: 1.65
success checks: 0.556
proof
1.63
GRP409-1
active equations: 46
iterations: 5
memory: 20 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.038
compute CPs: 0.593
main control loop: 1.158
rewriting: 0.513
SMT solver: 0.001
selection: 0.174
success checks: 0.056
proof
3.95
GRP410-1
active equations: 70
iterations: 7
memory: 59 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.068
ground joinability: 0
find TRSs: 0.1
compute CPs: 1.03
main control loop: 3.743
rewriting: 1.153
SMT solver: 0.002
selection: 0.382
success checks: 0.249
proof
4.31
GRP411-1
active equations: 55
iterations: 5
memory: 61 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.172
ground joinability: 0
find TRSs: 0.237
compute CPs: 1.222
main control loop: 3.995
rewriting: 1.222
SMT solver: 0.005
selection: 0.38
success checks: 0.236
proof
3.49
GRP412-1
active equations: 57
iterations: 6
memory: 43 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.041
ground joinability: 0
find TRSs: 0.065
compute CPs: 1.064
main control loop: 2.587
rewriting: 1.235
SMT solver: 0.001
selection: 0.356
success checks: 0.204
proof
13.23
GRP413-1
active equations: 103
iterations: 9
memory: 200 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.252
ground joinability: 0
find TRSs: 0.342
compute CPs: 3.706
main control loop: 12.726
rewriting: 4.126
SMT solver: 0.006
selection: 0.643
success checks: 1.388
proof
12.10
GRP414-1
active equations: 88
iterations: 8
memory: 200 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 0.556
ground joinability: 0
find TRSs: 0.722
compute CPs: 3.822
main control loop: 11.21
rewriting: 2.746
SMT solver: 0.012
selection: 0.634
success checks: 1.961
proof
9.24
GRP415-1
active equations: 58
iterations: 6
memory: 80 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.031
ground joinability: 0
find TRSs: 0.054
compute CPs: 3.656
main control loop: 7.21
rewriting: 3.225
SMT solver: 0.001
selection: 0.744
success checks: 0.173
proof
31.32
GRP416-1
active equations: 56
iterations: 5
memory: 275 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.122
ground joinability: 0
find TRSs: 0.186
compute CPs: 9.528
main control loop: 30.174
rewriting: 11.857
SMT solver: 0.004
selection: 2.147
success checks: 1.406
proof
30.58
GRP417-1
active equations: 140
iterations: 12
memory: 269 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.376
ground joinability: 0
find TRSs: 0.501
compute CPs: 9.339
main control loop: 29.816
rewriting: 10.937
SMT solver: 0.01
selection: 2.153
success checks: 1.408
proof
16.60
GRP418-1
active equations: 69
iterations: 7
memory: 166 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.06
ground joinability: 0
find TRSs: 0.089
compute CPs: 6.467
main control loop: 11.608
rewriting: 4.984
SMT solver: 0.002
selection: 1.334
success checks: 0.485
proof
proof
proof
5.61
GRP421-1
active equations: 58
iterations: 6
memory: 70 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.04
ground joinability: 0
find TRSs: 0.062
compute CPs: 1.914
main control loop: 4.485
rewriting: 1.798
SMT solver: 0.001
selection: 0.462
success checks: 0.217
proof
proof
proof
1.73
GRP424-1
active equations: 34
iterations: 4
memory: 23 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.024
compute CPs: 0.575
main control loop: 0.836
rewriting: 0.709
SMT solver: 0.001
selection: 0.161
success checks: 0.06
proof
4.28
GRP425-1
active equations: 58
iterations: 6
memory: 31 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.03
ground joinability: 0
find TRSs: 0.053
compute CPs: 1.222
main control loop: 3.346
rewriting: 1.879
SMT solver: 0.001
selection: 0.355
success checks: 0.111
proof
4.47
GRP426-1
active equations: 67
iterations: 6
memory: 44 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.154
ground joinability: 0
find TRSs: 0.231
compute CPs: 1.228
main control loop: 4.167
rewriting: 1.796
SMT solver: 0.005
selection: 0.346
success checks: 0.147
proof
14.10
GRP427-1
active equations: 115
iterations: 10
memory: 201 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.281
ground joinability: 0
find TRSs: 0.388
compute CPs: 4.231
main control loop: 13.617
rewriting: 3.96
SMT solver: 0.008
selection: 0.904
success checks: 2.042
proof
13.65
GRP428-1
active equations: 115
iterations: 10
memory: 188 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.261
ground joinability: 0
find TRSs: 0.367
compute CPs: 3.691
main control loop: 13.178
rewriting: 4.159
SMT solver: 0.009
selection: 0.955
success checks: 2.099
proof
17.32
GRP429-1
active equations: 129
iterations: 11
memory: 220 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 0.625
ground joinability: 0
find TRSs: 0.856
compute CPs: 4.824
main control loop: 16.063
rewriting: 4.874
SMT solver: 0.029
selection: 1.049
success checks: 1.284
proof
0.93
GRP430-1
active equations: 70
iterations: 7
memory: 15 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.048
ground joinability: 0
find TRSs: 0.08
compute CPs: 0.343
main control loop: 0.795
rewriting: 0.225
SMT solver: 0.003
selection: 0.084
success checks: 0.054
proof
0.91
GRP431-1
active equations: 70
iterations: 7
memory: 15 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.045
ground joinability: 0
find TRSs: 0.074
compute CPs: 0.309
main control loop: 0.774
rewriting: 0.242
SMT solver: 0.002
selection: 0.079
success checks: 0.063
proof
0.72
GRP432-1
active equations: 94
iterations: 9
memory: 13 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.062
ground joinability: 0
find TRSs: 0.098
compute CPs: 0.262
main control loop: 0.596
rewriting: 0.168
SMT solver: 0.003
selection: 0.063
success checks: 0.035
proof
22.25
GRP433-1
active equations: 81
iterations: 8
memory: 134 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.06
ground joinability: 0
find TRSs: 0.092
compute CPs: 8.13
main control loop: 22.107
rewriting: 6.339
SMT solver: 0.002
selection: 0.937
success checks: 0.552
proof
14.14
GRP434-1
active equations: 81
iterations: 8
memory: 116 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.046
ground joinability: 0
find TRSs: 0.071
compute CPs: 5.194
main control loop: 14.002
rewriting: 4.068
SMT solver: 0.001
selection: 0.705
success checks: 0.357
proof
21.28
GRP435-1
active equations: 40
iterations: 4
memory: 134 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.101
ground joinability: 0
find TRSs: 0.155
compute CPs: 8.005
main control loop: 21.037
rewriting: 6.352
SMT solver: 0.004
selection: 0.935
success checks: 0.575
proof
21.29
GRP436-1
active equations: 7
iterations: 1
memory: 230 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.103
ground joinability: 0
find TRSs: 0.161
compute CPs: 7.275
main control loop: 21.073
rewriting: 7.809
SMT solver: 0.003
selection: 1.758
success checks: 0.794
proof
14.22
GRP437-1
active equations: 7
iterations: 1
memory: 218 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.062
ground joinability: 0
find TRSs: 0.101
compute CPs: 5.242
main control loop: 14.084
rewriting: 4.818
SMT solver: 0.002
selection: 1.231
success checks: 0.478
proof
19.98
GRP438-1
active equations: 55
iterations: 5
memory: 216 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.112
ground joinability: 0
find TRSs: 0.179
compute CPs: 7.167
main control loop: 19.648
rewriting: 6.954
SMT solver: 0.005
selection: 1.676
success checks: 0.67
proof
23.81
GRP439-1
active equations: 69
iterations: 7
memory: 123 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.04
ground joinability: 0
find TRSs: 0.068
compute CPs: 8.399
main control loop: 17.93
rewriting: 10.146
SMT solver: 0.001
selection: 1.205
success checks: 0.073
proof
42.43
GRP440-1
active equations: 81
iterations: 8
memory: 140 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.072
ground joinability: 0
find TRSs: 0.114
compute CPs: 14.288
main control loop: 31.583
rewriting: 19.167
SMT solver: 0.002
selection: 1.794
success checks: 0.145
proof
46.85
GRP441-1
active equations: 55
iterations: 5
memory: 216 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.139
ground joinability: 0
find TRSs: 0.209
compute CPs: 15.923
main control loop: 46.595
rewriting: 20.878
SMT solver: 0.005
selection: 2.079
success checks: 0.19
proof
20.96
GRP442-1
active equations: 93
iterations: 9
memory: 210 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.076
ground joinability: 0
find TRSs: 0.12
compute CPs: 7.616
main control loop: 20.526
rewriting: 6.582
SMT solver: 0.003
selection: 1.402
success checks: 0.6
proof
20.99
GRP443-1
active equations: 93
iterations: 9
memory: 228 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.089
ground joinability: 0
find TRSs: 0.135
compute CPs: 8.181
main control loop: 20.494
rewriting: 6.302
SMT solver: 0.003
selection: 1.276
success checks: 0.56
proof
21.39
GRP444-1
active equations: 87
iterations: 8
memory: 225 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.163
ground joinability: 0
find TRSs: 0.235
compute CPs: 8.367
main control loop: 21.1
rewriting: 6.215
SMT solver: 0.007
selection: 1.331
success checks: 0.613
proof
0.05
GRP445-1
active equations: 24
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.014
main control loop: 0.014
rewriting: 0.01
SMT solver: 0.001
selection: 0.002
success checks: 0.001
proof
0.13
GRP446-1
active equations: 48
iterations: 5
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.027
compute CPs: 0.031
main control loop: 0.088
rewriting: 0.023
SMT solver: 0.002
selection: 0.004
success checks: 0.016
proof
0.48
GRP447-1
active equations: 72
iterations: 7
memory: 9 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.038
ground joinability: 0
find TRSs: 0.07
compute CPs: 0.059
main control loop: 0.284
rewriting: 0.125
SMT solver: 0.005
selection: 0.01
success checks: 0.026
proof
0.05
GRP448-1
active equations: 24
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.008
compute CPs: 0.013
main control loop: 0.013
rewriting: 0.009
SMT solver: 0.001
selection: 0.002
success checks: 0.001
proof
0.14
GRP449-1
active equations: 48
iterations: 5
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.029
compute CPs: 0.029
main control loop: 0.094
rewriting: 0.026
SMT solver: 0.003
selection: 0.003
success checks: 0.017
proof
0.53
GRP450-1
active equations: 72
iterations: 7
memory: 9 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.071
compute CPs: 0.064
main control loop: 0.294
rewriting: 0.136
SMT solver: 0.006
selection: 0.011
success checks: 0.028
proof
0.08
GRP451-1
active equations: 36
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.023
main control loop: 0.039
rewriting: 0.014
SMT solver: 0.002
selection: 0.004
success checks: 0.002
proof
0.68
GRP452-1
active equations: 72
iterations: 7
memory: 15 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.042
ground joinability: 0
find TRSs: 0.074
compute CPs: 0.162
main control loop: 0.407
rewriting: 0.116
SMT solver: 0.005
selection: 0.016
success checks: 0.088
proof
1.91
GRP453-1
active equations: 90
iterations: 8
memory: 35 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.163
ground joinability: 0
find TRSs: 0.25
compute CPs: 0.279
main control loop: 1.525
rewriting: 0.527
SMT solver: 0.013
selection: 0.027
success checks: 0.247
proof
0.00
GRP454-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.07
GRP455-1
active equations: 53
iterations: 4
memory: 1 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.018
ground joinability: 0
find TRSs: 0.035
compute CPs: 0.008
main control loop: 0.021
rewriting: 0.016
SMT solver: 0.001
selection: 0.001
success checks: 0
proof
0.30
GRP456-1
active equations: 113
iterations: 7
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.12
ground joinability: 0
find TRSs: 0.185
compute CPs: 0.031
main control loop: 0.076
rewriting: 0.027
SMT solver: 0.01
selection: 0.004
success checks: 0.007
proof
0.00
GRP457-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.07
GRP458-1
active equations: 39
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.013
main control loop: 0.033
rewriting: 0.015
SMT solver: 0.001
selection: 0.003
success checks: 0.002
proof
0.24
GRP459-1
active equations: 61
iterations: 5
memory: 6 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.029
ground joinability: 0
find TRSs: 0.052
compute CPs: 0.064
main control loop: 0.065
rewriting: 0.067
SMT solver: 0.004
selection: 0.011
success checks: 0.007
proof
0.00
GRP460-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.06
GRP461-1
active equations: 57
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.017
ground joinability: 0
find TRSs: 0.036
compute CPs: 0.004
main control loop: 0.013
rewriting: 0.006
SMT solver: 0.002
selection: 0
success checks: 0.001
proof
0.31
GRP462-1
active equations: 117
iterations: 7
memory: 6 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.111
ground joinability: 0
find TRSs: 0.17
compute CPs: 0.038
main control loop: 0.086
rewriting: 0.036
SMT solver: 0.011
selection: 0.004
success checks: 0.01
proof
0.00
GRP463-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP464-1
active equations: 45
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.002
main control loop: 0.004
rewriting: 0.004
SMT solver: 0.001
selection: 0
success checks: 0
proof
0.41
GRP465-1
active equations: 127
iterations: 8
memory: 7 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.157
ground joinability: 0
find TRSs: 0.229
compute CPs: 0.038
main control loop: 0.133
rewriting: 0.069
SMT solver: 0.011
selection: 0.005
success checks: 0.013
proof
0.05
GRP466-1
active equations: 19
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.012
main control loop: 0.007
rewriting: 0.011
SMT solver: 0.001
selection: 0.002
success checks: 0
proof
3.94
GRP467-1
active equations: 67
iterations: 7
memory: 61 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.064
compute CPs: 0.873
main control loop: 2.274
rewriting: 1.307
SMT solver: 0.003
selection: 0.127
success checks: 0.208
proof
3.63
GRP468-1
active equations: 79
iterations: 7
memory: 61 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.136
ground joinability: 0
find TRSs: 0.2
compute CPs: 0.867
main control loop: 3.137
rewriting: 0.878
SMT solver: 0.01
selection: 0.131
success checks: 0.437
proof
3.72
GRP469-1
active equations: 56
iterations: 5
memory: 40 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.123
ground joinability: 0
find TRSs: 0.203
compute CPs: 0.89
main control loop: 3.458
rewriting: 1.491
SMT solver: 0.008
selection: 0.207
success checks: 0.048
proof
4.46
GRP470-1
active equations: 56
iterations: 5
memory: 43 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.121
ground joinability: 0
find TRSs: 0.2
compute CPs: 0.846
main control loop: 4.209
rewriting: 2.123
SMT solver: 0.008
selection: 0.225
success checks: 0.055
proof
12.36
GRP471-1
active equations: 93
iterations: 8
memory: 107 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 0.535
ground joinability: 0
find TRSs: 0.75
compute CPs: 1.562
main control loop: 11.29
rewriting: 5.274
SMT solver: 0.029
selection: 0.252
success checks: 1.599
proof
7.97
GRP472-1
active equations: 20
iterations: 2
memory: 93 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.087
ground joinability: 0
find TRSs: 0.146
compute CPs: 1.773
main control loop: 7.768
rewriting: 3.178
SMT solver: 0.006
selection: 0.497
success checks: 0.257
proof
9.34
GRP473-1
active equations: 8
iterations: 1
memory: 93 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.088
ground joinability: 0
find TRSs: 0.145
compute CPs: 1.571
main control loop: 9.134
rewriting: 4.441
SMT solver: 0.005
selection: 0.513
success checks: 0.305
proof
11.37
GRP474-1
active equations: 140
iterations: 12
memory: 130 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.325
ground joinability: 0
find TRSs: 0.457
compute CPs: 1.858
main control loop: 9.116
rewriting: 4.947
SMT solver: 0.016
selection: 0.519
success checks: 0.925
proof
2.18
GRP475-1
active equations: 71
iterations: 7
memory: 35 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.037
ground joinability: 0
find TRSs: 0.064
compute CPs: 0.524
main control loop: 1.538
rewriting: 0.856
SMT solver: 0.002
selection: 0.118
success checks: 0.062
proof
2.61
GRP476-1
active equations: 83
iterations: 8
memory: 34 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.061
ground joinability: 0
find TRSs: 0.101
compute CPs: 0.605
main control loop: 2.2
rewriting: 1.123
SMT solver: 0.003
selection: 0.123
success checks: 0.073
proof
8.02
GRP477-1
active equations: 140
iterations: 12
memory: 73 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.355
ground joinability: 0
find TRSs: 0.488
compute CPs: 1.106
main control loop: 5.267
rewriting: 3.36
SMT solver: 0.016
selection: 0.156
success checks: 0.928
proof
1.38
GRP478-1
active equations: 70
iterations: 7
memory: 35 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.069
compute CPs: 0.362
main control loop: 1.224
rewriting: 0.389
SMT solver: 0.003
selection: 0.076
success checks: 0.118
proof
1.72
GRP479-1
active equations: 82
iterations: 8
memory: 35 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.067
ground joinability: 0
find TRSs: 0.11
compute CPs: 0.391
main control loop: 1.534
rewriting: 0.549
SMT solver: 0.004
selection: 0.095
success checks: 0.175
proof
1.82
GRP480-1
active equations: 94
iterations: 9
memory: 32 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.1
ground joinability: 0
find TRSs: 0.156
compute CPs: 0.378
main control loop: 1.583
rewriting: 0.408
SMT solver: 0.007
selection: 0.101
success checks: 0.246
proof
0.13
GRP481-1
active equations: 79
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.047
ground joinability: 0
find TRSs: 0.081
compute CPs: 0.007
main control loop: 0.033
rewriting: 0.015
SMT solver: 0.005
selection: 0.003
success checks: 0.002
proof
0.08
GRP482-1
active equations: 79
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.025
ground joinability: 0
find TRSs: 0.046
compute CPs: 0.008
main control loop: 0.019
rewriting: 0.011
SMT solver: 0.004
selection: 0.002
success checks: 0
proof
0.50
GRP483-1
active equations: 121
iterations: 7
memory: 8 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.145
ground joinability: 0
find TRSs: 0.223
compute CPs: 0.069
main control loop: 0.212
rewriting: 0.089
SMT solver: 0.012
selection: 0.016
success checks: 0.019
proof
0.05
GRP484-1
active equations: 35
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.008
main control loop: 0.003
rewriting: 0.009
SMT solver: 0.002
selection: 0.002
success checks: 0
proof
0.10
GRP485-1
active equations: 55
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.02
ground joinability: 0
find TRSs: 0.04
compute CPs: 0.014
main control loop: 0.028
rewriting: 0.017
SMT solver: 0.002
selection: 0.004
success checks: 0.001
proof
0.53
GRP486-1
active equations: 135
iterations: 8
memory: 8 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.191
ground joinability: 0
find TRSs: 0.28
compute CPs: 0.066
main control loop: 0.196
rewriting: 0.085
SMT solver: 0.014
selection: 0.013
success checks: 0.013
proof
0.33
GRP487-1
active equations: 110
iterations: 7
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.119
ground joinability: 0
find TRSs: 0.188
compute CPs: 0.028
main control loop: 0.094
rewriting: 0.041
SMT solver: 0.011
selection: 0.009
success checks: 0.003
proof
2.23
GRP488-1
active equations: 144
iterations: 8
memory: 20 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.531
ground joinability: 0
find TRSs: 0.689
compute CPs: 0.085
main control loop: 1.033
rewriting: 0.918
SMT solver: 0.018
selection: 0.039
success checks: 0.111
proof
2.82
GRP489-1
active equations: 126
iterations: 7
memory: 26 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.412
ground joinability: 0
find TRSs: 0.56
compute CPs: 0.115
main control loop: 1.331
rewriting: 1.088
SMT solver: 0.025
selection: 0.031
success checks: 0.647
proof
0.17
GRP490-1
active equations: 75
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.047
ground joinability: 0
find TRSs: 0.088
compute CPs: 0.018
main control loop: 0.039
rewriting: 0.025
SMT solver: 0.007
selection: 0.006
success checks: 0.001
proof
0.14
GRP491-1
active equations: 75
iterations: 5
memory: 1 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.049
ground joinability: 0
find TRSs: 0.086
compute CPs: 0.009
main control loop: 0.033
rewriting: 0.014
SMT solver: 0.005
selection: 0.003
success checks: 0.002
proof
1.08
GRP492-1
active equations: 125
iterations: 7
memory: 15 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.44
ground joinability: 0
find TRSs: 0.593
compute CPs: 0.113
main control loop: 0.275
rewriting: 0.16
SMT solver: 0.026
selection: 0.017
success checks: 0.021
proof
0.12
GRP493-1
active equations: 31
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.036
main control loop: 0.009
rewriting: 0.033
SMT solver: 0.001
selection: 0.007
success checks: 0
proof
0.14
GRP494-1
active equations: 71
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.036
ground joinability: 0
find TRSs: 0.066
compute CPs: 0.019
main control loop: 0.05
rewriting: 0.022
SMT solver: 0.004
selection: 0.004
success checks: 0.001
proof
1.54
GRP495-1
active equations: 114
iterations: 7
memory: 20 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.439
ground joinability: 0
find TRSs: 0.592
compute CPs: 0.078
main control loop: 0.826
rewriting: 0.451
SMT solver: 0.025
selection: 0.016
success checks: 0.099
proof
0.03
GRP496-1
active equations: 32
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.001
main control loop: 0.001
rewriting: 0.002
SMT solver: 0.001
selection: 0
success checks: 0
proof
0.12
GRP497-1
active equations: 75
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.045
ground joinability: 0
find TRSs: 0.079
compute CPs: 0.007
main control loop: 0.026
rewriting: 0.013
SMT solver: 0.006
selection: 0.003
success checks: 0
proof
0.57
GRP498-1
active equations: 155
iterations: 9
memory: 6 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.282
ground joinability: 0
find TRSs: 0.408
compute CPs: 0.043
main control loop: 0.105
rewriting: 0.036
SMT solver: 0.033
selection: 0.006
success checks: 0.009
proof
8.51
GRP499-1
active equations: 91
iterations: 8
memory: 81 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.168
ground joinability: 0
find TRSs: 0.249
compute CPs: 0.841
main control loop: 7.424
rewriting: 4.554
SMT solver: 0.009
selection: 0.19
success checks: 0.805
proof
6.64
GRP500-1
active equations: 91
iterations: 8
memory: 84 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.133
ground joinability: 0
find TRSs: 0.199
compute CPs: 0.729
main control loop: 6.311
rewriting: 3.342
SMT solver: 0.007
selection: 0.144
success checks: 1.145
proof
6.21
GRP501-1
active equations: 81
iterations: 7
memory: 123 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 0.466
ground joinability: 0
find TRSs: 0.64
compute CPs: 1.817
main control loop: 5.357
rewriting: 1.526
SMT solver: 0.025
selection: 0.277
success checks: 0.88
proof
30.04
GRP502-1
active equations: 116
iterations: 10
memory: 316 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.228
ground joinability: 0
find TRSs: 0.33
compute CPs: 3.975
main control loop: 23.602
rewriting: 11.091
SMT solver: 0.013
selection: 1.128
success checks: 5.643
proof
42.78
GRP503-1
active equations: 128
iterations: 11
memory: 329 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.297
ground joinability: 0
find TRSs: 0.419
compute CPs: 3.909
main control loop: 41.507
rewriting: 19.297
SMT solver: 0.014
selection: 0.933
success checks: 7.793
proof
31.92
GRP504-1
active equations: 116
iterations: 10
memory: 275 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.237
ground joinability: 0
find TRSs: 0.348
compute CPs: 5.39
main control loop: 24.092
rewriting: 14.52
SMT solver: 0.015
selection: 0.942
success checks: 3.409
proof
 
 
 
 
0.34
GRP509-1
active equations: 46
iterations: 5
memory: 8 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.026
compute CPs: 0.144
main control loop: 0.214
rewriting: 0.09
SMT solver: 0.001
selection: 0.027
success checks: 0.007
proof
0.19
GRP510-1
active equations: 34
iterations: 4
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.005
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.08
main control loop: 0.12
rewriting: 0.055
SMT solver: 0
selection: 0.016
success checks: 0.003
proof
0.68
GRP511-1
active equations: 70
iterations: 7
memory: 15 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.044
ground joinability: 0
find TRSs: 0.071
compute CPs: 0.26
main control loop: 0.47
rewriting: 0.182
SMT solver: 0.003
selection: 0.038
success checks: 0.048
proof
0.25
GRP512-1
active equations: 34
iterations: 4
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.005
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.101
main control loop: 0.116
rewriting: 0.08
SMT solver: 0
selection: 0.024
success checks: 0.004
proof
0.77
GRP513-1
active equations: 45
iterations: 5
memory: 9 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.016
ground joinability: 0
find TRSs: 0.029
compute CPs: 0.331
main control loop: 0.501
rewriting: 0.253
SMT solver: 0
selection: 0.043
success checks: 0.007
proof
0.59
GRP514-1
active equations: 33
iterations: 4
memory: 8 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.261
main control loop: 0.222
rewriting: 0.199
SMT solver: 0
selection: 0.033
success checks: 0.004
proof
1.18
GRP515-1
active equations: 45
iterations: 5
memory: 15 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.027
compute CPs: 0.534
main control loop: 0.57
rewriting: 0.394
SMT solver: 0.001
selection: 0.06
success checks: 0.011
proof
0.55
GRP516-1
active equations: 33
iterations: 4
memory: 8 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.015
compute CPs: 0.246
main control loop: 0.192
rewriting: 0.18
SMT solver: 0
selection: 0.031
success checks: 0.003
proof
0.10
GRP517-1
active equations: 21
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.037
main control loop: 0.044
rewriting: 0.027
SMT solver: 0
selection: 0.008
success checks: 0.002
proof
0.05
GRP518-1
active equations: 9
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0.018
main control loop: 0.002
rewriting: 0.013
SMT solver: 0
selection: 0.004
success checks: 0.001
proof
0.17
GRP519-1
active equations: 21
iterations: 3
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.067
main control loop: 0.045
rewriting: 0.047
SMT solver: 0
selection: 0.015
success checks: 0.004
proof
0.15
GRP520-1
active equations: 21
iterations: 3
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.066
main control loop: 0.04
rewriting: 0.039
SMT solver: 0
selection: 0.013
success checks: 0.002
proof
0.02
GRP521-1
active equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.003
main control loop: 0.005
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP522-1
active equations: 27
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.008
compute CPs: 0.007
main control loop: 0.011
rewriting: 0.003
SMT solver: 0.001
selection: 0
success checks: 0.001
proof
0.30
GRP523-1
active equations: 87
iterations: 8
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.064
ground joinability: 0
find TRSs: 0.109
compute CPs: 0.051
main control loop: 0.129
rewriting: 0.047
SMT solver: 0.007
selection: 0.003
success checks: 0.018
proof
0.07
GRP524-1
active equations: 39
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.021
main control loop: 0.022
rewriting: 0.008
SMT solver: 0.001
selection: 0.001
success checks: 0.002
proof
0.01
GRP525-1
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP526-1
active equations: 27
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.003
SMT solver: 0.001
selection: 0.001
success checks: 0.001
proof
0.33
GRP527-1
active equations: 75
iterations: 7
memory: 6 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.048
ground joinability: 0
find TRSs: 0.083
compute CPs: 0.038
main control loop: 0.134
rewriting: 0.072
SMT solver: 0.006
selection: 0.007
success checks: 0.02
proof
0.05
GRP528-1
active equations: 39
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.009
main control loop: 0.019
rewriting: 0.004
SMT solver: 0.002
selection: 0.001
success checks: 0.002
proof
0.03
GRP529-1
active equations: 27
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.006
main control loop: 0.01
rewriting: 0.002
SMT solver: 0.001
selection: 0
success checks: 0.001
proof
0.01
GRP530-1
active equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.002
main control loop: 0.004
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.32
GRP531-1
active equations: 75
iterations: 7
memory: 7 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.047
ground joinability: 0
find TRSs: 0.081
compute CPs: 0.07
main control loop: 0.19
rewriting: 0.06
SMT solver: 0.005
selection: 0.01
success checks: 0.017
proof
0.05
GRP532-1
active equations: 39
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.011
main control loop: 0.023
rewriting: 0.005
SMT solver: 0.001
selection: 0
success checks: 0.002
proof
0.01
GRP533-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.02
GRP534-1
active equations: 20
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.003
main control loop: 0.005
rewriting: 0.002
SMT solver: 0.001
selection: 0
success checks: 0
proof
0.29
GRP535-1
active equations: 80
iterations: 5
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.05
ground joinability: 0
find TRSs: 0.082
compute CPs: 0.056
main control loop: 0.088
rewriting: 0.058
SMT solver: 0.009
selection: 0.009
success checks: 0.011
proof
0.11
GRP536-1
active equations: 60
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.02
ground joinability: 0
find TRSs: 0.038
compute CPs: 0.029
main control loop: 0.017
rewriting: 0.019
SMT solver: 0.003
selection: 0.004
success checks: 0.001
proof
0.01
GRP537-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP538-1
active equations: 22
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.006
main control loop: 0.008
rewriting: 0.004
SMT solver: 0.001
selection: 0.001
success checks: 0.001
proof
0.14
GRP539-1
active equations: 62
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.045
compute CPs: 0.028
main control loop: 0.048
rewriting: 0.023
SMT solver: 0.005
selection: 0.005
success checks: 0.011
proof
0.06
GRP540-1
active equations: 42
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.015
main control loop: 0.018
rewriting: 0.013
SMT solver: 0.002
selection: 0.003
success checks: 0.002
proof
0.01
GRP541-1
active equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP542-1
active equations: 37
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.006
main control loop: 0.001
rewriting: 0.007
SMT solver: 0.001
selection: 0.001
success checks: 0
proof
1.05
GRP543-1
active equations: 157
iterations: 9
memory: 13 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.334
ground joinability: 0
find TRSs: 0.45
compute CPs: 0.044
main control loop: 0.48
rewriting: 0.187
SMT solver: 0.023
selection: 0.015
success checks: 0.096
proof
0.14
GRP544-1
active equations: 77
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.047
ground joinability: 0
find TRSs: 0.079
compute CPs: 0.02
main control loop: 0.048
rewriting: 0.018
SMT solver: 0.004
selection: 0.002
success checks: 0.001
proof
0.01
GRP545-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
GRP546-1
active equations: 24
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.008
compute CPs: 0.003
main control loop: 0.003
rewriting: 0.005
SMT solver: 0.001
selection: 0
success checks: 0.001
proof
0.32
GRP547-1
active equations: 84
iterations: 5
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.061
ground joinability: 0
find TRSs: 0.101
compute CPs: 0.035
main control loop: 0.139
rewriting: 0.08
SMT solver: 0.008
selection: 0.004
success checks: 0.012
proof
0.02
GRP548-1
active equations: 24
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.002
main control loop: 0.003
rewriting: 0.002
SMT solver: 0.001
selection: 0.001
success checks: 0
proof
0.01
GRP549-1
active equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0.001
SMT solver: 0.001
selection: 0
success checks: 0
proof
0.06
GRP550-1
active equations: 57
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.019
ground joinability: 0
find TRSs: 0.036
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.007
SMT solver: 0.002
selection: 0
success checks: 0
proof
2.44
GRP551-1
active equations: 124
iterations: 7
memory: 23 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.528
ground joinability: 0
find TRSs: 0.685
compute CPs: 0.225
main control loop: 1.602
rewriting: 0.709
SMT solver: 0.027
selection: 0.041
success checks: 0.16
proof
0.06
GRP552-1
active equations: 57
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.041
compute CPs: 0.002
main control loop: 0.01
rewriting: 0.004
SMT solver: 0.004
selection: 0
success checks: 0.001
proof
0.08
GRP553-1
active equations: 43
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.026
compute CPs: 0.018
main control loop: 0.035
rewriting: 0.012
SMT solver: 0.002
selection: 0.002
success checks: 0.002
proof
0.05
GRP554-1
active equations: 31
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.011
main control loop: 0.018
rewriting: 0.008
SMT solver: 0.001
selection: 0.002
success checks: 0.001
proof
0.09
GRP555-1
active equations: 43
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.025
compute CPs: 0.019
main control loop: 0.036
rewriting: 0.018
SMT solver: 0.002
selection: 0.003
success checks: 0.003
proof
0.08
GRP556-1
active equations: 43
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.024
compute CPs: 0.018
main control loop: 0.032
rewriting: 0.014
SMT solver: 0.001
selection: 0.003
success checks: 0.002
proof
0.18
GRP557-1
active equations: 43
iterations: 5
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.025
compute CPs: 0.081
main control loop: 0.064
rewriting: 0.042
SMT solver: 0.001
selection: 0.007
success checks: 0
proof
0.22
GRP558-1
active equations: 55
iterations: 6
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.02
ground joinability: 0
find TRSs: 0.041
compute CPs: 0.087
main control loop: 0.153
rewriting: 0.054
SMT solver: 0.002
selection: 0.008
success checks: 0.001
proof
1.32
GRP559-1
active equations: 128
iterations: 11
memory: 20 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.31
ground joinability: 0
find TRSs: 0.41
compute CPs: 0.3
main control loop: 0.698
rewriting: 0.224
SMT solver: 0.016
selection: 0.034
success checks: 0.105
proof
0.25
GRP560-1
active equations: 67
iterations: 7
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.035
ground joinability: 0
find TRSs: 0.061
compute CPs: 0.087
main control loop: 0.155
rewriting: 0.059
SMT solver: 0.003
selection: 0.01
success checks: 0.001
proof
0.11
GRP561-1
active equations: 41
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.023
compute CPs: 0.043
main control loop: 0.04
rewriting: 0.025
SMT solver: 0.002
selection: 0.005
success checks: 0
proof
0.06
GRP562-1
active equations: 29
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.02
main control loop: 0.016
rewriting: 0.012
SMT solver: 0.001
selection: 0.003
success checks: 0
proof
1.24
GRP563-1
active equations: 128
iterations: 11
memory: 23 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.318
ground joinability: 0
find TRSs: 0.43
compute CPs: 0.257
main control loop: 0.682
rewriting: 0.21
SMT solver: 0.016
selection: 0.04
success checks: 0.09
proof
0.19
GRP564-1
active equations: 65
iterations: 7
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.034
ground joinability: 0
find TRSs: 0.062
compute CPs: 0.055
main control loop: 0.112
rewriting: 0.04
SMT solver: 0.003
selection: 0.007
success checks: 0.001
proof
0.09
GRP565-1
active equations: 52
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.017
ground joinability: 0
find TRSs: 0.036
compute CPs: 0.012
main control loop: 0.026
rewriting: 0.015
SMT solver: 0.003
selection: 0.003
success checks: 0.002
proof
0.13
GRP566-1
active equations: 72
iterations: 5
memory: 2 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.044
ground joinability: 0
find TRSs: 0.075
compute CPs: 0.016
main control loop: 0.028
rewriting: 0.018
SMT solver: 0.004
selection: 0.002
success checks: 0
proof
1.87
GRP567-1
active equations: 188
iterations: 10
memory: 20 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.87
ground joinability: 0
find TRSs: 1.086
compute CPs: 0.109
main control loop: 0.643
rewriting: 0.227
SMT solver: 0.033
selection: 0.033
success checks: 0.078
proof
0.72
GRP568-1
active equations: 60
iterations: 4
memory: 9 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.308
ground joinability: 0
find TRSs: 0.447
compute CPs: 0.053
main control loop: 0.184
rewriting: 0.075
SMT solver: 0.029
selection: 0.007
success checks: 0.019
proof
0.06
GRP569-1
active equations: 33
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.016
compute CPs: 0.01
main control loop: 0.002
rewriting: 0.016
SMT solver: 0.002
selection: 0.002
success checks: 0
proof
0.07
GRP570-1
active equations: 53
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.019
ground joinability: 0
find TRSs: 0.039
compute CPs: 0.006
main control loop: 0.019
rewriting: 0.009
SMT solver: 0.003
selection: 0.001
success checks: 0
proof
1.16
GRP571-1
active equations: 153
iterations: 9
memory: 20 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.27
ground joinability: 0
find TRSs: 0.382
compute CPs: 0.032
main control loop: 0.653
rewriting: 0.482
SMT solver: 0.028
selection: 0.01
success checks: 0.08
proof
0.25
GRP572-1
active equations: 93
iterations: 6
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.077
ground joinability: 0
find TRSs: 0.129
compute CPs: 0.03
main control loop: 0.068
rewriting: 0.036
SMT solver: 0.01
selection: 0.004
success checks: 0.007
proof
0.11
GRP573-1
active equations: 53
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.027
ground joinability: 0
find TRSs: 0.061
compute CPs: 0.007
main control loop: 0.03
rewriting: 0.014
SMT solver: 0.005
selection: 0.002
success checks: 0.001
proof
0.27
GRP574-1
active equations: 113
iterations: 7
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.117
ground joinability: 0
find TRSs: 0.186
compute CPs: 0.008
main control loop: 0.04
rewriting: 0.03
SMT solver: 0.012
selection: 0.003
success checks: 0.003
proof
2.43
GRP575-1
active equations: 209
iterations: 11
memory: 30 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 1.095
ground joinability: 0
find TRSs: 1.358
compute CPs: 0.141
main control loop: 0.887
rewriting: 0.351
SMT solver: 0.05
selection: 0.031
success checks: 0.127
proof
0.31
GRP576-1
active equations: 113
iterations: 7
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.123
ground joinability: 0
find TRSs: 0.195
compute CPs: 0.023
main control loop: 0.071
rewriting: 0.037
SMT solver: 0.014
selection: 0.005
success checks: 0.007
proof
0.17
GRP577-1
active equations: 75
iterations: 5
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.027
ground joinability: 0
find TRSs: 0.049
compute CPs: 0.032
main control loop: 0.105
rewriting: 0.048
SMT solver: 0.004
selection: 0.008
success checks: 0.003
proof
0.29
GRP578-1
active equations: 75
iterations: 5
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.073
compute CPs: 0.057
main control loop: 0.121
rewriting: 0.092
SMT solver: 0.005
selection: 0.016
success checks: 0.003
proof
2.72
GRP579-1
active equations: 176
iterations: 10
memory: 29 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.816
ground joinability: 0
find TRSs: 1.034
compute CPs: 0.227
main control loop: 1.475
rewriting: 0.681
SMT solver: 0.033
selection: 0.049
success checks: 0.207
proof
0.45
GRP580-1
active equations: 95
iterations: 6
memory: 6 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.087
ground joinability: 0
find TRSs: 0.144
compute CPs: 0.069
main control loop: 0.237
rewriting: 0.118
SMT solver: 0.01
selection: 0.018
success checks: 0.008
proof
0.13
GRP581-1
active equations: 51
iterations: 4
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.018
ground joinability: 0
find TRSs: 0.037
compute CPs: 0.024
main control loop: 0.079
rewriting: 0.03
SMT solver: 0.001
selection: 0.007
success checks: 0.005
proof
0.29
GRP582-1
active equations: 91
iterations: 6
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.079
ground joinability: 0
find TRSs: 0.13
compute CPs: 0.039
main control loop: 0.129
rewriting: 0.054
SMT solver: 0.006
selection: 0.013
success checks: 0.006
proof
1.90
GRP583-1
active equations: 186
iterations: 10
memory: 23 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.882
ground joinability: 0
find TRSs: 1.109
compute CPs: 0.13
main control loop: 0.596
rewriting: 0.217
SMT solver: 0.03
selection: 0.024
success checks: 0.093
proof
0.65
GRP584-1
active equations: 157
iterations: 9
memory: 7 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.308
ground joinability: 0
find TRSs: 0.427
compute CPs: 0.053
main control loop: 0.138
rewriting: 0.062
SMT solver: 0.012
selection: 0.011
success checks: 0.007
proof
0.15
GRP585-1
active equations: 55
iterations: 6
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.021
ground joinability: 0
find TRSs: 0.044
compute CPs: 0.028
main control loop: 0.092
rewriting: 0.043
SMT solver: 0.002
selection: 0.007
success checks: 0.003
proof
0.29
GRP586-1
active equations: 67
iterations: 7
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.04
ground joinability: 0
find TRSs: 0.075
compute CPs: 0.049
main control loop: 0.161
rewriting: 0.099
SMT solver: 0.003
selection: 0.012
success checks: 0.005
proof
5.69
GRP587-1
active equations: 202
iterations: 17
memory: 74 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 1.445
ground joinability: 0
find TRSs: 1.879
compute CPs: 1.299
main control loop: 3.31
rewriting: 1.093
SMT solver: 0.111
selection: 0.088
success checks: 0.415
proof
0.39
GRP588-1
active equations: 79
iterations: 8
memory: 7 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.051
ground joinability: 0
find TRSs: 0.09
compute CPs: 0.045
main control loop: 0.175
rewriting: 0.122
SMT solver: 0.003
selection: 0.015
success checks: 0.017
proof
0.28
GRP589-1
active equations: 55
iterations: 6
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.021
ground joinability: 0
find TRSs: 0.043
compute CPs: 0.101
main control loop: 0.135
rewriting: 0.079
SMT solver: 0.002
selection: 0.021
success checks: 0.001
proof
0.31
GRP590-1
active equations: 55
iterations: 6
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.021
ground joinability: 0
find TRSs: 0.043
compute CPs: 0.117
main control loop: 0.135
rewriting: 0.088
SMT solver: 0.002
selection: 0.022
success checks: 0.001
proof
1.04
GRP591-1
active equations: 80
iterations: 7
memory: 17 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.102
ground joinability: 0
find TRSs: 0.161
compute CPs: 0.325
main control loop: 0.836
rewriting: 0.245
SMT solver: 0.009
selection: 0.054
success checks: 0.073
proof
0.38
GRP592-1
active equations: 67
iterations: 7
memory: 7 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.039
ground joinability: 0
find TRSs: 0.077
compute CPs: 0.126
main control loop: 0.273
rewriting: 0.107
SMT solver: 0.004
selection: 0.026
success checks: 0.003
proof
0.17
GRP593-1
active equations: 41
iterations: 5
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.05
main control loop: 0.086
rewriting: 0.043
SMT solver: 0.001
selection: 0.013
success checks: 0.007
proof
0.26
GRP594-1
active equations: 53
iterations: 6
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.017
ground joinability: 0
find TRSs: 0.037
compute CPs: 0.056
main control loop: 0.17
rewriting: 0.085
SMT solver: 0.002
selection: 0.019
success checks: 0.013
proof
0.15
GRP595-1
active equations: 41
iterations: 5
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.037
main control loop: 0.102
rewriting: 0.037
SMT solver: 0.002
selection: 0.017
success checks: 0.005
proof
0.23
GRP596-1
active equations: 53
iterations: 6
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.017
ground joinability: 0
find TRSs: 0.037
compute CPs: 0.068
main control loop: 0.155
rewriting: 0.054
SMT solver: 0.002
selection: 0.02
success checks: 0.008
proof
0.13
GRP597-1
active equations: 43
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.026
compute CPs: 0.043
main control loop: 0.057
rewriting: 0.031
SMT solver: 0.001
selection: 0.007
success checks: 0
proof
0.18
GRP598-1
active equations: 55
iterations: 6
memory: 4 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.017
ground joinability: 0
find TRSs: 0.039
compute CPs: 0.057
main control loop: 0.106
rewriting: 0.049
SMT solver: 0.002
selection: 0.01
success checks: 0.001
proof
1.04
GRP599-1
active equations: 92
iterations: 8
memory: 17 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.177
ground joinability: 0
find TRSs: 0.257
compute CPs: 0.235
main control loop: 0.589
rewriting: 0.264
SMT solver: 0.012
selection: 0.034
success checks: 0.062
proof
0.36
GRP600-1
active equations: 67
iterations: 7
memory: 6 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.036
ground joinability: 0
find TRSs: 0.064
compute CPs: 0.116
main control loop: 0.231
rewriting: 0.114
SMT solver: 0.003
selection: 0.016
success checks: 0.002
proof
0.79
GRP601-1
active equations: 77
iterations: 9
memory: 16 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.043
ground joinability: 0
find TRSs: 0.083
compute CPs: 0.337
main control loop: 0.459
rewriting: 0.21
SMT solver: 0.005
selection: 0.069
success checks: 0.011
proof
0.76
GRP602-1
active equations: 77
iterations: 9
memory: 15 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.044
ground joinability: 0
find TRSs: 0.083
compute CPs: 0.32
main control loop: 0.442
rewriting: 0.201
SMT solver: 0.005
selection: 0.069
success checks: 0.01
proof
0.81
GRP603-1
active equations: 77
iterations: 9
memory: 14 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.048
ground joinability: 0
find TRSs: 0.094
compute CPs: 0.35
main control loop: 0.523
rewriting: 0.2
SMT solver: 0.007
selection: 0.067
success checks: 0.013
proof
0.85
GRP604-1
active equations: 32
iterations: 3
memory: 17 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.05
ground joinability: 0
find TRSs: 0.095
compute CPs: 0.286
main control loop: 0.703
rewriting: 0.237
SMT solver: 0.006
selection: 0.082
success checks: 0.044
proof
0.70
GRP605-1
active equations: 79
iterations: 8
memory: 13 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.049
ground joinability: 0
find TRSs: 0.088
compute CPs: 0.088
main control loop: 0.431
rewriting: 0.243
SMT solver: 0.003
selection: 0.03
success checks: 0.044
proof
0.75
GRP606-1
active equations: 79
iterations: 8
memory: 13 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.045
ground joinability: 0
find TRSs: 0.082
compute CPs: 0.104
main control loop: 0.48
rewriting: 0.299
SMT solver: 0.003
selection: 0.033
success checks: 0.066
proof
2.11
GRP607-1
active equations: 140
iterations: 12
memory: 25 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.384
ground joinability: 0
find TRSs: 0.503
compute CPs: 0.35
main control loop: 1.503
rewriting: 0.555
SMT solver: 0.016
selection: 0.066
success checks: 0.16
proof
0.45
GRP608-1
active equations: 79
iterations: 8
memory: 11 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.038
ground joinability: 0
find TRSs: 0.074
compute CPs: 0.096
main control loop: 0.246
rewriting: 0.142
SMT solver: 0.004
selection: 0.04
success checks: 0.01
proof
1.25
GRP609-1
active equations: 91
iterations: 9
memory: 17 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.072
ground joinability: 0
find TRSs: 0.125
compute CPs: 0.451
main control loop: 0.787
rewriting: 0.348
SMT solver: 0.006
selection: 0.123
success checks: 0.033
proof
0.86
GRP610-1
active equations: 79
iterations: 8
memory: 17 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.045
ground joinability: 0
find TRSs: 0.084
compute CPs: 0.34
main control loop: 0.468
rewriting: 0.231
SMT solver: 0.005
selection: 0.087
success checks: 0.021
proof
0.69
GRP611-1
active equations: 79
iterations: 8
memory: 9 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.042
ground joinability: 0
find TRSs: 0.081
compute CPs: 0.237
main control loop: 0.462
rewriting: 0.205
SMT solver: 0.006
selection: 0.066
success checks: 0.016
proof
1.13
GRP612-1
active equations: 91
iterations: 9
memory: 16 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.137
ground joinability: 0
find TRSs: 0.184
compute CPs: 0.392
main control loop: 0.744
rewriting: 0.29
SMT solver: 0.006
selection: 0.098
success checks: 0.024
proof
0.50
GRP613-1
active equations: 79
iterations: 8
memory: 9 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.055
ground joinability: 0
find TRSs: 0.098
compute CPs: 0.176
main control loop: 0.306
rewriting: 0.137
SMT solver: 0.004
selection: 0.024
success checks: 0.004
proof
0.45
GRP614-1
active equations: 79
iterations: 8
memory: 9 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.049
ground joinability: 0
find TRSs: 0.089
compute CPs: 0.153
main control loop: 0.278
rewriting: 0.125
SMT solver: 0.003
selection: 0.023
success checks: 0.004
proof
1.52
GRP615-1
active equations: 104
iterations: 9
memory: 24 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.218
ground joinability: 0
find TRSs: 0.309
compute CPs: 0.375
main control loop: 1.125
rewriting: 0.347
SMT solver: 0.013
selection: 0.066
success checks: 0.054
proof
0.35
GRP616-1
active equations: 67
iterations: 7
memory: 5 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.038
ground joinability: 0
find TRSs: 0.07
compute CPs: 0.126
main control loop: 0.237
rewriting: 0.093
SMT solver: 0.003
selection: 0.021
success checks: 0.002
proof
 
 
 
 
 
 
 
 
 
 
 
 
16.99
GRP669-1
active equations: 302
iterations: 15
memory: 133 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 5.9
ground joinability: 0
find TRSs: 6.693
compute CPs: 2.086
main control loop: 8.73
rewriting: 4.466
SMT solver: 0.084
selection: 0.42
success checks: 0.781
 
 
0.05
GRP671-1
active equations: 29
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.012
main control loop: 0.005
rewriting: 0.011
SMT solver: 0.001
selection: 0.003
success checks: 0
proof
 
 
 
 
0.11
GRP679-1
active equations: 48
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.032
compute CPs: 0.025
main control loop: 0.012
rewriting: 0.024
SMT solver: 0.002
selection: 0.005
success checks: 0.003
proof
5.45
GRP680-1
active equations: 239
iterations: 12
memory: 46 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 1.349
ground joinability: 0
find TRSs: 1.653
compute CPs: 0.141
main control loop: 2.41
rewriting: 1.748
SMT solver: 0.038
selection: 0.032
success checks: 0.28
 
 
0.10
GRP684-1
active equations: 54
iterations: 5
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.026
ground joinability: 0
find TRSs: 0.047
compute CPs: 0.012
main control loop: 0.035
rewriting: 0.018
SMT solver: 0.002
selection: 0.003
success checks: 0.003
proof
1.36
GRP686-1
active equations: 167
iterations: 9
memory: 16 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.429
ground joinability: 0
find TRSs: 0.56
compute CPs: 0.125
main control loop: 0.542
rewriting: 0.257
SMT solver: 0.018
selection: 0.029
success checks: 0.059
proof
33.88
GRP687-1
active equations: 359
iterations: 18
memory: 141 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 7.732
ground joinability: 0
find TRSs: 8.721
compute CPs: 1.562
main control loop: 22.878
rewriting: 13.539
SMT solver: 0.103
selection: 0.345
success checks: 1.512
proof
 
 
 
 
 
 
 
 
 
281.66
GRP697-1
active equations: 280
iterations: 22
memory: 699 MB
restarts: 4
problem shape: none
time (sec): 
reducibility constraints: 33.521
ground joinability: 0
find TRSs: 36.927
compute CPs: 56.415
main control loop: 240.4
rewriting: 144.231
SMT solver: 0.297
selection: 6.49
success checks: 7.342
 
6.65
GRP698-1
active equations: 160
iterations: 8
memory: 65 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 2.016
ground joinability: 0
find TRSs: 2.401
compute CPs: 1.192
main control loop: 3.551
rewriting: 1.528
SMT solver: 0.041
selection: 0.327
success checks: 0.181
proof
 
 
 
 
 
1.29
GRP708-1
active equations: 59
iterations: 3
memory: 16 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.385
ground joinability: 0
find TRSs: 0.518
compute CPs: 0.231
main control loop: 0.62
rewriting: 0.244
SMT solver: 0.024
selection: 0.047
success checks: 0.034
proof
0.07
GRP709-1
active equations: 49
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.023
compute CPs: 0.013
main control loop: 0.009
rewriting: 0.011
SMT solver: 0.002
selection: 0.002
success checks: 0.002
proof
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
218.26
GRP731-1
active equations: 484
iterations: 38
memory: 1532 MB
restarts: 4
problem shape: none
time (sec): 
reducibility constraints: 36.399
ground joinability: 0
find TRSs: 41.8
compute CPs: 11.482
main control loop: 155.332
rewriting: 68.782
SMT solver: 1.536
selection: 2.858
success checks: 20.031
 
 
 
 
47.82
GRP750-1
active equations: 230
iterations: 19
memory: 435 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 2.223
ground joinability: 0
find TRSs: 2.735
compute CPs: 6.819
main control loop: 41.238
rewriting: 15.771
SMT solver: 0.039
selection: 2.93
success checks: 10.727
proof
158.91
GRP751-1
active equations: 363
iterations: 30
memory: 998 MB
restarts: 2
problem shape: elio
time (sec): 
reducibility constraints: 8.942
ground joinability: 0
find TRSs: 10.259
compute CPs: 23.503
main control loop: 137.804
rewriting: 58.252
SMT solver: 0.077
selection: 8.71
success checks: 5.782
proof
 
 
44.69
GRP754-1
active equations: 254
iterations: 21
memory: 435 MB
restarts: 2
problem shape: none
time (sec): 
reducibility constraints: 3.032
ground joinability: 0
find TRSs: 3.661
compute CPs: 10.038
main control loop: 38.35
rewriting: 15.083
SMT solver: 0.047
selection: 3.41
success checks: 3.938
proof
0.74
GRP756-1
active equations: 77
iterations: 7
memory: 15 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.054
ground joinability: 0
find TRSs: 0.087
compute CPs: 0.243
main control loop: 0.43
rewriting: 0.166
SMT solver: 0.002
selection: 0.055
success checks: 0.029
proof
 
 
 
 
 
 
 
 
 
6.00
LAT006-1
active equations: 205
iterations: 8
memory: 120 MB
restarts: 1
problem shape: boro
time (sec): 
reducibility constraints: 1.003
ground joinability: 0
find TRSs: 1.122
compute CPs: 3.221
main control loop: 3.5
rewriting: 0.621
SMT solver: 0.006
selection: 0.077
success checks: 0.237
proof
317.69
LAT007-1
active equations: 626
iterations: 23
memory: 2492 MB
restarts: 1
problem shape: boro
time (sec): 
reducibility constraints: 35.309
ground joinability: 0.001
find TRSs: 37.072
compute CPs: 194.409
main control loop: 239.065
rewriting: 15.794
SMT solver: 0.047
selection: 0.716
success checks: 25.077
proof
0.16
LAT008-1
active equations: 11
iterations: 1
memory: 3 MB
restarts: 1
problem shape: boro
time (sec): 
reducibility constraints: 0.019
ground joinability: 0
find TRSs: 0.035
compute CPs: 0.047
main control loop: 0.106
rewriting: 0.038
SMT solver: 0.001
selection: 0.007
success checks: 0.003
proof
138.80
LAT009-1
active equations: 389
iterations: 20
memory: 1158 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 9.613
ground joinability: 0
find TRSs: 10.166
compute CPs: 17.569
main control loop: 112.359
rewriting: 63.682
SMT solver: 0.023
selection: 2.19
success checks: 9.188
proof
52.86
LAT010-1
active equations: 311
iterations: 16
memory: 576 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 4.338
ground joinability: 0
find TRSs: 4.646
compute CPs: 8.303
main control loop: 41.656
rewriting: 25.78
SMT solver: 0.016
selection: 1.212
success checks: 5.079
proof
12.45
LAT011-1
active equations: 253
iterations: 13
memory: 163 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 1.489
ground joinability: 0
find TRSs: 1.657
compute CPs: 4.342
main control loop: 8.902
rewriting: 3.063
SMT solver: 0.007
selection: 0.264
success checks: 0.715
proof
 
 
0.01
LAT014-1
active equations: 4
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
 
 
0.86
LAT019-1
active equations: 83
iterations: 7
memory: 13 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.185
ground joinability: 0
find TRSs: 0.224
compute CPs: 0.112
main control loop: 0.512
rewriting: 0.266
SMT solver: 0.003
selection: 0.016
success checks: 0.066
proof
 
46.90
LAT021-1
active equations: 235
iterations: 19
memory: 876 MB
restarts: 2
problem shape: none
time (sec): 
reducibility constraints: 7.222
ground joinability: 0
find TRSs: 7.756
compute CPs: 3.445
main control loop: 37.179
rewriting: 10.175
SMT solver: 0.034
selection: 0.557
success checks: 11.916
proof
 
80.58
LAT023-1
active equations: 283
iterations: 23
memory: 1705 MB
restarts: 2
problem shape: none
time (sec): 
reducibility constraints: 11.537
ground joinability: 0
find TRSs: 12.244
compute CPs: 4.571
main control loop: 63.902
rewriting: 13.593
SMT solver: 0.04
selection: 0.746
success checks: 20.828
proof
146.84
LAT026-1
active equations: 456
iterations: 17
memory: 2026 MB
restarts: 1
problem shape: boro
time (sec): 
reducibility constraints: 7.458
ground joinability: 0.001
find TRSs: 8.195
compute CPs: 107.01
main control loop: 119.425
rewriting: 6.659
SMT solver: 0.02
selection: 0.324
success checks: 11.723
proof
325.02
LAT027-1
active equations: 624
iterations: 23
memory: 3888 MB
restarts: 1
problem shape: boro
time (sec): 
reducibility constraints: 23.098
ground joinability: 0.002
find TRSs: 24.778
compute CPs: 232.808
main control loop: 292.488
rewriting: 12.079
SMT solver: 0.047
selection: 0.672
success checks: 25.781
proof
2.74
LAT028-1
active equations: 177
iterations: 7
memory: 70 MB
restarts: 1
problem shape: boro
time (sec): 
reducibility constraints: 0.354
ground joinability: 0
find TRSs: 0.438
compute CPs: 1.592
main control loop: 1.154
rewriting: 0.161
SMT solver: 0.003
selection: 0.023
success checks: 0.137
proof
2.02
LAT031-1
active equations: 95
iterations: 8
memory: 26 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.152
ground joinability: 0
find TRSs: 0.196
compute CPs: 0.192
main control loop: 1.408
rewriting: 0.803
SMT solver: 0.003
selection: 0.028
success checks: 0.138
proof
2.26
LAT032-1
active equations: 95
iterations: 8
memory: 26 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.172
ground joinability: 0
find TRSs: 0.223
compute CPs: 0.199
main control loop: 1.613
rewriting: 0.89
SMT solver: 0.003
selection: 0.03
success checks: 0.164
proof
0.03
LAT033-1
active equations: 8
iterations: 1
memory: 3 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.005
main control loop: 0
rewriting: 0.009
SMT solver: 0
selection: 0.001
success checks: 0
proof
0.02
LAT034-1
active equations: 8
iterations: 1
memory: 3 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.003
main control loop: 0
rewriting: 0.005
SMT solver: 0
selection: 0
success checks: 0
proof
 
1.29
LAT039-1
active equations: 109
iterations: 9
memory: 17 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.2
ground joinability: 0
find TRSs: 0.264
compute CPs: 0.147
main control loop: 0.75
rewriting: 0.318
SMT solver: 0.005
selection: 0.018
success checks: 0.147
proof
0.01
LAT039-2
active equations: 13
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.002
main control loop: 0
rewriting: 0.004
SMT solver: 0
selection: 0
success checks: 0
proof
1.31
LAT040-1
active equations: 68
iterations: 5
memory: 17 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.249
ground joinability: 0
find TRSs: 0.344
compute CPs: 0.172
main control loop: 0.699
rewriting: 0.311
SMT solver: 0.007
selection: 0.025
success checks: 0.119
proof
0.10
LAT042-1
active equations: 42
iterations: 2
memory: 2 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.016
compute CPs: 0.011
main control loop: 0.028
rewriting: 0.028
SMT solver: 0.002
selection: 0.002
success checks: 0.011
proof
2.75
LAT043-1
active equations: 181
iterations: 9
memory: 35 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.54
ground joinability: 0
find TRSs: 0.634
compute CPs: 0.396
main control loop: 1.929
rewriting: 1.01
SMT solver: 0.01
selection: 0.031
success checks: 0.135
proof
382.11
LAT044-1
active equations: 572
iterations: 29
memory: 876 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 22.291
ground joinability: 0
find TRSs: 23.716
compute CPs: 2.77
main control loop: 280.613
rewriting: 249.207
SMT solver: 0.09
selection: 0.31
success checks: 26.323
 
0.13
LAT045-1
active equations: 55
iterations: 3
memory: 3 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 0.018
ground joinability: 0
find TRSs: 0.028
compute CPs: 0.025
main control loop: 0.047
rewriting: 0.034
SMT solver: 0.001
selection: 0.005
success checks: 0.008
proof
 
 
 
 
 
 
 
 
25.55
LAT080-1
active equations: 84
iterations: 7
memory: 438 MB
restarts: 0
problem shape: piombo
time (sec): 
reducibility constraints: 0.119
ground joinability: 0
find TRSs: 0.164
compute CPs: 11.058
main control loop: 24.876
rewriting: 11.345
SMT solver: 0.001
selection: 0.27
success checks: 0.024
proof
 
 
24.98
LAT083-1
active equations: 84
iterations: 7
memory: 487 MB
restarts: 0
problem shape: piombo
time (sec): 
reducibility constraints: 0.116
ground joinability: 0
find TRSs: 0.165
compute CPs: 10.592
main control loop: 24.541
rewriting: 11.212
SMT solver: 0.001
selection: 0.247
success checks: 0.022
proof
25.20
LAT084-1
active equations: 66
iterations: 4
memory: 486 MB
restarts: 1
problem shape: piombo
time (sec): 
reducibility constraints: 0.272
ground joinability: 0
find TRSs: 0.357
compute CPs: 10.805
main control loop: 24.697
rewriting: 11.187
SMT solver: 0.002
selection: 0.284
success checks: 0.029
proof
 
26.37
LAT086-1
active equations: 46
iterations: 3
memory: 524 MB
restarts: 1
problem shape: piombo
time (sec): 
reducibility constraints: 0.273
ground joinability: 0
find TRSs: 0.357
compute CPs: 11.248
main control loop: 25.92
rewriting: 11.565
SMT solver: 0.002
selection: 0.294
success checks: 0.035
proof
25.13
LAT087-1
active equations: 124
iterations: 9
memory: 456 MB
restarts: 0
problem shape: piombo
time (sec): 
reducibility constraints: 0.239
ground joinability: 0
find TRSs: 0.319
compute CPs: 10.759
main control loop: 24.669
rewriting: 11.155
SMT solver: 0.002
selection: 0.273
success checks: 0.025
proof
0.03
LAT088-1
active equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.009
main control loop: 0.004
rewriting: 0.005
SMT solver: 0
selection: 0.001
success checks: 0
proof
12.91
LAT089-1
active equations: 143
iterations: 12
memory: 163 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.523
ground joinability: 0
find TRSs: 0.65
compute CPs: 6.79
main control loop: 9.199
rewriting: 3.171
SMT solver: 0.006
selection: 0.5
success checks: 0.306
proof
0.05
LAT090-1
active equations: 29
iterations: 3
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.017
main control loop: 0.02
rewriting: 0.011
SMT solver: 0
selection: 0.003
success checks: 0
proof
0.56
LAT091-1
active equations: 47
iterations: 4
memory: 10 MB
restarts: 1
problem shape: elio
time (sec): 
reducibility constraints: 0.094
ground joinability: 0
find TRSs: 0.151
compute CPs: 0.177
main control loop: 0.279
rewriting: 0.103
SMT solver: 0.002
selection: 0.014
success checks: 0.006
proof
18.48
LAT092-1
active equations: 82
iterations: 7
memory: 49 MB
restarts: 0
problem shape: piombo
time (sec): 
reducibility constraints: 0.089
ground joinability: 0
find TRSs: 0.131
compute CPs: 6.946
main control loop: 14.872
rewriting: 9.682
SMT solver: 0.001
selection: 0.223
success checks: 0.018
proof
36.98
LAT093-1
active equations: 221
iterations: 12
memory: 284 MB
restarts: 2
problem shape: piombo
time (sec): 
reducibility constraints: 1.836
ground joinability: 0
find TRSs: 2.119
compute CPs: 17.211
main control loop: 31.594
rewriting: 12.306
SMT solver: 0.01
selection: 0.78
success checks: 0.456
proof
17.97
LAT094-1
active equations: 82
iterations: 7
memory: 296 MB
restarts: 0
problem shape: piombo
time (sec): 
reducibility constraints: 0.099
ground joinability: 0
find TRSs: 0.145
compute CPs: 6.761
main control loop: 14.528
rewriting: 9.356
SMT solver: 0.001
selection: 0.242
success checks: 0.02
proof
26.01
LAT095-1
active equations: 121
iterations: 7
memory: 56 MB
restarts: 1
problem shape: piombo
time (sec): 
reducibility constraints: 0.396
ground joinability: 0
find TRSs: 0.508
compute CPs: 8.464
main control loop: 25.355
rewriting: 14.885
SMT solver: 0.004
selection: 0.351
success checks: 0.043
proof
40.88
LAT096-1
active equations: 81
iterations: 5
memory: 177 MB
restarts: 2
problem shape: piombo
time (sec): 
reducibility constraints: 1.853
ground joinability: 0
find TRSs: 2.118
compute CPs: 15.656
main control loop: 38.022
rewriting: 17.743
SMT solver: 0.012
selection: 0.914
success checks: 0.497
proof
22.29
LAT097-1
active equations: 122
iterations: 9
memory: 54 MB
restarts: 0
problem shape: piombo
time (sec): 
reducibility constraints: 0.208
ground joinability: 0
find TRSs: 0.279
compute CPs: 7.805
main control loop: 18.556
rewriting: 12.29
SMT solver: 0.002
selection: 0.302
success checks: 0.035
proof
 
 
 
 
 
 
 
 
 
 
 
 
 
 
503.90
LAT152-1
active equations: 530
iterations: 27
memory: 4076 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 29.018
ground joinability: 0
find TRSs: 30.545
compute CPs: 64.958
main control loop: 450.187
rewriting: 219.266
SMT solver: 0.111
selection: 6.694
success checks: 46.411
proof
549.75
LAT153-1
active equations: 530
iterations: 27
memory: 4688 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 31.032
ground joinability: 0
find TRSs: 32.29
compute CPs: 70.32
main control loop: 491.048
rewriting: 256.411
SMT solver: 0.04
selection: 6.765
success checks: 45.357
proof
380.78
LAT154-1
active equations: 470
iterations: 24
memory: 3544 MB
restarts: 0
problem shape: silicio
time (sec): 
reducibility constraints: 20.578
ground joinability: 0
find TRSs: 21.593
compute CPs: 49.079
main control loop: 321.384
rewriting: 172.331
SMT solver: 0.032
selection: 4.717
success checks: 45.089
proof
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
31.49
LAT389-1
active equations: 88
iterations: 5
memory: 185 MB
restarts: 2
problem shape: piombo
time (sec): 
reducibility constraints: 1.391
ground joinability: 0
find TRSs: 1.647
compute CPs: 13.729
main control loop: 29.351
rewriting: 11.753
SMT solver: 0.01
selection: 0.526
success checks: 0.124
proof
32.58
LAT390-1
active equations: 68
iterations: 4
memory: 185 MB
restarts: 2
problem shape: piombo
time (sec): 
reducibility constraints: 1.363
ground joinability: 0
find TRSs: 1.612
compute CPs: 14.372
main control loop: 30.59
rewriting: 12.623
SMT solver: 0.009
selection: 0.569
success checks: 0.14
proof
25.10
LAT391-1
active equations: 84
iterations: 7
memory: 532 MB
restarts: 0
problem shape: piombo
time (sec): 
reducibility constraints: 0.111
ground joinability: 0
find TRSs: 0.16
compute CPs: 11.785
main control loop: 24.67
rewriting: 10.275
SMT solver: 0.001
selection: 0.28
success checks: 0.051
proof
33.63
LAT392-1
active equations: 108
iterations: 6
memory: 154 MB
restarts: 2
problem shape: piombo
time (sec): 
reducibility constraints: 1.447
ground joinability: 0
find TRSs: 1.742
compute CPs: 14.913
main control loop: 31.129
rewriting: 12.732
SMT solver: 0.01
selection: 0.626
success checks: 0.161
proof
 
 
5.63
LAT394-1
active equations: 80
iterations: 7
memory: 42 MB
restarts: 2
problem shape: none
time (sec): 
reducibility constraints: 0.643
ground joinability: 0
find TRSs: 0.852
compute CPs: 1.196
main control loop: 4.581
rewriting: 2.282
SMT solver: 0.028
selection: 0.259
success checks: 0.092
proof
10.66
LAT394-2
active equations: 35
iterations: 3
memory: 100 MB
restarts: 1
problem shape: carbonio
time (sec): 
reducibility constraints: 0.037
ground joinability: 0
find TRSs: 0.061
compute CPs: 4.989
main control loop: 10.263
rewriting: 4.288
SMT solver: 0.001
selection: 0.275
success checks: 0.065
proof
 
 
0.14
LCL110-2
active equations: 40
iterations: 4
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.025
main control loop: 0.05
rewriting: 0.034
SMT solver: 0.001
selection: 0.002
success checks: 0.003
proof
1.94
LCL111-2
active equations: 58
iterations: 5
memory: 30 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.127
ground joinability: 0
find TRSs: 0.214
compute CPs: 0.284
main control loop: 1.602
rewriting: 0.434
SMT solver: 0.013
selection: 0.023
success checks: 0.138
proof
0.23
LCL112-2
active equations: 52
iterations: 5
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.017
ground joinability: 0
find TRSs: 0.036
compute CPs: 0.04
main control loop: 0.123
rewriting: 0.053
SMT solver: 0.001
selection: 0.003
success checks: 0.004
proof
0.59
LCL113-2
active equations: 76
iterations: 7
memory: 11 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.043
ground joinability: 0
find TRSs: 0.079
compute CPs: 0.114
main control loop: 0.349
rewriting: 0.15
SMT solver: 0.003
selection: 0.007
success checks: 0.013
proof
0.56
LCL114-2
active equations: 76
iterations: 7
memory: 11 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.043
ground joinability: 0
find TRSs: 0.079
compute CPs: 0.07
main control loop: 0.28
rewriting: 0.142
SMT solver: 0.004
selection: 0.008
success checks: 0.01
proof
0.51
LCL115-2
active equations: 76
iterations: 7
memory: 8 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.04
ground joinability: 0
find TRSs: 0.075
compute CPs: 0.091
main control loop: 0.259
rewriting: 0.131
SMT solver: 0.004
selection: 0.009
success checks: 0.011
proof
1.79
LCL116-2
active equations: 100
iterations: 9
memory: 21 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.098
ground joinability: 0
find TRSs: 0.157
compute CPs: 0.271
main control loop: 1.079
rewriting: 0.357
SMT solver: 0.005
selection: 0.017
success checks: 0.024
proof
0.02
LCL132-1
active equations: 16
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.004
main control loop: 0.007
rewriting: 0.003
SMT solver: 0
selection: 0
success checks: 0
proof
0.03
LCL133-1
active equations: 29
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.004
main control loop: 0.014
rewriting: 0.003
SMT solver: 0.001
selection: 0.001
success checks: 0.003
proof
0.03
LCL134-1
active equations: 16
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.006
main control loop: 0.007
rewriting: 0.006
SMT solver: 0
selection: 0.001
success checks: 0.001
proof
0.06
LCL135-1
active equations: 28
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.01
main control loop: 0.021
rewriting: 0.011
SMT solver: 0.001
selection: 0.003
success checks: 0.002
proof
 
0.45
LCL139-1
active equations: 64
iterations: 6
memory: 6 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.024
ground joinability: 0
find TRSs: 0.048
compute CPs: 0.039
main control loop: 0.321
rewriting: 0.157
SMT solver: 0.001
selection: 0.006
success checks: 0.006
proof
0.18
LCL140-1
active equations: 64
iterations: 6
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.028
ground joinability: 0
find TRSs: 0.053
compute CPs: 0.056
main control loop: 0.093
rewriting: 0.036
SMT solver: 0.002
selection: 0.003
success checks: 0.003
proof
0.43
LCL141-1
active equations: 88
iterations: 8
memory: 9 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.066
ground joinability: 0
find TRSs: 0.112
compute CPs: 0.165
main control loop: 0.208
rewriting: 0.085
SMT solver: 0.004
selection: 0.008
success checks: 0.007
proof
1.47
LCL153-1
active equations: 25
iterations: 1
memory: 19 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.161
ground joinability: 0
find TRSs: 0.285
compute CPs: 0.181
main control loop: 1.1
rewriting: 0.286
SMT solver: 0.048
selection: 0.013
success checks: 0.069
proof
3.91
LCL154-1
active equations: 25
iterations: 1
memory: 40 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.169
ground joinability: 0
find TRSs: 0.294
compute CPs: 0.505
main control loop: 3.54
rewriting: 1.339
SMT solver: 0.044
selection: 0.024
success checks: 0.069
proof
1.52
LCL155-1
active equations: 25
iterations: 1
memory: 23 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.131
ground joinability: 0
find TRSs: 0.238
compute CPs: 0.149
main control loop: 1.217
rewriting: 0.276
SMT solver: 0.046
selection: 0.01
success checks: 0.029
proof
0.09
LCL156-1
active equations: 43
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.032
compute CPs: 0.01
main control loop: 0.021
rewriting: 0.018
SMT solver: 0.008
selection: 0.002
success checks: 0.003
proof
0.13
LCL157-1
active equations: 55
iterations: 4
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.017
ground joinability: 0
find TRSs: 0.047
compute CPs: 0.007
main control loop: 0.062
rewriting: 0.03
SMT solver: 0.011
selection: 0.001
success checks: 0.004
proof
3.00
LCL158-1
active equations: 61
iterations: 4
memory: 40 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.18
ground joinability: 0
find TRSs: 0.303
compute CPs: 0.465
main control loop: 2.579
rewriting: 0.996
SMT solver: 0.038
selection: 0.024
success checks: 0.055
proof
3.04
LCL159-1
active equations: 37
iterations: 2
memory: 30 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.191
ground joinability: 0
find TRSs: 0.353
compute CPs: 0.365
main control loop: 2.558
rewriting: 0.745
SMT solver: 0.08
selection: 0.031
success checks: 0.04
proof
3.99
LCL160-1
active equations: 61
iterations: 4
memory: 30 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.158
ground joinability: 0
find TRSs: 0.309
compute CPs: 0.294
main control loop: 3.541
rewriting: 1.89
SMT solver: 0.069
selection: 0.014
success checks: 0.103
proof
0.06
LCL161-1
active equations: 38
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.006
main control loop: 0.013
rewriting: 0.011
SMT solver: 0.004
selection: 0
success checks: 0.003
proof
 
 
0.08
LCL164-1
active equations: 38
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.024
compute CPs: 0.004
main control loop: 0.03
rewriting: 0.024
SMT solver: 0.005
selection: 0
success checks: 0.01
proof
0.05
LDA001-1
active equations: 26
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.005
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.009
main control loop: 0.014
rewriting: 0.011
SMT solver: 0.001
selection: 0.002
success checks: 0
proof
26.76
LDA002-1
active equations: 331
iterations: 27
memory: 66 MB
restarts: 2
problem shape: none
time (sec): 
reducibility constraints: 7.729
ground joinability: 0
find TRSs: 10.253
compute CPs: 1.903
main control loop: 13.354
rewriting: 4.576
SMT solver: 0.774
selection: 0.31
success checks: 0.354
proof
0.02
LDA007-3
active equations: 18
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.001
main control loop: 0.001
rewriting: 0.001
SMT solver: 0.003
selection: 0
success checks: 0
proof
0.46
REL001-1
active equations: 113
iterations: 6
memory: 7 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.136
ground joinability: 0
find TRSs: 0.214
compute CPs: 0.041
main control loop: 0.177
rewriting: 0.098
SMT solver: 0.019
selection: 0.009
success checks: 0.025
proof
1.35
REL002-1
active equations: 134
iterations: 7
memory: 17 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.224
ground joinability: 0
find TRSs: 0.326
compute CPs: 0.074
main control loop: 0.755
rewriting: 0.555
SMT solver: 0.022
selection: 0.026
success checks: 0.091
proof
12.83
REL004-1
active equations: 442
iterations: 22
memory: 188 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 4.179
ground joinability: 0
find TRSs: 5.145
compute CPs: 2.037
main control loop: 5.673
rewriting: 2.131
SMT solver: 0.218
selection: 0.214
success checks: 0.641
proof
12.28
REL004-2
active equations: 325
iterations: 16
memory: 93 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 4.569
ground joinability: 0
find TRSs: 5.505
compute CPs: 1.57
main control loop: 5.556
rewriting: 2.994
SMT solver: 0.156
selection: 0.234
success checks: 0.232
proof
12.12
REL004-3
active equations: 325
iterations: 16
memory: 93 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 4.479
ground joinability: 0
find TRSs: 5.391
compute CPs: 1.537
main control loop: 5.498
rewriting: 2.973
SMT solver: 0.151
selection: 0.235
success checks: 0.23
proof
411.29
REL005-1
active equations: 412
iterations: 20
memory: 1007 MB
restarts: 4
problem shape: xeno
time (sec): 
reducibility constraints: 61.439
ground joinability: 0
find TRSs: 68.909
compute CPs: 26.424
main control loop: 323.834
rewriting: 146.538
SMT solver: 1.492
selection: 1.409
success checks: 6.751
proof
65.38
REL005-3
active equations: 408
iterations: 20
memory: 216 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 6.563
ground joinability: 0
find TRSs: 8.054
compute CPs: 2.693
main control loop: 42.855
rewriting: 34.855
SMT solver: 0.331
selection: 0.301
success checks: 0.513
proof
4.77
REL006-1
active equations: 204
iterations: 10
memory: 52 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 1.07
ground joinability: 0
find TRSs: 1.376
compute CPs: 0.642
main control loop: 2.955
rewriting: 1.189
SMT solver: 0.074
selection: 0.082
success checks: 0.204
proof
3.49
REL007-1
active equations: 184
iterations: 9
memory: 35 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.953
ground joinability: 0
find TRSs: 1.262
compute CPs: 0.367
main control loop: 1.836
rewriting: 0.957
SMT solver: 0.066
selection: 0.063
success checks: 0.109
proof
 
 
 
102.06
REL010-2
active equations: 669
iterations: 33
memory: 742 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 28.634
ground joinability: 0
find TRSs: 32.509
compute CPs: 16.452
main control loop: 55.125
rewriting: 21.058
SMT solver: 0.88
selection: 1.506
success checks: 1.803
proof
 
17.87
REL011-2
active equations: 289
iterations: 14
memory: 175 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 3.623
ground joinability: 0
find TRSs: 4.509
compute CPs: 2.807
main control loop: 10.775
rewriting: 4.997
SMT solver: 0.232
selection: 0.316
success checks: 0.433
proof
285.28
REL012-1
active equations: 554
iterations: 27
memory: 1332 MB
restarts: 4
problem shape: xeno
time (sec): 
reducibility constraints: 75.3
ground joinability: 0
find TRSs: 83.167
compute CPs: 31.711
main control loop: 183.821
rewriting: 80.468
SMT solver: 1.368
selection: 2.484
success checks: 5.083
proof
69.75
REL012-2
active equations: 724
iterations: 36
memory: 500 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 36.312
ground joinability: 0
find TRSs: 40.654
compute CPs: 8.77
main control loop: 24.21
rewriting: 10.42
SMT solver: 0.765
selection: 0.883
success checks: 1.241
 
2.41
REL015-1
active equations: 64
iterations: 3
memory: 35 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.435
ground joinability: 0
find TRSs: 0.597
compute CPs: 0.218
main control loop: 1.692
rewriting: 0.862
SMT solver: 0.031
selection: 0.044
success checks: 0.078
proof
 
 
 
 
13.34
REL018-1
active equations: 247
iterations: 12
memory: 107 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 2.859
ground joinability: 0
find TRSs: 3.541
compute CPs: 1.216
main control loop: 8.362
rewriting: 3.805
SMT solver: 0.119
selection: 0.193
success checks: 0.335
proof
 
 
 
 
 
 
 
 
0.38
REL023-1
active equations: 93
iterations: 5
memory: 7 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.073
ground joinability: 0
find TRSs: 0.135
compute CPs: 0.046
main control loop: 0.149
rewriting: 0.102
SMT solver: 0.024
selection: 0.011
success checks: 0.023
proof
1.61
REL023-2
active equations: 105
iterations: 5
memory: 30 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.373
ground joinability: 0
find TRSs: 0.513
compute CPs: 0.205
main control loop: 0.94
rewriting: 0.5
SMT solver: 0.041
selection: 0.045
success checks: 0.091
proof
368.85
REL024-1
active equations: 484
iterations: 23
memory: 1762 MB
restarts: 5
problem shape: xeno
time (sec): 
reducibility constraints: 178.593
ground joinability: 0
find TRSs: 193.687
compute CPs: 84.458
main control loop: 132.082
rewriting: 25.202
SMT solver: 2.658
selection: 1.919
success checks: 5.968
 
11.63
REL024-2
active equations: 288
iterations: 14
memory: 92 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 3.636
ground joinability: 0
find TRSs: 4.461
compute CPs: 1.382
main control loop: 6.137
rewriting: 3.301
SMT solver: 0.182
selection: 0.225
success checks: 0.992
 
 
 
 
 
 
 
 
 
 
 
 
142.24
REL031-1
active equations: 803
iterations: 40
memory: 723 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 47.564
ground joinability: 0
find TRSs: 53.635
compute CPs: 9.414
main control loop: 72.547
rewriting: 41.476
SMT solver: 1.612
selection: 1.021
success checks: 3.21
proof
66.38
REL031-2
active equations: 567
iterations: 28
memory: 378 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 17.447
ground joinability: 0
find TRSs: 20.278
compute CPs: 5.86
main control loop: 38.885
rewriting: 24.382
SMT solver: 0.593
selection: 0.832
success checks: 1.258
proof
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
490.05
REL041-2
active equations: 777
iterations: 38
memory: 2680 MB
restarts: 4
problem shape: xeno
time (sec): 
reducibility constraints: 117.375
ground joinability: 0
find TRSs: 127.495
compute CPs: 53.966
main control loop: 323.096
rewriting: 127.692
SMT solver: 1.508
selection: 4.806
success checks: 19.517
 
 
77.95
REL042-2
active equations: 648
iterations: 32
memory: 435 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 28.457
ground joinability: 0
find TRSs: 32.085
compute CPs: 12.809
main control loop: 38.171
rewriting: 19.045
SMT solver: 0.635
selection: 1.113
success checks: 1.298
proof
 
 
 
152.74
REL044-2
active equations: 849
iterations: 42
memory: 876 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 61.655
ground joinability: 0
find TRSs: 68.289
compute CPs: 22.709
main control loop: 69.246
rewriting: 33.702
SMT solver: 1.441
selection: 2.432
success checks: 2.935
proof
 
551.89
REL045-2
active equations: 858
iterations: 42
memory: 2080 MB
restarts: 4
problem shape: xeno
time (sec): 
reducibility constraints: 147.346
ground joinability: 0
find TRSs: 157.932
compute CPs: 108.775
main control loop: 347.974
rewriting: 124.313
SMT solver: 1.306
selection: 5.516
success checks: 11.775
 
 
0.02
REL049-1
active equations: 16
iterations: 1
memory: 3 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0.002
SMT solver: 0.004
selection: 0
success checks: 0
proof
25.69
REL050-1
active equations: 365
iterations: 18
memory: 188 MB
restarts: 2
problem shape: xeno
time (sec): 
reducibility constraints: 6.088
ground joinability: 0
find TRSs: 7.205
compute CPs: 2.102
main control loop: 16.355
rewriting: 7.107
SMT solver: 0.185
selection: 0.329
success checks: 0.723
 
proof
0.04
RNG007-4
active equations: 36
iterations: 2
memory: 3 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.007
SMT solver: 0
selection: 0
success checks: 0.001
proof
0.56
RNG008-3
active equations: 115
iterations: 6
memory: 11 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.119
ground joinability: 0
find TRSs: 0.176
compute CPs: 0.113
main control loop: 0.278
rewriting: 0.142
SMT solver: 0.009
selection: 0.018
success checks: 0.02
proof
0.64
RNG008-4
active equations: 115
iterations: 6
memory: 11 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.138
ground joinability: 0
find TRSs: 0.21
compute CPs: 0.108
main control loop: 0.258
rewriting: 0.166
SMT solver: 0.012
selection: 0.022
success checks: 0.021
proof
2.29
RNG008-7
active equations: 80
iterations: 4
memory: 35 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.501
ground joinability: 0
find TRSs: 0.669
compute CPs: 0.357
main control loop: 1.398
rewriting: 0.662
SMT solver: 0.029
selection: 0.074
success checks: 0.086
proof
 
 
0.02
RNG011-5
active equations: 22
iterations: 1
memory: 3 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.001
selection: 0
success checks: 0
proof
1.50
RNG012-6
active equations: 135
iterations: 7
memory: 26 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.194
ground joinability: 0
find TRSs: 0.278
compute CPs: 0.197
main control loop: 0.826
rewriting: 0.586
SMT solver: 0.016
selection: 0.042
success checks: 0.061
proof
0.38
RNG013-6
active equations: 95
iterations: 5
memory: 9 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.069
ground joinability: 0
find TRSs: 0.111
compute CPs: 0.063
main control loop: 0.221
rewriting: 0.091
SMT solver: 0.009
selection: 0.011
success checks: 0.043
proof
1.24
RNG014-6
active equations: 116
iterations: 6
memory: 23 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.128
ground joinability: 0
find TRSs: 0.183
compute CPs: 0.15
main control loop: 0.671
rewriting: 0.479
SMT solver: 0.011
selection: 0.04
success checks: 0.081
proof
1.39
RNG015-6
active equations: 134
iterations: 7
memory: 23 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.213
ground joinability: 0
find TRSs: 0.303
compute CPs: 0.205
main control loop: 0.898
rewriting: 0.472
SMT solver: 0.021
selection: 0.042
success checks: 0.091
proof
1.44
RNG016-6
active equations: 135
iterations: 7
memory: 23 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.177
ground joinability: 0
find TRSs: 0.262
compute CPs: 0.172
main control loop: 0.909
rewriting: 0.497
SMT solver: 0.021
selection: 0.046
success checks: 0.063
proof
1.97
RNG017-6
active equations: 154
iterations: 8
memory: 30 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.311
ground joinability: 0
find TRSs: 0.425
compute CPs: 0.336
main control loop: 1.334
rewriting: 0.707
SMT solver: 0.028
selection: 0.069
success checks: 0.121
proof
1.84
RNG018-6
active equations: 134
iterations: 7
memory: 30 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.207
ground joinability: 0
find TRSs: 0.289
compute CPs: 0.311
main control loop: 0.933
rewriting: 0.7
SMT solver: 0.021
selection: 0.071
success checks: 0.167
proof
4.54
RNG019-6
active equations: 106
iterations: 5
memory: 61 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.511
ground joinability: 0
find TRSs: 0.702
compute CPs: 0.437
main control loop: 3.672
rewriting: 2.008
SMT solver: 0.053
selection: 0.134
success checks: 0.249
proof
12.60
RNG019-7
active equations: 210
iterations: 10
memory: 107 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 1.305
ground joinability: 0
find TRSs: 1.639
compute CPs: 0.85
main control loop: 8.571
rewriting: 7.647
SMT solver: 0.079
selection: 0.18
success checks: 0.662
proof
6.83
RNG020-6
active equations: 86
iterations: 4
memory: 70 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.529
ground joinability: 0
find TRSs: 0.725
compute CPs: 1.214
main control loop: 5.803
rewriting: 2.671
SMT solver: 0.051
selection: 0.184
success checks: 1.093
proof
42.20
RNG020-7
active equations: 251
iterations: 12
memory: 188 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 1.665
ground joinability: 0
find TRSs: 2.03
compute CPs: 0.947
main control loop: 11.422
rewriting: 35.708
SMT solver: 0.084
selection: 0.214
success checks: 1.252
proof
5.33
RNG021-6
active equations: 86
iterations: 4
memory: 63 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.46
ground joinability: 0
find TRSs: 0.624
compute CPs: 0.495
main control loop: 4.114
rewriting: 2.246
SMT solver: 0.042
selection: 0.145
success checks: 0.294
proof
12.67
RNG021-7
active equations: 210
iterations: 10
memory: 107 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 1.249
ground joinability: 0
find TRSs: 1.559
compute CPs: 0.784
main control loop: 8.922
rewriting: 7.476
SMT solver: 0.073
selection: 0.192
success checks: 0.509
proof
0.02
RNG023-6
active equations: 16
iterations: 1
memory: 3 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.003
main control loop: 0
rewriting: 0.004
SMT solver: 0
selection: 0
success checks: 0
proof
0.06
RNG023-7
active equations: 43
iterations: 2
memory: 3 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.009
main control loop: 0.016
rewriting: 0.015
SMT solver: 0.003
selection: 0.002
success checks: 0.001
proof
0.02
RNG024-6
active equations: 16
iterations: 1
memory: 3 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.003
main control loop: 0
rewriting: 0.004
SMT solver: 0
selection: 0
success checks: 0
proof
0.07
RNG024-7
active equations: 43
iterations: 2
memory: 3 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.024
compute CPs: 0.01
main control loop: 0.018
rewriting: 0.017
SMT solver: 0.003
selection: 0.002
success checks: 0.001
proof
10.99
RNG025-4
active equations: 166
iterations: 8
memory: 117 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.797
ground joinability: 0
find TRSs: 1.025
compute CPs: 0.843
main control loop: 7.804
rewriting: 6.105
SMT solver: 0.058
selection: 0.202
success checks: 0.914
 
 
 
 
9.09
RNG026-6
active equations: 66
iterations: 3
memory: 50 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.431
ground joinability: 0
find TRSs: 0.609
compute CPs: 0.581
main control loop: 7.225
rewriting: 3.926
SMT solver: 0.05
selection: 0.126
success checks: 3.056
proof
5.90
RNG026-7
active equations: 173
iterations: 8
memory: 81 MB
restarts: 1
problem shape: xeno
time (sec): 
reducibility constraints: 0.535
ground joinability: 0
find TRSs: 0.702
compute CPs: 0.852
main control loop: 4.226
rewriting: 3.316
SMT solver: 0.041
selection: 0.087
success checks: 0.365
proof
 
 
 
 
 
 
 
 
 
 
 
 
0.28
RNG128-1
active equations: 86
iterations: 5
memory: 5 MB
restarts: 0
problem shape: xeno
time (sec): 
reducibility constraints: 0.083
ground joinability: 0
find TRSs: 0.117
compute CPs: 0.034
main control loop: 0.139
rewriting: 0.048
SMT solver: 0.005
selection: 0.005
success checks: 0.019
proof
 
0.27
ROB002-1
active equations: 17
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.017
main control loop: 0.033
rewriting: 0.205
SMT solver: 0
selection: 0.004
success checks: 0.003
proof
1.77
ROB003-1
active equations: 101
iterations: 9
memory: 17 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.16
ground joinability: 0
find TRSs: 0.221
compute CPs: 0.12
main control loop: 1.22
rewriting: 0.84
SMT solver: 0.004
selection: 0.01
success checks: 0.081
proof
14.10
ROB004-1
active equations: 135
iterations: 11
memory: 53 MB
restarts: 2
problem shape: none
time (sec): 
reducibility constraints: 1.207
ground joinability: 0
find TRSs: 1.545
compute CPs: 0.309
main control loop: 9.06
rewriting: 8.679
SMT solver: 0.062
selection: 0.046
success checks: 0.327
proof
 
 
 
0.15
ROB008-1
active equations: 29
iterations: 3
memory: 2 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.015
main control loop: 0.054
rewriting: 0.098
SMT solver: 0
selection: 0.003
success checks: 0.001
proof
0.02
ROB009-1
active equations: 5
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0.002
main control loop: 0
rewriting: 0.009
SMT solver: 0
selection: 0
success checks: 0
proof
0.09
ROB010-1
active equations: 17
iterations: 2
memory: 1 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.008
main control loop: 0.037
rewriting: 0.061
SMT solver: 0
selection: 0.002
success checks: 0.002
proof
0.07
ROB013-1
active equations: 17
iterations: 2
memory: 1 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.007
main control loop: 0.033
rewriting: 0.046
SMT solver: 0
selection: 0.001
success checks: 0.001
proof
297.46
ROB022-1
active equations: 137
iterations: 11
memory: 3544 MB
restarts: 3
problem shape: none
time (sec): 
reducibility constraints: 78.993
ground joinability: 0
find TRSs: 82.594
compute CPs: 13.632
main control loop: 187.245
rewriting: 80.576
SMT solver: 0.103
selection: 0.406
success checks: 70.574
proof
2.88
ROB023-1
active equations: 101
iterations: 9
memory: 18 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.297
ground joinability: 0
find TRSs: 0.357
compute CPs: 0.206
main control loop: 1.861
rewriting: 1.759
SMT solver: 0.003
selection: 0.03
success checks: 0.096
proof
 
0.01
ROB030-1
active equations: 5
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0.001
main control loop: 0
rewriting: 0.006
SMT solver: 0
selection: 0
success checks: 0
proof
 
 
 
 
 
 
 
0.01
SWV243-2
active equations: 2
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.01
SWV262-2
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.001
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
SWV818-1
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
SWV819-1
active equations: 3
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
SYN080-1
active equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
0.00
SYN083-1
active equations: 1
iterations: 1
memory: 3 MB
restarts: 0
problem shape: zolfo
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
proof
max_iterations 42
equalities 987
restarts 253
successes 621
timeouts 275
time/overlaps 2705s (22%)
time/maxk 2161s (18%)
time/rewrite 3793s (32%)
time/select 174s (1%)
time/sat 31s (0%)
time/success checks 691s (6%)
total time 12025.289
average time 19.36
average memory 215 MB
errors 1
OVERALL STATS
solved621
diff solved0