maedmax: Maximal Ordered Completion
Home web interface
maedmax
download experiments usage options
blabla

MaedMax Experiment : ConCon examples

maedmax make narrowing normalizing, select always 1 old goal --json -K 3
E -s
Vampire Vampire ConCon examples
waldmeister waldmeister waldmeister
272.0.0
0.02
272.0.0
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
∞
272.0.1
0.01
272.0.1
equations: 10
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
272.0.2
0.01
272.0.2
equations: 10
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
272.1.0
0.02
272.1.0
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
∞
272.1.1
0.01
272.1.1
equations: 10
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
272.1.2
0.01
272.1.2
equations: 10
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
273.0.0
0.01
273.0.0
equations: 6
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
0.00
0.00
0.00
274.0.0
0.00
274.0.0
equations: 7
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
0.00
0.00
0.00
274.0.1
0.01
274.0.1
equations: 7
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
0.00
0.00
0.00
274.0.2
0.01
274.0.2
equations: 7
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
0.00
0.00
0.00
274.1.0
0.01
274.1.0
equations: 7
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
0.00
0.00
0.00
274.2.0
0.01
274.2.0
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
274.3.0
0.01
274.3.0
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.001
selection: 0
success checks: 0
0.00
0.00
0.00
275.0.0
0.01
275.0.0
equations: 8
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
275.0.1
0.01
275.0.1
equations: 8
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
275.0.2
0.01
275.0.2
equations: 8
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
275.1.0
0.01
275.1.0
equations: 8
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
275.2.0
0.01
275.2.0
equations: 8
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
275.3.0
0.01
275.3.0
equations: 8
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
276.0.0
0.00
276.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
278.0.0
0.02
278.0.0
equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
278.0.1
0.03
278.0.1
equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
278.0.10
0.06
278.0.10
equations: 37
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.033
compute CPs: 0.001
main control loop: 0.006
rewriting: 0.004
SMT solver: 0.024
selection: 0.001
success checks: 0.001
0.00
0.00
0.00
278.0.11
∞
∞
∞
∞
278.0.12
0.10
278.0.12
equations: 34
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.073
compute CPs: 0
main control loop: 0.005
rewriting: 0.003
SMT solver: 0.062
selection: 0
success checks: 0.001
0.00
0.00
0.00
278.0.13
∞
∞
∞
∞
278.0.14
∞
∞
∞
∞
278.0.2
0.03
278.0.2
equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.016
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.013
selection: 0
success checks: 0
0.00
0.00
0.00
278.0.3
0.02
278.0.3
equations: 19
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
278.0.4
0.06
278.0.4
equations: 37
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.036
compute CPs: 0.002
main control loop: 0.005
rewriting: 0.001
SMT solver: 0.026
selection: 0
success checks: 0.001
0.00
0.00
0.00
278.0.5
∞
∞
∞
∞
278.0.6
0.03
278.0.6
equations: 19
iterations: 1
memory: 0 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
278.0.7
0.09
278.0.7
equations: 37
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.066
compute CPs: 0.001
main control loop: 0.009
rewriting: 0.002
SMT solver: 0.05
selection: 0
success checks: 0.002
0.00
0.00
0.00
278.0.8
0.11
278.0.8
equations: 37
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.047
compute CPs: 0.004
main control loop: 0.011
rewriting: 0.008
SMT solver: 0.03
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
278.0.9
0.11
278.0.9
equations: 31
iterations: 2
memory: 1 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.006
ground joinability: 0
find TRSs: 0.085
compute CPs: 0.001
main control loop: 0.003
rewriting: 0.001
SMT solver: 0.07
selection: 0
success checks: 0
0.00
0.00
0.00
279.0.0
0.05
279.0.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.013
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.0.1
0.09
279.0.1
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.053
compute CPs: 0.003
main control loop: 0.008
rewriting: 0.001
SMT solver: 0.034
selection: 0
success checks: 0.002
0.00
0.00
0.00
279.0.2
0.05
279.0.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.028
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.022
selection: 0
success checks: 0
0.00
0.00
0.00
279.0.3
0.26
279.0.3
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.027
ground joinability: 0
find TRSs: 0.146
compute CPs: 0.012
main control loop: 0.062
rewriting: 0.014
SMT solver: 0.1
selection: 0.003
success checks: 0.021
0.00
0.01
0.00
279.0.4
0.13
279.0.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.094
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.069
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.0.5
0.10
279.0.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.068
compute CPs: 0.003
main control loop: 0.009
rewriting: 0.003
SMT solver: 0.048
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.0.6
0.28
279.0.6
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.148
compute CPs: 0.013
main control loop: 0.088
rewriting: 0.022
SMT solver: 0.107
selection: 0.004
success checks: 0.022
0.00
0.02
∞
279.1.0
0.05
279.1.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.1.1
0.06
279.1.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.023
compute CPs: 0.004
main control loop: 0
rewriting: 0.002
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.1.2
0.06
279.1.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.032
compute CPs: 0.004
main control loop: 0
rewriting: 0.002
SMT solver: 0.022
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.1.3
0.14
279.1.3
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.088
compute CPs: 0.008
main control loop: 0.013
rewriting: 0.005
SMT solver: 0.064
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
279.1.4
0.13
279.1.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.082
compute CPs: 0.006
main control loop: 0.012
rewriting: 0.006
SMT solver: 0.064
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.1.5
0.15
279.1.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.112
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.087
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.1.6
0.14
279.1.6
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.076
compute CPs: 0.007
main control loop: 0.021
rewriting: 0.007
SMT solver: 0.051
selection: 0.002
success checks: 0.006
0.00
0.00
0.00
279.10.0
0.09
279.10.0
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.05
compute CPs: 0.004
main control loop: 0.013
rewriting: 0.002
SMT solver: 0.032
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.10.1
0.06
279.10.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.037
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.027
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.10.10
0.85
279.10.10
equations: 78
iterations: 4
memory: 15 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.103
ground joinability: 0
find TRSs: 0.418
compute CPs: 0.108
main control loop: 0.187
rewriting: 0.065
SMT solver: 0.279
selection: 0.008
success checks: 0.045
0.00
0.25
∞
279.10.11
0.62
279.10.11
equations: 79
iterations: 4
memory: 8 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.078
ground joinability: 0
find TRSs: 0.354
compute CPs: 0.075
main control loop: 0.172
rewriting: 0.034
SMT solver: 0.216
selection: 0.005
success checks: 0.03
0.00
0.14
∞
279.10.12
0.28
279.10.12
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.135
compute CPs: 0.016
main control loop: 0.106
rewriting: 0.024
SMT solver: 0.094
selection: 0.007
success checks: 0.026
0.00
0.03
∞
279.10.13
0.30
279.10.13
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.026
ground joinability: 0
find TRSs: 0.157
compute CPs: 0.016
main control loop: 0.108
rewriting: 0.024
SMT solver: 0.11
selection: 0.007
success checks: 0.027
0.00
0.03
∞
279.10.14
∞
0.00
29.78
∞
279.10.2
0.10
279.10.2
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.06
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.002
SMT solver: 0.04
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.10.3
0.04
279.10.3
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.026
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.017
selection: 0
success checks: 0
0.00
0.00
0.00
279.10.4
0.12
279.10.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.073
compute CPs: 0.004
main control loop: 0.017
rewriting: 0.003
SMT solver: 0.049
selection: 0.001
success checks: 0.004
0.00
0.00
0.00
279.10.5
0.16
279.10.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.082
compute CPs: 0.018
main control loop: 0.018
rewriting: 0.009
SMT solver: 0.056
selection: 0.002
success checks: 0.006
0.00
0.01
0.00
279.10.6
0.23
279.10.6
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.02
ground joinability: 0
find TRSs: 0.122
compute CPs: 0.013
main control loop: 0.068
rewriting: 0.016
SMT solver: 0.084
selection: 0.003
success checks: 0.024
0.00
0.01
0.00
279.10.7
0.26
279.10.7
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.137
compute CPs: 0.014
main control loop: 0.078
rewriting: 0.017
SMT solver: 0.093
selection: 0.004
success checks: 0.025
0.00
0.00
0.00
279.10.8
0.28
279.10.8
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.026
ground joinability: 0
find TRSs: 0.158
compute CPs: 0.013
main control loop: 0.077
rewriting: 0.016
SMT solver: 0.109
selection: 0.005
success checks: 0.026
0.00
0.00
0.00
279.10.9
0.38
279.10.9
equations: 80
iterations: 4
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.067
ground joinability: 0
find TRSs: 0.222
compute CPs: 0.025
main control loop: 0.106
rewriting: 0.018
SMT solver: 0.119
selection: 0.002
success checks: 0.019
0.00
0.02
0.00
279.11.0
0.05
279.11.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.11.1
0.14
279.11.1
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.016
ground joinability: 0
find TRSs: 0.085
compute CPs: 0.006
main control loop: 0.016
rewriting: 0.003
SMT solver: 0.051
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.11.2
0.05
279.11.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.029
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.023
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.11.3
0.25
279.11.3
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.029
ground joinability: 0
find TRSs: 0.145
compute CPs: 0.011
main control loop: 0.06
rewriting: 0.013
SMT solver: 0.095
selection: 0.003
success checks: 0.024
0.00
0.01
0.00
279.11.4
0.28
279.11.4
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.026
ground joinability: 0
find TRSs: 0.161
compute CPs: 0.024
main control loop: 0.062
rewriting: 0.014
SMT solver: 0.113
selection: 0.003
success checks: 0.013
0.00
0.00
0.00
279.11.5
0.14
279.11.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.095
compute CPs: 0.008
main control loop: 0.016
rewriting: 0.004
SMT solver: 0.071
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.11.6
0.40
279.11.6
equations: 80
iterations: 4
memory: 7 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.053
ground joinability: 0
find TRSs: 0.209
compute CPs: 0.019
main control loop: 0.134
rewriting: 0.034
SMT solver: 0.126
selection: 0.009
success checks: 0.031
0.00
0.06
0.00
279.12.0
0.05
279.12.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.12.1
0.05
279.12.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.013
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.12.2
0.15
279.12.2
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.11
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.085
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.13.0
0.05
279.13.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.13.1
0.05
279.13.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.13.2
0.06
279.13.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.031
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.022
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.13.3
0.11
279.13.3
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.06
compute CPs: 0.007
main control loop: 0.01
rewriting: 0.005
SMT solver: 0.045
selection: 0.001
success checks: 0.003
0.00
0.01
0.00
279.13.4
0.16
279.13.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.098
compute CPs: 0.008
main control loop: 0.018
rewriting: 0.007
SMT solver: 0.072
selection: 0.002
success checks: 0.004
0.00
0.00
0.00
279.13.5
0.19
279.13.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.098
compute CPs: 0.028
main control loop: 0.012
rewriting: 0.006
SMT solver: 0.069
selection: 0.002
success checks: 0.004
0.00
0.00
0.00
279.13.6
0.16
279.13.6
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.076
compute CPs: 0.013
main control loop: 0.02
rewriting: 0.012
SMT solver: 0.052
selection: 0.002
success checks: 0.008
0.00
0.00
0.00
279.14.0
0.05
279.14.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.14.1
0.04
279.14.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.017
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.14.2
0.06
279.14.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.03
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.022
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.14.3
0.13
279.14.3
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.068
compute CPs: 0.019
main control loop: 0.006
rewriting: 0.004
SMT solver: 0.048
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
279.14.4
0.14
279.14.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.081
compute CPs: 0.009
main control loop: 0.013
rewriting: 0.008
SMT solver: 0.064
selection: 0.001
success checks: 0.004
0.00
0.00
0.00
279.14.5
0.16
279.14.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.098
compute CPs: 0.008
main control loop: 0.019
rewriting: 0.008
SMT solver: 0.072
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.14.6
0.18
279.14.6
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.094
compute CPs: 0.013
main control loop: 0.02
rewriting: 0.011
SMT solver: 0.069
selection: 0.002
success checks: 0.009
0.00
0.01
0.00
279.15.0
0.05
279.15.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.15.1
0.04
279.15.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.014
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.15.2
0.05
279.15.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.15.3
0.16
279.15.3
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.113
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.087
selection: 0.002
success checks: 0.003
0.00
0.00
0.00
279.15.4
0.15
279.15.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.086
compute CPs: 0.008
main control loop: 0.019
rewriting: 0.008
SMT solver: 0.065
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.15.5
0.13
279.15.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.086
compute CPs: 0.007
main control loop: 0.012
rewriting: 0.005
SMT solver: 0.062
selection: 0
success checks: 0.002
0.00
0.00
0.00
279.15.6
0.09
279.15.6
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.049
compute CPs: 0.005
main control loop: 0.013
rewriting: 0.004
SMT solver: 0.034
selection: 0.001
success checks: 0.003
0.00
0.01
0.00
279.16.0
0.04
279.16.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.16.1
0.05
279.16.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.024
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.017
selection: 0
success checks: 0
0.00
0.00
0.00
279.16.2
0.05
279.16.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.023
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0.013
selection: 0
success checks: 0
0.00
0.00
0.00
279.16.3
0.14
279.16.3
equations: 44
iterations: 2
memory: 1 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.095
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.003
SMT solver: 0.07
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.16.4
0.11
279.16.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.069
compute CPs: 0.004
main control loop: 0.016
rewriting: 0.004
SMT solver: 0.045
selection: 0
success checks: 0.004
0.00
0.00
0.00
279.16.5
0.15
279.16.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.092
compute CPs: 0.007
main control loop: 0.018
rewriting: 0.007
SMT solver: 0.067
selection: 0.002
success checks: 0.004
0.00
0.00
0.00
279.16.6
0.28
279.16.6
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.041
ground joinability: 0
find TRSs: 0.17
compute CPs: 0.016
main control loop: 0.072
rewriting: 0.011
SMT solver: 0.105
selection: 0.002
success checks: 0.018
0.00
0.00
0.00
279.17.0
0.05
279.17.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.17.1
0.12
279.17.1
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.073
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.002
SMT solver: 0.047
selection: 0
success checks: 0.004
0.00
0.00
0.00
279.17.2
0.06
279.17.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.034
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.024
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.17.3
0.28
279.17.3
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.028
ground joinability: 0
find TRSs: 0.159
compute CPs: 0.015
main control loop: 0.076
rewriting: 0.017
SMT solver: 0.108
selection: 0.004
success checks: 0.025
0.00
0.01
0.00
279.17.4
0.16
279.17.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.104
compute CPs: 0.011
main control loop: 0.016
rewriting: 0.005
SMT solver: 0.079
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.17.5
0.24
279.17.5
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.023
ground joinability: 0
find TRSs: 0.14
compute CPs: 0.018
main control loop: 0.054
rewriting: 0.011
SMT solver: 0.095
selection: 0.003
success checks: 0.012
0.00
0.00
0.00
279.17.6
0.43
279.17.6
equations: 80
iterations: 4
memory: 7 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.056
ground joinability: 0
find TRSs: 0.232
compute CPs: 0.022
main control loop: 0.151
rewriting: 0.037
SMT solver: 0.143
selection: 0.01
success checks: 0.03
0.00
0.03
0.00
279.18.0
0.04
279.18.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.015
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.18.1
0.06
279.18.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.032
compute CPs: 0.004
main control loop: 0
rewriting: 0.002
SMT solver: 0.022
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.18.10
0.34
279.18.10
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.028
ground joinability: 0
find TRSs: 0.152
compute CPs: 0.03
main control loop: 0.097
rewriting: 0.031
SMT solver: 0.103
selection: 0.007
success checks: 0.027
0.00
0.03
0.00
279.18.11
0.29
279.18.11
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.021
ground joinability: 0
find TRSs: 0.154
compute CPs: 0.023
main control loop: 0.054
rewriting: 0.028
SMT solver: 0.112
selection: 0.006
success checks: 0.012
0.00
0.00
0.00
279.18.12
0.41
279.18.12
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.04
ground joinability: 0
find TRSs: 0.252
compute CPs: 0.032
main control loop: 0.093
rewriting: 0.02
SMT solver: 0.189
selection: 0.005
success checks: 0.019
0.00
0.01
0.00
279.18.13
1.92
279.18.13
equations: 133
iterations: 7
memory: 30 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.304
ground joinability: 0
find TRSs: 0.901
compute CPs: 0.3
main control loop: 0.623
rewriting: 0.162
SMT solver: 0.503
selection: 0.019
success checks: 0.084
0.00
0.06
∞
279.18.14
15.66
279.18.14
equations: 175
iterations: 9
memory: 476 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 1.813
ground joinability: 0
find TRSs: 3.287
compute CPs: 2.881
main control loop: 10.329
rewriting: 0.803
SMT solver: 1.238
selection: 0.038
success checks: 5.113
0.00
0.65
∞
279.18.2
0.11
279.18.2
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.072
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.002
SMT solver: 0.047
selection: 0
success checks: 0.004
0.00
0.00
0.00
279.18.3
0.06
279.18.3
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.035
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.026
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.18.4
0.13
279.18.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.084
compute CPs: 0.004
main control loop: 0.016
rewriting: 0.003
SMT solver: 0.062
selection: 0.001
success checks: 0.004
0.00
0.00
0.00
279.18.5
0.37
279.18.5
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.034
ground joinability: 0
find TRSs: 0.23
compute CPs: 0.026
main control loop: 0.081
rewriting: 0.017
SMT solver: 0.173
selection: 0.004
success checks: 0.016
0.00
0.01
0.00
279.18.6
0.30
279.18.6
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.03
ground joinability: 0
find TRSs: 0.167
compute CPs: 0.015
main control loop: 0.081
rewriting: 0.018
SMT solver: 0.114
selection: 0.004
success checks: 0.028
0.00
0.00
0.00
279.18.7
0.14
279.18.7
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.09
compute CPs: 0.006
main control loop: 0.018
rewriting: 0.006
SMT solver: 0.065
selection: 0.001
success checks: 0.004
0.00
0.00
0.00
279.18.8
0.13
279.18.8
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.015
ground joinability: 0
find TRSs: 0.093
compute CPs: 0.003
main control loop: 0.01
rewriting: 0.003
SMT solver: 0.065
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.18.9
0.26
279.18.9
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.023
ground joinability: 0
find TRSs: 0.153
compute CPs: 0.021
main control loop: 0.066
rewriting: 0.013
SMT solver: 0.109
selection: 0.003
success checks: 0.014
0.00
0.01
0.00
279.19.0
0.04
279.19.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.19.1
0.05
279.19.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.013
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.19.2
0.06
279.19.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.031
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.021
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.19.3
0.13
279.19.3
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.082
compute CPs: 0.006
main control loop: 0.012
rewriting: 0.004
SMT solver: 0.059
selection: 0
success checks: 0.002
0.00
0.00
0.00
279.19.4
0.15
279.19.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.11
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.086
selection: 0.002
success checks: 0.003
0.00
0.00
0.00
279.19.5
0.15
279.19.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.091
compute CPs: 0.008
main control loop: 0.018
rewriting: 0.008
SMT solver: 0.067
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.19.6
0.16
279.19.6
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.084
compute CPs: 0.007
main control loop: 0.022
rewriting: 0.007
SMT solver: 0.058
selection: 0.002
success checks: 0.006
0.00
0.01
0.00
279.2.0
0.04
279.2.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.008
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.2.1
0.11
279.2.1
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.067
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.002
SMT solver: 0.043
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.2.10
∞
∞
∞
∞
279.2.11
0.19
279.2.11
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.102
compute CPs: 0.01
main control loop: 0.021
rewriting: 0.014
SMT solver: 0.081
selection: 0.001
success checks: 0.009
0.00
0.02
0.00
279.2.12
0.11
279.2.12
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.046
compute CPs: 0.007
main control loop: 0.012
rewriting: 0.011
SMT solver: 0.032
selection: 0.002
success checks: 0.008
0.00
0.01
0.00
279.2.13
∞
∞
∞
∞
279.2.14
∞
∞
∞
∞
279.2.2
0.05
279.2.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.025
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.019
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.2.3
0.11
279.2.3
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.008
ground joinability: 0
find TRSs: 0.062
compute CPs: 0.006
main control loop: 0
rewriting: 0.003
SMT solver: 0.043
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.2.4
0.18
279.2.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.102
compute CPs: 0.022
main control loop: 0.015
rewriting: 0.008
SMT solver: 0.077
selection: 0.003
success checks: 0.004
0.00
0.00
0.00
279.2.5
0.22
279.2.5
equations: 62
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.019
ground joinability: 0
find TRSs: 0.137
compute CPs: 0.013
main control loop: 0.036
rewriting: 0.01
SMT solver: 0.101
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.2.6
∞
∞
∞
∞
279.2.7
0.29
279.2.7
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.029
ground joinability: 0
find TRSs: 0.161
compute CPs: 0.015
main control loop: 0.081
rewriting: 0.018
SMT solver: 0.111
selection: 0.004
success checks: 0.028
0.00
0.01
0.00
279.2.8
0.14
279.2.8
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.084
compute CPs: 0.008
main control loop: 0.019
rewriting: 0.008
SMT solver: 0.058
selection: 0.002
success checks: 0.005
0.00
0.01
0.00
279.2.9
0.15
279.2.9
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.092
compute CPs: 0.007
main control loop: 0.016
rewriting: 0.005
SMT solver: 0.067
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.20.0
0.11
279.20.0
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.069
compute CPs: 0.005
main control loop: 0.014
rewriting: 0.002
SMT solver: 0.044
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.20.1
0.06
279.20.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.034
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.025
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.20.2
0.04
279.20.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.008
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.20.3
0.12
279.20.3
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.084
compute CPs: 0.003
main control loop: 0.01
rewriting: 0.003
SMT solver: 0.056
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.20.4
0.26
279.20.4
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.023
ground joinability: 0
find TRSs: 0.137
compute CPs: 0.015
main control loop: 0.079
rewriting: 0.017
SMT solver: 0.095
selection: 0.004
success checks: 0.027
0.00
0.01
0.00
279.20.5
0.15
279.20.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.109
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.081
selection: 0
success checks: 0.003
0.00
0.01
0.00
279.20.6
0.29
279.20.6
equations: 62
iterations: 3
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.02
ground joinability: 0
find TRSs: 0.136
compute CPs: 0.013
main control loop: 0.106
rewriting: 0.026
SMT solver: 0.095
selection: 0.004
success checks: 0.027
0.00
0.01
∞
279.3.0
0.05
279.3.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.3.1
0.12
279.3.1
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.013
ground joinability: 0
find TRSs: 0.073
compute CPs: 0.005
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.046
selection: 0
success checks: 0.004
0.00
0.00
0.00
279.3.2
0.06
279.3.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.035
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.026
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.3.3
0.29
279.3.3
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.03
ground joinability: 0
find TRSs: 0.163
compute CPs: 0.015
main control loop: 0.082
rewriting: 0.018
SMT solver: 0.111
selection: 0.004
success checks: 0.028
0.00
0.01
0.00
279.3.4
0.11
279.3.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.074
compute CPs: 0.003
main control loop: 0.01
rewriting: 0.002
SMT solver: 0.047
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.3.5
0.24
279.3.5
equations: 62
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.031
ground joinability: 0
find TRSs: 0.179
compute CPs: 0.007
main control loop: 0.031
rewriting: 0.006
SMT solver: 0.129
selection: 0
success checks: 0.007
0.00
0.01
0.00
279.3.6
1.10
279.3.6
equations: 98
iterations: 5
memory: 15 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.203
ground joinability: 0
find TRSs: 0.609
compute CPs: 0.148
main control loop: 0.403
rewriting: 0.06
SMT solver: 0.349
selection: 0.006
success checks: 0.106
0.00
0.02
∞
279.4.0
0.05
279.4.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.4.1
0.05
279.4.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.4.2
0.14
279.4.2
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.094
compute CPs: 0.01
main control loop: 0.014
rewriting: 0.004
SMT solver: 0.07
selection: 0.002
success checks: 0.003
0.00
0.00
0.00
279.5.0
0.05
279.5.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.5.1
0.05
279.5.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.5.2
0.15
279.5.2
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.109
compute CPs: 0.004
main control loop: 0.015
rewriting: 0.002
SMT solver: 0.085
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.6.0
0.05
279.6.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.6.1
0.09
279.6.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.037
compute CPs: 0.006
main control loop: 0
rewriting: 0.002
SMT solver: 0.02
selection: 0
success checks: 0.002
0.00
0.00
0.00
279.6.10
0.15
279.6.10
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.073
compute CPs: 0.014
main control loop: 0.02
rewriting: 0.012
SMT solver: 0.053
selection: 0.002
success checks: 0.009
0.00
0.01
0.00
279.6.11
0.16
279.6.11
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.086
compute CPs: 0.012
main control loop: 0.024
rewriting: 0.01
SMT solver: 0.067
selection: 0.002
success checks: 0.006
0.00
0.01
0.00
279.6.12
0.18
279.6.12
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.079
compute CPs: 0.014
main control loop: 0.02
rewriting: 0.022
SMT solver: 0.059
selection: 0.003
success checks: 0.01
0.00
0.01
0.00
279.6.13
0.19
279.6.13
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.093
compute CPs: 0.014
main control loop: 0.022
rewriting: 0.019
SMT solver: 0.069
selection: 0.003
success checks: 0.01
0.00
0.01
0.00
279.6.14
1.31
279.6.14
equations: 115
iterations: 6
memory: 17 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.191
ground joinability: 0
find TRSs: 0.665
compute CPs: 0.116
main control loop: 0.531
rewriting: 0.131
SMT solver: 0.402
selection: 0.01
success checks: 0.077
0.00
0.02
0.00
279.6.2
0.06
279.6.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.031
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.022
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.6.3
0.08
279.6.3
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.041
compute CPs: 0.005
main control loop: 0
rewriting: 0.002
SMT solver: 0.03
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.6.4
0.13
279.6.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.069
compute CPs: 0.02
main control loop: 0.009
rewriting: 0.005
SMT solver: 0.047
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.6.5
0.15
279.6.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.09
compute CPs: 0.008
main control loop: 0.019
rewriting: 0.008
SMT solver: 0.066
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.6.6
0.17
279.6.6
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.094
compute CPs: 0.011
main control loop: 0.016
rewriting: 0.009
SMT solver: 0.07
selection: 0.002
success checks: 0.006
0.00
0.01
0.00
279.6.7
0.13
279.6.7
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.081
compute CPs: 0.006
main control loop: 0.019
rewriting: 0.006
SMT solver: 0.057
selection: 0.001
success checks: 0.004
0.00
0.00
0.00
279.6.8
0.13
279.6.8
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.079
compute CPs: 0.005
main control loop: 0.018
rewriting: 0.005
SMT solver: 0.055
selection: 0
success checks: 0.004
0.00
0.00
0.00
279.6.9
0.10
279.6.9
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.007
ground joinability: 0
find TRSs: 0.059
compute CPs: 0.005
main control loop: 0.012
rewriting: 0.005
SMT solver: 0.044
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
279.7.0
0.05
279.7.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.7.1
0.06
279.7.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.029
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.02
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.7.10
0.17
279.7.10
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.074
compute CPs: 0.011
main control loop: 0.021
rewriting: 0.017
SMT solver: 0.05
selection: 0.004
success checks: 0.012
0.00
0.02
0.00
279.7.11
∞
∞
∞
∞
279.7.12
0.18
279.7.12
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.104
compute CPs: 0.009
main control loop: 0.019
rewriting: 0.013
SMT solver: 0.079
selection: 0.001
success checks: 0.008
0.00
0.02
0.00
279.7.13
∞
∞
∞
∞
279.7.14
∞
∞
∞
∞
279.7.2
0.10
279.7.2
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.058
compute CPs: 0.004
main control loop: 0.013
rewriting: 0.002
SMT solver: 0.034
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.7.3
0.06
279.7.3
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.034
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.025
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.7.4
0.13
279.7.4
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.083
compute CPs: 0.007
main control loop: 0.016
rewriting: 0.005
SMT solver: 0.062
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.7.5
∞
∞
∞
∞
279.7.6
0.26
279.7.6
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.026
ground joinability: 0
find TRSs: 0.141
compute CPs: 0.014
main control loop: 0.079
rewriting: 0.017
SMT solver: 0.093
selection: 0.004
success checks: 0.027
0.00
0.00
0.00
279.7.7
0.25
279.7.7
equations: 62
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.145
compute CPs: 0.019
main control loop: 0.04
rewriting: 0.014
SMT solver: 0.104
selection: 0.002
success checks: 0.007
0.00
0.01
0.00
279.7.8
0.15
279.7.8
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.09
compute CPs: 0.007
main control loop: 0.018
rewriting: 0.007
SMT solver: 0.065
selection: 0.002
success checks: 0.005
0.00
0.00
0.00
279.7.9
0.17
279.7.9
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.011
ground joinability: 0
find TRSs: 0.097
compute CPs: 0.022
main control loop: 0.015
rewriting: 0.007
SMT solver: 0.075
selection: 0.002
success checks: 0.004
0.00
0.00
0.00
279.8.0
0.10
279.8.0
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.065
compute CPs: 0.004
main control loop: 0.013
rewriting: 0.002
SMT solver: 0.041
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.8.1
0.06
279.8.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.036
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.026
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.8.2
0.05
279.8.2
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.013
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.8.3
0.12
279.8.3
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.01
ground joinability: 0
find TRSs: 0.072
compute CPs: 0.005
main control loop: 0.019
rewriting: 0.004
SMT solver: 0.05
selection: 0.001
success checks: 0.004
0.00
0.00
0.00
279.8.4
0.23
279.8.4
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.024
ground joinability: 0
find TRSs: 0.129
compute CPs: 0.012
main control loop: 0.065
rewriting: 0.015
SMT solver: 0.087
selection: 0.003
success checks: 0.023
0.00
0.01
0.00
279.8.5
0.27
279.8.5
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.033
ground joinability: 0
find TRSs: 0.161
compute CPs: 0.015
main control loop: 0.067
rewriting: 0.008
SMT solver: 0.106
selection: 0.001
success checks: 0.019
0.00
0.01
0.00
279.8.6
0.72
279.8.6
equations: 97
iterations: 5
memory: 15 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.125
ground joinability: 0
find TRSs: 0.395
compute CPs: 0.096
main control loop: 0.264
rewriting: 0.044
SMT solver: 0.235
selection: 0.004
success checks: 0.065
0.00
0.03
∞
279.9.0
0.05
279.9.0
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.9.1
0.06
279.9.1
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.029
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.021
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.9.10
0.16
279.9.10
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.094
compute CPs: 0.008
main control loop: 0.023
rewriting: 0.01
SMT solver: 0.069
selection: 0.001
success checks: 0.006
0.00
0.00
0.00
279.9.11
0.29
279.9.11
equations: 62
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.026
ground joinability: 0
find TRSs: 0.154
compute CPs: 0.015
main control loop: 0.061
rewriting: 0.024
SMT solver: 0.106
selection: 0.003
success checks: 0.013
0.00
0.02
0.00
279.9.12
1.39
279.9.12
equations: 116
iterations: 6
memory: 17 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.221
ground joinability: 0
find TRSs: 0.633
compute CPs: 0.166
main control loop: 0.487
rewriting: 0.131
SMT solver: 0.334
selection: 0.014
success checks: 0.064
0.00
0.07
∞
279.9.13
0.42
279.9.13
equations: 80
iterations: 4
memory: 7 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.051
ground joinability: 0
find TRSs: 0.218
compute CPs: 0.021
main control loop: 0.146
rewriting: 0.036
SMT solver: 0.134
selection: 0.01
success checks: 0.029
0.00
0.02
0.00
279.9.14
8.41
279.9.14
equations: 103
iterations: 5
memory: 216 MB
restarts: 1
problem shape: none
time (sec): 
reducibility constraints: 0.963
ground joinability: 0
find TRSs: 2
compute CPs: 1.025
main control loop: 6.048
rewriting: 0.573
SMT solver: 0.852
selection: 0.033
success checks: 2.042
0.00
0.73
0.00
279.9.2
0.11
279.9.2
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.068
compute CPs: 0.005
main control loop: 0.013
rewriting: 0.002
SMT solver: 0.044
selection: 0
success checks: 0.003
0.00
0.00
0.00
279.9.3
0.06
279.9.3
equations: 26
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.033
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.024
selection: 0
success checks: 0.001
0.00
0.00
0.00
279.9.4
0.23
279.9.4
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.019
ground joinability: 0
find TRSs: 0.12
compute CPs: 0.013
main control loop: 0.072
rewriting: 0.016
SMT solver: 0.084
selection: 0.004
success checks: 0.024
0.00
0.00
0.00
279.9.5
0.15
279.9.5
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.012
ground joinability: 0
find TRSs: 0.101
compute CPs: 0.011
main control loop: 0.015
rewriting: 0.004
SMT solver: 0.077
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
279.9.6
0.37
279.9.6
equations: 80
iterations: 4
memory: 5 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.059
ground joinability: 0
find TRSs: 0.228
compute CPs: 0.027
main control loop: 0.067
rewriting: 0.021
SMT solver: 0.134
selection: 0.003
success checks: 0.008
0.00
0.01
0.00
279.9.7
0.28
279.9.7
equations: 62
iterations: 3
memory: 4 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.022
ground joinability: 0
find TRSs: 0.162
compute CPs: 0.023
main control loop: 0.063
rewriting: 0.015
SMT solver: 0.117
selection: 0.003
success checks: 0.014
0.00
0.01
0.00
279.9.8
0.13
279.9.8
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.075
compute CPs: 0.007
main control loop: 0.018
rewriting: 0.007
SMT solver: 0.055
selection: 0.002
success checks: 0.004
0.00
0.00
0.00
279.9.9
0.13
279.9.9
equations: 44
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.009
ground joinability: 0
find TRSs: 0.073
compute CPs: 0.006
main control loop: 0.011
rewriting: 0.007
SMT solver: 0.054
selection: 0.002
success checks: 0.007
0.00
0.01
0.00
284.0.0
0.01
284.0.0
equations: 7
iterations: 1
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
0.00
0.00
0.00
284.0.1
0.00
284.0.1
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
284.0.2
0.01
284.0.2
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
284.1.0
0.01
284.1.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
284.2.0
0.01
284.2.0
equations: 7
iterations: 1
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
0.00
0.00
∞
284.3.0
0.00
284.3.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
284.4.0
0.00
284.4.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
284.4.1
0.00
284.4.1
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
284.4.2
0.01
284.4.2
equations: 7
iterations: 1
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
0.00
0.00
0.00
285.0.0
0.00
285.0.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
285.1.0
0.00
285.1.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
285.2.0
0.00
285.2.0
equations: 6
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
0.00
0.00
0.00
285.3.0
0.00
285.3.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
285.3.1
0.00
285.3.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
285.3.2
0.00
285.3.2
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
285.4.0
0.00
285.4.0
equations: 6
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
0.00
0.00
0.00
288.0.0
0.01
288.0.0
equations: 4
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
288.0.1
0.00
288.0.1
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
288.0.2
0.01
288.0.2
equations: 4
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
289.0.0
0.01
289.0.0
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
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
0.00
0.00
0.00
289.1.0
0.01
289.1.0
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: carbonio
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
0.00
0.00
0.00
289.2.0
0.01
289.2.0
equations: 7
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
291.0.0
0.01
291.0.0
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0.001
0.00
0.00
0.00
291.1.0
0.01
291.1.0
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
292.0.0
0.01
292.0.0
equations: 6
iterations: 1
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
0.00
0.00
0.00
292.1.0
0.01
292.1.0
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
292.1.1
0.01
292.1.1
equations: 6
iterations: 1
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
0.00
0.00
0.00
292.1.2
0.01
292.1.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
292.2.0
0.01
292.2.0
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
292.3.0
0.01
292.3.0
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
292.3.1
0.01
292.3.1
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
292.3.2
0.01
292.3.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
295.0.0
0.00
295.0.0
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
0.00
0.00
0.00
295.0.1
0.00
295.0.1
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
0.00
0.00
0.00
295.0.10
0.00
295.0.10
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
0.00
0.00
0.00
295.0.11
0.00
295.0.11
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
0.00
0.00
0.00
295.0.12
0.00
295.0.12
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
0.00
0.00
0.00
295.0.13
0.00
295.0.13
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
0.00
0.00
0.00
295.0.14
0.00
295.0.14
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
0.00
0.00
0.00
295.0.2
0.00
295.0.2
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
0.00
0.00
0.00
295.0.3
0.00
295.0.3
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
0.00
0.00
0.00
295.0.4
0.00
295.0.4
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
0.00
0.00
0.00
295.0.5
0.00
295.0.5
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
0.00
0.00
0.00
295.0.6
0.00
295.0.6
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
0.00
0.00
0.00
295.0.7
0.00
295.0.7
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
0.00
0.00
0.00
295.0.8
0.00
295.0.8
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
0.00
0.00
0.00
295.0.9
0.00
295.0.9
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
0.00
0.00
0.00
298.0.0
0.00
298.0.0
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.1
0.00
298.0.1
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.10
0.00
298.0.10
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.11
0.00
298.0.11
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.12
0.00
298.0.12
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.13
0.00
298.0.13
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.14
0.00
298.0.14
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.2
0.00
298.0.2
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.3
0.00
298.0.3
equations: 5
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
0.00
0.00
0.00
298.0.4
0.00
298.0.4
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.5
0.00
298.0.5
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.6
0.00
298.0.6
equations: 5
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
0.00
0.00
0.00
298.0.7
0.00
298.0.7
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.8
0.00
298.0.8
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
298.0.9
0.00
298.0.9
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
299.0.0
0.00
299.0.0
equations: 5
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
303.0.0
0.00
303.0.0
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
304.0.0
0.00
304.0.0
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
304.0.1
0.00
304.0.1
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
304.0.2
0.00
304.0.2
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
305.0.0
0.00
305.0.0
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
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
308.0.0
0.00
308.0.0
equations: 2
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
308.0.1
0.00
308.0.1
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
0.00
0.00
0.00
308.0.2
0.00
308.0.2
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
0.00
0.00
0.00
309.0.0
0.16
309.0.0
equations: 75
iterations: 5
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.045
ground joinability: 0
find TRSs: 0.121
compute CPs: 0.002
main control loop: 0.026
rewriting: 0.002
SMT solver: 0.045
selection: 0
success checks: 0.009

