MaedMax Experiment : TPTP UEQ SAT
|
maedmax test SAT after changes in narrowing e24316c --json
|
E E sat 600
|
Vampire Vampire UEQ SAT examples
|
||||||||||||||||||||||||||||||||
| ALG299-1 | (0.67) |
0.00
ALG299-1
Convergent TRS(VAR oduct(B,A)) -> )
(RULES ) |
0.00
|
0.00
|
||||||||||||||||||||||||||||||
| ALG300-1 | (0.67) |
109.38
ALG300-1
Convergent TRS(VAR product(product(product(product(product(product(product(B,B),B),C),product(product(product(B,B),B),C)),product(product(product(B,B),B),C)),A),C)
(RULES A = product(product(product(product(B,B),B),A),product(B,C)) → product(product(product(product(product(product(product(B,B),B),C),product(product(product(B,B),B),C)),product(product(product(B,B),B),C)),A),C) = A → → ) |
0.01
|
0.00
|
||||||||||||||||||||||||||||||
| ALG301-1 | (1.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| ALG302-1 | (0.67) |
0.00
ALG302-1
|
0.01
|
0.00
|
||||||||||||||||||||||||||||||
| BOO019-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO027-1 | (0.00) |
0.01
BOO027-1
Convergent TRS(VAR X,inverse(X)) -> on)
(RULES add(multiply(X,inverse(Y)),multiply(X,add(X,inverse(Y)))) → X add(multiply(X,inverse(Y)),multiply(Y,add(X,inverse(Y)))) → X) |
0.01
|
0.00
|
||||||||||||||||||||||||||||||
| BOO030-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO032-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO033-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO036-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO037-2 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO037-3 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO077-1 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| BOO106-1 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| COL005-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| COL047-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| COL069-1 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| COL071-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| COL073-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP204-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP207-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP393-2 | (0.00) |
0.00
GRP393-2
|
0.00
|
0.00
|
||||||||||||||||||||||||||||||
| GRP394-3 | (0.00) |
2.15
GRP394-3
Convergent TRS(VAR iply(inverse(X),X) -> identit)
(RULES multiply(identity,X) → X multiply(inverse(Y),multiply(Y,X)) → X multiply(multiply(X,Y),Z) → multiply(X,multiply(Y,Z)) inverse(inverse(X)) → X inverse(identity) → identity multiply(X,identity) → X multiply(X,inverse(X)) → identity) |
0.00
|
∞
|
||||||||||||||||||||||||||||||
| GRP399-1 | (0.33) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP722-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP735-1 | (0.67) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP737-1 | (0.33) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP738-1 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP739-1 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP741-1 | (0.33) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP742-1 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP743-1 | (0.33) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP744-1 | (1.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| GRP773-1 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| HWC004-1 | (0.20) |
0.01
HWC004-1
Convergent TRS(VAR > not(n0)
(RULES and(>not(n0>),n0) → n0 or(>not(n0>),n0) → >not(n0>) or(>not(n0>),>not(n0>)) → >not(n0>) not(>not(n0>)) → n0 or(n0,n0) → n0 and(n0,n0) → n0 and(>not(n0>),>not(n0>)) → >not(n0>)) |
0.01
|
0.00
|
||||||||||||||||||||||||||||||
| HWC004-2 | (0.00) |
0.01
HWC004-2
Convergent TRS(VAR X,n0) -> n)
(RULES n1 → not(n0) or(X,not(n0)) → not(n0) not(not(n0)) → n0) |
0.01
|
0.00
|
||||||||||||||||||||||||||||||
| LAT016-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT024-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT025-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT046-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT047-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT048-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT049-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT050-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT051-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT052-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT053-1 | (0.67) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT054-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT055-2 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT059-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT060-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT061-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT062-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT063-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT098-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT099-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT100-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT101-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT102-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT103-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT104-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT105-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT106-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT107-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT108-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT109-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT110-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT111-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT112-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT113-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT114-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT115-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT116-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT117-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT118-1 | (0.67) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT119-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT120-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT121-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT122-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT123-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT124-1 | (0.33) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT125-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT126-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT127-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT128-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT129-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT130-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT131-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT132-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT133-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT134-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT135-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT136-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LAT137-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LCL136-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LCL137-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LCL165-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LCL407-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LCL407-2 | (0.00) |
2.00
LCL407-2
Convergent TRS(VAR star(X,not(falsehood)) -> )
(RULES xor(xor(falsehood,X),X) → falsehood and_star(not(falsehood),xor(falsehood,X)) → and_star(not(falsehood),X) and_star(not(and_star(xor(falsehood,X),xor(falsehood,Y))),xor(falsehood,Y)) → and_star(not(and_star(xor(falsehood,X),Y)),Y) and_star(not(and_star(xor(not(falsehood),X),xor(falsehood,Y))),xor(falsehood,Y)) → and_star(not(and_star(xor(not(falsehood),X),Y)),Y) and_star(xor(not(falsehood),X),xor(falsehood,X)) → falsehood and_star(not(and_star(not(falsehood),X)),xor(falsehood,X)) → falsehood xor(X,X) → falsehood not(not(X)) → X and_star(X,falsehood) → falsehood and_star(xor(falsehood,X),xor(not(falsehood),X)) → falsehood and_star(not(and_star(not(falsehood),X)),X) → falsehood xor(X,xor(falsehood,Y)) → xor(X,Y) and_star(xor(not(falsehood),X),X) → falsehood and_star(not(and_star(falsehood,X)),X) → not(xor(not(falsehood),X)) xor(X,not(falsehood)) → not(X) xor(not(xor(not(falsehood),X)),X) → falsehood xor(X,xor(not(falsehood),Y)) → xor(not(X),Y) xor(X,falsehood) → X and_star(not(and_star(xor(falsehood,X),xor(not(falsehood),Y))),xor(not(falsehood),Y)) = and_star(not(and_star(xor(falsehood,Y),xor(not(falsehood),X))),xor(not(falsehood),X)) → and_star(not(and_star(xor(falsehood,Y),X)),X) = and_star(not(and_star(xor(not(falsehood),X),xor(not(falsehood),Y))),xor(not(falsehood),Y)) → → and_star(not(and_star(xor(not(falsehood),X),Y)),Y) = and_star(not(and_star(xor(not(falsehood),Y),X)),X) → → ) |
0.01
|
0.01
|
||||||||||||||||||||||||||||||
| LCL409-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LCL410-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LCL905-1 | (0.00) |
1.50
LCL905-1
Convergent TRS(VAR ehood -> not(truth)
(RULES and_star(not(and_star(truth,X)),xor(truth,xor(truth,X))) → not(truth) and_star(not(and_star(truth,X)),X) → not(truth) xor(X,not(truth)) → X xor(X,xor(truth,xor(truth,Y))) → xor(X,Y) and_star(truth,xor(truth,xor(truth,X))) → and_star(truth,X) and_star(not(and_star(not(truth),X)),X) → not(xor(truth,X)) and_star(xor(truth,X),X) → not(truth) xor(X,X) → not(truth) and_star(X,not(truth)) → not(truth) xor(xor(truth,xor(truth,X)),X) → not(truth) and_star(X,truth) → X xor(not(X),Y) → xor(X,xor(truth,Y)) not(not(X)) → X and_star(xor(truth,X),xor(truth,xor(truth,X))) → not(truth) xor(X,truth) → not(X) and_star(not(and_star(xor(truth,X),xor(truth,xor(truth,Y)))),xor(truth,xor(truth,Y))) = and_star(not(and_star(xor(truth,Y),xor(truth,xor(truth,X)))),xor(truth,xor(truth,X))) → and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(not(and_star(xor(truth,Y),X)),X) → → and_star(not(and_star(xor(truth,Y),xor(truth,xor(truth,X)))),xor(truth,xor(truth,X))) = and_star(not(and_star(xor(truth,X),Y)),Y) → → and_star(not(and_star(xor(truth,X),xor(truth,xor(truth,Y)))),xor(truth,xor(truth,Y))) = and_star(not(and_star(xor(truth,X),Y)),Y) → → and_star(not(and_star(xor(truth,X),Y)),Y) = and_star(not(and_star(xor(truth,X),xor(truth,xor(truth,Y)))),xor(truth,xor(truth,Y))) → → ) |
0.01
|
0.01
|
||||||||||||||||||||||||||||||
| LDA015-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA016-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA017-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA018-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA019-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA020-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA021-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA022-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA023-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA024-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA025-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA026-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA027-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA028-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA029-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA030-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA031-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA032-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA033-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA034-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA035-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA036-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA037-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA038-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA039-1 | (0.67) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| LDA040-1 | (0.67) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| REL014-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| REL053-1 | (0.00) |
⊥
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG025-8 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG025-9 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG030-6 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG030-7 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG031-6 | (0.33) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG031-7 | (0.33) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG032-6 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG032-7 | (1.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG042-2 | (0.00) |
5.55
RNG042-2
Convergent TRS(VAR Y,add(X,additive_inverse(Y))) -> )
(RULES multiply(additive_inverse(X),Y) → additive_inverse(multiply(X,Y)) add(additive_inverse(X),X) → additive_identity add(Y,add(additive_inverse(Y),X)) → X multiply(add(X,Z),Y) → add(multiply(X,Y),multiply(Z,Y)) multiply(additive_identity,X) → additive_identity add(additive_identity,X) → X multiply(X,additive_inverse(Y)) → additive_inverse(multiply(X,Y)) add(additive_inverse(Y),add(X,Y)) → X add(add(X,Y),Z) → add(X,add(Y,Z)) multiply(X,additive_identity) → additive_identity additive_inverse(additive_identity) → additive_identity add(X,additive_identity) → X additive_inverse(additive_inverse(X)) → X multiply(X,add(Y,Z)) → add(multiply(X,Y),multiply(X,Z)) add(X,additive_inverse(X)) → additive_identity additive_inverse(add(X,Y)) → add(additive_inverse(X),additive_inverse(Y)) add(Y,add(Z,X)) = add(X,add(Y,Z)) add(X,add(Y,Z)) = add(Y,add(X,Z)) → → add(X,add(Y,Z)) = add(Y,add(Z,X)) → ) |
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG042-3 | (0.00) |
3.09
RNG042-3
Convergent TRS(VAR Y,add(X,additive_inverse(Y))) -> )
(RULES add(Y,add(additive_inverse(Y),X)) → X add(additive_inverse(Y),add(X,Y)) → X add(Z,add(X,add(additive_inverse(Z),Y))) → add(X,Y) add(Z,add(X,add(Y,additive_inverse(Z)))) → add(X,Y) multiply(additive_inverse(X),Y) → additive_inverse(multiply(X,Y)) additive_inverse(additive_identity) → additive_identity add(X,additive_identity) → X add(X,additive_inverse(X)) → additive_identity multiply(multiply(X,Y),Z) → multiply(X,multiply(Y,Z)) multiply(add(X,Z),Y) → add(multiply(X,Y),multiply(Z,Y)) multiply(additive_identity,X) → additive_identity add(additive_identity,X) → X multiply(X,additive_inverse(Y)) → additive_inverse(multiply(X,Y)) add(add(X,Y),Z) → add(X,add(Y,Z)) multiply(X,additive_identity) → additive_identity additive_inverse(additive_inverse(X)) → X multiply(X,add(Y,Z)) → add(multiply(X,Y),multiply(X,Z)) additive_inverse(add(Y,X)) → add(additive_inverse(X),additive_inverse(Y)) add(additive_inverse(Z),add(X,add(Z,Y))) → add(X,Y) add(additive_inverse(Z),add(X,add(Y,Z))) → add(X,Y) add(Y,add(Z,X)) = add(X,add(Y,Z)) add(X,add(Y,Z)) = add(Y,add(X,Z)) → → add(X,add(Y,Z)) = add(Y,add(Z,X)) → ) |
∞
|
∞
|
||||||||||||||||||||||||||||||
| RNG043-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| ROB028-1 | (0.00) |
∞
|
∞
|
∞
|
||||||||||||||||||||||||||||||
| SYN305-1 | (0.67) |
0.00
SYN305-1
Convergent TRS(VAR (X)) -> )
(RULES ) |
0.01
|
0.00
|
||||||||||||||||||||||||||||||
| SYN552-1 | (0.00) |
0.00
SYN552-1
|
0.00
|
0.00
|
||||||||||||||||||||||||||||||
| max_iterations | 14 | |||||||||||||||||||||||||||||||||
| max_restarts | 2 | |||||||||||||||||||||||||||||||||
| equalities | 146 | |||||||||||||||||||||||||||||||||
| total equalities | 508 | |||||||||||||||||||||||||||||||||
| goals | ||||||||||||||||||||||||||||||||||
| restarts | 7 | |||||||||||||||||||||||||||||||||
| hard restarts | ||||||||||||||||||||||||||||||||||
| successes | 14 | 12 | 11 | |||||||||||||||||||||||||||||||
| timeouts | 115 | 132 | 133 | |||||||||||||||||||||||||||||||
| median time | 0.014 | 0.008 | ||||||||||||||||||||||||||||||||
| time/overlaps | 2s (1%) | |||||||||||||||||||||||||||||||||
| time/rewrite | 3s (3%) | |||||||||||||||||||||||||||||||||
| time/select | 0s (0%) | |||||||||||||||||||||||||||||||||
| time/subsumption checks | ||||||||||||||||||||||||||||||||||
| time/success checks | 112s (91%) | |||||||||||||||||||||||||||||||||
| time/sat | 0s (0%) | |||||||||||||||||||||||||||||||||
| total time | 123.709 | 0.08 | 0.025 | |||||||||||||||||||||||||||||||
| average time | 8.84 | 0.01 | ||||||||||||||||||||||||||||||||
| errors | 15 | |||||||||||||||||||||||||||||||||
| average memory | 215 MB | |||||||||||||||||||||||||||||||||
| OVERALL STATS | ||||||||||||||||||||||||||||||||||
| solved | 14 | |||||||||||||||||||||||||||||||||
| diff solved | 3 | |||||||||||||||||||||||||||||||||