0.52/0.56 MAYBE 0.52/0.56 /export/starexec/sandbox/benchmark/theBenchmark.trs 0.52/0.56 Input rules: 0.52/0.56 [ g(?x:o,?x:o,?y:o) -> ?y:o, 0.52/0.56 g(?x:o,?y:o,?y:o) -> ?x:o, 0.52/0.56 f(?x:o,?y:o,?x:o,?y:o,?z:o) -> f(a,b,?z:o,?z:o,?z:o), 0.52/0.56 a -> 0, 0.52/0.56 b -> 0 ] 0.52/0.56 Sorts having no ground terms: 0.52/0.56 Rules applicable to ground terms: 0.52/0.56 [ g(?x:o,?x:o,?y:o) -> ?y:o, 0.52/0.56 g(?x:o,?y:o,?y:o) -> ?x:o, 0.52/0.56 f(?x:o,?y:o,?x:o,?y:o,?z:o) -> f(a,b,?z:o,?z:o,?z:o), 0.52/0.56 a -> 0, 0.52/0.56 b -> 0 ] 0.52/0.56 Constructor pattern: [0] 0.52/0.56 Defined pattern: [b,a,f(?x_5,?x_6,?x_7,?x_8,?x_9),g(?x_3,?x_4,?x_5)] 0.52/0.56 Constructor subsystem: 0.52/0.56 [ ] 0.52/0.56 Modified Constructor subsystem: 0.52/0.56 [ ] 0.52/0.56 candidate for b: 0.52/0.56 [ b -> 0 ] 0.52/0.56 candidate for a: 0.52/0.56 [ a -> 0 ] 0.52/0.56 No orientable rules for f(?x_5,?x_6,?x_7,?x_8,?x_9). Add rules, and retry... 0.52/0.56 Added rules: 0.52/0.56 [ f(0,0,0,0,0) -> f(a,b,0,0,0) ] 0.52/0.56 candidate for f(?x_5,?x_6,?x_7,?x_8,?x_9): 0.52/0.56 [ f(0,0,0,0,0) -> f(a,b,0,0,0) ] 0.52/0.56 No orientable rules for g(?x_3,?x_4,?x_5). Add rules, and retry... 0.52/0.56 Added rules: 0.52/0.56 [ g(0,0,0) -> 0 ] 0.52/0.56 candidate for g(?x_3,?x_4,?x_5): 0.52/0.56 [ g(0,0,0) -> 0 ] 0.52/0.56 Find a quasi-ordering ... 0.52/0.56 encodeSameNthStatus f/0, f/1 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/0, f/2 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/0, f/3 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/0, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/1, f/2 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/1, f/3 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/1, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/2, f/3 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/2, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/3, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus g/0, g/1 0.52/0.56 encodeSameNthStatus(sub) logArF:2, logArG:2 0.52/0.56 encodeSameNthStatus g/0, g/2 0.52/0.56 encodeSameNthStatus(sub) logArF:2, logArG:2 0.52/0.56 encodeSameNthStatus g/1, g/2 0.52/0.56 encodeSameNthStatus(sub) logArF:2, logArG:2 0.52/0.56 failed to find an ordering. 0.52/0.56 Try to supplement auxiliary rules. 0.52/0.56 {}{}{f(a,b,?z,?z,?z)}{}{}Supplemented Rules: 0.52/0.56 [ f(?x,?y,?x,?y,?z) -> f(0,0,?z,?z,?z) ] 0.52/0.56 Constructor subsystem: 0.52/0.56 [ ] 0.52/0.56 Modified Constructor subsystem: 0.52/0.56 [ ] 0.52/0.56 candidate for b: 0.52/0.56 [ b -> 0 ] 0.52/0.56 candidate for a: 0.52/0.56 [ a -> 0 ] 0.52/0.56 No orientable rules for f(?x_5,?x_6,?x_7,?x_8,?x_9). Add rules, and retry... 0.52/0.56 Added rules: 0.52/0.56 [ f(0,0,0,0,0) -> f(a,b,0,0,0) ] 0.52/0.56 candidate for f(?x_5,?x_6,?x_7,?x_8,?x_9): 0.52/0.56 [ f(0,0,0,0,0) -> f(a,b,0,0,0) ] 0.52/0.56 No orientable rules for g(?x_3,?x_4,?x_5). Add rules, and retry... 0.52/0.56 Added rules: 0.52/0.56 [ g(0,0,0) -> 0 ] 0.52/0.56 candidate for g(?x_3,?x_4,?x_5): 0.52/0.56 [ g(0,0,0) -> 0 ] 0.52/0.56 Find a quasi-ordering ... 0.52/0.56 encodeSameNthStatus f/0, f/1 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/0, f/2 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/0, f/3 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/0, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/1, f/2 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/1, f/3 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/1, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/2, f/3 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/2, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus f/3, f/4 0.52/0.56 encodeSameNthStatus(sub) logArF:3, logArG:3 0.52/0.56 encodeSameNthStatus g/0, g/1 0.52/0.56 encodeSameNthStatus(sub) logArF:2, logArG:2 0.52/0.56 encodeSameNthStatus g/0, g/2 0.52/0.56 encodeSameNthStatus(sub) logArF:2, logArG:2 0.52/0.56 encodeSameNthStatus g/1, g/2 0.52/0.56 encodeSameNthStatus(sub) logArF:2, logArG:2 0.52/0.56 failed to find an ordering. 0.52/0.56 Try to supplement auxiliary rules. 0.52/0.56 {}{}{f(a,b,?z,?z,?z)}{}{}{f(0,0,?z,?z,?z)}Supplemented Rules: 0.52/0.56 [ ] 0.52/0.56 failed to supplement auxiliary rules 0.52/0.56 Retry with a different D/C-partition. 0.52/0.56 Constructor pattern: [0,g(?x_3,?x_4,?x_5)] 0.52/0.56 Defined pattern: [b,a,f(?x_5,?x_6,?x_7,?x_8,?x_9)] 0.52/0.56 Constructor subsystem: 0.52/0.56 [ g(?x,?x,?y) -> ?y, 0.52/0.56 g(?x,?y,?y) -> ?x ] 0.52/0.56 Modified Constructor subsystem: 0.52/0.56 [ g(?x,?x,?y) -> ?y, 0.52/0.56 g(?x,?y,?y) -> ?x ] 0.52/0.56 candidate for b: 0.52/0.56 [ b -> 0 ] 0.52/0.56 candidate for a: 0.52/0.56 [ a -> 0 ] 0.52/0.56 No orientable rules for f(?x_5,?x_6,?x_7,?x_8,?x_9). Add rules, and retry... 0.52/0.56 Added rules: 0.52/0.56 [ f(0,0,0,0,0) -> f(a,b,0,0,0), 0.52/0.56 f(0,0,0,0,g(?x_3,?x_4,?x_5)) -> f(a,b,g(?x_3,?x_4,?x_5),g(?x_3,?x_4,?x_5),g(?x_3,?x_4,?x_5)) ] 0.52/0.56 candidate for f(?x_5,?x_6,?x_7,?x_8,?x_9): 0.52/0.56 No canditates. Supplement rules, and retry... 0.52/0.56 patlist: 0.52/0.56 {0,0,0,0,0} 0.52/0.56 {0,0,0,0,g(?x_3,?x_4,?x_5)} 0.52/0.56 Required Patterns: {f(0,0,0,g(?x_3,?x_4,?x_5),0),f(0,0,0,g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8)),f(0,0,g(?x_3,?x_4,?x_5),0,0),f(0,0,g(?x_3,?x_4,?x_5),0,g(?x_6,?x_7,?x_8)),f(0,0,g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),0),f(0,0,g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11)),f(0,g(?x_3,?x_4,?x_5),0,0,0),f(0,g(?x_3,?x_4,?x_5),0,0,g(?x_6,?x_7,?x_8)),f(0,g(?x_3,?x_4,?x_5),0,g(?x_6,?x_7,?x_8),0),f(0,g(?x_3,?x_4,?x_5),0,g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11)),f(0,g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),0,0),f(0,g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),0,g(?x_9,?x_10,?x_11)),f(0,g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),0),f(0,g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),g(?x_12,?x_13,?x_14)),f(g(?x_3,?x_4,?x_5),0,0,0,0),f(g(?x_3,?x_4,?x_5),0,0,0,g(?x_6,?x_7,?x_8)),f(g(?x_3,?x_4,?x_5),0,0,g(?x_6,?x_7,?x_8),0),f(g(?x_3,?x_4,?x_5),0,0,g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11)),f(g(?x_3,?x_4,?x_5),0,g(?x_6,?x_7,?x_8),0,0),f(g(?x_3,?x_4,?x_5),0,g(?x_6,?x_7,?x_8),0,g(?x_9,?x_10,?x_11)),f(g(?x_3,?x_4,?x_5),0,g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),0),f(g(?x_3,?x_4,?x_5),0,g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),g(?x_12,?x_13,?x_14)),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),0,0,0),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),0,0,g(?x_9,?x_10,?x_11)),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),0,g(?x_9,?x_10,?x_11),0),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),0,g(?x_9,?x_10,?x_11),g(?x_12,?x_13,?x_14)),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),0,0),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),0,g(?x_12,?x_13,?x_14)),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),g(?x_12,?x_13,?x_14),0),f(g(?x_3,?x_4,?x_5),g(?x_6,?x_7,?x_8),g(?x_9,?x_10,?x_11),g(?x_12,?x_13,?x_14),g(?x_15,?x_16,?x_17))} 0.52/0.56 failed to construct defining rules 0.52/0.56 Retry with a different D/C-partition. 0.52/0.56 Constructor pattern: [0,g(?x_3,?x_4,?x_5),f(?x_5,?x_6,?x_7,?x_8,?x_9)] 0.52/0.56 Defined pattern: [b,a] 0.52/0.56 Constructor subsystem: 0.52/0.56 [ g(?x,?x,?y) -> ?y, 0.52/0.56 g(?x,?y,?y) -> ?x ] 0.52/0.56 Modified Constructor subsystem: 0.52/0.56 [ g(?x,?x,?y) -> ?y, 0.52/0.56 g(?x,?y,?y) -> ?x ] 0.52/0.56 candidate for b: 0.52/0.56 [ b -> 0 ] 0.52/0.56 candidate for a: 0.52/0.56 [ a -> 0 ] 0.52/0.56 Find a quasi-ordering ... 0.52/0.56 order successfully found 0.52/0.56 Precedence: 0.52/0.56 f : Mul; 0.52/0.56 b : Mul, a : Mul; 0.52/0.56 0 : Mul; 0.52/0.56 g : Mul; 0.52/0.56 Rules: 0.52/0.56 [ b -> 0, 0.52/0.56 a -> 0, 0.52/0.56 g(?x,?x,?y) -> ?y, 0.52/0.56 g(?x,?y,?y) -> ?x ] 0.52/0.56 Check confluence of constructor subsystem... 0.52/0.56 Check Termination... 0.52/0.56 Terminating, WCR: CR 0.52/0.56 Conjectures: 0.52/0.56 [ f(?x,?y,?x,?y,?z) = f(a,b,?z,?z,?z) ] 0.52/0.56 STEP 0 0.52/0.56 ES: 0.52/0.56 [ f(?x,?y,?x,?y,?z) = f(a,b,?z,?z,?z) ] 0.52/0.56 HS: 0.52/0.56 [ ] 0.52/0.56 ES0: 0.52/0.56 [ f(?x,?y,?x,?y,?z) = f(0,0,?z,?z,?z) ] 0.52/0.56 HS0: 0.52/0.56 [ ] 0.52/0.56 ES1: 0.52/0.56 [ f(?x,?y,?x,?y,?z) = f(0,0,?z,?z,?z) ] 0.52/0.56 HS1: 0.52/0.56 [ ] 0.52/0.56 No equation to expand 0.52/0.56 check Non-Ground-Confluence... 0.52/0.56 ground constructor terms for instantiation: {0} 0.52/0.56 ground terms for instantiation: {0:o} 0.52/0.56 obtain 9 rules by 3 steps unfolding 0.52/0.56 obtain 3 candidates for checking non-joinability 0.52/0.56 check by TCAP-Approximation (failure) 0.52/0.56 check by Ordering(rpo), check by Tree-Automata Approximation (failure) 0.52/0.56 check by Interpretation(mod2) (failure) 0.52/0.56 check by Descendants-Approximation, check by Ordering(poly) (failure) 0.52/0.56 : Failure(unknown) 0.52/0.56 (399 msec.) 0.52/0.56 0.52/0.56 ============================= 0.52/0.56 Total: 0 Success, 1 Failure: 400 millisec. 0.52/0.56 EOF