Convergent TRS

(VAR Y) -> ihalf(0)
(RULES
tp2(Y,X) → imul(0)
tp1(Y) → ihalf(0)
ihalf(half(Y)) → ihalf(0)
imul(s(Y)) → imul(0)
iadd(Y) → imul(0)
)
0.00
0.00
0.00
309.0.1
0.02
309.0.1
equations: 12
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
309.0.2
0.15
309.0.2
equations: 44
iterations: 5
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.016
ground joinability: 0
find TRSs: 0.088
compute CPs: 0.002
main control loop: 0.04
rewriting: 0.01
SMT solver: 0.049
selection: 0
success checks: 0.01

Convergent TRS

(VAR Y) -> ihalf(0)
(RULES
iadd(Y) → imul(0)
ihalf(s(Y)) → ihalf(0)
ihalf(half(Y)) → ihalf(0)
tp2(Y,X) → imul(0)
tp1(Y) → ihalf(0)
)
0.00
0.00
0.00
309.1.0
0.01
309.1.0
equations: 12
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
310.0.0
∞
∞
∞
∞
310.1.0
∞
∞
∞
∞
310.2.0
∞
∞
∞
∞
310.3.0
∞
∞
∞
∞
311.0.0
0.01
311.0.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
311.1.0
0.01
311.1.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
311.2.0
0.01
311.2.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
311.3.0
0.01
311.3.0
equations: 7
iterations: 1
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
0.00
0.00
0.00
311.4.0
0.01
311.4.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
311.5.0
0.01
311.5.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
311.5.1
0.01
311.5.1
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
311.5.2
0.01
311.5.2
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
312.0.0
0.01
312.0.0
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
312.1.0
0.01
312.1.0
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
312.2.0
0.01
312.2.0
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
312.3.0
0.01
312.3.0
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
312.4.0
0.01
312.4.0
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
312.4.1
0.01
312.4.1
equations: 8
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
312.4.2
0.01
312.4.2
equations: 8
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
314.0.0
0.00
314.0.0
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
318.0.0
0.01
318.0.0
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
321.0.0
0.01
321.0.0
equations: 12
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.007
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
322.0.0
0.01
322.0.0
equations: 6
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
SMT solver: 0.001
selection: 0
success checks: 0
0.00
0.00
0.00
322.0.1
0.01
322.0.1
equations: 6
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
∞
322.0.10
0.02
322.0.10
equations: 6
iterations: 1
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.001
SMT solver: 0.003
selection: 0.001
success checks: 0.001
0.00
0.01
0.00
322.0.11
∞
∞
∞
∞
322.0.12
∞
∞
∞
∞
322.0.13
0.02
322.0.13
equations: 6
iterations: 1
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.002
selection: 0
success checks: 0.001
0.00
0.01
0.00
322.0.14
∞
∞
∞
∞
322.0.2
0.01
322.0.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
∞
322.0.3
0.01
322.0.3
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
322.0.4
0.02
322.0.4
equations: 6
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0.002
0.00
0.00
0.00
322.0.5
0.02
322.0.5
equations: 6
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.003
selection: 0
success checks: 0.002
0.00
0.00
0.00
322.0.6
0.02
322.0.6
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.001
main control loop: 0.005
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0.005

