----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Tue Sep 04 22:07:02 2001 The command was "C:\BIN\OTTER95.EXE". WARNING: clear(symbol_elim) flag already clear. clear(symbol_elim). set(order_eq). set(sort_literals). set(unit_deletion). set(dynamic_demod_all). dependent: set(dynamic_demod). set(back_demod). set(process_input). clear(print_given). set(print_lists_at_end). set(lrpo). set(lex_order_vars). lex([Id,V,pair(x,x),first(x),second(x),singleton(x),union(x,x),cart(x,x),P(x),SINGLETON,CUP,cross(x,x),PSM(x),intersection(x,x),complement(x),D(x),R(x),apply(x,x),image(x,x),composite(x,x),K,S,inverse(x),DUP,SWAP,FUNCTION(x),equal(x,x),member(x,x),subclass(x,x)]). assign(max_mem,300). assign(stats_level,0). list(usable). 0 [] subclass(x,x). end_of_list. formula_list(sos). equal(PSM(composite(inverse(DUP),cross(S,S))),CUP). subclass(CUP,cart(V,V)). subclass(CUP,cart(cart(V,V),V)). subclass(D(CUP),cart(V,V)). all x y z (subclass(union(x,y),z)&member(z,V)->member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S)))). all x y z (member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S)))->subclass(union(x,y),z)). all x y z (member(pair(pair(x,y),z),CUP)->equal(union(x,y),z)). all x y (member(pair(x,y),CUP)->equal(union(first(x),second(x)),y)). all x y (member(pair(x,y),cart(V,V))->member(pair(pair(x,y),union(x,y)),CUP)). all x y z (member(pair(x,y),image(inverse(CUP),z))->member(union(x,y),z)). all x y z (member(union(x,y),z)->member(pair(x,y),image(inverse(CUP),z))). all x y z (member(pair(x,y),image(inverse(CUP),singleton(z)))->equal(union(x,y),z)). all x y subclass(image(CUP,cart(P(x),P(y))),P(union(x,y))). all x y equal(image(CUP,cart(P(x),P(y))),P(union(x,y))). all x y z (member(x,z)&subclass(image(CUP,cart(z,R(SINGLETON))),z)->member(union(x,singleton(y)),z)). all w x y z (member(x,z)&member(y,w)&subclass(image(CUP,cart(z,image(SINGLETON,w))),z)->member(union(x,singleton(y)),z)). all x y z (member(x,y)&member(intersection(y,complement(singleton(x))),z)&subclass(image(CUP,cart(z,R(SINGLETON))),z)->member(y,z)). all w x y z (member(x,y)&subclass(y,w)&member(intersection(y,complement(singleton(x))),z)&subclass(image(CUP,cart(z,image(SINGLETON,w))),z)->member(y,z)). all x subclass(x,image(CUP,cart(x,x))). equal(composite(CUP,SWAP),CUP). all x equal(inverse(image(inverse(CUP),x)),image(inverse(CUP),x)). subclass(inverse(DUP),CUP). FUNCTION(CUP). equal(composite(CUP,DUP),Id). all x y (member(pair(x,y),cart(V,V))->equal(apply(CUP,pair(x,y)),union(x,y))). all x (member(x,cart(V,V))->equal(apply(CUP,x),union(first(x),second(x)))). equal(D(CUP),cart(V,V)). equal(R(CUP),V). all x subclass(image(CUP,cart(x,R(SINGLETON))),union(x,image(K,x))). end_of_list. -------> sos clausifies to: list(sos). 0 [] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP). 0 [] subclass(CUP,cart(V,V)). 0 [] subclass(CUP,cart(cart(V,V),V)). 0 [] subclass(D(CUP),cart(V,V)). 0 [] -subclass(union(x,y),z)| -member(z,V)|member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S))). 0 [] -member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S)))|subclass(union(x,y),z). 0 [] -member(pair(pair(x,y),z),CUP)|equal(union(x,y),z). 0 [] -member(pair(x,y),CUP)|equal(union(first(x),second(x)),y). 0 [] -member(pair(x,y),cart(V,V))|member(pair(pair(x,y),union(x,y)),CUP). 0 [] -member(pair(x,y),image(inverse(CUP),z))|member(union(x,y),z). 0 [] -member(union(x,y),z)|member(pair(x,y),image(inverse(CUP),z)). 0 [] -member(pair(x,y),image(inverse(CUP),singleton(z)))|equal(union(x,y),z). 0 [] subclass(image(CUP,cart(P(x),P(y))),P(union(x,y))). 0 [] equal(image(CUP,cart(P(x),P(y))),P(union(x,y))). 0 [] -member(x,z)| -subclass(image(CUP,cart(z,R(SINGLETON))),z)|member(union(x,singleton(y)),z). 0 [] -member(x,z)| -member(y,w)| -subclass(image(CUP,cart(z,image(SINGLETON,w))),z)|member(union(x,singleton(y)),z). 0 [] -member(x,y)| -member(intersection(y,complement(singleton(x))),z)| -subclass(image(CUP,cart(z,R(SINGLETON))),z)|member(y,z). 0 [] -member(x,y)| -subclass(y,w)| -member(intersection(y,complement(singleton(x))),z)| -subclass(image(CUP,cart(z,image(SINGLETON,w))),z)|member(y,z). 0 [] subclass(x,image(CUP,cart(x,x))). 0 [] equal(composite(CUP,SWAP),CUP). 0 [] equal(inverse(image(inverse(CUP),x)),image(inverse(CUP),x)). 0 [] subclass(inverse(DUP),CUP). 0 [] FUNCTION(CUP). 0 [] equal(composite(CUP,DUP),Id). 0 [] -member(pair(x,y),cart(V,V))|equal(apply(CUP,pair(x,y)),union(x,y)). 0 [] -member(x,cart(V,V))|equal(apply(CUP,x),union(first(x),second(x))). 0 [] equal(D(CUP),cart(V,V)). 0 [] equal(R(CUP),V). 0 [] subclass(image(CUP,cart(x,R(SINGLETON))),union(x,image(K,x))). end_of_list. list(demodulators). 1 [] equal(intersection(x,y),intersection(y,x)). 2 [] equal(union(x,y),union(y,x)). end_of_list. LRPO dependent demodulator: 1 [] equal(intersection(x,y),intersection(y,x)). LRPO dependent demodulator: 2 [] equal(union(x,y),union(y,x)). ------------> process usable: ** KEPT (pick-wt=3): 3 [] subclass(x,x). ------------> process sos: ** KEPT (pick-wt=9): 4 [] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP). ---> New Demodulator: 5 [new_demod,4] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP). ** KEPT (pick-wt=5): 6 [] subclass(CUP,cart(V,V)). ** KEPT (pick-wt=7): 7 [] subclass(CUP,cart(cart(V,V),V)). ** KEPT (pick-wt=6): 8 [] subclass(D(CUP),cart(V,V)). ** KEPT (pick-wt=20): 9 [] -member(x,V)| -subclass(union(y,z),x)|member(pair(pair(y,z),x),composite(inverse(DUP),cross(S,S))). ** KEPT (pick-wt=17): 10 [] -member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S)))|subclass(union(x,y),z). ** KEPT (pick-wt=12): 11 [] -member(pair(pair(x,y),z),CUP)|equal(union(x,y),z). ** KEPT (pick-wt=12): 12 [] -member(pair(x,y),CUP)|equal(union(first(x),second(x)),y). ** KEPT (pick-wt=16): 13 [] -member(pair(x,y),cart(V,V))|member(pair(pair(x,y),union(x,y)),CUP). ** KEPT (pick-wt=13): 14 [] -member(pair(x,y),image(inverse(CUP),z))|member(union(x,y),z). ** KEPT (pick-wt=13): 15 [] -member(union(x,y),z)|member(pair(x,y),image(inverse(CUP),z)). ** KEPT (pick-wt=14): 16 [] -member(pair(x,y),image(inverse(CUP),singleton(z)))|equal(union(x,y),z). ** KEPT (pick-wt=12): 17 [] subclass(image(CUP,cart(P(x),P(y))),P(union(x,y))). ** KEPT (pick-wt=12): 18 [] equal(image(CUP,cart(P(x),P(y))),P(union(x,y))). ---> New Demodulator: 19 [new_demod,18] equal(image(CUP,cart(P(x),P(y))),P(union(x,y))). ** KEPT (pick-wt=17): 20 [] -member(x,y)| -subclass(image(CUP,cart(y,R(SINGLETON))),y)|member(union(x,singleton(z)),y). ** KEPT (pick-wt=21): 21 [] -member(x,y)| -member(z,u)| -subclass(image(CUP,cart(y,image(SINGLETON,u))),y)|member(union(x,singleton(z)),y). ** KEPT (pick-wt=21): 22 [] -member(x,y)| -member(intersection(y,complement(singleton(x))),z)| -subclass(image(CUP,cart(z,R(SINGLETON))),z)|member(y,z). ** KEPT (pick-wt=25): 23 [] -member(x,y)| -member(intersection(y,complement(singleton(x))),z)| -subclass(y,u)| -subclass(image(CUP,cart(z,image(SINGLETON,u))),z)|member(y,z). ** KEPT (pick-wt=7): 24 [] subclass(x,image(CUP,cart(x,x))). ** KEPT (pick-wt=5): 25 [] equal(composite(CUP,SWAP),CUP). ---> New Demodulator: 26 [new_demod,25] equal(composite(CUP,SWAP),CUP). ** KEPT (pick-wt=10): 27 [] equal(inverse(image(inverse(CUP),x)),image(inverse(CUP),x)). ---> New Demodulator: 28 [new_demod,27] equal(inverse(image(inverse(CUP),x)),image(inverse(CUP),x)). ** KEPT (pick-wt=4): 29 [] subclass(inverse(DUP),CUP). ** KEPT (pick-wt=2): 30 [] FUNCTION(CUP). ** KEPT (pick-wt=5): 31 [] equal(composite(CUP,DUP),Id). ---> New Demodulator: 32 [new_demod,31] equal(composite(CUP,DUP),Id). ** KEPT (pick-wt=16): 33 [] -member(pair(x,y),cart(V,V))|equal(apply(CUP,pair(x,y)),union(x,y)). ** KEPT (pick-wt=14): 34 [] -member(x,cart(V,V))|equal(apply(CUP,x),union(first(x),second(x))). ** KEPT (pick-wt=6): 35 [] equal(D(CUP),cart(V,V)). ---> New Demodulator: 36 [new_demod,35] equal(D(CUP),cart(V,V)). ** KEPT (pick-wt=4): 37 [] equal(R(CUP),V). ---> New Demodulator: 38 [new_demod,37] equal(R(CUP),V). ** KEPT (pick-wt=12): 39 [] subclass(image(CUP,cart(x,R(SINGLETON))),union(x,image(K,x))). >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 19. >> back demodulating 17 with 19. >>>> Starting back demodulation with 26. >>>> Starting back demodulation with 28. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 36. >> back demodulating 8 with 36. >>>> Starting back demodulation with 38. ======= end of input processing ======= =========== start of search =========== Search stopped because sos empty. ============ end of search ============ list(usable). 3 [] subclass(x,x). 30 [] FUNCTION(CUP). 29 [] subclass(inverse(DUP),CUP). 37 [] equal(R(CUP),V). 6 [] subclass(CUP,cart(V,V)). 25 [] equal(composite(CUP,SWAP),CUP). 31 [] equal(composite(CUP,DUP),Id). 35 [] equal(D(CUP),cart(V,V)). 7 [] subclass(CUP,cart(cart(V,V),V)). 24 [] subclass(x,image(CUP,cart(x,x))). 4 [] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP). 27 [] equal(inverse(image(inverse(CUP),x)),image(inverse(CUP),x)). 11 [] -member(pair(pair(x,y),z),CUP)|equal(union(x,y),z). 12 [] -member(pair(x,y),CUP)|equal(union(first(x),second(x)),y). 18 [] equal(image(CUP,cart(P(x),P(y))),P(union(x,y))). 39 [] subclass(image(CUP,cart(x,R(SINGLETON))),union(x,image(K,x))). 14 [] -member(pair(x,y),image(inverse(CUP),z))|member(union(x,y),z). 15 [] -member(union(x,y),z)|member(pair(x,y),image(inverse(CUP),z)). 16 [] -member(pair(x,y),image(inverse(CUP),singleton(z)))|equal(union(x,y),z). 34 [] -member(x,cart(V,V))|equal(apply(CUP,x),union(first(x),second(x))). 13 [] -member(pair(x,y),cart(V,V))|member(pair(pair(x,y),union(x,y)),CUP). 33 [] -member(pair(x,y),cart(V,V))|equal(apply(CUP,pair(x,y)),union(x,y)). 10 [] -member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S)))|subclass(union(x,y),z). 20 [] -member(x,y)| -subclass(image(CUP,cart(y,R(SINGLETON))),y)|member(union(x,singleton(z)),y). 9 [] -member(x,V)| -subclass(union(y,z),x)|member(pair(pair(y,z),x),composite(inverse(DUP),cross(S,S))). 21 [] -member(x,y)| -member(z,u)| -subclass(image(CUP,cart(y,image(SINGLETON,u))),y)|member(union(x,singleton(z)),y). 22 [] -member(x,y)| -member(intersection(y,complement(singleton(x))),z)| -subclass(image(CUP,cart(z,R(SINGLETON))),z)|member(y,z). 23 [] -member(x,y)| -member(intersection(y,complement(singleton(x))),z)| -subclass(y,u)| -subclass(image(CUP,cart(z,image(SINGLETON,u))),z)|member(y,z). end_of_list. list(sos). end_of_list. list(demodulators). 1 [] equal(intersection(x,y),intersection(y,x)). 2 [] equal(union(x,y),union(y,x)). 5 [new_demod,4] equal(PSM(composite(inverse(DUP),cross(S,S))),CUP). 19 [new_demod,18] equal(image(CUP,cart(P(x),P(y))),P(union(x,y))). 26 [new_demod,25] equal(composite(CUP,SWAP),CUP). 28 [new_demod,27] equal(inverse(image(inverse(CUP),x)),image(inverse(CUP),x)). 32 [new_demod,31] equal(composite(CUP,DUP),Id). 36 [new_demod,35] equal(D(CUP),cart(V,V)). 38 [new_demod,37] equal(R(CUP),V). end_of_list. The job finished Tue Sep 04 22:07:02 2001