============================== FOF-Prover9 =========================== FOF-Prover9 (32) version 22-May-2007, May 2007. Process 27407 was started by mccune on cleo, Tue May 22 14:45:23 2007 The command was "/home/mccune/bin/fof-prover9 -f SWC339+1.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file SWC339+1.in assign(max_seconds,30). set(prolog_style_variables). assign(literal_selection,none). formulas(assumptions). (all U (ssItem(U) -> (all V (ssItem(V) -> (neq(U,V) <-> U != V))))). (exists U (ssItem(U) & (exists V (ssItem(V) & U != V)))). (all U (ssList(U) -> (all V (ssItem(V) -> (memberP(U,V) <-> (exists W (ssList(W) & (exists X (ssList(X) & app(W,cons(V,X)) = U))))))))). (all U (ssList(U) -> (singletonP(U) <-> (exists V (ssItem(V) & cons(V,nil) = U))))). (all U (ssList(U) -> (all V (ssList(V) -> (frontsegP(U,V) <-> (exists W (ssList(W) & app(V,W) = U))))))). (all U (ssList(U) -> (all V (ssList(V) -> (rearsegP(U,V) <-> (exists W (ssList(W) & app(W,V) = U))))))). (all U (ssList(U) -> (all V (ssList(V) -> (segmentP(U,V) <-> (exists W (ssList(W) & (exists X (ssList(X) & app(app(W,V),X) = U))))))))). (all U (ssList(U) -> (cyclefreeP(U) <-> (all V (ssItem(V) -> (all W (ssItem(W) -> (all X (ssList(X) -> (all Y (ssList(Y) -> (all Z (ssList(Z) -> (app(app(X,cons(V,Y)),cons(W,Z)) = U -> -(leq(V,W) & leq(W,V)))))))))))))))). (all U (ssList(U) -> (totalorderP(U) <-> (all V (ssItem(V) -> (all W (ssItem(W) -> (all X (ssList(X) -> (all Y (ssList(Y) -> (all Z (ssList(Z) -> (app(app(X,cons(V,Y)),cons(W,Z)) = U -> leq(V,W) | leq(W,V))))))))))))))). (all U (ssList(U) -> (strictorderP(U) <-> (all V (ssItem(V) -> (all W (ssItem(W) -> (all X (ssList(X) -> (all Y (ssList(Y) -> (all Z (ssList(Z) -> (app(app(X,cons(V,Y)),cons(W,Z)) = U -> lt(V,W) | lt(W,V))))))))))))))). (all U (ssList(U) -> (totalorderedP(U) <-> (all V (ssItem(V) -> (all W (ssItem(W) -> (all X (ssList(X) -> (all Y (ssList(Y) -> (all Z (ssList(Z) -> (app(app(X,cons(V,Y)),cons(W,Z)) = U -> leq(V,W))))))))))))))). (all U (ssList(U) -> (strictorderedP(U) <-> (all V (ssItem(V) -> (all W (ssItem(W) -> (all X (ssList(X) -> (all Y (ssList(Y) -> (all Z (ssList(Z) -> (app(app(X,cons(V,Y)),cons(W,Z)) = U -> lt(V,W))))))))))))))). (all U (ssList(U) -> (duplicatefreeP(U) <-> (all V (ssItem(V) -> (all W (ssItem(W) -> (all X (ssList(X) -> (all Y (ssList(Y) -> (all Z (ssList(Z) -> (app(app(X,cons(V,Y)),cons(W,Z)) = U -> V != W)))))))))))))). (all U (ssList(U) -> (equalelemsP(U) <-> (all V (ssItem(V) -> (all W (ssItem(W) -> (all X (ssList(X) -> (all Y (ssList(Y) -> (app(X,cons(V,cons(W,Y))) = U -> V = W)))))))))))). (all U (ssList(U) -> (all V (ssList(V) -> (neq(U,V) <-> U != V))))). (all U (ssList(U) -> (all V (ssItem(V) -> ssList(cons(V,U)))))). ssList(nil). (all U (ssList(U) -> (all V (ssItem(V) -> cons(V,U) != U)))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssItem(W) -> (all X (ssItem(X) -> (cons(W,U) = cons(X,V) -> W = X & V = U))))))))). (all U (ssList(U) -> nil = U | (exists V (ssList(V) & (exists W (ssItem(W) & cons(W,V) = U)))))). (all U (ssList(U) -> (all V (ssItem(V) -> nil != cons(V,U))))). (all U (ssList(U) -> (nil != U -> ssItem(hd(U))))). (all U (ssList(U) -> (all V (ssItem(V) -> hd(cons(V,U)) = V)))). (all U (ssList(U) -> (nil != U -> ssList(tl(U))))). (all U (ssList(U) -> (all V (ssItem(V) -> tl(cons(V,U)) = U)))). (all U (ssList(U) -> (all V (ssList(V) -> ssList(app(U,V)))))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssItem(W) -> cons(W,app(V,U)) = app(cons(W,V),U))))))). (all U (ssList(U) -> app(nil,U) = U)). (all U (ssItem(U) -> (all V (ssItem(V) -> (leq(U,V) & leq(V,U) -> U = V))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (all W (ssItem(W) -> (leq(U,V) & leq(V,W) -> leq(U,W)))))))). (all U (ssItem(U) -> leq(U,U))). (all U (ssItem(U) -> (all V (ssItem(V) -> (geq(U,V) <-> leq(V,U)))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (lt(U,V) -> -lt(V,U)))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (all W (ssItem(W) -> (lt(U,V) & lt(V,W) -> lt(U,W)))))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (gt(U,V) <-> lt(V,U)))))). (all U (ssItem(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (memberP(app(V,W),U) <-> memberP(V,U) | memberP(W,U)))))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (all W (ssList(W) -> (memberP(cons(V,W),U) <-> U = V | memberP(W,U)))))))). (all U (ssItem(U) -> -memberP(nil,U))). -singletonP(nil). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (frontsegP(U,V) & frontsegP(V,W) -> frontsegP(U,W)))))))). (all U (ssList(U) -> (all V (ssList(V) -> (frontsegP(U,V) & frontsegP(V,U) -> U = V))))). (all U (ssList(U) -> frontsegP(U,U))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (frontsegP(U,V) -> frontsegP(app(U,W),V)))))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (all W (ssList(W) -> (all X (ssList(X) -> (frontsegP(cons(U,W),cons(V,X)) <-> U = V & frontsegP(W,X)))))))))). (all U (ssList(U) -> frontsegP(U,nil))). (all U (ssList(U) -> (frontsegP(nil,U) <-> nil = U))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (rearsegP(U,V) & rearsegP(V,W) -> rearsegP(U,W)))))))). (all U (ssList(U) -> (all V (ssList(V) -> (rearsegP(U,V) & rearsegP(V,U) -> U = V))))). (all U (ssList(U) -> rearsegP(U,U))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (rearsegP(U,V) -> rearsegP(app(W,U),V)))))))). (all U (ssList(U) -> rearsegP(U,nil))). (all U (ssList(U) -> (rearsegP(nil,U) <-> nil = U))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (segmentP(U,V) & segmentP(V,W) -> segmentP(U,W)))))))). (all U (ssList(U) -> (all V (ssList(V) -> (segmentP(U,V) & segmentP(V,U) -> U = V))))). (all U (ssList(U) -> segmentP(U,U))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (all X (ssList(X) -> (segmentP(U,V) -> segmentP(app(app(W,U),X),V)))))))))). (all U (ssList(U) -> segmentP(U,nil))). (all U (ssList(U) -> (segmentP(nil,U) <-> nil = U))). (all U (ssItem(U) -> cyclefreeP(cons(U,nil)))). cyclefreeP(nil). (all U (ssItem(U) -> totalorderP(cons(U,nil)))). totalorderP(nil). (all U (ssItem(U) -> strictorderP(cons(U,nil)))). strictorderP(nil). (all U (ssItem(U) -> totalorderedP(cons(U,nil)))). totalorderedP(nil). (all U (ssItem(U) -> (all V (ssList(V) -> (totalorderedP(cons(U,V)) <-> nil = V | nil != V & totalorderedP(V) & leq(U,hd(V))))))). (all U (ssItem(U) -> strictorderedP(cons(U,nil)))). strictorderedP(nil). (all U (ssItem(U) -> (all V (ssList(V) -> (strictorderedP(cons(U,V)) <-> nil = V | nil != V & strictorderedP(V) & lt(U,hd(V))))))). (all U (ssItem(U) -> duplicatefreeP(cons(U,nil)))). duplicatefreeP(nil). (all U (ssItem(U) -> equalelemsP(cons(U,nil)))). equalelemsP(nil). (all U (ssList(U) -> (nil != U -> (exists V (ssItem(V) & hd(U) = V))))). (all U (ssList(U) -> (nil != U -> (exists V (ssList(V) & tl(U) = V))))). (all U (ssList(U) -> (all V (ssList(V) -> (nil != V & nil != U & hd(V) = hd(U) & tl(V) = tl(U) -> V = U))))). (all U (ssList(U) -> (nil != U -> cons(hd(U),tl(U)) = U))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (app(W,V) = app(U,V) -> W = U))))))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (app(V,W) = app(V,U) -> W = U))))))). (all U (ssList(U) -> (all V (ssItem(V) -> cons(V,U) = app(cons(V,nil),U))))). (all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> app(app(U,V),W) = app(U,app(V,W)))))))). (all U (ssList(U) -> (all V (ssList(V) -> (nil = app(U,V) <-> nil = V & nil = U))))). (all U (ssList(U) -> app(U,nil) = U)). (all U (ssList(U) -> (all V (ssList(V) -> (nil != U -> hd(app(U,V)) = hd(U)))))). (all U (ssList(U) -> (all V (ssList(V) -> (nil != U -> tl(app(U,V)) = app(tl(U),V)))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (geq(U,V) & geq(V,U) -> U = V))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (all W (ssItem(W) -> (geq(U,V) & geq(V,W) -> geq(U,W)))))))). (all U (ssItem(U) -> geq(U,U))). (all U (ssItem(U) -> -lt(U,U))). (all U (ssItem(U) -> (all V (ssItem(V) -> (all W (ssItem(W) -> (leq(U,V) & lt(V,W) -> lt(U,W)))))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (leq(U,V) -> U = V | lt(U,V)))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (lt(U,V) <-> U != V & leq(U,V)))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (gt(U,V) -> -gt(V,U)))))). (all U (ssItem(U) -> (all V (ssItem(V) -> (all W (ssItem(W) -> (gt(U,V) & gt(V,W) -> gt(U,W)))))))). -(all U (ssList(U) -> (all V (ssList(V) -> (all W (ssList(W) -> (all X (ssList(X) -> V != X | U != W | (all Y (ssList(Y) -> (all Z (ssList(Z) -> app(app(Y,W),Z) != X | -totalorderedP(W) | (exists X1 (ssItem(X1) & (exists X2 (ssList(X2) & app(X2,cons(X1,nil)) = Y & (exists X3 (ssItem(X3) & (exists X4 (ssList(X4) & app(cons(X3,nil),X4) = W & leq(X1,X3))))))))) | (exists X5 (ssItem(X5) & (exists X6 (ssList(X6) & app(cons(X5,nil),X6) = Z & (exists X7 (ssItem(X7) & (exists X8 (ssList(X8) & app(X8,cons(X7,nil)) = W & leq(X7,X5))))))))))))) | nil != X & nil = W | segmentP(V,U) & totalorderedP(U))))))))). end_of_list. ============================== end of input ========================== % clear(auto_denials), because it is incompatiable with FOF reduction. Attempting problem reduction; original problem has = <1554,322>. Problem reduction (0.02 sec) gives 4 independent subproblems: ( <2096,265> <2096,265> <2097,265> <2097,265> ). Max nnf_size of subproblems is 2097; max cnf_max is 265. ============================== FOF REDUCTION MULTISEARCH ============= Subproblem 1 of 4 (negated): ((all U (- ssItem(U) | (all V (- ssItem(V) | neq(U,V) | =(V,U))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - =(V,U) | - neq(U,V))))) & (exists U (ssItem(U) & (exists V (ssItem(V) & - =(V,U))))) & (all U (- ssList(U) | (all V (- ssItem(V) | memberP(U,V) | (all W (- ssList(W) | (all X (- ssList(X) | - =(app(W,cons(V,X)),U))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (exists W (ssList(W) & (exists X (ssList(X) & =(app(W,cons(V,X)),U))))) | - memberP(U,V))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (exists W (ssList(W) & (exists X (ssList(X) & =(app(W,cons(V,X)),U))))) | (all W (- ssList(W) | (all X (- ssList(X) | - =(app(W,cons(V,X)),U))))))))) & (all U (- ssList(U) | singletonP(U) | (all V (- ssItem(V) | - =(cons(V,nil),U))))) & (all U (- ssList(U) | (exists V (ssItem(V) & =(cons(V,nil),U))) | - singletonP(U))) & (all U (- ssList(U) | (exists V (ssItem(V) & =(cons(V,nil),U))) | (all V (- ssItem(V) | - =(cons(V,nil),U))))) & (all U (- ssList(U) | (all V (- ssList(V) | frontsegP(U,V) | (all W (- ssList(W) | - =(app(V,W),U))))))) & (all U (- ssList(U) | (all V (- ssList(V) | (exists W (ssList(W) & =(app(V,W),U))) | - frontsegP(U,V))))) & (all U (- ssList(U) | (all V (- ssList(V) | (exists W (ssList(W) & =(app(V,W),U))) | (all W (- ssList(W) | - =(app(V,W),U))))))) & (all U (- ssList(U) | (all V (- ssList(V) | rearsegP(U,V) | (all W (- ssList(W) | - =(app(W,V),U))))))) & (all U (- ssList(U) | (all V (- ssList(V) | (exists W (ssList(W) & =(app(W,V),U))) | - rearsegP(U,V))))) & (all U (- ssList(U) | (all V (- ssList(V) | (exists W (ssList(W) & =(app(W,V),U))) | (all W (- ssList(W) | - =(app(W,V),U))))))) & (all U (- ssList(U) | (all V (- ssList(V) | segmentP(U,V) | (all W (- ssList(W) | (all X (- ssList(X) | - =(app(app(W,V),X),U))))))))) & (all U (- ssList(U) | (all V (- ssList(V) | (exists W (ssList(W) & (exists X (ssList(X) & =(app(app(W,V),X),U))))) | - segmentP(U,V))))) & (all U (- ssList(U) | (all V (- ssList(V) | (exists W (ssList(W) & (exists X (ssList(X) & =(app(app(W,V),X),U))))) | (all W (- ssList(W) | (all X (- ssList(X) | - =(app(app(W,V),X),U))))))))) & (all U (- ssList(U) | cyclefreeP(U) | (exists V (ssItem(V) & (exists W (ssItem(W) & leq(V,W) & leq(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | - leq(V,W) | - leq(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | - cyclefreeP(U))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | - leq(V,W) | - leq(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | (exists V (ssItem(V) & (exists W (ssItem(W) & leq(V,W) & leq(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | totalorderP(U) | (exists V (ssItem(V) & (exists W (ssItem(W) & - leq(V,W) & - leq(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | leq(V,W) | leq(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | - totalorderP(U))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | leq(V,W) | leq(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | (exists V (ssItem(V) & (exists W (ssItem(W) & - leq(V,W) & - leq(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | strictorderP(U) | (exists V (ssItem(V) & (exists W (ssItem(W) & - lt(V,W) & - lt(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | lt(V,W) | lt(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | - strictorderP(U))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | lt(V,W) | lt(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | (exists V (ssItem(V) & (exists W (ssItem(W) & - lt(V,W) & - lt(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | totalorderedP(U) | (exists V (ssItem(V) & (exists W (ssItem(W) & - leq(V,W) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | leq(V,W) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | - totalorderedP(U))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | leq(V,W) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | (exists V (ssItem(V) & (exists W (ssItem(W) & - leq(V,W) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | strictorderedP(U) | (exists V (ssItem(V) & (exists W (ssItem(W) & - lt(V,W) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | lt(V,W) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | - strictorderedP(U))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | lt(V,W) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | (exists V (ssItem(V) & (exists W (ssItem(W) & - lt(V,W) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | duplicatefreeP(U) | (exists V (ssItem(V) & (exists W (ssItem(W) & =(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | - =(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | - duplicatefreeP(U))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | - =(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | (all Z (- ssList(Z) | - =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))) | (exists V (ssItem(V) & (exists W (ssItem(W) & =(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & (exists Z (ssList(Z) & =(app(app(X,cons(V,Y)),cons(W,Z)),U))))))))))))) & (all U (- ssList(U) | equalelemsP(U) | (exists V (ssItem(V) & (exists W (ssItem(W) & - =(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & =(app(X,cons(V,cons(W,Y))),U))))))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | =(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | - =(app(X,cons(V,cons(W,Y))),U))))))))) | - equalelemsP(U))) & (all U (- ssList(U) | (all V (- ssItem(V) | (all W (- ssItem(W) | =(W,V) | (all X (- ssList(X) | (all Y (- ssList(Y) | - =(app(X,cons(V,cons(W,Y))),U))))))))) | (exists V (ssItem(V) & (exists W (ssItem(W) & - =(W,V) & (exists X (ssList(X) & (exists Y (ssList(Y) & =(app(X,cons(V,cons(W,Y))),U))))))))))) & (all U (- ssList(U) | (all V (- ssList(V) | neq(U,V) | =(V,U))))) & (all U (- ssList(U) | (all V (- ssList(V) | - =(V,U) | - neq(U,V))))) & (all U (- ssList(U) | (all V (- ssItem(V) | ssList(cons(V,U)))))) & ssList(nil) & (all U (- ssList(U) | (all V (- ssItem(V) | - =(cons(V,U),U))))) & (all U (- ssList(U) | (all V (- ssList(V) | (all W (- ssItem(W) | (all X (- ssItem(X) | - =(cons(X,V),cons(W,U)) | =(X,W))))))))) & (all U (- ssList(U) | (all V (- ssList(V) | =(V,U) | (all W (- ssItem(W) | (all X (- ssItem(X) | - =(cons(X,V),cons(W,U)))))))))) & (all U (- ssList(U) | =(nil,U) | (exists V (ssList(V) & (exists W (ssItem(W) & =(cons(W,V),U))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | - =(cons(V,U),nil))))) & (all U (- ssList(U) | =(nil,U) | ssItem(hd(U)))) & (all U (- ssList(U) | (all V (- ssItem(V) | =(hd(cons(V,U)),V))))) & (all U (- ssList(U) | =(nil,U) | ssList(tl(U)))) & (all U (- ssList(U) | (all V (- ssItem(V) | =(tl(cons(V,U)),U))))) & (all U (- ssList(U) | (all V (- ssList(V) | ssList(app(U,V)))))) & (all U (- ssList(U) | (all V (- ssList(V) | (all W (- ssItem(W) | =(app(cons(W,V),U),cons(W,app(V,U))))))))) & (all U (- ssList(U) | =(app(nil,U),U))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - leq(U,V) | - leq(V,U) | =(V,U))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - leq(U,V) | (all W (- ssItem(W) | - leq(V,W) | leq(U,W))))))) & (all U (- ssItem(U) | leq(U,U))) & (all U (- ssItem(U) | (all V (- ssItem(V) | geq(U,V) | - leq(V,U))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | leq(V,U) | - geq(U,V))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - lt(U,V) | - lt(V,U))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - lt(U,V) | (all W (- ssItem(W) | - lt(V,W) | lt(U,W))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | gt(U,V) | - lt(V,U))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | lt(V,U) | - gt(U,V))))) & (all U (- ssItem(U) | (all V (- ssList(V) | - memberP(V,U) | (all W (- ssList(W) | memberP(app(V,W),U))))))) & (all U (- ssItem(U) | (all V (- ssList(V) | (all W (- ssList(W) | memberP(app(V,W),U) | - memberP(W,U))))))) & (all U (- ssItem(U) | (all V (- ssList(V) | memberP(V,U) | (all W (- ssList(W) | memberP(W,U) | - memberP(app(V,W),U))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - =(V,U) | (all W (- ssList(W) | memberP(cons(V,W),U))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | (all W (- ssList(W) | memberP(cons(V,W),U) | - memberP(W,U))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | =(V,U) | (all W (- ssList(W) | memberP(W,U) | - memberP(cons(V,W),U))))))) & (all U (- ssItem(U) | - memberP(nil,U))) & - singletonP(nil) & (all U (- ssList(U) | (all V (- ssList(V) | - frontsegP(U,V) | (all W (- ssList(W) | - frontsegP(V,W) | frontsegP(U,W))))))) & (all U (- ssList(U) | (all V (- ssList(V) | - frontsegP(U,V) | - frontsegP(V,U) | =(V,U))))) & (all U (- ssList(U) | frontsegP(U,U))) & (all U (- ssList(U) | (all V (- ssList(V) | - frontsegP(U,V) | (all W (- ssList(W) | frontsegP(app(U,W),V))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - =(V,U) | (all W (- ssList(W) | (all X (- ssList(X) | frontsegP(cons(U,W),cons(V,X)) | - frontsegP(W,X))))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | =(V,U) | (all W (- ssList(W) | (all X (- ssList(X) | - frontsegP(cons(U,W),cons(V,X)))))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | (all W (- ssList(W) | (all X (- ssList(X) | frontsegP(W,X) | - frontsegP(cons(U,W),cons(V,X)))))))))) & (all U (- ssList(U) | frontsegP(U,nil))) & (all U (- ssList(U) | frontsegP(nil,U) | - =(nil,U))) & (all U (- ssList(U) | =(nil,U) | - frontsegP(nil,U))) & (all U (- ssList(U) | (all V (- ssList(V) | - rearsegP(U,V) | (all W (- ssList(W) | - rearsegP(V,W) | rearsegP(U,W))))))) & (all U (- ssList(U) | (all V (- ssList(V) | - rearsegP(U,V) | - rearsegP(V,U) | =(V,U))))) & (all U (- ssList(U) | rearsegP(U,U))) & (all U (- ssList(U) | (all V (- ssList(V) | - rearsegP(U,V) | (all W (- ssList(W) | rearsegP(app(W,U),V))))))) & (all U (- ssList(U) | rearsegP(U,nil))) & (all U (- ssList(U) | rearsegP(nil,U) | - =(nil,U))) & (all U (- ssList(U) | =(nil,U) | - rearsegP(nil,U))) & (all U (- ssList(U) | (all V (- ssList(V) | - segmentP(U,V) | (all W (- ssList(W) | - segmentP(V,W) | segmentP(U,W))))))) & (all U (- ssList(U) | (all V (- ssList(V) | - segmentP(U,V) | - segmentP(V,U) | =(V,U))))) & (all U (- ssList(U) | segmentP(U,U))) & (all U (- ssList(U) | (all V (- ssList(V) | - segmentP(U,V) | (all W (- ssList(W) | (all X (- ssList(X) | segmentP(app(app(W,U),X),V))))))))) & (all U (- ssList(U) | segmentP(U,nil))) & (all U (- ssList(U) | segmentP(nil,U) | - =(nil,U))) & (all U (- ssList(U) | =(nil,U) | - segmentP(nil,U))) & (all U (- ssItem(U) | cyclefreeP(cons(U,nil)))) & cyclefreeP(nil) & (all U (- ssItem(U) | totalorderP(cons(U,nil)))) & totalorderP(nil) & (all U (- ssItem(U) | strictorderP(cons(U,nil)))) & strictorderP(nil) & (all U (- ssItem(U) | totalorderedP(cons(U,nil)))) & totalorderedP(nil) & (all U (- ssItem(U) | (all V (- ssList(V) | totalorderedP(cons(U,V)) | - =(nil,V))))) & (all U (- ssItem(U) | (all V (- ssList(V) | totalorderedP(cons(U,V)) | =(nil,V) | - totalorderedP(V) | - leq(U,hd(V)))))) & (all U (- ssItem(U) | (all V (- ssList(V) | =(nil,V) | totalorderedP(V) | - totalorderedP(cons(U,V)))))) & (all U (- ssItem(U) | (all V (- ssList(V) | =(nil,V) | leq(U,hd(V)) | - totalorderedP(cons(U,V)))))) & (all U (- ssItem(U) | strictorderedP(cons(U,nil)))) & strictorderedP(nil) & (all U (- ssItem(U) | (all V (- ssList(V) | strictorderedP(cons(U,V)) | - =(nil,V))))) & (all U (- ssItem(U) | (all V (- ssList(V) | strictorderedP(cons(U,V)) | =(nil,V) | - strictorderedP(V) | - lt(U,hd(V)))))) & (all U (- ssItem(U) | (all V (- ssList(V) | =(nil,V) | strictorderedP(V) | - strictorderedP(cons(U,V)))))) & (all U (- ssItem(U) | (all V (- ssList(V) | =(nil,V) | lt(U,hd(V)) | - strictorderedP(cons(U,V)))))) & (all U (- ssItem(U) | duplicatefreeP(cons(U,nil)))) & duplicatefreeP(nil) & (all U (- ssItem(U) | equalelemsP(cons(U,nil)))) & equalelemsP(nil) & (all U (- ssList(U) | =(nil,U) | (exists V (ssItem(V) & =(hd(U),V))))) & (all U (- ssList(U) | =(nil,U) | (exists V (ssList(V) & =(tl(U),V))))) & (all U (- ssList(U) | =(nil,U) | (all V (- ssList(V) | =(nil,V) | - =(hd(V),hd(U)) | - =(tl(V),tl(U)) | =(V,U))))) & (all U (- ssList(U) | =(nil,U) | =(cons(hd(U),tl(U)),U))) & (all U (- ssList(U) | (all V (- ssList(V) | (all W (- ssList(W) | - =(app(W,V),app(U,V)) | =(W,U))))))) & (all U (- ssList(U) | (all V (- ssList(V) | (all W (- ssList(W) | - =(app(V,W),app(V,U)) | =(W,U))))))) & (all U (- ssList(U) | (all V (- ssItem(V) | =(app(cons(V,nil),U),cons(V,U)))))) & (all U (- ssList(U) | (all V (- ssList(V) | (all W (- ssList(W) | =(app(app(U,V),W),app(U,app(V,W))))))))) & (all U (- ssList(U) | - =(nil,U) | (all V (- ssList(V) | =(app(U,V),nil) | - =(nil,V))))) & (all U (- ssList(U) | (all V (- ssList(V) | =(nil,V) | - =(app(U,V),nil))))) & (all U (- ssList(U) | =(nil,U) | (all V (- ssList(V) | - =(app(U,V),nil))))) & (all U (- ssList(U) | =(app(U,nil),U))) & (all U (- ssList(U) | =(nil,U) | (all V (- ssList(V) | =(hd(app(U,V)),hd(U)))))) & (all U (- ssList(U) | =(nil,U) | (all V (- ssList(V) | =(tl(app(U,V)),app(tl(U),V)))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - geq(U,V) | - geq(V,U) | =(V,U))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - geq(U,V) | (all W (- ssItem(W) | - geq(V,W) | geq(U,W))))))) & (all U (- ssItem(U) | geq(U,U))) & (all U (- ssItem(U) | - lt(U,U))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - leq(U,V) | (all W (- ssItem(W) | - lt(V,W) | lt(U,W))))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - leq(U,V) | =(V,U) | lt(U,V))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | lt(U,V) | =(V,U) | - leq(U,V))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - =(V,U) | - lt(U,V))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | leq(U,V) | - lt(U,V))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - gt(U,V) | - gt(V,U))))) & (all U (- ssItem(U) | (all V (- ssItem(V) | - gt(U,V) | (all W (- ssItem(W) | - gt(V,W) | gt(U,W))))))) & (exists U (ssList(U) & (exists V (ssList(V) & - segmentP(V,U) & (exists W (ssList(W) & =(W,U) & totalorderedP(W) & (exists X (ssList(X) & =(X,V) & (exists Y (ssList(Y) & (all X1 (- ssItem(X1) | (all X3 (- ssItem(X3) | - leq(X1,X3) | (all X4 (- ssList(X4) | - =(app(cons(X3,nil),X4),W))))) | (all X2 (- ssList(X2) | - =(app(X2,cons(X1,nil)),Y))))) & (exists Z (ssList(Z) & =(app(app(Y,W),Z),X) & (all X5 (- ssItem(X5) | (all X7 (- ssItem(X7) | - leq(X7,X5) | (all X8 (- ssList(X8) | - =(app(X8,cons(X7,nil)),W))))) | (all X6 (- ssList(X6) | - =(app(cons(X5,nil),X6),Z))))))))) & =(nil,X)))))))))). Max_seconds is 30 for this subproblem. Child search process 27408 started. ============================== PROCESS INITIAL CLAUSES =============== % Clauses before input processing: formulas(usable). end_of_list. formulas(sos). -ssItem(A) | -ssItem(B) | neq(A,B) | B = A. [assumption]. -ssItem(A) | -ssItem(B) | B != A | -neq(A,B). [assumption]. ssItem(c1). [assumption]. ssItem(c2). [assumption]. c2 != c1. [assumption]. -ssList(A) | -ssItem(B) | memberP(A,B) | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. -ssList(A) | -ssItem(B) | ssList(f1(A,B)) | -memberP(A,B). [assumption]. -ssList(A) | -ssItem(B) | ssList(f2(A,B)) | -memberP(A,B). [assumption]. -ssList(A) | -ssItem(B) | app(f1(A,B),cons(B,f2(A,B))) = A | -memberP(A,B). [assumption]. -ssList(A) | -ssItem(B) | ssList(f3(A,B)) | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. -ssList(A) | -ssItem(B) | ssList(f4(A,B)) | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. -ssList(A) | -ssItem(B) | app(f3(A,B),cons(B,f4(A,B))) = A | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. -ssList(A) | singletonP(A) | -ssItem(B) | cons(B,nil) != A. [assumption]. -ssList(A) | ssItem(f5(A)) | -singletonP(A). [assumption]. -ssList(A) | cons(f5(A),nil) = A | -singletonP(A). [assumption]. -ssList(A) | ssItem(f6(A)) | -ssItem(B) | cons(B,nil) != A. [assumption]. -ssList(A) | cons(f6(A),nil) = A | -ssItem(B) | cons(B,nil) != A. [assumption]. -ssList(A) | -ssList(B) | frontsegP(A,B) | -ssList(C) | app(B,C) != A. [assumption]. -ssList(A) | -ssList(B) | ssList(f7(A,B)) | -frontsegP(A,B). [assumption]. -ssList(A) | -ssList(B) | app(B,f7(A,B)) = A | -frontsegP(A,B). [assumption]. -ssList(A) | -ssList(B) | ssList(f8(A,B)) | -ssList(C) | app(B,C) != A. [assumption]. -ssList(A) | -ssList(B) | app(B,f8(A,B)) = A | -ssList(C) | app(B,C) != A. [assumption]. -ssList(A) | -ssList(B) | rearsegP(A,B) | -ssList(C) | app(C,B) != A. [assumption]. -ssList(A) | -ssList(B) | ssList(f9(A,B)) | -rearsegP(A,B). [assumption]. -ssList(A) | -ssList(B) | app(f9(A,B),B) = A | -rearsegP(A,B). [assumption]. -ssList(A) | -ssList(B) | ssList(f10(A,B)) | -ssList(C) | app(C,B) != A. [assumption]. -ssList(A) | -ssList(B) | app(f10(A,B),B) = A | -ssList(C) | app(C,B) != A. [assumption]. -ssList(A) | -ssList(B) | segmentP(A,B) | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. -ssList(A) | -ssList(B) | ssList(f11(A,B)) | -segmentP(A,B). [assumption]. -ssList(A) | -ssList(B) | ssList(f12(A,B)) | -segmentP(A,B). [assumption]. -ssList(A) | -ssList(B) | app(app(f11(A,B),B),f12(A,B)) = A | -segmentP(A,B). [assumption]. -ssList(A) | -ssList(B) | ssList(f13(A,B)) | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. -ssList(A) | -ssList(B) | ssList(f14(A,B)) | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. -ssList(A) | -ssList(B) | app(app(f13(A,B),B),f14(A,B)) = A | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. -ssList(A) | cyclefreeP(A) | ssItem(f15(A)). [assumption]. -ssList(A) | cyclefreeP(A) | ssItem(f16(A)). [assumption]. -ssList(A) | cyclefreeP(A) | leq(f15(A),f16(A)). [assumption]. -ssList(A) | cyclefreeP(A) | leq(f16(A),f15(A)). [assumption]. -ssList(A) | cyclefreeP(A) | ssList(f17(A)). [assumption]. -ssList(A) | cyclefreeP(A) | ssList(f18(A)). [assumption]. -ssList(A) | cyclefreeP(A) | ssList(f19(A)). [assumption]. -ssList(A) | cyclefreeP(A) | app(app(f17(A),cons(f15(A),f18(A))),cons(f16(A),f19(A))) = A. [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -cyclefreeP(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f20(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f21(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | leq(f20(A),f21(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | leq(f21(A),f20(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f22(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f23(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f24(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [assumption]. -ssList(A) | totalorderP(A) | ssItem(f25(A)). [assumption]. -ssList(A) | totalorderP(A) | ssItem(f26(A)). [assumption]. -ssList(A) | totalorderP(A) | -leq(f25(A),f26(A)). [assumption]. -ssList(A) | totalorderP(A) | -leq(f26(A),f25(A)). [assumption]. -ssList(A) | totalorderP(A) | ssList(f27(A)). [assumption]. -ssList(A) | totalorderP(A) | ssList(f28(A)). [assumption]. -ssList(A) | totalorderP(A) | ssList(f29(A)). [assumption]. -ssList(A) | totalorderP(A) | app(app(f27(A),cons(f25(A),f28(A))),cons(f26(A),f29(A))) = A. [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -totalorderP(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f30(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f31(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f30(A),f31(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f31(A),f30(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f32(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f33(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f34(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [assumption]. -ssList(A) | strictorderP(A) | ssItem(f35(A)). [assumption]. -ssList(A) | strictorderP(A) | ssItem(f36(A)). [assumption]. -ssList(A) | strictorderP(A) | -lt(f35(A),f36(A)). [assumption]. -ssList(A) | strictorderP(A) | -lt(f36(A),f35(A)). [assumption]. -ssList(A) | strictorderP(A) | ssList(f37(A)). [assumption]. -ssList(A) | strictorderP(A) | ssList(f38(A)). [assumption]. -ssList(A) | strictorderP(A) | ssList(f39(A)). [assumption]. -ssList(A) | strictorderP(A) | app(app(f37(A),cons(f35(A),f38(A))),cons(f36(A),f39(A))) = A. [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -strictorderP(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f40(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f41(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f40(A),f41(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f41(A),f40(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f42(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f43(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f44(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [assumption]. -ssList(A) | totalorderedP(A) | ssItem(f45(A)). [assumption]. -ssList(A) | totalorderedP(A) | ssItem(f46(A)). [assumption]. -ssList(A) | totalorderedP(A) | -leq(f45(A),f46(A)). [assumption]. -ssList(A) | totalorderedP(A) | ssList(f47(A)). [assumption]. -ssList(A) | totalorderedP(A) | ssList(f48(A)). [assumption]. -ssList(A) | totalorderedP(A) | ssList(f49(A)). [assumption]. -ssList(A) | totalorderedP(A) | app(app(f47(A),cons(f45(A),f48(A))),cons(f46(A),f49(A))) = A. [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -totalorderedP(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f50(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f51(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f50(A),f51(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f52(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f53(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f54(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f52(A),cons(f50(A),f53(A))),cons(f51(A),f54(A))) = A. [assumption]. -ssList(A) | strictorderedP(A) | ssItem(f55(A)). [assumption]. -ssList(A) | strictorderedP(A) | ssItem(f56(A)). [assumption]. -ssList(A) | strictorderedP(A) | -lt(f55(A),f56(A)). [assumption]. -ssList(A) | strictorderedP(A) | ssList(f57(A)). [assumption]. -ssList(A) | strictorderedP(A) | ssList(f58(A)). [assumption]. -ssList(A) | strictorderedP(A) | ssList(f59(A)). [assumption]. -ssList(A) | strictorderedP(A) | app(app(f57(A),cons(f55(A),f58(A))),cons(f56(A),f59(A))) = A. [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -strictorderedP(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f60(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f61(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f60(A),f61(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f62(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f63(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f64(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f62(A),cons(f60(A),f63(A))),cons(f61(A),f64(A))) = A. [assumption]. -ssList(A) | duplicatefreeP(A) | ssItem(f65(A)). [assumption]. -ssList(A) | duplicatefreeP(A) | ssItem(f66(A)). [assumption]. -ssList(A) | duplicatefreeP(A) | f66(A) = f65(A). [assumption]. -ssList(A) | duplicatefreeP(A) | ssList(f67(A)). [assumption]. -ssList(A) | duplicatefreeP(A) | ssList(f68(A)). [assumption]. -ssList(A) | duplicatefreeP(A) | ssList(f69(A)). [assumption]. -ssList(A) | duplicatefreeP(A) | app(app(f67(A),cons(f65(A),f68(A))),cons(f66(A),f69(A))) = A. [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -duplicatefreeP(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f70(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f71(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | f71(A) = f70(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f72(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f73(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f74(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f72(A),cons(f70(A),f73(A))),cons(f71(A),f74(A))) = A. [assumption]. -ssList(A) | equalelemsP(A) | ssItem(f75(A)). [assumption]. -ssList(A) | equalelemsP(A) | ssItem(f76(A)). [assumption]. -ssList(A) | equalelemsP(A) | f76(A) != f75(A). [assumption]. -ssList(A) | equalelemsP(A) | ssList(f77(A)). [assumption]. -ssList(A) | equalelemsP(A) | ssList(f78(A)). [assumption]. -ssList(A) | equalelemsP(A) | app(f77(A),cons(f75(A),cons(f76(A),f78(A)))) = A. [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -equalelemsP(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssItem(f79(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssItem(f80(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | f80(A) != f79(A). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssList(f81(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssList(f82(A)). [assumption]. -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | app(f81(A),cons(f79(A),cons(f80(A),f82(A)))) = A. [assumption]. -ssList(A) | -ssList(B) | neq(A,B) | B = A. [assumption]. -ssList(A) | -ssList(B) | B != A | -neq(A,B). [assumption]. -ssList(A) | -ssItem(B) | ssList(cons(B,A)). [assumption]. ssList(nil). [assumption]. -ssList(A) | -ssItem(B) | cons(B,A) != A. [assumption]. -ssList(A) | -ssList(B) | -ssItem(C) | -ssItem(D) | cons(D,B) != cons(C,A) | D = C. [assumption]. -ssList(A) | -ssList(B) | B = A | -ssItem(C) | -ssItem(D) | cons(D,B) != cons(C,A). [assumption]. -ssList(A) | nil = A | ssList(f83(A)). [assumption]. -ssList(A) | nil = A | ssItem(f84(A)). [assumption]. -ssList(A) | nil = A | cons(f84(A),f83(A)) = A. [assumption]. -ssList(A) | -ssItem(B) | cons(B,A) != nil. [assumption]. -ssList(A) | nil = A | ssItem(hd(A)). [assumption]. -ssList(A) | -ssItem(B) | hd(cons(B,A)) = B. [assumption]. -ssList(A) | nil = A | ssList(tl(A)). [assumption]. -ssList(A) | -ssItem(B) | tl(cons(B,A)) = A. [assumption]. -ssList(A) | -ssList(B) | ssList(app(A,B)). [assumption]. -ssList(A) | -ssList(B) | -ssItem(C) | app(cons(C,B),A) = cons(C,app(B,A)). [assumption]. -ssList(A) | app(nil,A) = A. [assumption]. -ssItem(A) | -ssItem(B) | -leq(A,B) | -leq(B,A) | B = A. [assumption]. -ssItem(A) | -ssItem(B) | -leq(A,B) | -ssItem(C) | -leq(B,C) | leq(A,C). [assumption]. -ssItem(A) | leq(A,A). [assumption]. -ssItem(A) | -ssItem(B) | geq(A,B) | -leq(B,A). [assumption]. -ssItem(A) | -ssItem(B) | leq(B,A) | -geq(A,B). [assumption]. -ssItem(A) | -ssItem(B) | -lt(A,B) | -lt(B,A). [assumption]. -ssItem(A) | -ssItem(B) | -lt(A,B) | -ssItem(C) | -lt(B,C) | lt(A,C). [assumption]. -ssItem(A) | -ssItem(B) | gt(A,B) | -lt(B,A). [assumption]. -ssItem(A) | -ssItem(B) | lt(B,A) | -gt(A,B). [assumption]. -ssItem(A) | -ssList(B) | -memberP(B,A) | -ssList(C) | memberP(app(B,C),A). [assumption]. -ssItem(A) | -ssList(B) | -ssList(C) | memberP(app(B,C),A) | -memberP(C,A). [assumption]. -ssItem(A) | -ssList(B) | memberP(B,A) | -ssList(C) | memberP(C,A) | -memberP(app(B,C),A). [assumption]. -ssItem(A) | -ssItem(B) | B != A | -ssList(C) | memberP(cons(B,C),A). [assumption]. -ssItem(A) | -ssItem(B) | -ssList(C) | memberP(cons(B,C),A) | -memberP(C,A). [assumption]. -ssItem(A) | -ssItem(B) | B = A | -ssList(C) | memberP(C,A) | -memberP(cons(B,C),A). [assumption]. -ssItem(A) | -memberP(nil,A). [assumption]. -singletonP(nil). [assumption]. -ssList(A) | -ssList(B) | -frontsegP(A,B) | -ssList(C) | -frontsegP(B,C) | frontsegP(A,C). [assumption]. -ssList(A) | -ssList(B) | -frontsegP(A,B) | -frontsegP(B,A) | B = A. [assumption]. -ssList(A) | frontsegP(A,A). [assumption]. -ssList(A) | -ssList(B) | -frontsegP(A,B) | -ssList(C) | frontsegP(app(A,C),B). [assumption]. -ssItem(A) | -ssItem(B) | B != A | -ssList(C) | -ssList(D) | frontsegP(cons(A,C),cons(B,D)) | -frontsegP(C,D). [assumption]. -ssItem(A) | -ssItem(B) | B = A | -ssList(C) | -ssList(D) | -frontsegP(cons(A,C),cons(B,D)). [assumption]. -ssItem(A) | -ssItem(B) | -ssList(C) | -ssList(D) | frontsegP(C,D) | -frontsegP(cons(A,C),cons(B,D)). [assumption]. -ssList(A) | frontsegP(A,nil). [assumption]. -ssList(A) | frontsegP(nil,A) | nil != A. [assumption]. -ssList(A) | nil = A | -frontsegP(nil,A). [assumption]. -ssList(A) | -ssList(B) | -rearsegP(A,B) | -ssList(C) | -rearsegP(B,C) | rearsegP(A,C). [assumption]. -ssList(A) | -ssList(B) | -rearsegP(A,B) | -rearsegP(B,A) | B = A. [assumption]. -ssList(A) | rearsegP(A,A). [assumption]. -ssList(A) | -ssList(B) | -rearsegP(A,B) | -ssList(C) | rearsegP(app(C,A),B). [assumption]. -ssList(A) | rearsegP(A,nil). [assumption]. -ssList(A) | rearsegP(nil,A) | nil != A. [assumption]. -ssList(A) | nil = A | -rearsegP(nil,A). [assumption]. -ssList(A) | -ssList(B) | -segmentP(A,B) | -ssList(C) | -segmentP(B,C) | segmentP(A,C). [assumption]. -ssList(A) | -ssList(B) | -segmentP(A,B) | -segmentP(B,A) | B = A. [assumption]. -ssList(A) | segmentP(A,A). [assumption]. -ssList(A) | -ssList(B) | -segmentP(A,B) | -ssList(C) | -ssList(D) | segmentP(app(app(C,A),D),B). [assumption]. -ssList(A) | segmentP(A,nil). [assumption]. -ssList(A) | segmentP(nil,A) | nil != A. [assumption]. -ssList(A) | nil = A | -segmentP(nil,A). [assumption]. -ssItem(A) | cyclefreeP(cons(A,nil)). [assumption]. cyclefreeP(nil). [assumption]. -ssItem(A) | totalorderP(cons(A,nil)). [assumption]. totalorderP(nil). [assumption]. -ssItem(A) | strictorderP(cons(A,nil)). [assumption]. strictorderP(nil). [assumption]. -ssItem(A) | totalorderedP(cons(A,nil)). [assumption]. totalorderedP(nil). [assumption]. -ssItem(A) | -ssList(B) | totalorderedP(cons(A,B)) | nil != B. [assumption]. -ssItem(A) | -ssList(B) | totalorderedP(cons(A,B)) | nil = B | -totalorderedP(B) | -leq(A,hd(B)). [assumption]. -ssItem(A) | -ssList(B) | nil = B | totalorderedP(B) | -totalorderedP(cons(A,B)). [assumption]. -ssItem(A) | -ssList(B) | nil = B | leq(A,hd(B)) | -totalorderedP(cons(A,B)). [assumption]. -ssItem(A) | strictorderedP(cons(A,nil)). [assumption]. strictorderedP(nil). [assumption]. -ssItem(A) | -ssList(B) | strictorderedP(cons(A,B)) | nil != B. [assumption]. -ssItem(A) | -ssList(B) | strictorderedP(cons(A,B)) | nil = B | -strictorderedP(B) | -lt(A,hd(B)). [assumption]. -ssItem(A) | -ssList(B) | nil = B | strictorderedP(B) | -strictorderedP(cons(A,B)). [assumption]. -ssItem(A) | -ssList(B) | nil = B | lt(A,hd(B)) | -strictorderedP(cons(A,B)). [assumption]. -ssItem(A) | duplicatefreeP(cons(A,nil)). [assumption]. duplicatefreeP(nil). [assumption]. -ssItem(A) | equalelemsP(cons(A,nil)). [assumption]. equalelemsP(nil). [assumption]. -ssList(A) | nil = A | ssItem(f85(A)). [assumption]. -ssList(A) | nil = A | hd(A) = f85(A). [assumption]. -ssList(A) | nil = A | ssList(f86(A)). [assumption]. -ssList(A) | nil = A | tl(A) = f86(A). [assumption]. -ssList(A) | nil = A | -ssList(B) | nil = B | hd(B) != hd(A) | tl(B) != tl(A) | B = A. [assumption]. -ssList(A) | nil = A | cons(hd(A),tl(A)) = A. [assumption]. -ssList(A) | -ssList(B) | -ssList(C) | app(C,B) != app(A,B) | C = A. [assumption]. -ssList(A) | -ssList(B) | -ssList(C) | app(B,C) != app(B,A) | C = A. [assumption]. -ssList(A) | -ssItem(B) | app(cons(B,nil),A) = cons(B,A). [assumption]. -ssList(A) | -ssList(B) | -ssList(C) | app(app(A,B),C) = app(A,app(B,C)). [assumption]. -ssList(A) | nil != A | -ssList(B) | app(A,B) = nil | nil != B. [assumption]. -ssList(A) | -ssList(B) | nil = B | app(A,B) != nil. [assumption]. -ssList(A) | nil = A | -ssList(B) | app(A,B) != nil. [assumption]. -ssList(A) | app(A,nil) = A. [assumption]. -ssList(A) | nil = A | -ssList(B) | hd(app(A,B)) = hd(A). [assumption]. -ssList(A) | nil = A | -ssList(B) | tl(app(A,B)) = app(tl(A),B). [assumption]. -ssItem(A) | -ssItem(B) | -geq(A,B) | -geq(B,A) | B = A. [assumption]. -ssItem(A) | -ssItem(B) | -geq(A,B) | -ssItem(C) | -geq(B,C) | geq(A,C). [assumption]. -ssItem(A) | geq(A,A). [assumption]. -ssItem(A) | -lt(A,A). [assumption]. -ssItem(A) | -ssItem(B) | -leq(A,B) | -ssItem(C) | -lt(B,C) | lt(A,C). [assumption]. -ssItem(A) | -ssItem(B) | -leq(A,B) | B = A | lt(A,B). [assumption]. -ssItem(A) | -ssItem(B) | lt(A,B) | B = A | -leq(A,B). [assumption]. -ssItem(A) | -ssItem(B) | B != A | -lt(A,B). [assumption]. -ssItem(A) | -ssItem(B) | leq(A,B) | -lt(A,B). [assumption]. -ssItem(A) | -ssItem(B) | -gt(A,B) | -gt(B,A). [assumption]. -ssItem(A) | -ssItem(B) | -gt(A,B) | -ssItem(C) | -gt(B,C) | gt(A,C). [assumption]. ssList(c3). [assumption]. ssList(c4). [assumption]. -segmentP(c4,c3). [assumption]. ssList(c5). [assumption]. c5 = c3. [assumption]. totalorderedP(c5). [assumption]. ssList(c6). [assumption]. c6 = c4. [assumption]. ssList(c7). [assumption]. -ssItem(A) | -ssItem(B) | -leq(A,B) | -ssList(C) | app(cons(B,nil),C) != c5 | -ssList(D) | app(D,cons(A,nil)) != c7. [assumption]. ssList(c8). [assumption]. app(app(c7,c5),c8) = c6. [assumption]. -ssItem(A) | -ssItem(B) | -leq(B,A) | -ssList(C) | app(C,cons(B,nil)) != c5 | -ssList(D) | app(cons(A,nil),D) != c8. [assumption]. nil = c6. [assumption]. end_of_list. formulas(demodulators). end_of_list. ============================== PREDICATE ELIMINATION ================= Eliminating neq/2 1 -ssItem(A) | -ssItem(B) | B != A | -neq(A,B). [assumption]. 2 -ssItem(A) | -ssItem(B) | neq(A,B) | B = A. [assumption]. 3 -ssList(A) | -ssList(B) | neq(A,B) | B = A. [assumption]. 4 -ssList(A) | -ssList(B) | B != A | -neq(A,B). [assumption]. Eliminating cyclefreeP/1 5 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -cyclefreeP(A). [assumption]. 6 -ssList(A) | cyclefreeP(A) | ssItem(f15(A)). [assumption]. 7 -ssList(A) | cyclefreeP(A) | ssItem(f16(A)). [assumption]. 8 -ssList(A) | cyclefreeP(A) | leq(f15(A),f16(A)). [assumption]. 9 -ssList(A) | cyclefreeP(A) | leq(f16(A),f15(A)). [assumption]. 10 -ssList(A) | cyclefreeP(A) | ssList(f17(A)). [assumption]. 11 -ssList(A) | cyclefreeP(A) | ssList(f18(A)). [assumption]. 12 -ssList(A) | cyclefreeP(A) | ssList(f19(A)). [assumption]. 13 -ssList(A) | cyclefreeP(A) | app(app(f17(A),cons(f15(A),f18(A))),cons(f16(A),f19(A))) = A. [assumption]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f15(A)). [resolve(5,j,6,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f16(A)). [resolve(5,j,7,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | leq(f15(A),f16(A)). [resolve(5,j,8,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | leq(f16(A),f15(A)). [resolve(5,j,9,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f17(A)). [resolve(5,j,10,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f18(A)). [resolve(5,j,11,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f19(A)). [resolve(5,j,12,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | app(app(f17(A),cons(f15(A),f18(A))),cons(f16(A),f19(A))) = A. [resolve(5,j,13,b)]. 14 -ssItem(A) | cyclefreeP(cons(A,nil)). [assumption]. Derived: -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(14,b,5,j)]. 15 cyclefreeP(nil). [assumption]. Derived: -ssList(nil) | -ssItem(A) | -ssItem(B) | -leq(A,B) | -leq(B,A) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [resolve(15,a,5,j)]. Eliminating totalorderP/1 16 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -totalorderP(A). [assumption]. 17 -ssList(A) | totalorderP(A) | ssItem(f25(A)). [assumption]. 18 -ssList(A) | totalorderP(A) | ssItem(f26(A)). [assumption]. 19 -ssList(A) | totalorderP(A) | -leq(f25(A),f26(A)). [assumption]. 20 -ssList(A) | totalorderP(A) | -leq(f26(A),f25(A)). [assumption]. 21 -ssList(A) | totalorderP(A) | ssList(f27(A)). [assumption]. 22 -ssList(A) | totalorderP(A) | ssList(f28(A)). [assumption]. 23 -ssList(A) | totalorderP(A) | ssList(f29(A)). [assumption]. 24 -ssList(A) | totalorderP(A) | app(app(f27(A),cons(f25(A),f28(A))),cons(f26(A),f29(A))) = A. [assumption]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f25(A)). [resolve(16,j,17,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f26(A)). [resolve(16,j,18,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | -leq(f25(A),f26(A)). [resolve(16,j,19,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | -leq(f26(A),f25(A)). [resolve(16,j,20,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f27(A)). [resolve(16,j,21,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f28(A)). [resolve(16,j,22,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f29(A)). [resolve(16,j,23,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | app(app(f27(A),cons(f25(A),f28(A))),cons(f26(A),f29(A))) = A. [resolve(16,j,24,b)]. 25 -ssItem(A) | totalorderP(cons(A,nil)). [assumption]. Derived: -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(25,b,16,j)]. 26 totalorderP(nil). [assumption]. Derived: -ssList(nil) | -ssItem(A) | -ssItem(B) | leq(A,B) | leq(B,A) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [resolve(26,a,16,j)]. Eliminating strictorderP/1 27 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -strictorderP(A). [assumption]. 28 -ssList(A) | strictorderP(A) | ssItem(f35(A)). [assumption]. 29 -ssList(A) | strictorderP(A) | ssItem(f36(A)). [assumption]. 30 -ssList(A) | strictorderP(A) | -lt(f35(A),f36(A)). [assumption]. 31 -ssList(A) | strictorderP(A) | -lt(f36(A),f35(A)). [assumption]. 32 -ssList(A) | strictorderP(A) | ssList(f37(A)). [assumption]. 33 -ssList(A) | strictorderP(A) | ssList(f38(A)). [assumption]. 34 -ssList(A) | strictorderP(A) | ssList(f39(A)). [assumption]. 35 -ssList(A) | strictorderP(A) | app(app(f37(A),cons(f35(A),f38(A))),cons(f36(A),f39(A))) = A. [assumption]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f35(A)). [resolve(27,j,28,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f36(A)). [resolve(27,j,29,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | -lt(f35(A),f36(A)). [resolve(27,j,30,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | -lt(f36(A),f35(A)). [resolve(27,j,31,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f37(A)). [resolve(27,j,32,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f38(A)). [resolve(27,j,33,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f39(A)). [resolve(27,j,34,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | app(app(f37(A),cons(f35(A),f38(A))),cons(f36(A),f39(A))) = A. [resolve(27,j,35,b)]. 36 -ssItem(A) | strictorderP(cons(A,nil)). [assumption]. Derived: -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(36,b,27,j)]. 37 strictorderP(nil). [assumption]. Derived: -ssList(nil) | -ssItem(A) | -ssItem(B) | lt(A,B) | lt(B,A) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [resolve(37,a,27,j)]. Eliminating duplicatefreeP/1 38 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -duplicatefreeP(A). [assumption]. 39 -ssList(A) | duplicatefreeP(A) | ssItem(f65(A)). [assumption]. 40 -ssList(A) | duplicatefreeP(A) | ssItem(f66(A)). [assumption]. 41 -ssList(A) | duplicatefreeP(A) | f66(A) = f65(A). [assumption]. 42 -ssList(A) | duplicatefreeP(A) | ssList(f67(A)). [assumption]. 43 -ssList(A) | duplicatefreeP(A) | ssList(f68(A)). [assumption]. 44 -ssList(A) | duplicatefreeP(A) | ssList(f69(A)). [assumption]. 45 -ssList(A) | duplicatefreeP(A) | app(app(f67(A),cons(f65(A),f68(A))),cons(f66(A),f69(A))) = A. [assumption]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f65(A)). [resolve(38,i,39,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssItem(f66(A)). [resolve(38,i,40,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | f66(A) = f65(A). [resolve(38,i,41,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f67(A)). [resolve(38,i,42,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f68(A)). [resolve(38,i,43,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | ssList(f69(A)). [resolve(38,i,44,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -ssList(A) | app(app(f67(A),cons(f65(A),f68(A))),cons(f66(A),f69(A))) = A. [resolve(38,i,45,b)]. 46 -ssItem(A) | duplicatefreeP(cons(A,nil)). [assumption]. Derived: -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(46,b,38,i)]. 47 duplicatefreeP(nil). [assumption]. Derived: -ssList(nil) | -ssItem(A) | -ssItem(B) | B != A | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [resolve(47,a,38,i)]. Eliminating equalelemsP/1 48 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -equalelemsP(A). [assumption]. 49 -ssList(A) | equalelemsP(A) | ssItem(f75(A)). [assumption]. 50 -ssList(A) | equalelemsP(A) | ssItem(f76(A)). [assumption]. 51 -ssList(A) | equalelemsP(A) | f76(A) != f75(A). [assumption]. 52 -ssList(A) | equalelemsP(A) | ssList(f77(A)). [assumption]. 53 -ssList(A) | equalelemsP(A) | ssList(f78(A)). [assumption]. 54 -ssList(A) | equalelemsP(A) | app(f77(A),cons(f75(A),cons(f76(A),f78(A)))) = A. [assumption]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -ssList(A) | ssItem(f75(A)). [resolve(48,h,49,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -ssList(A) | ssItem(f76(A)). [resolve(48,h,50,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -ssList(A) | f76(A) != f75(A). [resolve(48,h,51,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -ssList(A) | ssList(f77(A)). [resolve(48,h,52,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -ssList(A) | ssList(f78(A)). [resolve(48,h,53,b)]. Derived: -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | -ssList(A) | app(f77(A),cons(f75(A),cons(f76(A),f78(A)))) = A. [resolve(48,h,54,b)]. 55 -ssItem(A) | equalelemsP(cons(A,nil)). [assumption]. Derived: -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != cons(A,nil). [resolve(55,b,48,h)]. 56 equalelemsP(nil). [assumption]. Derived: -ssList(nil) | -ssItem(A) | -ssItem(B) | B = A | -ssList(C) | -ssList(D) | app(C,cons(A,cons(B,D))) != nil. [resolve(56,a,48,h)]. ============================== end predicate elimination ============= Term ordering decisions: Predicate symbol precedence: predicate_order([ =, ssList, ssItem, totalorderedP, strictorderedP, singletonP, leq, lt, frontsegP, memberP, segmentP, rearsegP, geq, gt ]). Function symbol precedence: function_order([ nil, c1, c2, c3, c4, c5, c6, c7, c8, cons, app, f1, f2, f3, f4, f7, f8, f9, f10, f11, f12, f13, f14, hd, tl, f5, f6, f15, f16, f17, f18, f19, f20, f21, f22, f23, f24, f25, f26, f27, f28, f29, f30, f31, f32, f33, f34, f35, f36, f37, f38, f39, f40, f41, f42, f43, f44, f45, f46, f47, f48, f49, f50, f51, f52, f53, f54, f55, f56, f57, f58, f59, f60, f61, f62, f63, f64, f65, f66, f67, f68, f69, f70, f71, f72, f73, f74, f75, f76, f77, f78, f79, f80, f81, f82, f83, f84, f85, f86 ]). After inverse_order: (no changes). Unfolding symbols: (none). Auto_inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) Auto_process settings: % set(factor). % (non-Horn) % set(back_unit_deletion). % (non-Horn) % set(back_unit_deletion) -> set(unit_deletion). ============================== end of process initial clauses ======== ============================== CLAUSES FOR SEARCH ==================== % Clauses after input processing: formulas(usable). end_of_list. formulas(sos). 57 ssItem(c1). [assumption]. 58 ssItem(c2). [assumption]. 59 c2 != c1. [assumption]. 60 -ssList(A) | -ssItem(B) | memberP(A,B) | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. 61 -ssList(A) | -ssItem(B) | ssList(f1(A,B)) | -memberP(A,B). [assumption]. 62 -ssList(A) | -ssItem(B) | ssList(f2(A,B)) | -memberP(A,B). [assumption]. 63 -ssList(A) | -ssItem(B) | app(f1(A,B),cons(B,f2(A,B))) = A | -memberP(A,B). [assumption]. 64 -ssList(A) | -ssItem(B) | ssList(f3(A,B)) | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. 65 -ssList(A) | -ssItem(B) | ssList(f4(A,B)) | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. 66 -ssList(A) | -ssItem(B) | app(f3(A,B),cons(B,f4(A,B))) = A | -ssList(C) | -ssList(D) | app(C,cons(B,D)) != A. [assumption]. 67 -ssList(A) | singletonP(A) | -ssItem(B) | cons(B,nil) != A. [assumption]. 68 -ssList(A) | ssItem(f5(A)) | -singletonP(A). [assumption]. 69 -ssList(A) | cons(f5(A),nil) = A | -singletonP(A). [assumption]. 70 -ssList(A) | ssItem(f6(A)) | -ssItem(B) | cons(B,nil) != A. [assumption]. 71 -ssList(A) | cons(f6(A),nil) = A | -ssItem(B) | cons(B,nil) != A. [assumption]. 72 -ssList(A) | -ssList(B) | frontsegP(A,B) | -ssList(C) | app(B,C) != A. [assumption]. 73 -ssList(A) | -ssList(B) | ssList(f7(A,B)) | -frontsegP(A,B). [assumption]. 74 -ssList(A) | -ssList(B) | app(B,f7(A,B)) = A | -frontsegP(A,B). [assumption]. 75 -ssList(A) | -ssList(B) | ssList(f8(A,B)) | -ssList(C) | app(B,C) != A. [assumption]. 76 -ssList(A) | -ssList(B) | app(B,f8(A,B)) = A | -ssList(C) | app(B,C) != A. [assumption]. 77 -ssList(A) | -ssList(B) | rearsegP(A,B) | -ssList(C) | app(C,B) != A. [assumption]. 78 -ssList(A) | -ssList(B) | ssList(f9(A,B)) | -rearsegP(A,B). [assumption]. 79 -ssList(A) | -ssList(B) | app(f9(A,B),B) = A | -rearsegP(A,B). [assumption]. 80 -ssList(A) | -ssList(B) | ssList(f10(A,B)) | -ssList(C) | app(C,B) != A. [assumption]. 81 -ssList(A) | -ssList(B) | app(f10(A,B),B) = A | -ssList(C) | app(C,B) != A. [assumption]. 82 -ssList(A) | -ssList(B) | segmentP(A,B) | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. 83 -ssList(A) | -ssList(B) | ssList(f11(A,B)) | -segmentP(A,B). [assumption]. 84 -ssList(A) | -ssList(B) | ssList(f12(A,B)) | -segmentP(A,B). [assumption]. 85 -ssList(A) | -ssList(B) | app(app(f11(A,B),B),f12(A,B)) = A | -segmentP(A,B). [assumption]. 86 -ssList(A) | -ssList(B) | ssList(f13(A,B)) | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. 87 -ssList(A) | -ssList(B) | ssList(f14(A,B)) | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. 88 -ssList(A) | -ssList(B) | app(app(f13(A,B),B),f14(A,B)) = A | -ssList(C) | -ssList(D) | app(app(C,B),D) != A. [assumption]. 89 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f20(A)). [assumption]. 90 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f21(A)). [assumption]. 91 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | leq(f20(A),f21(A)). [assumption]. 92 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | leq(f21(A),f20(A)). [assumption]. 93 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f22(A)). [assumption]. 94 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f23(A)). [assumption]. 95 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f24(A)). [assumption]. 96 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [assumption]. 97 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f30(A)). [assumption]. 98 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f31(A)). [assumption]. 99 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f30(A),f31(A)). [assumption]. 100 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f31(A),f30(A)). [assumption]. 101 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f32(A)). [assumption]. 102 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f33(A)). [assumption]. 103 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f34(A)). [assumption]. 104 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [assumption]. 105 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f40(A)). [assumption]. 106 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f41(A)). [assumption]. 107 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f40(A),f41(A)). [assumption]. 108 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f41(A),f40(A)). [assumption]. 109 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f42(A)). [assumption]. 110 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f43(A)). [assumption]. 111 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f44(A)). [assumption]. 112 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [assumption]. 113 -ssList(A) | totalorderedP(A) | ssItem(f45(A)). [assumption]. 114 -ssList(A) | totalorderedP(A) | ssItem(f46(A)). [assumption]. 115 -ssList(A) | totalorderedP(A) | -leq(f45(A),f46(A)). [assumption]. 116 -ssList(A) | totalorderedP(A) | ssList(f47(A)). [assumption]. 117 -ssList(A) | totalorderedP(A) | ssList(f48(A)). [assumption]. 118 -ssList(A) | totalorderedP(A) | ssList(f49(A)). [assumption]. 119 -ssList(A) | totalorderedP(A) | app(app(f47(A),cons(f45(A),f48(A))),cons(f46(A),f49(A))) = A. [assumption]. 120 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -totalorderedP(A). [assumption]. 121 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f50(A)). [assumption]. 122 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f51(A)). [assumption]. 123 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f50(A),f51(A)). [assumption]. 124 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f52(A)). [assumption]. 125 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f53(A)). [assumption]. 126 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f54(A)). [assumption]. 127 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f52(A),cons(f50(A),f53(A))),cons(f51(A),f54(A))) = A. [assumption]. 128 -ssList(A) | strictorderedP(A) | ssItem(f55(A)). [assumption]. 129 -ssList(A) | strictorderedP(A) | ssItem(f56(A)). [assumption]. 130 -ssList(A) | strictorderedP(A) | -lt(f55(A),f56(A)). [assumption]. 131 -ssList(A) | strictorderedP(A) | ssList(f57(A)). [assumption]. 132 -ssList(A) | strictorderedP(A) | ssList(f58(A)). [assumption]. 133 -ssList(A) | strictorderedP(A) | ssList(f59(A)). [assumption]. 134 -ssList(A) | strictorderedP(A) | app(app(f57(A),cons(f55(A),f58(A))),cons(f56(A),f59(A))) = A. [assumption]. 135 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -strictorderedP(A). [assumption]. 136 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f60(A)). [assumption]. 137 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f61(A)). [assumption]. 138 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f60(A),f61(A)). [assumption]. 139 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f62(A)). [assumption]. 140 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f63(A)). [assumption]. 141 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f64(A)). [assumption]. 142 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f62(A),cons(f60(A),f63(A))),cons(f61(A),f64(A))) = A. [assumption]. 143 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f70(A)). [assumption]. 144 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f71(A)). [assumption]. 145 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | f71(A) = f70(A). [assumption]. 146 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f72(A)). [assumption]. 147 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f73(A)). [assumption]. 148 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f74(A)). [assumption]. 149 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f72(A),cons(f70(A),f73(A))),cons(f71(A),f74(A))) = A. [assumption]. 150 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssItem(f79(A)). [assumption]. 151 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssItem(f80(A)). [assumption]. 152 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | f80(A) != f79(A). [assumption]. 153 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssList(f81(A)). [assumption]. 154 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssList(f82(A)). [assumption]. 155 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | app(f81(A),cons(f79(A),cons(f80(A),f82(A)))) = A. [assumption]. 156 -ssList(A) | -ssItem(B) | ssList(cons(B,A)). [assumption]. 157 ssList(nil). [assumption]. 158 -ssList(A) | -ssItem(B) | cons(B,A) != A. [assumption]. 159 -ssList(A) | -ssList(B) | -ssItem(C) | -ssItem(D) | cons(D,B) != cons(C,A) | D = C. [assumption]. 160 -ssList(A) | -ssList(B) | B = A | -ssItem(C) | -ssItem(D) | cons(D,B) != cons(C,A). [assumption]. 161 -ssList(A) | nil = A | ssList(f83(A)). [assumption]. 162 -ssList(A) | nil = A | ssItem(f84(A)). [assumption]. 163 -ssList(A) | nil = A | cons(f84(A),f83(A)) = A. [assumption]. 164 -ssList(A) | -ssItem(B) | cons(B,A) != nil. [assumption]. 165 -ssList(A) | nil = A | ssItem(hd(A)). [assumption]. 166 -ssList(A) | -ssItem(B) | hd(cons(B,A)) = B. [assumption]. 167 -ssList(A) | nil = A | ssList(tl(A)). [assumption]. 168 -ssList(A) | -ssItem(B) | tl(cons(B,A)) = A. [assumption]. 169 -ssList(A) | -ssList(B) | ssList(app(A,B)). [assumption]. 170 -ssList(A) | -ssList(B) | -ssItem(C) | app(cons(C,B),A) = cons(C,app(B,A)). [assumption]. 171 -ssList(A) | app(nil,A) = A. [assumption]. 172 -ssItem(A) | -ssItem(B) | -leq(A,B) | -leq(B,A) | B = A. [assumption]. 173 -ssItem(A) | -ssItem(B) | -leq(A,B) | -ssItem(C) | -leq(B,C) | leq(A,C). [assumption]. 174 -ssItem(A) | leq(A,A). [assumption]. 175 -ssItem(A) | -ssItem(B) | geq(A,B) | -leq(B,A). [assumption]. 176 -ssItem(A) | -ssItem(B) | leq(B,A) | -geq(A,B). [assumption]. 177 -ssItem(A) | -ssItem(B) | -lt(A,B) | -lt(B,A). [assumption]. 178 -ssItem(A) | -ssItem(B) | -lt(A,B) | -ssItem(C) | -lt(B,C) | lt(A,C). [assumption]. 179 -ssItem(A) | -ssItem(B) | gt(A,B) | -lt(B,A). [assumption]. 180 -ssItem(A) | -ssItem(B) | lt(B,A) | -gt(A,B). [assumption]. 181 -ssItem(A) | -ssList(B) | -memberP(B,A) | -ssList(C) | memberP(app(B,C),A). [assumption]. 182 -ssItem(A) | -ssList(B) | -ssList(C) | memberP(app(B,C),A) | -memberP(C,A). [assumption]. 183 -ssItem(A) | -ssList(B) | memberP(B,A) | -ssList(C) | memberP(C,A) | -memberP(app(B,C),A). [assumption]. 184 -ssItem(A) | -ssItem(B) | B != A | -ssList(C) | memberP(cons(B,C),A). [assumption]. 185 -ssItem(A) | -ssItem(B) | -ssList(C) | memberP(cons(B,C),A) | -memberP(C,A). [assumption]. 186 -ssItem(A) | -ssItem(B) | B = A | -ssList(C) | memberP(C,A) | -memberP(cons(B,C),A). [assumption]. 187 -ssItem(A) | -memberP(nil,A). [assumption]. 188 -singletonP(nil). [assumption]. 189 -ssList(A) | -ssList(B) | -frontsegP(A,B) | -ssList(C) | -frontsegP(B,C) | frontsegP(A,C). [assumption]. 190 -ssList(A) | -ssList(B) | -frontsegP(A,B) | -frontsegP(B,A) | B = A. [assumption]. 191 -ssList(A) | frontsegP(A,A). [assumption]. 192 -ssList(A) | -ssList(B) | -frontsegP(A,B) | -ssList(C) | frontsegP(app(A,C),B). [assumption]. 193 -ssItem(A) | -ssItem(B) | B != A | -ssList(C) | -ssList(D) | frontsegP(cons(A,C),cons(B,D)) | -frontsegP(C,D). [assumption]. 194 -ssItem(A) | -ssItem(B) | B = A | -ssList(C) | -ssList(D) | -frontsegP(cons(A,C),cons(B,D)). [assumption]. 195 -ssItem(A) | -ssItem(B) | -ssList(C) | -ssList(D) | frontsegP(C,D) | -frontsegP(cons(A,C),cons(B,D)). [assumption]. 196 -ssList(A) | frontsegP(A,nil). [assumption]. 197 -ssList(A) | frontsegP(nil,A) | nil != A. [assumption]. 198 -ssList(A) | nil = A | -frontsegP(nil,A). [assumption]. 199 -ssList(A) | -ssList(B) | -rearsegP(A,B) | -ssList(C) | -rearsegP(B,C) | rearsegP(A,C). [assumption]. 200 -ssList(A) | -ssList(B) | -rearsegP(A,B) | -rearsegP(B,A) | B = A. [assumption]. 201 -ssList(A) | rearsegP(A,A). [assumption]. 202 -ssList(A) | -ssList(B) | -rearsegP(A,B) | -ssList(C) | rearsegP(app(C,A),B). [assumption]. 203 -ssList(A) | rearsegP(A,nil). [assumption]. 204 -ssList(A) | rearsegP(nil,A) | nil != A. [assumption]. 205 -ssList(A) | nil = A | -rearsegP(nil,A). [assumption]. 206 -ssList(A) | -ssList(B) | -segmentP(A,B) | -ssList(C) | -segmentP(B,C) | segmentP(A,C). [assumption]. 207 -ssList(A) | -ssList(B) | -segmentP(A,B) | -segmentP(B,A) | B = A. [assumption]. 208 -ssList(A) | segmentP(A,A). [assumption]. 209 -ssList(A) | -ssList(B) | -segmentP(A,B) | -ssList(C) | -ssList(D) | segmentP(app(app(C,A),D),B). [assumption]. 210 -ssList(A) | segmentP(A,nil). [assumption]. 211 -ssList(A) | segmentP(nil,A) | nil != A. [assumption]. 212 -ssList(A) | nil = A | -segmentP(nil,A). [assumption]. 213 -ssItem(A) | totalorderedP(cons(A,nil)). [assumption]. 214 totalorderedP(nil). [assumption]. 215 -ssItem(A) | -ssList(B) | totalorderedP(cons(A,B)) | nil != B. [assumption]. 216 -ssItem(A) | -ssList(B) | totalorderedP(cons(A,B)) | nil = B | -totalorderedP(B) | -leq(A,hd(B)). [assumption]. 217 -ssItem(A) | -ssList(B) | nil = B | totalorderedP(B) | -totalorderedP(cons(A,B)). [assumption]. 218 -ssItem(A) | -ssList(B) | nil = B | leq(A,hd(B)) | -totalorderedP(cons(A,B)). [assumption]. 219 -ssItem(A) | strictorderedP(cons(A,nil)). [assumption]. 220 strictorderedP(nil). [assumption]. 221 -ssItem(A) | -ssList(B) | strictorderedP(cons(A,B)) | nil != B. [assumption]. 222 -ssItem(A) | -ssList(B) | strictorderedP(cons(A,B)) | nil = B | -strictorderedP(B) | -lt(A,hd(B)). [assumption]. 223 -ssItem(A) | -ssList(B) | nil = B | strictorderedP(B) | -strictorderedP(cons(A,B)). [assumption]. 224 -ssItem(A) | -ssList(B) | nil = B | lt(A,hd(B)) | -strictorderedP(cons(A,B)). [assumption]. 225 -ssList(A) | nil = A | ssItem(f85(A)). [assumption]. 227 -ssList(A) | nil = A | f85(A) = hd(A). [copy(226),flip(c)]. 228 -ssList(A) | nil = A | ssList(f86(A)). [assumption]. 230 -ssList(A) | nil = A | f86(A) = tl(A). [copy(229),flip(c)]. 231 -ssList(A) | nil = A | -ssList(B) | nil = B | hd(B) != hd(A) | tl(B) != tl(A) | B = A. [assumption]. 232 -ssList(A) | nil = A | cons(hd(A),tl(A)) = A. [assumption]. 233 -ssList(A) | -ssList(B) | -ssList(C) | app(C,B) != app(A,B) | C = A. [assumption]. 234 -ssList(A) | -ssList(B) | -ssList(C) | app(B,C) != app(B,A) | C = A. [assumption]. 235 -ssList(A) | -ssItem(B) | app(cons(B,nil),A) = cons(B,A). [assumption]. 236 -ssList(A) | -ssList(B) | -ssList(C) | app(app(A,B),C) = app(A,app(B,C)). [assumption]. 237 -ssList(A) | nil != A | -ssList(B) | app(A,B) = nil | nil != B. [assumption]. 238 -ssList(A) | -ssList(B) | nil = B | app(A,B) != nil. [assumption]. 239 -ssList(A) | nil = A | -ssList(B) | app(A,B) != nil. [assumption]. 240 -ssList(A) | app(A,nil) = A. [assumption]. 241 -ssList(A) | nil = A | -ssList(B) | hd(app(A,B)) = hd(A). [assumption]. 242 -ssList(A) | nil = A | -ssList(B) | tl(app(A,B)) = app(tl(A),B). [assumption]. 243 -ssItem(A) | -ssItem(B) | -geq(A,B) | -geq(B,A) | B = A. [assumption]. 244 -ssItem(A) | -ssItem(B) | -geq(A,B) | -ssItem(C) | -geq(B,C) | geq(A,C). [assumption]. 245 -ssItem(A) | geq(A,A). [assumption]. 246 -ssItem(A) | -lt(A,A). [assumption]. 247 -ssItem(A) | -ssItem(B) | -leq(A,B) | -ssItem(C) | -lt(B,C) | lt(A,C). [assumption]. 248 -ssItem(A) | -ssItem(B) | -leq(A,B) | B = A | lt(A,B). [assumption]. 249 -ssItem(A) | -ssItem(B) | B != A | -lt(A,B). [assumption]. 250 -ssItem(A) | -ssItem(B) | leq(A,B) | -lt(A,B). [assumption]. 251 -ssItem(A) | -ssItem(B) | -gt(A,B) | -gt(B,A). [assumption]. 252 -ssItem(A) | -ssItem(B) | -gt(A,B) | -ssItem(C) | -gt(B,C) | gt(A,C). [assumption]. 253 ssList(c3). [assumption]. 257 c5 = c3. [assumption]. 259 totalorderedP(c3). [copy(258),rewrite([257(1)])]. 262 ssList(c7). [assumption]. 264 -ssItem(A) | -ssItem(B) | -leq(A,B) | -ssList(C) | app(cons(B,nil),C) != c3 | -ssList(D) | app(D,cons(A,nil)) != c7. [copy(263),rewrite([257(8)])]. 265 ssList(c8). [assumption]. 269 -ssItem(A) | -ssItem(B) | -leq(B,A) | -ssList(C) | app(C,cons(B,nil)) != c3 | -ssList(D) | app(cons(A,nil),D) != c8. [copy(268),rewrite([257(8)])]. 271 c4 = nil. [copy(270),rewrite([261(2)]),flip(a)]. 273 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f15(A)). [copy(272),merge(j)]. 275 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f16(A)). [copy(274),merge(j)]. 277 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | leq(f15(A),f16(A)). [copy(276),merge(j)]. 279 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | leq(f16(A),f15(A)). [copy(278),merge(j)]. 281 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f17(A)). [copy(280),merge(j)]. 283 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f18(A)). [copy(282),merge(j)]. 285 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f19(A)). [copy(284),merge(j)]. 287 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f17(A),cons(f15(A),f18(A))),cons(f16(A),f19(A))) = A. [copy(286),merge(j)]. 288 -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(14,b,5,j)]. 290 -ssItem(A) | -ssItem(B) | -leq(A,B) | -leq(B,A) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [copy(289),unit_del(a,157)]. 292 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f25(A)). [copy(291),merge(j)]. 294 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f26(A)). [copy(293),merge(j)]. 296 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f25(A),f26(A)). [copy(295),merge(j)]. 298 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -leq(f26(A),f25(A)). [copy(297),merge(j)]. 300 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f27(A)). [copy(299),merge(j)]. 302 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f28(A)). [copy(301),merge(j)]. 304 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f29(A)). [copy(303),merge(j)]. 306 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f27(A),cons(f25(A),f28(A))),cons(f26(A),f29(A))) = A. [copy(305),merge(j)]. 307 -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(25,b,16,j)]. 309 -ssItem(A) | -ssItem(B) | leq(A,B) | leq(B,A) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [copy(308),unit_del(a,157)]. 311 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f35(A)). [copy(310),merge(j)]. 313 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f36(A)). [copy(312),merge(j)]. 315 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f35(A),f36(A)). [copy(314),merge(j)]. 317 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | -lt(f36(A),f35(A)). [copy(316),merge(j)]. 319 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f37(A)). [copy(318),merge(j)]. 321 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f38(A)). [copy(320),merge(j)]. 323 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f39(A)). [copy(322),merge(j)]. 325 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f37(A),cons(f35(A),f38(A))),cons(f36(A),f39(A))) = A. [copy(324),merge(j)]. 326 -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(36,b,27,j)]. 328 -ssItem(A) | -ssItem(B) | lt(A,B) | lt(B,A) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [copy(327),unit_del(a,157)]. 330 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f65(A)). [copy(329),merge(i)]. 332 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssItem(f66(A)). [copy(331),merge(i)]. 334 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | f66(A) = f65(A). [copy(333),merge(i)]. 336 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f67(A)). [copy(335),merge(i)]. 338 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f68(A)). [copy(337),merge(i)]. 340 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | ssList(f69(A)). [copy(339),merge(i)]. 342 -ssList(A) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != A | app(app(f67(A),cons(f65(A),f68(A))),cons(f66(A),f69(A))) = A. [copy(341),merge(i)]. 343 -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | C != B | -ssList(D) | -ssList(E) | -ssList(F) | app(app(D,cons(B,E)),cons(C,F)) != cons(A,nil). [resolve(46,b,38,i)]. 345 -ssItem(A) | -ssItem(B) | B != A | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(A,D)),cons(B,E)) != nil. [copy(344),unit_del(a,157)]. 347 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssItem(f75(A)). [copy(346),merge(h)]. 349 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssItem(f76(A)). [copy(348),merge(h)]. 351 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | f76(A) != f75(A). [copy(350),merge(h)]. 353 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssList(f77(A)). [copy(352),merge(h)]. 355 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | ssList(f78(A)). [copy(354),merge(h)]. 357 -ssList(A) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != A | app(f77(A),cons(f75(A),cons(f76(A),f78(A)))) = A. [copy(356),merge(h)]. 358 -ssItem(A) | -ssList(cons(A,nil)) | -ssItem(B) | -ssItem(C) | C = B | -ssList(D) | -ssList(E) | app(D,cons(B,cons(C,E))) != cons(A,nil). [resolve(55,b,48,h)]. 360 -ssItem(A) | -ssItem(B) | B = A | -ssList(C) | -ssList(D) | app(C,cons(A,cons(B,D))) != nil. [copy(359),unit_del(a,157)]. 361 -ssList(A) | -ssItem(B) | memberP(A,B) | -ssList(C) | app(A,cons(B,C)) != A. [factor(60,a,d)]. 362 -ssList(A) | -ssItem(B) | memberP(A,B) | -ssList(C) | app(C,cons(B,A)) != A. [factor(60,a,e)]. 363 -ssList(A) | -ssItem(B) | memberP(A,B) | -ssList(C) | app(C,cons(B,C)) != A. [factor(60,d,e)]. 364 -ssList(A) | -ssItem(B) | ssList(f3(A,B)) | -ssList(C) | app(A,cons(B,C)) != A. [factor(64,a,d)]. 365 -ssList(A) | -ssItem(B) | ssList(f3(A,B)) | -ssList(C) | app(C,cons(B,A)) != A. [factor(64,a,e)]. 366 -ssList(A) | -ssItem(B) | ssList(f3(A,B)) | -ssList(C) | app(C,cons(B,C)) != A. [factor(64,d,e)]. 367 -ssList(A) | -ssItem(B) | ssList(f4(A,B)) | -ssList(C) | app(A,cons(B,C)) != A. [factor(65,a,d)]. 368 -ssList(A) | -ssItem(B) | ssList(f4(A,B)) | -ssList(C) | app(C,cons(B,A)) != A. [factor(65,a,e)]. 369 -ssList(A) | -ssItem(B) | ssList(f4(A,B)) | -ssList(C) | app(C,cons(B,C)) != A. [factor(65,d,e)]. 370 -ssList(A) | -ssItem(B) | app(f3(A,B),cons(B,f4(A,B))) = A | -ssList(C) | app(A,cons(B,C)) != A. [factor(66,a,d)]. 371 -ssList(A) | -ssItem(B) | app(f3(A,B),cons(B,f4(A,B))) = A | -ssList(C) | app(C,cons(B,A)) != A. [factor(66,a,e)]. 372 -ssList(A) | -ssItem(B) | app(f3(A,B),cons(B,f4(A,B))) = A | -ssList(C) | app(C,cons(B,C)) != A. [factor(66,d,e)]. 373 -ssList(A) | -ssList(B) | frontsegP(A,B) | app(B,A) != A. [factor(72,a,d)]. 374 -ssList(A) | -ssList(B) | frontsegP(A,B) | app(B,B) != A. [factor(72,b,d)]. 375 -ssList(A) | ssList(f7(A,A)) | -frontsegP(A,A). [factor(73,a,b)]. 376 -ssList(A) | app(A,f7(A,A)) = A | -frontsegP(A,A). [factor(74,a,b)]. 377 -ssList(A) | ssList(f8(A,A)) | -ssList(B) | app(A,B) != A. [factor(75,a,b)]. 378 -ssList(A) | -ssList(B) | ssList(f8(A,B)) | app(B,A) != A. [factor(75,a,d)]. 379 -ssList(A) | -ssList(B) | ssList(f8(A,B)) | app(B,B) != A. [factor(75,b,d)]. 380 -ssList(A) | app(A,f8(A,A)) = A | -ssList(B) | app(A,B) != A. [factor(76,a,b)]. 381 -ssList(A) | -ssList(B) | app(B,f8(A,B)) = A | app(B,A) != A. [factor(76,a,d)]. 382 -ssList(A) | -ssList(B) | app(B,f8(A,B)) = A | app(B,B) != A. [factor(76,b,d)]. 383 -ssList(A) | -ssList(B) | rearsegP(A,B) | app(A,B) != A. [factor(77,a,d)]. 384 -ssList(A) | -ssList(B) | rearsegP(A,B) | app(B,B) != A. [factor(77,b,d)]. 385 -ssList(A) | ssList(f9(A,A)) | -rearsegP(A,A). [factor(78,a,b)]. 386 -ssList(A) | app(f9(A,A),A) = A | -rearsegP(A,A). [factor(79,a,b)]. 387 -ssList(A) | ssList(f10(A,A)) | -ssList(B) | app(B,A) != A. [factor(80,a,b)]. 388 -ssList(A) | -ssList(B) | ssList(f10(A,B)) | app(A,B) != A. [factor(80,a,d)]. 389 -ssList(A) | -ssList(B) | ssList(f10(A,B)) | app(B,B) != A. [factor(80,b,d)]. 390 -ssList(A) | app(f10(A,A),A) = A | -ssList(B) | app(B,A) != A. [factor(81,a,b)]. 391 -ssList(A) | -ssList(B) | app(f10(A,B),B) = A | app(A,B) != A. [factor(81,a,d)]. 392 -ssList(A) | -ssList(B) | app(f10(A,B),B) = A | app(B,B) != A. [factor(81,b,d)]. 393 -ssList(A) | -ssList(B) | segmentP(A,B) | -ssList(C) | app(app(A,B),C) != A. [factor(82,a,d)]. 394 -ssList(A) | -ssList(B) | segmentP(A,B) | -ssList(C) | app(app(C,B),A) != A. [factor(82,a,e)]. 395 -ssList(A) | -ssList(B) | segmentP(A,B) | -ssList(C) | app(app(B,B),C) != A. [factor(82,b,d)]. 396 -ssList(A) | -ssList(B) | segmentP(A,B) | -ssList(C) | app(app(C,B),B) != A. [factor(82,b,e)]. 397 -ssList(A) | -ssList(B) | segmentP(A,B) | -ssList(C) | app(app(C,B),C) != A. [factor(82,d,e)]. 398 -ssList(A) | ssList(f11(A,A)) | -segmentP(A,A). [factor(83,a,b)]. 399 -ssList(A) | ssList(f12(A,A)) | -segmentP(A,A). [factor(84,a,b)]. 400 -ssList(A) | app(app(f11(A,A),A),f12(A,A)) = A | -segmentP(A,A). [factor(85,a,b)]. 401 -ssList(A) | ssList(f13(A,A)) | -ssList(B) | -ssList(C) | app(app(B,A),C) != A. [factor(86,a,b)]. 402 -ssList(A) | -ssList(B) | ssList(f13(A,B)) | -ssList(C) | app(app(A,B),C) != A. [factor(86,a,d)]. 403 -ssList(A) | -ssList(B) | ssList(f13(A,B)) | -ssList(C) | app(app(C,B),A) != A. [factor(86,a,e)]. 404 -ssList(A) | -ssList(B) | ssList(f13(A,B)) | -ssList(C) | app(app(B,B),C) != A. [factor(86,b,d)]. 405 -ssList(A) | -ssList(B) | ssList(f13(A,B)) | -ssList(C) | app(app(C,B),B) != A. [factor(86,b,e)]. 406 -ssList(A) | -ssList(B) | ssList(f13(A,B)) | -ssList(C) | app(app(C,B),C) != A. [factor(86,d,e)]. 407 -ssList(A) | ssList(f14(A,A)) | -ssList(B) | -ssList(C) | app(app(B,A),C) != A. [factor(87,a,b)]. 408 -ssList(A) | -ssList(B) | ssList(f14(A,B)) | -ssList(C) | app(app(A,B),C) != A. [factor(87,a,d)]. 409 -ssList(A) | -ssList(B) | ssList(f14(A,B)) | -ssList(C) | app(app(C,B),A) != A. [factor(87,a,e)]. 410 -ssList(A) | -ssList(B) | ssList(f14(A,B)) | -ssList(C) | app(app(B,B),C) != A. [factor(87,b,d)]. 411 -ssList(A) | -ssList(B) | ssList(f14(A,B)) | -ssList(C) | app(app(C,B),B) != A. [factor(87,b,e)]. 412 -ssList(A) | -ssList(B) | ssList(f14(A,B)) | -ssList(C) | app(app(C,B),C) != A. [factor(87,d,e)]. 413 -ssList(A) | app(app(f13(A,A),A),f14(A,A)) = A | -ssList(B) | -ssList(C) | app(app(B,A),C) != A. [factor(88,a,b)]. 414 -ssList(A) | -ssList(B) | app(app(f13(A,B),B),f14(A,B)) = A | -ssList(C) | app(app(A,B),C) != A. [factor(88,a,d)]. 415 -ssList(A) | -ssList(B) | app(app(f13(A,B),B),f14(A,B)) = A | -ssList(C) | app(app(C,B),A) != A. [factor(88,a,e)]. 416 -ssList(A) | -ssList(B) | app(app(f13(A,B),B),f14(A,B)) = A | -ssList(C) | app(app(B,B),C) != A. [factor(88,b,d)]. 417 -ssList(A) | -ssList(B) | app(app(f13(A,B),B),f14(A,B)) = A | -ssList(C) | app(app(C,B),B) != A. [factor(88,b,e)]. 418 -ssList(A) | -ssList(B) | app(app(f13(A,B),B),f14(A,B)) = A | -ssList(C) | app(app(C,B),C) != A. [factor(88,d,e)]. 419 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f20(A)). [factor(89,a,f)]. 420 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f20(A)). [factor(89,a,g)]. 421 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f20(A)). [factor(89,a,h)]. 422 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssItem(f20(A)). [factor(89,b,c),merge(d)]. 423 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f20(A)). [factor(89,f,g)]. 424 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f20(A)). [factor(89,f,h)]. 425 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f20(A)). [factor(89,g,h)]. 426 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f21(A)). [factor(90,a,f)]. 427 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f21(A)). [factor(90,a,g)]. 428 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f21(A)). [factor(90,a,h)]. 429 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssItem(f21(A)). [factor(90,b,c),merge(d)]. 430 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f21(A)). [factor(90,f,g)]. 431 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f21(A)). [factor(90,f,h)]. 432 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f21(A)). [factor(90,g,h)]. 433 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | leq(f20(A),f21(A)). [factor(91,a,f)]. 434 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | leq(f20(A),f21(A)). [factor(91,a,g)]. 435 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | leq(f20(A),f21(A)). [factor(91,a,h)]. 436 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | leq(f20(A),f21(A)). [factor(91,b,c),merge(d)]. 437 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | leq(f20(A),f21(A)). [factor(91,f,g)]. 438 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | leq(f20(A),f21(A)). [factor(91,f,h)]. 439 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | leq(f20(A),f21(A)). [factor(91,g,h)]. 440 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | leq(f21(A),f20(A)). [factor(92,a,f)]. 441 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | leq(f21(A),f20(A)). [factor(92,a,g)]. 442 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | leq(f21(A),f20(A)). [factor(92,a,h)]. 443 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | leq(f21(A),f20(A)). [factor(92,b,c),merge(d)]. 444 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | leq(f21(A),f20(A)). [factor(92,f,g)]. 445 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | leq(f21(A),f20(A)). [factor(92,f,h)]. 446 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | leq(f21(A),f20(A)). [factor(92,g,h)]. 447 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f22(A)). [factor(93,a,f)]. 448 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f22(A)). [factor(93,a,g)]. 449 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f22(A)). [factor(93,a,h)]. 450 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssList(f22(A)). [factor(93,b,c),merge(d)]. 451 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f22(A)). [factor(93,f,g)]. 452 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f22(A)). [factor(93,f,h)]. 453 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f22(A)). [factor(93,g,h)]. 454 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f23(A)). [factor(94,a,f)]. 455 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f23(A)). [factor(94,a,g)]. 456 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f23(A)). [factor(94,a,h)]. 457 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssList(f23(A)). [factor(94,b,c),merge(d)]. 458 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f23(A)). [factor(94,f,g)]. 459 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f23(A)). [factor(94,f,h)]. 460 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f23(A)). [factor(94,g,h)]. 461 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f24(A)). [factor(95,a,f)]. 462 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f24(A)). [factor(95,a,g)]. 463 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f24(A)). [factor(95,a,h)]. 464 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssList(f24(A)). [factor(95,b,c),merge(d)]. 465 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f24(A)). [factor(95,f,g)]. 466 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f24(A)). [factor(95,f,h)]. 467 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f24(A)). [factor(95,g,h)]. 468 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [factor(96,a,f)]. 469 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [factor(96,a,g)]. 470 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [factor(96,a,h)]. 471 -ssList(A) | -ssItem(B) | -leq(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [factor(96,b,c),merge(d)]. 472 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [factor(96,f,g)]. 473 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [factor(96,f,h)]. 474 -ssList(A) | -ssItem(B) | -ssItem(C) | -leq(B,C) | -leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | app(app(f22(A),cons(f20(A),f23(A))),cons(f21(A),f24(A))) = A. [factor(96,g,h)]. 475 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f30(A)). [factor(97,a,f)]. 476 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f30(A)). [factor(97,a,g)]. 477 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f30(A)). [factor(97,a,h)]. 478 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f30(A)). [factor(97,f,g)]. 479 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f30(A)). [factor(97,f,h)]. 480 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f30(A)). [factor(97,g,h)]. 481 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f31(A)). [factor(98,a,f)]. 482 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f31(A)). [factor(98,a,g)]. 483 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f31(A)). [factor(98,a,h)]. 484 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f31(A)). [factor(98,f,g)]. 485 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f31(A)). [factor(98,f,h)]. 486 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f31(A)). [factor(98,g,h)]. 487 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | -leq(f30(A),f31(A)). [factor(99,a,f)]. 488 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | -leq(f30(A),f31(A)). [factor(99,a,g)]. 489 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | -leq(f30(A),f31(A)). [factor(99,a,h)]. 490 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | -leq(f30(A),f31(A)). [factor(99,f,g)]. 491 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | -leq(f30(A),f31(A)). [factor(99,f,h)]. 492 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | -leq(f30(A),f31(A)). [factor(99,g,h)]. 493 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | -leq(f31(A),f30(A)). [factor(100,a,f)]. 494 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | -leq(f31(A),f30(A)). [factor(100,a,g)]. 495 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | -leq(f31(A),f30(A)). [factor(100,a,h)]. 496 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | -leq(f31(A),f30(A)). [factor(100,f,g)]. 497 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | -leq(f31(A),f30(A)). [factor(100,f,h)]. 498 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | -leq(f31(A),f30(A)). [factor(100,g,h)]. 499 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f32(A)). [factor(101,a,f)]. 500 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f32(A)). [factor(101,a,g)]. 501 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f32(A)). [factor(101,a,h)]. 502 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f32(A)). [factor(101,f,g)]. 503 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f32(A)). [factor(101,f,h)]. 504 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f32(A)). [factor(101,g,h)]. 505 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f33(A)). [factor(102,a,f)]. 506 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f33(A)). [factor(102,a,g)]. 507 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f33(A)). [factor(102,a,h)]. 508 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f33(A)). [factor(102,f,g)]. 509 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f33(A)). [factor(102,f,h)]. 510 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f33(A)). [factor(102,g,h)]. 511 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f34(A)). [factor(103,a,f)]. 512 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f34(A)). [factor(103,a,g)]. 513 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f34(A)). [factor(103,a,h)]. 514 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f34(A)). [factor(103,f,g)]. 515 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f34(A)). [factor(103,f,h)]. 516 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f34(A)). [factor(103,g,h)]. 517 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [factor(104,a,f)]. 518 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [factor(104,a,g)]. 519 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [factor(104,a,h)]. 520 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [factor(104,f,g)]. 521 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [factor(104,f,h)]. 522 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | leq(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | app(app(f32(A),cons(f30(A),f33(A))),cons(f31(A),f34(A))) = A. [factor(104,g,h)]. 523 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f40(A)). [factor(105,a,f)]. 524 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f40(A)). [factor(105,a,g)]. 525 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f40(A)). [factor(105,a,h)]. 526 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssItem(f40(A)). [factor(105,b,c),merge(d)]. 527 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f40(A)). [factor(105,f,g)]. 528 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f40(A)). [factor(105,f,h)]. 529 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f40(A)). [factor(105,g,h)]. 530 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f41(A)). [factor(106,a,f)]. 531 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f41(A)). [factor(106,a,g)]. 532 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f41(A)). [factor(106,a,h)]. 533 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssItem(f41(A)). [factor(106,b,c),merge(d)]. 534 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f41(A)). [factor(106,f,g)]. 535 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f41(A)). [factor(106,f,h)]. 536 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f41(A)). [factor(106,g,h)]. 537 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | -lt(f40(A),f41(A)). [factor(107,a,f)]. 538 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | -lt(f40(A),f41(A)). [factor(107,a,g)]. 539 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | -lt(f40(A),f41(A)). [factor(107,a,h)]. 540 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | -lt(f40(A),f41(A)). [factor(107,b,c),merge(d)]. 541 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | -lt(f40(A),f41(A)). [factor(107,f,g)]. 542 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | -lt(f40(A),f41(A)). [factor(107,f,h)]. 543 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | -lt(f40(A),f41(A)). [factor(107,g,h)]. 544 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | -lt(f41(A),f40(A)). [factor(108,a,f)]. 545 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | -lt(f41(A),f40(A)). [factor(108,a,g)]. 546 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | -lt(f41(A),f40(A)). [factor(108,a,h)]. 547 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | -lt(f41(A),f40(A)). [factor(108,b,c),merge(d)]. 548 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | -lt(f41(A),f40(A)). [factor(108,f,g)]. 549 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | -lt(f41(A),f40(A)). [factor(108,f,h)]. 550 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | -lt(f41(A),f40(A)). [factor(108,g,h)]. 551 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f42(A)). [factor(109,a,f)]. 552 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f42(A)). [factor(109,a,g)]. 553 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f42(A)). [factor(109,a,h)]. 554 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssList(f42(A)). [factor(109,b,c),merge(d)]. 555 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f42(A)). [factor(109,f,g)]. 556 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f42(A)). [factor(109,f,h)]. 557 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f42(A)). [factor(109,g,h)]. 558 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f43(A)). [factor(110,a,f)]. 559 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f43(A)). [factor(110,a,g)]. 560 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f43(A)). [factor(110,a,h)]. 561 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssList(f43(A)). [factor(110,b,c),merge(d)]. 562 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f43(A)). [factor(110,f,g)]. 563 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f43(A)). [factor(110,f,h)]. 564 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f43(A)). [factor(110,g,h)]. 565 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssList(f44(A)). [factor(111,a,f)]. 566 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssList(f44(A)). [factor(111,a,g)]. 567 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssList(f44(A)). [factor(111,a,h)]. 568 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | ssList(f44(A)). [factor(111,b,c),merge(d)]. 569 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssList(f44(A)). [factor(111,f,g)]. 570 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssList(f44(A)). [factor(111,f,h)]. 571 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssList(f44(A)). [factor(111,g,h)]. 572 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [factor(112,a,f)]. 573 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [factor(112,a,g)]. 574 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [factor(112,a,h)]. 575 -ssList(A) | -ssItem(B) | lt(B,B) | -ssList(C) | -ssList(D) | -ssList(E) | app(app(C,cons(B,D)),cons(B,E)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [factor(112,b,c),merge(d)]. 576 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [factor(112,f,g)]. 577 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [factor(112,f,h)]. 578 -ssList(A) | -ssItem(B) | -ssItem(C) | lt(B,C) | lt(C,B) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | app(app(f42(A),cons(f40(A),f43(A))),cons(f41(A),f44(A))) = A. [factor(112,g,h)]. 579 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | -totalorderedP(A). [factor(120,a,e)]. 580 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | -totalorderedP(A). [factor(120,a,f)]. 581 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | -totalorderedP(A). [factor(120,a,g)]. 582 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | -totalorderedP(A). [factor(120,e,f)]. 583 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | -totalorderedP(A). [factor(120,e,g)]. 584 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | -totalorderedP(A). [factor(120,f,g)]. 585 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f50(A)). [factor(121,a,e)]. 586 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f50(A)). [factor(121,a,f)]. 587 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f50(A)). [factor(121,a,g)]. 588 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f50(A)). [factor(121,e,f)]. 589 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f50(A)). [factor(121,e,g)]. 590 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f50(A)). [factor(121,f,g)]. 591 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | ssItem(f51(A)). [factor(122,a,e)]. 592 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | ssItem(f51(A)). [factor(122,a,f)]. 593 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | ssItem(f51(A)). [factor(122,a,g)]. 594 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | ssItem(f51(A)). [factor(122,e,f)]. 595 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,D)) != A | ssItem(f51(A)). [factor(122,e,g)]. 596 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,E)) != A | ssItem(f51(A)). [factor(122,f,g)]. 597 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(A,cons(B,D)),cons(C,E)) != A | -leq(f50(A),f51(A)). [factor(123,a,e)]. 598 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,A)),cons(C,E)) != A | -leq(f50(A),f51(A)). [factor(123,a,f)]. 599 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,E)),cons(C,A)) != A | -leq(f50(A),f51(A)). [factor(123,a,g)]. 600 -ssList(A) | -ssItem(B) | -ssItem(C) | leq(B,C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | -leq(f50(A),f51(A)). [fac