Convergent TRS

(VAR ,X) -> tru)
(RULES
le(s(X),s(Y)) → le(X,Y)
le(s(X),0) → false tp2(cons(Zs1,Zs2),X3) = tp2(X,cons(Y,Ys))
tp2(Zs1,cons(Zs2,X3)) = split(X,cons(Y,Ys)) →
→
tp2(cons(Zs1,Zs2),X3) = split(X,cons(Y,Ys)) →
tp2(X,cons(Y,Ys)) = tp2(cons(Zs1,Zs2),X3) →
→
split(X,cons(Y,Ys)) = split(Zs1,cons(Zs2,X3)) →
split(X,cons(Y,Ys)) = tp2(Zs1,cons(Zs2,X3)) →
→
)
0.00
0.00
∞
322.0.7
0.01
322.0.7
equations: 6
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
322.0.8
0.01
322.0.8
equations: 6
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.003
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0.001
0.00
0.00
0.00
322.0.9
0.02
322.0.9
equations: 6
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.004
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0.002
0.00
0.00
0.00
324.0.0
0.01
324.0.0
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
324.0.1
0.01
324.0.1
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
324.0.2
0.01
324.0.2
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
324.1.0
0.01
324.1.0
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
324.1.1
0.01
324.1.1
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
324.1.2
0.01
324.1.2
equations: 7
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
326.0.0
0.00
326.0.0
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

