0.00/0.15	MAYBE
0.00/0.15	/export/starexec/sandbox2/benchmark/theBenchmark.trs
0.00/0.15	Input rules:
0.00/0.15	   [ Ap(Ap(Ap(S,?x:o),?y:o),?z:o) -> Ap(Ap(?x:o,?z:o),Ap(?y:o,?z:o)),
0.00/0.15	     Ap(Ap(K,?x:o),?y:o) -> ?x:o,
0.00/0.15	     Ap(I,?x:o) -> ?x:o,
0.00/0.15	     Ap(Ap(Dk,?z:o),?z:o) -> Ap(E,?z:o) ]
0.00/0.15	Sorts having no ground terms: 
0.00/0.15	Rules applicable to ground terms:
0.00/0.15	   [ Ap(Ap(Ap(S,?x:o),?y:o),?z:o) -> Ap(Ap(?x:o,?z:o),Ap(?y:o,?z:o)),
0.00/0.15	     Ap(Ap(K,?x:o),?y:o) -> ?x:o,
0.00/0.15	     Ap(I,?x:o) -> ?x:o,
0.00/0.15	     Ap(Ap(Dk,?z:o),?z:o) -> Ap(E,?z:o) ]
0.00/0.15	Constructor pattern: [Ap(?x_1,?x_2),S,K,I,Dk,E]
0.00/0.15	Defined pattern: []
0.00/0.15	Constructor subsystem:
0.00/0.15	   [ Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)),
0.00/0.15	     Ap(Ap(K,?x),?y) -> ?x,
0.00/0.15	     Ap(I,?x) -> ?x,
0.00/0.15	     Ap(Ap(Dk,?z),?z) -> Ap(E,?z) ]
0.00/0.15	Modified Constructor subsystem:
0.00/0.15	   [ Ap(Ap(Ap(S,?x),?y),?z) -> Ap(Ap(?x,?z),Ap(?y,?z)),
0.00/0.15	     Ap(Ap(K,?x),?y) -> ?x,
0.00/0.15	     Ap(I,?x) -> ?x,
0.00/0.15	     Ap(Ap(Dk,?z),?z) -> Ap(E,?z) ]
0.00/0.15	Find a quasi-ordering ...
0.00/0.15	order successfully found
0.00/0.15	Precedence:
0.00/0.15	 K : Mul,  I : Mul;
0.00/0.15	 Ap : Mul;
0.00/0.15	 E : Mul;
0.00/0.15	 Dk : Mul,  S : Mul;
0.00/0.15	Rules:
0.00/0.15	   [ Ap(Ap(K,?x),?y) -> ?x,
0.00/0.15	     Ap(I,?x) -> ?x,
0.00/0.15	     Ap(Ap(Dk,?z),?z) -> Ap(E,?z) ]
0.00/0.15	Check confluence of constructor subsystem...
0.00/0.15	Check Termination...
0.00/0.15	Terminating, WCR: CR
0.00/0.15	Conjectures:
0.00/0.15	   [ Ap(Ap(Ap(S,?x),?y),?z) = Ap(Ap(?x,?z),Ap(?y,?z)) ]
0.00/0.15	STEP 0
0.00/0.15	ES:
0.00/0.15	   [ Ap(Ap(Ap(S,?x),?y),?z) = Ap(Ap(?x,?z),Ap(?y,?z)) ]
0.00/0.15	HS:
0.00/0.15	   [ ]
0.00/0.15	ES0:
0.00/0.15	   [ Ap(Ap(Ap(S,?x),?y),?z) = Ap(Ap(?x,?z),Ap(?y,?z)) ]
0.00/0.15	HS0:
0.00/0.15	   [ ]
0.00/0.15	ES1:
0.00/0.15	   [ Ap(Ap(Ap(S,?x),?y),?z) = Ap(Ap(?x,?z),Ap(?y,?z)) ]
0.00/0.15	HS1:
0.00/0.15	   [ ]
0.00/0.15	No equation to expand
0.00/0.15	check Non-Ground-Confluence...
0.00/0.15	ground constructor terms for instantiation: {S,K,I,Dk,E,Ap(S,S),Ap(S,K),Ap(S,I),Ap(S,Dk),Ap(S,E),Ap(K,S),Ap(K,K),Ap(K,I),Ap(K,Dk),Ap(K,E),Ap(I,S),Ap(I,K),Ap(I,I),Ap(I,Dk),Ap(I,E),Ap(Dk,S),Ap(Dk,K),Ap(Dk,I),Ap(Dk,Dk),Ap(Dk,E),Ap(E,S),Ap(E,K),Ap(E,I),Ap(E,Dk),Ap(E,E)}
0.00/0.15	ground terms for instantiation: {S:o,K:o,I:o,Dk:o,E:o,Ap(S,S):o,Ap(S,K):o,Ap(S,I):o,Ap(S,Dk):o,Ap(S,E):o,Ap(K,S):o,Ap(K,K):o,Ap(K,I):o,Ap(K,Dk):o,Ap(K,E):o,Ap(I,S):o,Ap(I,K):o,Ap(I,I):o,Ap(I,Dk):o,Ap(I,E):o,Ap(Dk,S):o,Ap(Dk,K):o,Ap(Dk,I):o,Ap(Dk,Dk):o,Ap(Dk,E):o,Ap(E,S):o,Ap(E,K):o,Ap(E,I):o,Ap(E,Dk):o,Ap(E,E):o}
0.00/0.15	obtain 6 rules by 3 steps unfolding
0.00/0.15	obtain 1 candidates for checking non-joinability
0.00/0.15	check by TCAP-Approximation (failure)
0.00/0.15	check by Ordering(rpo), check by Tree-Automata Approximation (failure)
0.00/0.15	check by Interpretation(mod2) (failure)
0.00/0.15	check by Descendants-Approximation, check by Ordering(poly) (failure)
0.00/0.15	: Failure(unknown)
0.00/0.15	(99 msec.)
0.00/0.15	
0.00/0.15	=============================
0.00/0.15	Total: 0 Success, 1 Failure: 100 millisec.
0.00/0.15	EOF