0.00/0.01	YES
0.00/0.01	
0.00/0.01	
0.00/0.01	Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs".
0.00/0.01	    (CONDITIONTYPE ORIENTED)
0.00/0.01	    (VAR c b a)
0.00/0.01	    (RULES
0.00/0.01	      App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) | a == I, b == I, c == I
0.00/0.01	      App(App(K,a),b) -> a | a == I, b == I
0.00/0.01	      App(I,a) -> a | a == I
0.00/0.01	    )
0.00/0.01	    (COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] Example 2.3.ii submitted by: Thomas Sternagel and Aart Middeldorp)
0.00/0.01	
0.00/0.01	No "->="-rules.
0.00/0.01	
0.00/0.01	Decomposed conditions if possible.
0.00/0.01	    (CONDITIONTYPE ORIENTED)
0.00/0.01	    (VAR c b a)
0.00/0.01	    (RULES
0.00/0.01	      App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) | a == I, b == I, c == I
0.00/0.01	      App(App(K,a),b) -> a | a == I, b == I
0.00/0.01	      App(I,a) -> a | a == I
0.00/0.01	    )
0.00/0.01	    (COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] Example 2.3.ii submitted by: Thomas Sternagel and Aart Middeldorp)
0.00/0.01	
0.00/0.01	Removed infeasible rules as much as possible.
0.00/0.01	    (CONDITIONTYPE ORIENTED)
0.00/0.01	    (VAR c b a)
0.00/0.01	    (RULES
0.00/0.01	      App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) | a == I, b == I, c == I
0.00/0.01	      App(App(K,a),b) -> a | a == I, b == I
0.00/0.01	      App(I,a) -> a | a == I
0.00/0.01	    )
0.00/0.01	    (COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] Example 2.3.ii submitted by: Thomas Sternagel and Aart Middeldorp)
0.00/0.01	
0.00/0.01	Try to disprove confluence of the following (C)TRS:
0.00/0.01	    (CONDITIONTYPE ORIENTED)
0.00/0.01	    (VAR c b a)
0.00/0.01	    (RULES
0.00/0.01	      App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) | a == I, b == I, c == I
0.00/0.01	      App(App(K,a),b) -> a | a == I, b == I
0.00/0.01	      App(I,a) -> a | a == I
0.00/0.01	    )
0.00/0.01	    (COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] Example 2.3.ii submitted by: Thomas Sternagel and Aart Middeldorp)
0.00/0.01	
0.00/0.01	Failed either to apply SR and U for normal 1CTRSs to the above CTRS or to prove confluence of any converted TRSs.
0.00/0.01	
0.00/0.01	Try to apply SR and U for 3DCTRSs to the above CTRS.
0.00/0.01	
0.00/0.01	Succeeded in applying U for 3DCTRSs to the above CTRS.
0.00/0.01	U(R) =
0.00/0.01	    (VAR x1 x2 x3)
0.00/0.01	    (RULES
0.00/0.01	      App(I,x1) -> u1(x1,x1)
0.00/0.01	      u1(I,x1) -> x1
0.00/0.01	      App(App(K,x1),x2) -> u2(x1,x1,x2)
0.00/0.01	      u2(I,x1,x2) -> u3(x2,x1,x2)
0.00/0.01	      u3(I,x1,x2) -> x1
0.00/0.01	      App(App(App(S,x1),x2),x3) -> u4(x1,x1,x2,x3)
0.00/0.01	      u4(I,x1,x2,x3) -> u5(x2,x1,x2,x3)
0.00/0.01	      u5(I,x1,x2,x3) -> u6(x3,x1,x2,x3)
0.00/0.01	      u6(I,x1,x2,x3) -> App(App(x1,x3),App(x2,x3))
0.00/0.01	    )
0.00/0.01	
0.00/0.01	U for 3DCTRSs is sound for the above CTRS.
0.00/0.01	
0.00/0.01	U(R) is confluent.
0.00/0.01	
0.00/0.01	YES
0.00/0.01	EOF