Convergent TRS

(VAR nil,Y) -> isnoc(cons(Y,nil)) tp2(cons(Y,Ys),Xs) = isnoc(cons(Y,X))
(RULES
)
0.00
0.00
0.00
327.0.0
0.01
327.0.0
equations: 11
iterations: 1
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
0.00
0.00
0.00
327.0.1
0.01
327.0.1
equations: 11
iterations: 1
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
0.00
0.00
0.00
327.0.2
0.08
327.0.2
equations: 47
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.037
compute CPs: 0.01
main control loop: 0.021
rewriting: 0.008
SMT solver: 0.007
selection: 0.001
success checks: 0.004
0.00
0.00
0.00
327.1.0
0.08
327.1.0
equations: 47
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.033
compute CPs: 0.009
main control loop: 0.02
rewriting: 0.009
SMT solver: 0.005
selection: 0.001
success checks: 0.006
0.00
0.00
0.00
327.2.0
0.08
327.2.0
equations: 47
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.014
ground joinability: 0
find TRSs: 0.033
compute CPs: 0.009
main control loop: 0.02
rewriting: 0.009
SMT solver: 0.005
selection: 0.001
success checks: 0.006
0.00
0.00
0.00
328.0.0
0.02
328.0.0
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
328.0.1
0.02
328.0.1
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.007
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
328.0.2
0.04
328.0.2
equations: 32
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.001
main control loop: 0.005
rewriting: 0.001
SMT solver: 0.01
selection: 0
success checks: 0.001
0.00
0.00
0.00
328.1.0
0.01
328.1.0
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.1
0.01
328.1.1
equations: 17
iterations: 1
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
SMT solver: 0.001
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.10
0.02
328.1.10
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.11
0.04
328.1.11
equations: 32
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.022
compute CPs: 0.001
main control loop: 0.009
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.001
0.00
0.00
0.00
328.1.12
0.02
328.1.12
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.13
0.01
328.1.13
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.14
0.05
328.1.14
equations: 32
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.024
compute CPs: 0.001
main control loop: 0.012
rewriting: 0.003
SMT solver: 0.011
selection: 0.001
success checks: 0.001
0.00
0.00
0.00
328.1.2
0.01
328.1.2
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.3
0.01
328.1.3
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.4
0.02
328.1.4
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.5
0.02
328.1.5
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.6
0.02
328.1.6
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.7
0.02
328.1.7
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.8
0.02
328.1.8
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
328.1.9
0.01
328.1.9
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
329.0.0
0.02
329.0.0
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
∞
329.0.1
0.02
329.0.1
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
∞
329.0.10
0.03
329.0.10
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.004
selection: 0
success checks: 0.001
0.00
0.13
0.00
329.0.11
0.03
329.0.11
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0.004
selection: 0
success checks: 0.001
0.00
0.13
0.00
329.0.12
∞
∞
∞
∞
329.0.13
∞
∞
∞
∞
329.0.14
∞
∞
∞
∞
329.0.2
0.02
329.0.2
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
329.0.3
0.04
329.0.3
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.014
selection: 0
success checks: 0.001
0.00
0.00
0.00
329.0.4
0.04
329.0.4
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0.001
success checks: 0.003
0.00
0.01
0.00
329.0.5
0.04
329.0.5
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0
success checks: 0.003
0.00
0.02
0.00
329.0.6
∞
∞
∞
∞
329.0.7
0.04
329.0.7
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0
success checks: 0.003
0.00
0.02
0.00
329.0.8
0.02
329.0.8
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.01
0.00
329.0.9
0.05
329.0.9
equations: 10
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.008
selection: 0
success checks: 0.004
0.00
0.01
0.00
330.0.0
0.00
330.0.0
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
0.00
0.00
∞
331.0.0
0.01
331.0.0
equations: 7
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
0.00
0.00
0.00
332.0.0
0.00
332.0.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
332.0.1
0.00
332.0.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
332.0.2
0.01
332.0.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
332.1.0
0.00
332.1.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
332.1.1
0.00
332.1.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
332.1.2
0.00
332.1.2
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
335.0.0
0.01
335.0.0
equations: 9
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
335.0.1
0.01
335.0.1
equations: 9
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
335.0.2
0.01
335.0.2
equations: 9
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
∞
335.0.3
0.02
335.0.3
equations: 13
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0.001
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0.001

