MAYBE /home/aoto/lab/www/tools/agcp/experiments/fscd17/problems55/insert.trs Input rules: [ ordered(nil) -> true, ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)), leList(?x:Nat,nil) -> true, leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)), le(0,?y:Nat) -> true, le(s(?x:Nat),0) -> false, le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat), and(true,true) -> true, and(?x:Bool,true) -> ?x:Bool, and(true,?y:Bool) -> ?y:Bool, and(false,false) -> false, sort(nil) -> nil, sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)), insert(?x:Nat,nil) -> cons(?x:Nat,nil), insert(?x:Nat,cons(?y:Nat,?ys:List)) -> if(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))), if(true,?y:List,?z:List) -> ?y:List, if(false,?y:List,?z:List) -> ?z:List, ordered(sort(?xs:List)) -> true ] Sorts having no ground terms: Rules applicable to ground terms: [ ordered(nil) -> true, ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)), leList(?x:Nat,nil) -> true, leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)), le(0,?y:Nat) -> true, le(s(?x:Nat),0) -> false, le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat), and(true,true) -> true, and(?x:Bool,true) -> ?x:Bool, and(true,?y:Bool) -> ?y:Bool, and(false,false) -> false, sort(nil) -> nil, sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)), insert(?x:Nat,nil) -> cons(?x:Nat,nil), insert(?x:Nat,cons(?y:Nat,?ys:List)) -> if(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))), if(true,?y:List,?z:List) -> ?y:List, if(false,?y:List,?z:List) -> ?z:List, ordered(sort(?xs:List)) -> true ] Constructor pattern: [cons(?x_1,?x_2),true,false,nil,s(?x_1),0] Defined pattern: [and(?x_2,?x_3),if(?x_3,?x_4,?x_5),insert(?x_2,?x_3),sort(?x_1),le(?x_2,?x_3),leList(?x_2,?x_3),ordered(?x_1)] Constructor subsystem: [ ] Modified Constructor subsystem: [ ] candidate for and(?x_2,?x_3): [ and(?x,true) -> ?x, and(true,?y) -> ?y, and(false,false) -> false ] candidate for if(?x_3,?x_4,?x_5): [ if(true,?y,?z) -> ?y, if(false,?y,?z) -> ?z ] candidate for insert(?x_2,?x_3): [ insert(?x,nil) -> cons(?x,nil), insert(?x,cons(?y,?ys)) -> if(le(?x,?y),cons(?x,cons(?y,?ys)),cons(?y,insert(?x,?ys))) ] candidate for sort(?x_1): [ sort(nil) -> nil, sort(cons(?x,?ys)) -> insert(?x,sort(?ys)) ] candidate for le(?x_2,?x_3): [ le(0,?y) -> true, le(s(?x),0) -> false, le(s(?x),s(?y)) -> le(?x,?y) ] candidate for leList(?x_2,?x_3): [ leList(?x,nil) -> true, leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)) ] candidate for ordered(?x_1): [ ordered(nil) -> true, ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)) ] Find a quasi-ordering ... order successfully found Precedence: ordered : Mul; sort : Mul; leList : Mul; nil : Mul, 0 : Mul; false : Mul; s : Mul; insert : Mul; if : Mul; true : Mul; and : Mul; cons : Mul, le : Mul; Rules: [ and(?x,true) -> ?x, and(true,?y) -> ?y, and(false,false) -> false, if(true,?y,?z) -> ?y, if(false,?y,?z) -> ?z, insert(?x,nil) -> cons(?x,nil), insert(?x,cons(?y,?ys)) -> if(le(?x,?y),cons(?x,cons(?y,?ys)),cons(?y,insert(?x,?ys))), sort(nil) -> nil, sort(cons(?x,?ys)) -> insert(?x,sort(?ys)), le(0,?y) -> true, le(s(?x),0) -> false, le(s(?x),s(?y)) -> le(?x,?y), leList(?x,nil) -> true, leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)), ordered(nil) -> true, ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)) ] Conjectures: [ ordered(sort(?xs)) = true, and(true,true) = true, true = true ] STEP 0 ES: [ ordered(sort(?xs)) = true, and(true,true) = true, true = true ] HS: [ ] ES0: [ ordered(sort(?xs)) = true, true = true, true = true ] HS0: [ ] ES1: [ ordered(sort(?xs)) = true ] HS1: [ ] Expand ordered(sort(?xs)) = true [ ordered(nil) = true, ordered(insert(?x_7,sort(?ys_7))) = true ] ES2: [ true = true, ordered(insert(?x_7,sort(?ys_7))) = true ] HS2: [ ordered(sort(?xs)) -> true ] STEP 1 ES: [ true = true, ordered(insert(?x_7,sort(?ys_7))) = true ] HS: [ ordered(sort(?xs)) -> true ] ES0: [ true = true, ordered(insert(?x_7,sort(?ys_7))) = true ] HS0: [ ordered(sort(?xs)) -> true ] ES1: [ ordered(insert(?x_7,sort(?ys_7))) = true ] HS1: [ ordered(sort(?xs)) -> true ] Expand ordered(insert(?x_7,sort(?ys_7))) = true [ ordered(insert(?x,nil)) = true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) = true ] ES2: [ true = true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) = true ] HS2: [ ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 2 ES: [ true = true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) = true ] HS: [ ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ true = true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) = true ] HS0: [ ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(insert(?x,insert(?x_7,sort(?ys_7)))) = true ] HS1: [ ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(insert(?x,insert(?x_7,sort(?ys_7)))) = true [ ordered(insert(?x,insert(?x_7,nil))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) = true ] ES2: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) = true ] HS2: [ ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 3 ES: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) = true ] HS: [ ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) = true ] HS0: [ ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) = true ] HS1: [ ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) = true [ ordered(insert(?x,insert(?x_7,insert(?x_14,nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) = true ] ES2: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true ] HS2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 4 ES: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true ] HS: [ ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true ] HS0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true ] HS1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) = true [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) = true ] ES2: [ ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true ] HS2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 5 ES: [ ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true ] HS: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true ] HS0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true ] HS1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) = true [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) = true ] ES2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true ] HS2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 6 ES: [ ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true ] HS: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true ] HS0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true ] HS1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) = true [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,nil))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true ] ES2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 7 ES: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) = true [ ordered(if(true,cons(0,cons(?y_15,nil)),cons(?y_15,cons(0,nil)))) = true, ordered(if(false,cons(s(?x_16),cons(0,nil)),cons(0,cons(s(?x_16),nil)))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true ] ES2: [ true = true, true = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true ] HS2: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 8 ES: [ true = true, true = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true ] HS: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ true = true, true = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true ] HS0: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true ] HS1: [ ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) = true [ ordered(insert(?x,if(true,cons(0,cons(?y_22,nil)),cons(?y_22,cons(0,nil))))) = true, ordered(insert(?x,if(false,cons(s(?x_23),cons(0,nil)),cons(0,cons(s(?x_23),nil))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true ] ES2: [ ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS2: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 9 ES: [ ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS0: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true ] HS1: [ ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Expand ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) = true [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,nil)))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,insert(?x_49,sort(?ys_49)))))))))) = true ] ES2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,if(le(?x_35,?x_42),cons(?x_35,cons(?x_42,nil)),cons(?x_42,cons(?x_35,nil))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,insert(?x_49,sort(?ys_49)))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true ] HS2: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) -> true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] STEP 10 ES: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,if(le(?x_35,?x_42),cons(?x_35,cons(?x_42,nil)),cons(?x_42,cons(?x_35,nil))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,insert(?x_49,sort(?ys_49)))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true ] HS: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) -> true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,if(le(?x_35,?x_42),cons(?x_35,cons(?x_42,nil)),cons(?x_42,cons(?x_35,nil))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,insert(?x_49,sort(?ys_49)))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true ] HS0: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) -> true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] ES1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,if(le(?x_35,?x_42),cons(?x_35,cons(?x_42,nil)),cons(?x_42,cons(?x_35,nil))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,insert(?x_49,sort(?ys_49)))))))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,if(le(?x_21,?x_28),cons(?x_21,cons(?x_28,nil)),cons(?x_28,cons(?x_21,nil))))))) = true, ordered(if(le(?x_17,?y_17),cons(s(?x_17),cons(s(?y_17),nil)),cons(s(?y_17),cons(s(?x_17),nil)))) = true, ordered(insert(?x,insert(?x_7,if(le(?x_14,?x_21),cons(?x_14,cons(?x_21,nil)),cons(?x_21,cons(?x_14,nil)))))) = true, ordered(insert(?x,if(le(?x_24,?y_24),cons(s(?x_24),cons(s(?y_24),nil)),cons(s(?y_24),cons(s(?x_24),nil))))) = true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,if(le(?x_28,?x_35),cons(?x_28,cons(?x_35,nil)),cons(?x_35,cons(?x_28,nil)))))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(?y_22,nil))),cons(0,if(le(?x,?y_22),cons(?x,cons(?y_22,nil)),cons(?y_22,cons(?x,nil)))))) = true, ordered(if(le(?x,0),cons(?x,cons(0,cons(s(?x_23),nil))),cons(0,if(le(?x,s(?x_23)),cons(?x,cons(s(?x_23),nil)),cons(s(?x_23),cons(?x,nil)))))) = true ] HS1: [ ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,insert(?x_42,sort(?ys_42))))))))) -> true, ordered(insert(?x,if(le(?x_7,?x_14),cons(?x_7,cons(?x_14,nil)),cons(?x_14,cons(?x_7,nil))))) -> true, ordered(if(le(?x,?x_7),cons(?x,cons(?x_7,nil)),cons(?x_7,cons(?x,nil)))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,insert(?x_35,sort(?ys_35)))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,insert(?x_28,sort(?ys_28))))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,insert(?x_21,sort(?ys_21)))))) -> true, ordered(insert(?x,insert(?x_7,insert(?x_14,sort(?ys_14))))) -> true, ordered(insert(?x,insert(?x_7,sort(?ys_7)))) -> true, ordered(insert(?x_7,sort(?ys_7))) -> true, ordered(sort(?xs)) -> true ] Stopped: the smallest size of equations exceeeds the limit. Try to select different rules for le ... check Non-Ground-Confluence... ground constructor terms for instantiation: {true,false,nil,0,cons(0,nil),s(0)} ground terms for instantiation: {true:Bool,false:Bool,nil:List,0:Nat,cons(0,nil):List,s(0):Nat} obtain 20 rules by 3 steps unfolding obtain 6 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (failure) : Failure(unknown) (2676 msec.)