----- Otter 3.2, August 2001 ----- The process was started by sandro on roke.hawke.org, Thu Sep 4 02:30:12 2003 The command was "otter". The process ID is 2239. set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(sigint_interact). include('otter/owlAx-card.otter'). ------- start included file otter/owlAx-card.otter------- formula_list(usable). all X (X=X). all X Y (rdf(X,owl_differentFrom,Y)->X!=Y). all X Y (rdf(X,owl_differentFrom,Y)->Y!=X). all X Y Z (rdf(X,'foo:succ',Y)&rdf(X,'foo:succ',Z)->Y=Z). all X Y Z (rdf(X,'foo:succ',Y)&rdf(Z,'foo:succ',Y)->X=Z). 'foo:zero'=i0. rdf('foo:zero','foo:succ',i1). rdf(i1,'foo:succ',i2). rdf(i2,'foo:succ',i3). all S (maxCardinality(S,i0)<-> -(exists A item(A,S))). all S (maxCardinality(S,i1)<-> -(exists A B (A!=B&item(A,S)&item(B,S)))). all S (maxCardinality(S,i2)<-> -(exists A B C (A!=B&A!=C&B!=C&B!=A&C!=A&C!=B&item(A,S)&item(B,S)&item(C,S)))). all S minCardinality(S,i0). all S (minCardinality(S,i1)<-> (exists A item(A,S))). all S (minCardinality(S,i2)<-> (exists A B (A!=B&item(A,S)&item(B,S)))). all S (minCardinality(S,i2)<-> (exists A B (A!=B&item(A,S)&item(B,S)))). all S (minCardinality(S,i3)<-> (exists A B C (A!=B&B!=C&A!=C&item(A,S)&item(B,S)&item(C,S)))). all RESTRICTION PROPERTY CARDINALITY INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_cardinality,CARDINALITY)&rdf(INST,rdf_type,RESTRICTION)-> (exists SET all VAL ((rdf(INST,PROPERTY,VAL)->item(VAL,SET))&minCardinality(SET,CARDINALITY)&maxCardinality(SET,CARDINALITY)))). all RESTRICTION PROPERTY CARDINALITY INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_maxCardinality,CARDINALITY)&rdf(INST,rdf_type,RESTRICTION)-> (exists SET all VAL ((rdf(INST,PROPERTY,VAL)->item(VAL,SET))&maxCardinality(SET,CARDINALITY)))). all RESTRICTION PROPERTY CARDINALITY INST (rdf(RESTRICTION,rdf_type,owl_Restriction)&rdf(RESTRICTION,owl_onProperty,PROPERTY)&rdf(RESTRICTION,owl_minCardinality,CARDINALITY)&rdf(INST,rdf_type,RESTRICTION)-> (exists SET all VAL ((rdf(INST,PROPERTY,VAL)->item(VAL,SET))&minCardinality(SET,CARDINALITY)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] x1=x1. 0 [] -rdf(x2,owl_differentFrom,x3)|x2!=x3. 0 [] -rdf(x4,owl_differentFrom,x5)|x5!=x4. 0 [] -rdf(x6,'foo:succ',x7)| -rdf(x6,'foo:succ',x8)|x7=x8. 0 [] -rdf(x9,'foo:succ',x10)| -rdf(x11,'foo:succ',x10)|x9=x11. 0 [] 'foo:zero'=i0. 0 [] rdf('foo:zero','foo:succ',i1). 0 [] rdf(i1,'foo:succ',i2). 0 [] rdf(i2,'foo:succ',i3). 0 [] -maxCardinality(x12,i0)| -item(x13,x12). 0 [] maxCardinality(x12,i0)|item($f1(x12),x12). 0 [] -maxCardinality(x14,i1)|x15=x16| -item(x15,x14)| -item(x16,x14). 0 [] maxCardinality(x14,i1)|$f3(x14)!=$f2(x14). 0 [] maxCardinality(x14,i1)|item($f3(x14),x14). 0 [] maxCardinality(x14,i1)|item($f2(x14),x14). 0 [] -maxCardinality(x17,i2)|x18=x19|x18=x20|x19=x20|x19=x18|x20=x18|x20=x19| -item(x18,x17)| -item(x19,x17)| -item(x20,x17). 0 [] maxCardinality(x17,i2)|$f6(x17)!=$f5(x17). 0 [] maxCardinality(x17,i2)|$f6(x17)!=$f4(x17). 0 [] maxCardinality(x17,i2)|$f5(x17)!=$f4(x17). 0 [] maxCardinality(x17,i2)|$f5(x17)!=$f6(x17). 0 [] maxCardinality(x17,i2)|$f4(x17)!=$f6(x17). 0 [] maxCardinality(x17,i2)|$f4(x17)!=$f5(x17). 0 [] maxCardinality(x17,i2)|item($f6(x17),x17). 0 [] maxCardinality(x17,i2)|item($f5(x17),x17). 0 [] maxCardinality(x17,i2)|item($f4(x17),x17). 0 [] minCardinality(x21,i0). 0 [] -minCardinality(x22,i1)|item($f7(x22),x22). 0 [] minCardinality(x22,i1)| -item(x23,x22). 0 [] -minCardinality(x24,i2)|$f9(x24)!=$f8(x24). 0 [] -minCardinality(x24,i2)|item($f9(x24),x24). 0 [] -minCardinality(x24,i2)|item($f8(x24),x24). 0 [] minCardinality(x24,i2)|x25=x26| -item(x25,x24)| -item(x26,x24). 0 [] -minCardinality(x27,i2)|$f11(x27)!=$f10(x27). 0 [] -minCardinality(x27,i2)|item($f11(x27),x27). 0 [] -minCardinality(x27,i2)|item($f10(x27),x27). 0 [] minCardinality(x27,i2)|x28=x29| -item(x28,x27)| -item(x29,x27). 0 [] -minCardinality(x30,i3)|$f14(x30)!=$f13(x30). 0 [] -minCardinality(x30,i3)|$f13(x30)!=$f12(x30). 0 [] -minCardinality(x30,i3)|$f14(x30)!=$f12(x30). 0 [] -minCardinality(x30,i3)|item($f14(x30),x30). 0 [] -minCardinality(x30,i3)|item($f13(x30),x30). 0 [] -minCardinality(x30,i3)|item($f12(x30),x30). 0 [] minCardinality(x30,i3)|x31=x32|x32=x33|x31=x33| -item(x31,x30)| -item(x32,x30)| -item(x33,x30). 0 [] -rdf(x34,rdf_type,owl_Restriction)| -rdf(x34,owl_onProperty,x35)| -rdf(x34,owl_cardinality,x36)| -rdf(x37,rdf_type,x34)| -rdf(x37,x35,x38)|item(x38,$f15(x34,x35,x36,x37)). 0 [] -rdf(x34,rdf_type,owl_Restriction)| -rdf(x34,owl_onProperty,x35)| -rdf(x34,owl_cardinality,x36)| -rdf(x37,rdf_type,x34)|minCardinality($f15(x34,x35,x36,x37),x36). 0 [] -rdf(x34,rdf_type,owl_Restriction)| -rdf(x34,owl_onProperty,x35)| -rdf(x34,owl_cardinality,x36)| -rdf(x37,rdf_type,x34)|maxCardinality($f15(x34,x35,x36,x37),x36). 0 [] -rdf(x39,rdf_type,owl_Restriction)| -rdf(x39,owl_onProperty,x40)| -rdf(x39,owl_maxCardinality,x41)| -rdf(x42,rdf_type,x39)| -rdf(x42,x40,x43)|item(x43,$f16(x39,x40,x41,x42)). 0 [] -rdf(x39,rdf_type,owl_Restriction)| -rdf(x39,owl_onProperty,x40)| -rdf(x39,owl_maxCardinality,x41)| -rdf(x42,rdf_type,x39)|maxCardinality($f16(x39,x40,x41,x42),x41). 0 [] -rdf(x44,rdf_type,owl_Restriction)| -rdf(x44,owl_onProperty,x45)| -rdf(x44,owl_minCardinality,x46)| -rdf(x47,rdf_type,x44)| -rdf(x47,x45,x48)|item(x48,$f17(x44,x45,x46,x47)). 0 [] -rdf(x44,rdf_type,owl_Restriction)| -rdf(x44,owl_onProperty,x45)| -rdf(x44,owl_minCardinality,x46)| -rdf(x47,rdf_type,x44)|minCardinality($f17(x44,x45,x46,x47),x46). end_of_list. ------- end included file otter/owlAx-card.otter------- formula_list(usable). exists s (rdf(s,rdf_type,owl_Restriction)&rdf(s,owl_maxCardinality,lit2)&rdf('foo:zero','foo:succ',lit1)&rdf(lit1,'foo:succ',lit2)&rdf(s,owl_onProperty,ns82_prop)&rdf(ns82_sb1,rdf_type,s)&rdf(ns82_sb1,ns82_prop,ns82_ob1)&rdf(ns82_sb1,ns82_prop,ns82_ob2)&rdf(ns82_sb1,ns82_prop,ns82_ob3)&rdf(ns82_ob1,owl_differentFrom,ns82_ob2)&rdf(ns82_ob1,owl_differentFrom,ns82_ob3)&rdf(ns82_ob2,owl_differentFrom,ns82_ob3)&rdf(ns82_prop,rdf_type,owl_ObjectProperty)). end_of_list. -------> usable clausifies to: list(usable). 0 [] rdf($c1,rdf_type,owl_Restriction). 0 [] rdf($c1,owl_maxCardinality,lit2). 0 [] rdf('foo:zero','foo:succ',lit1). 0 [] rdf(lit1,'foo:succ',lit2). 0 [] rdf($c1,owl_onProperty,ns82_prop). 0 [] rdf(ns82_sb1,rdf_type,$c1). 0 [] rdf(ns82_sb1,ns82_prop,ns82_ob1). 0 [] rdf(ns82_sb1,ns82_prop,ns82_ob2). 0 [] rdf(ns82_sb1,ns82_prop,ns82_ob3). 0 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob2). 0 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob3). 0 [] rdf(ns82_ob2,owl_differentFrom,ns82_ob3). 0 [] rdf(ns82_prop,rdf_type,owl_ObjectProperty). end_of_list. SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=10. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deletion, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: set(unit_deletion). dependent: set(factor). ------------> process usable: ** KEPT (pick-wt=7): 1 [] -rdf(x,owl_differentFrom,y)|x!=y. ** KEPT (pick-wt=7): 2 [] -rdf(x,owl_differentFrom,y)|y!=x. ** KEPT (pick-wt=11): 3 [] -rdf(x,'foo:succ',y)| -rdf(x,'foo:succ',z)|y=z. ** KEPT (pick-wt=11): 4 [] -rdf(x,'foo:succ',y)| -rdf(z,'foo:succ',y)|x=z. ** KEPT (pick-wt=6): 5 [] -maxCardinality(x,i0)| -item(y,x). ** KEPT (pick-wt=12): 6 [] -maxCardinality(x,i1)|y=z| -item(y,x)| -item(z,x). ** KEPT (pick-wt=8): 7 [] maxCardinality(x,i1)|$f3(x)!=$f2(x). ** KEPT (pick-wt=30): 8 [] -maxCardinality(x,i2)|y=z|y=u|z=u|z=y|u=y|u=z| -item(y,x)| -item(z,x)| -item(u,x). ** KEPT (pick-wt=8): 9 [] maxCardinality(x,i2)|$f6(x)!=$f5(x). ** KEPT (pick-wt=8): 10 [] maxCardinality(x,i2)|$f6(x)!=$f4(x). ** KEPT (pick-wt=8): 11 [] maxCardinality(x,i2)|$f5(x)!=$f4(x). Following clause subsumed by 9 during input processing: 0 [flip.2] maxCardinality(x,i2)|$f6(x)!=$f5(x). Following clause subsumed by 10 during input processing: 0 [flip.2] maxCardinality(x,i2)|$f6(x)!=$f4(x). Following clause subsumed by 11 during input processing: 0 [flip.2] maxCardinality(x,i2)|$f5(x)!=$f4(x). ** KEPT (pick-wt=7): 12 [] -minCardinality(x,i1)|item($f7(x),x). ** KEPT (pick-wt=6): 13 [] minCardinality(x,i1)| -item(y,x). ** KEPT (pick-wt=8): 14 [] -minCardinality(x,i2)|$f9(x)!=$f8(x). ** KEPT (pick-wt=7): 15 [] -minCardinality(x,i2)|item($f9(x),x). ** KEPT (pick-wt=7): 16 [] -minCardinality(x,i2)|item($f8(x),x). ** KEPT (pick-wt=12): 17 [] minCardinality(x,i2)|y=z| -item(y,x)| -item(z,x). ** KEPT (pick-wt=8): 18 [] -minCardinality(x,i2)|$f11(x)!=$f10(x). ** KEPT (pick-wt=7): 19 [] -minCardinality(x,i2)|item($f11(x),x). ** KEPT (pick-wt=7): 20 [] -minCardinality(x,i2)|item($f10(x),x). Following clause subsumed by 17 during input processing: 0 [] minCardinality(x,i2)|y=z| -item(y,x)| -item(z,x). ** KEPT (pick-wt=8): 21 [] -minCardinality(x,i3)|$f14(x)!=$f13(x). ** KEPT (pick-wt=8): 22 [] -minCardinality(x,i3)|$f13(x)!=$f12(x). ** KEPT (pick-wt=8): 23 [] -minCardinality(x,i3)|$f14(x)!=$f12(x). ** KEPT (pick-wt=7): 24 [] -minCardinality(x,i3)|item($f14(x),x). ** KEPT (pick-wt=7): 25 [] -minCardinality(x,i3)|item($f13(x),x). ** KEPT (pick-wt=7): 26 [] -minCardinality(x,i3)|item($f12(x),x). ** KEPT (pick-wt=21): 27 [] minCardinality(x,i3)|y=z|z=u|y=u| -item(y,x)| -item(z,x)| -item(u,x). ** KEPT (pick-wt=27): 28 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|item(v,$f15(x,y,z,u)). ** KEPT (pick-wt=23): 29 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdf_type,x)|minCardinality($f15(x,y,z,u),z). ** KEPT (pick-wt=23): 30 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_cardinality,z)| -rdf(u,rdf_type,x)|maxCardinality($f15(x,y,z,u),z). ** KEPT (pick-wt=27): 31 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_maxCardinality,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|item(v,$f16(x,y,z,u)). ** KEPT (pick-wt=23): 32 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_maxCardinality,z)| -rdf(u,rdf_type,x)|maxCardinality($f16(x,y,z,u),z). ** KEPT (pick-wt=27): 33 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_minCardinality,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|item(v,$f17(x,y,z,u)). ** KEPT (pick-wt=23): 34 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_minCardinality,z)| -rdf(u,rdf_type,x)|minCardinality($f17(x,y,z,u),z). ------------> process sos: ** KEPT (pick-wt=3): 69 [] x=x. ** KEPT (pick-wt=3): 71 [copy,70,flip.1] i0='foo:zero'. ---> New Demodulator: 72 [new_demod,71] i0='foo:zero'. ** KEPT (pick-wt=4): 73 [] rdf('foo:zero','foo:succ',i1). ** KEPT (pick-wt=4): 74 [] rdf(i1,'foo:succ',i2). ** KEPT (pick-wt=4): 75 [] rdf(i2,'foo:succ',i3). ** KEPT (pick-wt=7): 77 [copy,76,demod,72] maxCardinality(x,'foo:zero')|item($f1(x),x). ** KEPT (pick-wt=7): 78 [] maxCardinality(x,i1)|item($f3(x),x). ** KEPT (pick-wt=7): 79 [] maxCardinality(x,i1)|item($f2(x),x). ** KEPT (pick-wt=7): 80 [] maxCardinality(x,i2)|item($f6(x),x). ** KEPT (pick-wt=7): 81 [] maxCardinality(x,i2)|item($f5(x),x). ** KEPT (pick-wt=7): 82 [] maxCardinality(x,i2)|item($f4(x),x). ** KEPT (pick-wt=3): 84 [copy,83,demod,72] minCardinality(x,'foo:zero'). ** KEPT (pick-wt=4): 85 [] rdf($c1,rdf_type,owl_Restriction). ** KEPT (pick-wt=4): 86 [] rdf($c1,owl_maxCardinality,lit2). ** KEPT (pick-wt=4): 87 [] rdf('foo:zero','foo:succ',lit1). ** KEPT (pick-wt=4): 88 [] rdf(lit1,'foo:succ',lit2). ** KEPT (pick-wt=4): 89 [] rdf($c1,owl_onProperty,ns82_prop). ** KEPT (pick-wt=4): 90 [] rdf(ns82_sb1,rdf_type,$c1). ** KEPT (pick-wt=4): 91 [] rdf(ns82_sb1,ns82_prop,ns82_ob1). ** KEPT (pick-wt=4): 92 [] rdf(ns82_sb1,ns82_prop,ns82_ob2). ** KEPT (pick-wt=4): 93 [] rdf(ns82_sb1,ns82_prop,ns82_ob3). ** KEPT (pick-wt=4): 94 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob2). ** KEPT (pick-wt=4): 95 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob3). ** KEPT (pick-wt=4): 96 [] rdf(ns82_ob2,owl_differentFrom,ns82_ob3). ** KEPT (pick-wt=4): 97 [] rdf(ns82_prop,rdf_type,owl_ObjectProperty). Following clause subsumed by 69 during input processing: 0 [copy,69,flip.1] x=x. 69 back subsumes 40. 69 back subsumes 39. 69 back subsumes 38. 69 back subsumes 37. 69 back subsumes 36. 69 back subsumes 35. >>>> Starting back demodulation with 72. >> back demodulating 5 with 72. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=3) 69 [] x=x. given clause #2: (wt=3) 71 [copy,70,flip.1] i0='foo:zero'. given clause #3: (wt=3) 84 [copy,83,demod,72] minCardinality(x,'foo:zero'). given clause #4: (wt=4) 73 [] rdf('foo:zero','foo:succ',i1). given clause #5: (wt=4) 74 [] rdf(i1,'foo:succ',i2). given clause #6: (wt=4) 75 [] rdf(i2,'foo:succ',i3). given clause #7: (wt=4) 85 [] rdf($c1,rdf_type,owl_Restriction). given clause #8: (wt=4) 86 [] rdf($c1,owl_maxCardinality,lit2). given clause #9: (wt=4) 87 [] rdf('foo:zero','foo:succ',lit1). given clause #10: (wt=3) 231 [hyper,87,3,73,flip.1] lit1=i1. given clause #11: (wt=7) 77 [copy,76,demod,72] maxCardinality(x,'foo:zero')|item($f1(x),x). given clause #12: (wt=4) 89 [] rdf($c1,owl_onProperty,ns82_prop). given clause #13: (wt=4) 90 [] rdf(ns82_sb1,rdf_type,$c1). given clause #14: (wt=4) 91 [] rdf(ns82_sb1,ns82_prop,ns82_ob1). given clause #15: (wt=4) 92 [] rdf(ns82_sb1,ns82_prop,ns82_ob2). given clause #16: (wt=7) 78 [] maxCardinality(x,i1)|item($f3(x),x). given clause #17: (wt=4) 93 [] rdf(ns82_sb1,ns82_prop,ns82_ob3). given clause #18: (wt=4) 94 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob2). given clause #19: (wt=4) 95 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob3). given clause #20: (wt=4) 96 [] rdf(ns82_ob2,owl_differentFrom,ns82_ob3). given clause #21: (wt=7) 79 [] maxCardinality(x,i1)|item($f2(x),x). given clause #22: (wt=4) 97 [] rdf(ns82_prop,rdf_type,owl_ObjectProperty). given clause #23: (wt=4) 233 [back_demod,88,demod,232] rdf(i1,'foo:succ',lit2). given clause #24: (wt=3) 501 [hyper,233,3,74,flip.1] lit2=i2. given clause #25: (wt=4) 531 [back_demod,86,demod,502] rdf($c1,owl_maxCardinality,i2). given clause #26: (wt=7) 80 [] maxCardinality(x,i2)|item($f6(x),x). given clause #27: (wt=6) 98 [back_demod,5,demod,72] -maxCardinality(x,'foo:zero')| -item(y,x). given clause #28: (wt=7) 81 [] maxCardinality(x,i2)|item($f5(x),x). given clause #29: (wt=7) 82 [] maxCardinality(x,i2)|item($f4(x),x). given clause #30: (wt=7) 503 [back_demod,365,demod,502] item(ns82_ob3,$f16($c1,ns82_prop,i2,ns82_sb1)). given clause #31: (wt=21) 99 [para_into,71.1.1,27.4.1,demod,72,72] x='foo:zero'|minCardinality(y,i3)|'foo:zero'=z|z=x| -item('foo:zero',y)| -item(z,y)| -item(x,y). given clause #32: (wt=7) 504 [back_demod,325,demod,502] item(ns82_ob2,$f16($c1,ns82_prop,i2,ns82_sb1)). given clause #33: (wt=7) 505 [back_demod,300,demod,502] item(ns82_ob1,$f16($c1,ns82_prop,i2,ns82_sb1)). given clause #34: (wt=7) 506 [back_demod,275,demod,502,502] maxCardinality($f16($c1,ns82_prop,i2,ns82_sb1),i2). given clause #35: (wt=7) 593 [hyper,503,13] minCardinality($f16($c1,ns82_prop,i2,ns82_sb1),i1). given clause #36: (wt=27) 100 [para_into,71.1.1,8.7.1,demod,72,72,72,72,factor_simp] x='foo:zero'| -maxCardinality(y,i2)|z=x|z='foo:zero'|x=z|'foo:zero'=z| -item(z,y)| -item(x,y)| -item('foo:zero',y). given clause #37: (wt=9) 111 [factor,104.1.2] minCardinality(x,i2)| -item('foo:zero',x)| -item(i2,x). given clause #38: (wt=9) 560 [factor,553.1.3,factor_simp] -maxCardinality(x,i1)| -item('foo:zero',x)| -item(i1,x). given clause #39: (wt=9) 2115 [hyper,506,8,505,504,503,factor_simp,factor_simp,factor_simp] ns82_ob2=ns82_ob1|ns82_ob3=ns82_ob1|ns82_ob3=ns82_ob2. given clause #40: (wt=6) 2328 [hyper,2115,2,94] ns82_ob3=ns82_ob1|ns82_ob3=ns82_ob2. given clause #41: (wt=21) 101 [para_into,84.1.2,27.4.1] minCardinality(x,y)|minCardinality(z,i3)|'foo:zero'=u|u=y| -item('foo:zero',z)| -item(u,z)| -item(y,z). given clause #42: (wt=3) 2333 [hyper,2328,2,96,demod,2332] ns82_ob2=ns82_ob1.  Resetting weight limit to 15. Resetting weight limit to 15. sos_size=3355 given clause #43: (wt=3) 2363 [back_demod,2331,demod,2334] ns82_ob3=ns82_ob1. given clause #44: (wt=4) 2362 [back_demod,96,demod,2334,2332,2334] rdf(ns82_ob1,owl_differentFrom,ns82_ob1). -- HEY sandro, WE HAVE A PROOF!! -- -----> EMPTY CLAUSE at 99.86 sec ----> 3847 [hyper,2362,2,69] $F. Length of proof is 16. Level of proof is 9. ---------------- PROOF ---------------- 2 [] -rdf(x,owl_differentFrom,y)|y!=x. 3 [] -rdf(x,'foo:succ',y)| -rdf(x,'foo:succ',z)|y=z. 8 [] -maxCardinality(x,i2)|y=z|y=u|z=u|z=y|u=y|u=z| -item(y,x)| -item(z,x)| -item(u,x). 31 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_maxCardinality,z)| -rdf(u,rdf_type,x)| -rdf(u,y,v)|item(v,$f16(x,y,z,u)). 32 [] -rdf(x,rdf_type,owl_Restriction)| -rdf(x,owl_onProperty,y)| -rdf(x,owl_maxCardinality,z)| -rdf(u,rdf_type,x)|maxCardinality($f16(x,y,z,u),z). 69 [] x=x. 73 [] rdf('foo:zero','foo:succ',i1). 74 [] rdf(i1,'foo:succ',i2). 85 [] rdf($c1,rdf_type,owl_Restriction). 86 [] rdf($c1,owl_maxCardinality,lit2). 87 [] rdf('foo:zero','foo:succ',lit1). 88 [] rdf(lit1,'foo:succ',lit2). 89 [] rdf($c1,owl_onProperty,ns82_prop). 90 [] rdf(ns82_sb1,rdf_type,$c1). 91 [] rdf(ns82_sb1,ns82_prop,ns82_ob1). 92 [] rdf(ns82_sb1,ns82_prop,ns82_ob2). 93 [] rdf(ns82_sb1,ns82_prop,ns82_ob3). 94 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob2). 95 [] rdf(ns82_ob1,owl_differentFrom,ns82_ob3). 96 [] rdf(ns82_ob2,owl_differentFrom,ns82_ob3). 232,231 [hyper,87,3,73,flip.1] lit1=i1. 233 [back_demod,88,demod,232] rdf(i1,'foo:succ',lit2). 275 [hyper,90,32,85,89,86] maxCardinality($f16($c1,ns82_prop,lit2,ns82_sb1),lit2). 300 [hyper,91,31,85,89,86,90] item(ns82_ob1,$f16($c1,ns82_prop,lit2,ns82_sb1)). 325 [hyper,92,31,85,89,86,90] item(ns82_ob2,$f16($c1,ns82_prop,lit2,ns82_sb1)). 365 [hyper,93,31,85,89,86,90] item(ns82_ob3,$f16($c1,ns82_prop,lit2,ns82_sb1)). 502,501 [hyper,233,3,74,flip.1] lit2=i2. 503 [back_demod,365,demod,502] item(ns82_ob3,$f16($c1,ns82_prop,i2,ns82_sb1)). 504 [back_demod,325,demod,502] item(ns82_ob2,$f16($c1,ns82_prop,i2,ns82_sb1)). 505 [back_demod,300,demod,502] item(ns82_ob1,$f16($c1,ns82_prop,i2,ns82_sb1)). 506 [back_demod,275,demod,502,502] maxCardinality($f16($c1,ns82_prop,i2,ns82_sb1),i2). 2115 [hyper,506,8,505,504,503,factor_simp,factor_simp,factor_simp] ns82_ob2=ns82_ob1|ns82_ob3=ns82_ob1|ns82_ob3=ns82_ob2. 2328 [hyper,2115,2,94] ns82_ob3=ns82_ob1|ns82_ob3=ns82_ob2. 2332,2331 [hyper,2328,2,95] ns82_ob3=ns82_ob2. 2334,2333 [hyper,2328,2,96,demod,2332] ns82_ob2=ns82_ob1. 2362 [back_demod,96,demod,2334,2332,2334] rdf(ns82_ob1,owl_differentFrom,ns82_ob1). 3847 [hyper,2362,2,69] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 44 clauses generated 17987 clauses kept 3837 clauses forward subsumed 14485 clauses back subsumed 96 Kbytes malloced 4853 ----------- times (seconds) ----------- user CPU time 99.86 (0 hr, 1 min, 39 sec) system CPU time 0.48 (0 hr, 0 min, 0 sec) wall-clock time 101 (0 hr, 1 min, 41 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.02 for_sub time 72.50 back_sub time 4.38 conflict time 0.01 demod time 0.03 That finishes the proof of the theorem. Process 2239 finished Thu Sep 4 02:31:53 2003