NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (?,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (?,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (?,1) 3. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 4. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= X] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [X >= 1] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,2,1 + D,E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C = 2] (?,1) 8. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,P,Q,R,S,T,U,V,W) [Y >= 1 && B >= 1 + A] (?,1) 9. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && B1 >= 2] (?,1) 10. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && 0 >= B1] (?,1) 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(1 + A,B,1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,R,1,1,1,0,W) [0 >= Y && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) True (1,1) Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,23)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},4->{},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,2,7},10->{1,2,7},11->{0,8,9 ,10,11},12->{0,8,9,10,11}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,2),(10,1),(10,7)] * Step 2: UnreachableRules NO + Considered Problem: Rules: 0. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (?,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (?,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (?,1) 3. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 4. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= X] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [X >= 1] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,2,1 + D,E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C = 2] (?,1) 8. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,P,Q,R,S,T,U,V,W) [Y >= 1 && B >= 1 + A] (?,1) 9. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && B1 >= 2] (?,1) 10. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && 0 >= B1] (?,1) 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(1 + A,B,1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,R,1,1,1,0,W) [0 >= Y && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) True (1,1) Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,23)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},4->{},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,7},10->{2},11->{0,8,9,10 ,11},12->{0,8,9,10,11}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [4] * Step 3: FromIts NO + Considered Problem: Rules: 0. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [A >= B] (?,1) 1. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C >= 3] (?,1) 2. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [1 >= C] (?,1) 3. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) True (?,1) 5. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= X] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [X >= 1] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,2,1 + D,E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C = 2] (?,1) 8. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,P,Q,R,S,T,U,V,W) [Y >= 1 && B >= 1 + A] (?,1) 9. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && B1 >= 2] (?,1) 10. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && 0 >= B1] (?,1) 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(1 + A,B,1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,R,1,1,1,0,W) [0 >= Y && B >= 1 + A] (?,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) True (1,1) Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,23)} Flow Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,7},10->{2},11->{0,8,9,10,11} ,12->{0,8,9,10,11}] + Applied Processor: FromIts + Details: () * Step 4: CloseWith NO + Considered Problem: Rules: f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [A >= B] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [C >= 3] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [1 >= C] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) True f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [0 >= X] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [X >= 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,2,1 + D,E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W) [C = 2] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,C,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,P,Q,R,S,T,U,V ,W) [Y >= 1 && B >= 1 + A] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0 ,W) [B >= 1 + A && 0 >= Y && B1 >= 2] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0 ,W) [B >= 1 + A && 0 >= Y && 0 >= B1] f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(1 + A,B,1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,R,1,1,1,0 ,W) [0 >= Y && B >= 1 + A] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,0) True Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,23)} Rule Graph: [0->{5,6},1->{5,6},2->{5,6},3->{3},5->{3},6->{3},7->{5,6},8->{5,6},9->{1,7},10->{2},11->{0,8,9,10,11} ,12->{0,8,9,10,11}] + Applied Processor: CloseWith False + Details: () NO