Convergent TRS

(VAR ,s(X)) -> tru)
(RULES
div(s(X),s(Y)) → pair(0,s(X))
lt(s(X),s(Y)) → lt(X,Y)
m(X,0) → X
m(s(X),s(Y)) → m(X,Y)
m(0,s(X)) → 0
lt(X,0) → false pair(0,s(X)) = pair(s(Y),Q)
)
0.00
0.00
∞
335.0.4
0.01
335.0.4
equations: 9
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
335.0.5
0.01
335.0.5
equations: 9
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
335.0.6
∞
∞
∞
∞
336.0.0
0.00
336.0.0
equations: 3
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
0.00
0.00
0.00
336.0.1
0.02
336.0.1
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0.003
rewriting: 0
SMT solver: 0.005
selection: 0.001
success checks: 0.004

Convergent TRS

(VAR er(N,R,cons(X,Xs)) -> pair(X,Xs)
(RULES
)
0.00
0.00
0.00
336.0.2
0.02
336.0.2
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0
main control loop: 0.002
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0.003

Convergent TRS

(VAR er(N,R,cons(X,Xs)) -> pair(X,Xs)
(RULES
)
0.00
0.00
0.00
336.0.3
0.04
336.0.3
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0.005
rewriting: 0.001
SMT solver: 0.007
selection: 0.001
success checks: 0.015

Convergent TRS

(VAR er(N,R,cons(X,Xs)) -> pair(X,Xs)
(RULES
)
0.00
0.01
0.00
336.0.4
0.03
336.0.4
equations: 15
iterations: 3
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.015
compute CPs: 0
main control loop: 0.01
rewriting: 0.001
SMT solver: 0.011
selection: 0
success checks: 0.006

Convergent TRS

(VAR er(N,R,cons(X,Xs)) -> pair(X,Xs)
(RULES
)
0.00
0.01
0.00
336.0.5
0.06
336.0.5
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.015
compute CPs: 0
main control loop: 0.008
rewriting: 0.003
SMT solver: 0.011
selection: 0.001
success checks: 0.017

Convergent TRS

(VAR er(N,R,cons(X,Xs)) -> pair(X,Xs)
(RULES
)
0.00
0.01
0.00
336.0.6
0.06
336.0.6
equations: 11
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.014
compute CPs: 0
main control loop: 0.008
rewriting: 0.005
SMT solver: 0.011
selection: 0.001
success checks: 0.024

Convergent TRS

(VAR er(N,R,cons(X,Xs)) -> pair(X,Xs)
(RULES
)
0.00
0.02
0.00
337.0.0
0.00
337.0.0
equations: 4
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
0.00
0.00
∞
337.0.1
0.01
337.0.1
equations: 4
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.001
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
337.0.2
0.59
337.0.2
equations: 17
iterations: 2
memory: 13 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.003
ground joinability: 0
find TRSs: 0.008
compute CPs: 0.319
main control loop: 0.033
rewriting: 0.062
SMT solver: 0.001
selection: 0.011
success checks: 0.07
0.00
0.00
0.00
340.0.0
0.00
340.0.0
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
0.00
0.00
0.00
340.0.1
0.00
340.0.1
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
0.00
0.00
0.00
340.0.10
0.00
340.0.10
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
0.00
0.00
0.00
340.0.11
0.00
340.0.11
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
0.00
0.00
0.00
340.0.12
0.00
340.0.12
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
0.00
0.00
0.00
340.0.13
0.00
340.0.13
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
0.00
0.00
0.00
340.0.14
0.00
340.0.14
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

Convergent TRS

(VAR = f(Xp,Xpp)
(RULES
)
0.00
0.00
0.00
340.0.2
0.00
340.0.2
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
0.00
0.00
0.00
340.0.3
0.00
340.0.3
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
0.00
0.00
0.00
340.0.4
0.00
340.0.4
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
0.00
0.00
0.00
340.0.5
0.00
340.0.5
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
0.00
0.00
0.00
340.0.6
0.00
340.0.6
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
0.00
0.00
0.00
340.0.7
0.00
340.0.7
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
0.00
0.00
0.00
340.0.8
0.00
340.0.8
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
0.00
0.00
0.00
340.0.9
0.00
340.0.9
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
0.00
0.00
0.00
342.0.0
0.00
342.0.0
equations: 3
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
0.00
0.00
0.00
342.0.1
0.00
342.0.1
equations: 3
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
0.00
0.00
0.00
342.0.10
0.00
342.0.10
equations: 3
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
0.00
0.00
0.00
342.0.11
0.00
342.0.11
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.12
0.00
342.0.12
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.13
0.00
342.0.13
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.14
∞
∞
∞
∞
342.0.2
0.00
342.0.2
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.3
0.00
342.0.3
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.4
0.00
342.0.4
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.5
0.00
342.0.5
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.6
0.00
342.0.6
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.7
0.00
342.0.7
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.8
0.00
342.0.8
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
342.0.9
0.00
342.0.9
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
351.0.0
0.00
351.0.0
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
351.0.1
0.00
351.0.1
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
351.0.2
0.01
351.0.2
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
351.0.3
0.01
351.0.3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
351.0.4
0.01
351.0.4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
351.0.5
0.01
351.0.5
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
351.0.6
0.01
351.0.6
equations: 5
iterations: 1
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.001
selection: 0.001
success checks: 0
0.00
0.00
0.00
352.0.0
0.02
352.0.0
equations: 9
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
353.0.0
0.01
353.0.0
equations: 7
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.0
0.01
353.1.0
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.1
0.01
353.1.1
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.002
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.10
0.01
353.1.10
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.11
0.01
353.1.11
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.12
0.01
353.1.12
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.13
0.01
353.1.13
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.14
0.01
353.1.14
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.15
0.01
353.1.15
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.16
0.01
353.1.16
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.17
0.01
353.1.17
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.18
0.01
353.1.18
equations: 7
iterations: 1
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
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.19
0.01
353.1.19
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.2
0.01
353.1.2
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.20
0.01
353.1.20
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.21
0.01
353.1.21
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.22
0.01
353.1.22
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.01
0.00
353.1.23
0.01
353.1.23
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.24
0.01
353.1.24
equations: 7
iterations: 1
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
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.25
0.01
353.1.25
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.26
0.01
353.1.26
equations: 7
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
SMT solver: 0.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.27
0.01
353.1.27
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.28
0.01
353.1.28
equations: 7
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.29
0.01
353.1.29
equations: 7
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.3
0.01
353.1.3
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.30
0.01
353.1.30
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.4
0.01
353.1.4
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.5
0.01
353.1.5
equations: 7
iterations: 1
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
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.6
0.01
353.1.6
equations: 7
iterations: 1
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
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.7
0.01
353.1.7
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.8
0.02
353.1.8
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
353.1.9
0.01
353.1.9
equations: 7
iterations: 1
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
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
353.2.0
0.01
353.2.0
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.2.1
0.01
353.2.1
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.2.2
0.02
353.2.2
equations: 7
iterations: 1
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
rewriting: 0
SMT solver: 0.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.2.3
0.01
353.2.3
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.2.4
0.01
353.2.4
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.2.5
0.01
353.2.5
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.2.6
0.01
353.2.6
equations: 7
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.3.0
0.01
353.3.0
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
353.3.1
0.01
353.3.1
equations: 7
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
353.3.2
0.01
353.3.2
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
361.0.0
0.01
361.0.0
equations: 9
iterations: 1
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
0.00
0.00
∞
361.0.1
0.01
361.0.1
equations: 9
iterations: 1
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
0.00
0.00
∞
361.0.2
0.01
361.0.2
equations: 9
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
361.0.3
0.02
361.0.3
equations: 12
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0.001
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0.001

Convergent TRS

(VAR s(X),s(Y)) -> leq(X,Y)
(RULES
m(s(X),s(Y)) → m(X,Y)
div(X,Y) → pair(0,Y)
m(X,0) → X
greater(s(X),0) → true
greater(s(X),s(Y)) → greater(X,Y)
leq(0,X) → true pair(0,X) = pair(s(Y),Q)
)
0.00
0.00
0.00
361.0.4
0.01
361.0.4
equations: 9
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
361.0.5
0.01
361.0.5
equations: 9
iterations: 1
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
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
361.0.6
0.02
361.0.6
equations: 15
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0.003
rewriting: 0.001
SMT solver: 0.005
selection: 0
success checks: 0.004

Convergent TRS

(VAR s(X),s(Y)) -> leq(X,Y)
(RULES
m(s(X),s(Y)) → m(X,Y)
div(X,Y) → pair(0,Y)
m(X,0) → X
greater(s(X),0) → true
greater(s(X),s(Y)) → greater(X,Y)
leq(0,X) → true pair(0,X) = pair(s(Y),Q)
)
0.00
0.00
0.00
365.0.0
0.01
365.0.0
equations: 6
iterations: 1
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
0.00
0.00
0.00
365.1.0
0.01
365.1.0
equations: 6
iterations: 1
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
0.00
0.00
0.00
378.0.0
0.01
378.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
378.1.0
0.01
378.1.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
378.2.0
0.01
378.2.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
378.2.1
0.01
378.2.1
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
378.2.2
0.03
378.2.2
equations: 20
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.004
main control loop: 0.017
rewriting: 0.001
SMT solver: 0
selection: 0
success checks: 0.004
0.00
0.01
0.00
378.3.0
0.01
378.3.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
383.0.0
0.01
383.0.0
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
384.0.0
0.01
384.0.0
equations: 7
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
387.0.0
0.00
387.0.0
equations: 2
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
0.00
0.00
0.00
391.0.0
0.01
391.0.0
equations: 4
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
391.0.1
0.01
391.0.1
equations: 4
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
391.0.2
0.01
391.0.2
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
403.0.0
0.00
403.0.0
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
403.0.1
0.00
403.0.1
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
403.0.2
0.00
403.0.2
equations: 3
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
404.0.0
0.00
404.0.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
404.0.1
0.00
404.0.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
404.0.2
0.01
404.0.2
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
404.1.0
0.00
404.1.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
404.1.1
0.00
404.1.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
404.1.2
0.01
404.1.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
405.0.0
0.01
405.0.0
equations: 7
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
selection: 0
success checks: 0
0.00
0.00
∞
405.0.1
0.01
405.0.1
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
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
0.00
0.00
∞
405.0.2
0.01
405.0.2
equations: 7
iterations: 1
memory: 3 MB
restarts: 0
problem shape: elio
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
0.00
0.00
0.00
406.0.0
0.00
406.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
406.0.1
0.00
406.0.1
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
406.0.2
0.01
406.0.2
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
407.0.0
0.00
407.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
407.0.1
0.00
407.0.1
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
407.0.2
0.00
407.0.2
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
408.0.0
0.00
408.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
408.0.1
0.01
408.0.1
equations: 4
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
408.0.2
0.00
408.0.2
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
409.0.0
0.00
409.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
409.0.1
0.00
409.0.1
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
409.0.2
0.01
409.0.2
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
410.0.0
0.01
410.0.0
equations: 6
iterations: 1
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
0.00
0.00
0.00
410.0.1
0.01
410.0.1
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
410.0.2
0.01
410.0.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
411.0.0
0.01
411.0.0
equations: 6
iterations: 1
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
0.00
0.00
0.00
411.0.1
0.01
411.0.1
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
411.0.2
0.01
411.0.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
439.0.0
0.00
439.0.0
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
0.00
0.00
0.00
439.0.1
0.00
439.0.1
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
0.00
0.00
0.00
439.0.2
0.00
439.0.2
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
0.00
0.00
0.00
439.0.3
0.00
439.0.3
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
0.00
0.00
0.00
439.0.4
0.00
439.0.4
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
0.00
0.00
0.00
439.0.5
0.00
439.0.5
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
0.00
0.00
0.00
439.0.6
0.00
439.0.6
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
0.00
0.00
0.00
440.0.0
0.00
440.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
440.0.1
0.00
440.0.1
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
440.0.2
∞
∞
∞
0.00
441.0.0
0.01
441.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
441.0.1
0.00
441.0.1
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
441.0.2
0.01
441.0.2
equations: 4
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.002
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
489.0.0
0.01
489.0.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
489.0.1
0.00
489.0.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
489.0.2
0.01
489.0.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
489.1.0
0.01
489.1.0
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
∞
489.1.1
0.00
489.1.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
489.1.2
0.01
489.1.2
equations: 6
iterations: 1
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
0.00
0.00
0.00
491.0.0
0.00
491.0.0
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
0.00
0.00
0.00
491.0.1
0.00
491.0.1
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
0.00
0.00
0.00
491.0.2
0.01
491.0.2
equations: 4
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.001
selection: 0
success checks: 0

Convergent TRS

(VAR -> )
(RULES
)
0.00
0.00
0.00
492.0.0
0.00
492.0.0
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
0.00
0.00
0.00
492.0.1
0.00
492.0.1
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
0.00
0.00
0.00
492.0.2
0.00
492.0.2
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
0.00
0.00
0.00
493.0.0
0.02
493.0.0
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
493.0.1
0.02
493.0.1
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.007
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
493.0.2
0.03
493.0.2
equations: 32
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.001
main control loop: 0.005
rewriting: 0.001
SMT solver: 0.009
selection: 0
success checks: 0.001
0.00
0.00
0.00
493.1.0
0.02
493.1.0
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.1
0.01
493.1.1
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.10
0.04
493.1.10
equations: 32
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.024
compute CPs: 0
main control loop: 0.009
rewriting: 0.002
SMT solver: 0.012
selection: 0.001
success checks: 0.001
0.00
0.00
0.00
493.1.11
0.05
493.1.11
equations: 32
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.028
compute CPs: 0.001
main control loop: 0.01
rewriting: 0.002
SMT solver: 0.014
selection: 0
success checks: 0.001
0.00
0.00
0.00
493.1.12
0.02
493.1.12
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0.001
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.13
0.02
493.1.13
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.14
0.04
493.1.14
equations: 32
iterations: 2
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.004
ground joinability: 0
find TRSs: 0.019
compute CPs: 0.001
main control loop: 0.011
rewriting: 0.003
SMT solver: 0.008
selection: 0
success checks: 0.001
0.00
0.00
0.00
493.1.2
0.01
493.1.2
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.3
0.02
493.1.3
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.4
0.01
493.1.4
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.5
0.02
493.1.5
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.6
0.02
493.1.6
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.7
0.02
493.1.7
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.8
0.01
493.1.8
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.005
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
493.1.9
0.02
493.1.9
equations: 17
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
494.0.0
0.00
494.0.0
equations: 4
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
494.0.1
0.01
494.0.1
equations: 6
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.001
selection: 0
success checks: 0

Convergent TRS

(VAR X) -> )
(RULES
c → d
f(b,X) → b g(a,X) = d
)
0.00
0.00
0.00
494.0.2
0.01
494.0.2
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
SMT solver: 0.002
selection: 0
success checks: 0

Convergent TRS

(VAR X) -> )
(RULES
g(X,a) → d
f(b,X) → b g(a,X) = d
)
0.00
0.00
0.00
495.0.0
0.00
495.0.0
equations: 3
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
0.00
0.00
0.00
499.0.0
0.03
499.0.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.002
main control loop: 0
rewriting: 0.002
SMT solver: 0.006
selection: 0
success checks: 0.002
0.00
0.00
0.00
499.0.1
0.02
499.0.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
499.0.2
0.03
499.0.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
499.1.0
0.04
499.1.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.022
compute CPs: 0
main control loop: 0
rewriting: 0.001
SMT solver: 0.012
selection: 0
success checks: 0
0.00
0.00
0.00
499.1.1
0.02
499.1.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
499.1.2
0.02
499.1.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
499.2.0
0.06
499.2.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.02
compute CPs: 0.003
main control loop: 0
rewriting: 0.004
SMT solver: 0.013
selection: 0
success checks: 0.004
0.00
0.00
0.00
499.3.0
0.02
499.3.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.1
0.02
499.3.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.10
0.01
499.3.10
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.11
0.04
499.3.11
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
499.3.12
0.02
499.3.12
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.01
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.13
0.04
499.3.13
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.007
selection: 0
success checks: 0.002
0.00
0.00
0.00
499.3.14
0.05
499.3.14
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.002
main control loop: 0
rewriting: 0.006
SMT solver: 0.008
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
499.3.2
0.01
499.3.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.3
0.02
499.3.3
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.4
0.03
499.3.4
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
499.3.5
0.02
499.3.5
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.012
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.6
0.02
499.3.6
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.7
0.02
499.3.7
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.8
0.02
499.3.8
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
499.3.9
0.02
499.3.9
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
499.4.0
0.03
499.4.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.002
main control loop: 0
rewriting: 0.002
SMT solver: 0.006
selection: 0
success checks: 0.002
0.00
0.00
0.00
499.4.1
0.02
499.4.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
499.4.2
0.02
499.4.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
499.4.3
0.02
499.4.3
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
499.4.4
0.03
499.4.4
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0.001
0.00
0.00
0.00
499.4.5
0.02
499.4.5
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
499.4.6
0.02
499.4.6
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.004
selection: 0
success checks: 0.001
0.00
0.00
0.00
499.5.0
0.02
499.5.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0.004
selection: 0
success checks: 0.001
0.00
0.00
0.00
499.5.1
0.01
499.5.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.003
selection: 0
success checks: 0
0.00
0.00
0.00
499.5.2
0.02
499.5.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.005
selection: 0
success checks: 0.001
0.00
0.00
0.00
522.0.0
0.00
522.0.0
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
522.0.1
0.00
522.0.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
522.0.2
0.01
522.0.2
equations: 6
iterations: 1
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
0.00
0.00
0.00
522.1.0
0.01
522.1.0
equations: 6
iterations: 1
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
0.00
0.00
∞
522.1.1
0.00
522.1.1
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
∞
522.1.2
0.00
522.1.2
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
529.0.0
0.02
529.0.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.006
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.003
selection: 0
success checks: 0.001
0.00
0.00
0.00
529.0.1
0.02
529.0.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.0.2
0.02
529.0.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0.001
0.00
0.00
0.00
529.1.0
0.02
529.1.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.1.1
0.03
529.1.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.009
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0.005
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.1.2
0.02
529.1.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.1.3
0.02
529.1.3
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.002
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0.001
0.00
0.00
0.00
529.1.4
0.01
529.1.4
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.1.5
0.04
529.1.5
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.002
main control loop: 0
rewriting: 0.002
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.1.6
0.04
529.1.6
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.009
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
529.2.0
0.02
529.2.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.2.1
0.03
529.2.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.006
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.2.2
0.03
529.2.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.002
main control loop: 0
rewriting: 0.001
SMT solver: 0.005
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.2.3
0.04
529.2.3
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.002
main control loop: 0
rewriting: 0.002
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.2.4
0.03
529.2.4
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.008
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.2.5
0.03
529.2.5
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.002
main control loop: 0
rewriting: 0.002
SMT solver: 0.007
selection: 0
success checks: 0.003
0.00
0.00
0.00
529.2.6
0.04
529.2.6
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.004
main control loop: 0
rewriting: 0.003
SMT solver: 0.009
selection: 0
success checks: 0.003
0.00
0.00
0.00
529.3.0
0.03
529.3.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.002
main control loop: 0
rewriting: 0.002
SMT solver: 0.006
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.4.0
0.02
529.4.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.1
0.02
529.4.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.10
0.02
529.4.10
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.11
0.03
529.4.11
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.01
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.12
0.02
529.4.12
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.13
0.01
529.4.13
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.006
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.14
0.02
529.4.14
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.15
0.02
529.4.15
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.16
0.02
529.4.16
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.17
0.04
529.4.17
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.002
ground joinability: 0
find TRSs: 0.022
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.015
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.18
0.02
529.4.18
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.19
0.02
529.4.19
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.015
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.01
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.2
0.02
529.4.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.20
0.02
529.4.20
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.21
0.04
529.4.21
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.22
0.02
529.4.22
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.23
0.02
529.4.23
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.24
0.02
529.4.24
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.25
0.04
529.4.25
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.007
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.4.26
0.02
529.4.26
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.27
0.03
529.4.27
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.01
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.28
0.02
529.4.28
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.01
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.29
0.03
529.4.29
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.01
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.3
0.02
529.4.3
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.004
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.30
0.04
529.4.30
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.003
main control loop: 0
rewriting: 0.003
SMT solver: 0.006
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.4.31
0.02
529.4.31
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.32
0.02
529.4.32
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.33
0.02
529.4.33
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.004
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.4.34
0.02
529.4.34
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.35
0.05
529.4.35
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.015
selection: 0
success checks: 0.003
0.00
0.00
0.00
529.4.36
0.02
529.4.36
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.37
0.03
529.4.37
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.018
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.012
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.38
0.04
529.4.38
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.004
main control loop: 0
rewriting: 0.003
SMT solver: 0.007
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.4.39
0.04
529.4.39
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.007
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.4
0.02
529.4.4
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.009
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.40
0.04
529.4.40
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.021
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.015
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.41
0.02
529.4.41
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.42
0.04
529.4.42
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.002
main control loop: 0
rewriting: 0.003
SMT solver: 0.008
selection: 0
success checks: 0.003
0.00
0.00
0.00
529.4.43
0.04
529.4.43
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.002
main control loop: 0
rewriting: 0.003
SMT solver: 0.008
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.44
0.04
529.4.44
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0.002
main control loop: 0
rewriting: 0.003
SMT solver: 0.008
selection: 0
success checks: 0.003
0.00
0.00
0.00
529.4.45
0.06
529.4.45
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.018
compute CPs: 0.003
main control loop: 0
rewriting: 0.005
SMT solver: 0.011
selection: 0.001
success checks: 0.003
0.00
0.00
0.00
529.4.46
0.04
529.4.46
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.002
main control loop: 0
rewriting: 0.005
SMT solver: 0.007
selection: 0.002
success checks: 0.002
0.00
0.00
0.00
529.4.47
0.04
529.4.47
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.007
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.48
0.01
529.4.48
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.49
0.03
529.4.49
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.014
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.01
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.5
0.02
529.4.5
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.50
0.01
529.4.50
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.51
0.04
529.4.51
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.002
SMT solver: 0.007
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.52
0.02
529.4.52
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.53
0.02
529.4.53
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.009
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.54
0.03
529.4.54
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.002
main control loop: 0
rewriting: 0.005
SMT solver: 0.004
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.55
0.04
529.4.55
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.005
SMT solver: 0.007
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.56
0.05
529.4.56
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.002
main control loop: 0
rewriting: 0.006
SMT solver: 0.007
selection: 0.003
success checks: 0.002
0.00
0.00
0.00
529.4.57
0.05
529.4.57
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.005
SMT solver: 0.007
selection: 0.002
success checks: 0.002
0.00
0.00
0.00
529.4.58
0.04
529.4.58
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.005
SMT solver: 0.007
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.59
0.05
529.4.59
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.003
main control loop: 0
rewriting: 0.005
SMT solver: 0.007
selection: 0.002
success checks: 0.002
0.00
0.00
0.00
529.4.6
0.04
529.4.6
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.004
main control loop: 0
rewriting: 0.001
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.4.60
0.02
529.4.60
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.012
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.008
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.61
0.04
529.4.61
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.003
main control loop: 0
rewriting: 0.005
SMT solver: 0.007
selection: 0.001
success checks: 0.002
0.00
0.00
0.00
529.4.62
0.05
529.4.62
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.002
main control loop: 0
rewriting: 0.008
SMT solver: 0.007
selection: 0.002
success checks: 0.002
0.00
0.00
0.00
529.4.7
0.01
529.4.7
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.008
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.8
0.02
529.4.8
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.006
selection: 0
success checks: 0
0.00
0.00
0.00
529.4.9
0.03
529.4.9
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.5.0
0.03
529.5.0
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.01
compute CPs: 0.002
main control loop: 0
rewriting: 0.002
SMT solver: 0.006
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.5.1
0.02
529.5.1
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.5.2
0.02
529.5.2
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.5.3
0.02
529.5.3
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.011
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.007
selection: 0
success checks: 0
0.00
0.00
0.00
529.5.4
0.03
529.5.4
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0.001
ground joinability: 0
find TRSs: 0.013
compute CPs: 0.003
main control loop: 0
rewriting: 0.001
SMT solver: 0.009
selection: 0
success checks: 0.002
0.00
0.00
0.00
529.5.5
0.02
529.5.5
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.001
main control loop: 0
rewriting: 0
SMT solver: 0.005
selection: 0
success checks: 0
0.00
0.00
0.00
529.5.6
0.02
529.5.6
equations: 20
iterations: 1
memory: 3 MB
restarts: 0
problem shape: none
time (sec): 
reducibility constraints: 0
ground joinability: 0
find TRSs: 0.007
compute CPs: 0.001
main control loop: 0
rewriting: 0.001
SMT solver: 0.005
selection: 0
success checks: 0.001
0.00
0.00
0.00
546.0.0
0.00
546.0.0
equations: 1
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
0.00
0.00
0.00
547.0.0
0.00
547.0.0
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
0.00
0.00
0.00
547.0.1
0.00
547.0.1
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
0.00
0.00
0.00
547.0.2
0.00
547.0.2
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
0.00
0.00
0.00
551.0.0
0.01
551.0.0
equations: 6
iterations: 1
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
0.00
0.00
0.00
551.0.1
0.01
551.0.1
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.0.2
0.01
551.0.2
equations: 6
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
SMT solver: 0.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.0
0.01
551.1.0
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.1
0.01
551.1.1
equations: 6
iterations: 1
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
0.00
0.00
0.00
551.1.10
0.01
551.1.10
equations: 6
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.11
0.01
551.1.11
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.12
0.01
551.1.12
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.13
0.01
551.1.13
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.14
0.01
551.1.14
equations: 6
iterations: 1
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.001
SMT solver: 0.002
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.2
0.00
551.1.2
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.3
0.00
551.1.3
equations: 6
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
SMT solver: 0
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.4
0.01
551.1.4
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.5
0.01
551.1.5
equations: 6
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.6
0.01
551.1.6
equations: 6
iterations: 1
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.002
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.7
0.01
551.1.7
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.8
0.01
551.1.8
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
551.1.9
0.01
551.1.9
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
552.0.0
0.01
552.0.0
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
552.1.0
0.01
552.1.0
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
552.1.1
0.01
552.1.1
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
552.1.2
0.01
552.1.2
equations: 6
iterations: 1
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.001
selection: 0
success checks: 0
0.00
0.00
0.00
553.0.0
0.01
553.0.0
equations: 6
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
0.00
0.00
0.00
max_iterations 9
max_restarts 1
equalities 175
total equalities 13808
goals
restarts 2
hard restarts
successes 704705705657
timeouts 27262674
median time 0.0160.001
time/overlaps 7s (11%)
time/rewrite 3s (5%)
time/select 0s (1%)
time/subsumption checks
time/success checks 9s (14%)
time/sat 16s (24%)
total time 64.22433.106
average time 0.090.05
average memory 215 MB
OVERALL STATS
solved706
diff solved50