Skip to content
Permalink
Browse files

Prover9 translations of multidim_space_space updated

  • Loading branch information...
thahmann committed Nov 9, 2018
1 parent e972564 commit bb58c2cf99da63e41034007e46565bee27c2c669
@@ -5,13 +5,13 @@ formulas(sos).
( all x11 (- (ped(x11)) | - (s(x11)))) .
( all x21 s(r(x21))) .
( all x31 ( (s(x31)) <-> ((x31=r(x31))) )) .
( all x42 all x41 ( (cont(x42, x41)) -> ((s(x42) & s(x41))) )) .
( all x52 all x51 ( (lt(x52, x51)) -> ((s(x52) & s(x51))) )) .
( all x41 all x42 ( (cont(x41, x42)) -> ((s(x41) & s(x42))) )) .
( all x51 all x52 ( (lt(x51, x52)) -> ((s(x51) & s(x52))) )) .
( all x61 ( (zex(x61)) -> (s(x61)) )) .
( all x72 all x71 ( (bcont(x72, x71)) -> ((s(x72) & s(x71))) )) .
( all x71 all x72 ( (bcont(x71, x72)) -> ((s(x71) & s(x72))) )) .
( all x81 ( (ped(x81)) -> (maxdim(r(x81))) )) .
( all x92 all x91 ( (dk1(x92, x91)) -> (p(r(x92), r(x91))) )) .
( all x102 all x101 ( (hosts(x102, x101)) -> (( (rpf(x101)) <-> (p(r(x101), r(x102))) )) )) .
( all x112 all x111 all x113 all x114 ( ((hosts(x112, x111) & rpf(x111) & dk1(x113, x112) & dk1(x114, x111))) -> (p(r(x114), r(x113))) )) .
( all x122 all x121 ( (hosts(x122, x121)) -> (( (dpf(x121)) <-> (- (po(r(x122), r(x121)))) )) )) .
( all x91 all x92 ( (dk1(x91, x92)) -> (p(r(x91), r(x92))) )) .
( all x101 all x102 ( (hosts(x101, x102)) -> (( (rpf(x102)) <-> (p(r(x102), r(x101))) )) )) .
( all x111 all x114 all x113 all x112 ( ((hosts(x111, x114) & rpf(x114) & dk1(x113, x111) & dk1(x112, x114))) -> (p(r(x112), r(x113))) )) .
( all x121 all x122 ( (hosts(x121, x122)) -> (( (dpf(x122)) <-> (- (po(r(x121), r(x122)))) )) )) .
end_of_list.
@@ -5,11 +5,11 @@ formulas(sos).
( all x11 (- (ped(x11)) | - (s(x11)))) .
( all x21 s(r(x21))) .
( all x31 ( (s(x31)) <-> ((x31=r(x31))) )) .
( all x42 all x41 ( (cont(x42, x41)) -> ((s(x42) & s(x41))) )) .
( all x52 all x51 ( (lt(x52, x51)) -> ((s(x52) & s(x51))) )) .
( all x41 all x42 ( (cont(x41, x42)) -> ((s(x41) & s(x42))) )) .
( all x51 all x52 ( (lt(x51, x52)) -> ((s(x51) & s(x52))) )) .
( all x61 ( (zex(x61)) -> (s(x61)) )) .
( all x72 all x71 ( (bcont(x72, x71)) -> ((s(x72) & s(x71))) )) .
( all x71 all x72 ( (bcont(x71, x72)) -> ((s(x71) & s(x72))) )) .
( all x81 ( (ped(x81)) -> (maxdim(r(x81))) )) .
( all x92 all x91 ( (hosts(x92, x91)) -> (( (rpf(x91)) <-> (p(r(x91), r(x92))) )) )) .
( all x102 all x101 ( (hosts(x102, x101)) -> (( (dpf(x101)) <-> (- (po(r(x102), r(x101)))) )) )) .
( all x91 all x92 ( (hosts(x91, x92)) -> (( (rpf(x92)) <-> (p(r(x92), r(x91))) )) )) .
( all x101 all x102 ( (hosts(x101, x102)) -> (( (dpf(x102)) <-> (- (po(r(x101), r(x102)))) )) )) .
end_of_list.
@@ -7,11 +7,11 @@ formulas(sos).
( all x41 (ch(x41)=ch(ch(x41)))) .
( all x51 ( (- (zex(x51))) -> (cont(r(x51), ch(x51))) )) .
( all x61 ( ((- (zex(x61)) & - (closed(r(x61))))) -> (tcont(r(x61), ch(x61))) )) .
( all x72 all x71 ( (cont(r(x72), r(x71))) -> (cont(ch(x72), ch(x71))) )) .
( all x82 all x81 ( (((ch(x82)=ch(x81)) & - (zex(x82)))) -> (c(r(x82), r(x81))) )) .
( all x92 all x91 ( ((maxdim(r(x92)) & maxdim(r(x91)) & (r(x92)=ch(x92)) & (r(x91)=ch(x91)))) -> ((intersection(ch(x92), ch(x91))=ch(intersection(ch(x92), ch(x91))))) )) .
( all x102 all x101 ( ((icont(r(x102), r(x101)) & - (closed(difference(r(x101), r(x102)))))) -> (- ((difference(r(x101), r(x102))=ch(difference(r(x101), r(x102)))))) )) .
( all x112 all x111 ( ((icont(r(x112), r(x111)) & maxdim(r(x112)) & maxdim(r(x111)))) -> (cont(r(x112), ch(difference(r(x111), r(x112))))) )) .
( all x122 all x121 ( ((- (zex(x122)) | - (zex(x121)))) -> (( exists x123 exists x124 (tsum(r(x122), r(x121), r(x123)) & tsum(ch(x122), ch(x121), r(x124)) & cont(x124, ch(x123)))) ) )) .
( all x132 all x131 all x133 all x135 all x134 ( ((eqdim(x132, x131) & eqdim(x131, x133) & sc(x132, x131) & sc(x131, x133) & - (c(x132, x133)) & tsum(x132, x131, x135) & tsum(x131, x133, x134) & (x135=ch(x135)) & (x134=ch(x134)))) -> ((x131=ch(x131))) )) .
( all x71 all x72 ( (cont(r(x71), r(x72))) -> (cont(ch(x71), ch(x72))) )) .
( all x81 all x82 ( (((ch(x81)=ch(x82)) & - (zex(x81)))) -> (c(r(x81), r(x82))) )) .
( all x91 all x92 ( ((maxdim(r(x91)) & maxdim(r(x92)) & (r(x91)=ch(x91)) & (r(x92)=ch(x92)))) -> ((intersection(ch(x91), ch(x92))=ch(intersection(ch(x91), ch(x92))))) )) .
( all x101 all x102 ( ((icont(r(x101), r(x102)) & - (closed(difference(r(x102), r(x101)))))) -> (- ((difference(r(x102), r(x101))=ch(difference(r(x102), r(x101)))))) )) .
( all x111 all x112 ( ((icont(r(x111), r(x112)) & maxdim(r(x111)) & maxdim(r(x112)))) -> (cont(r(x111), ch(difference(r(x112), r(x111))))) )) .
( all x122 all x124 ( ((- (zex(x122)) | - (zex(x124)))) -> (( exists x121 exists x123 (tsum(r(x122), r(x124), r(x121)) & tsum(ch(x122), ch(x124), r(x123)) & cont(x123, ch(x121)))) ) )) .
( all x132 all x135 all x131 all x134 all x133 ( ((eqdim(x132, x135) & eqdim(x135, x131) & sc(x132, x135) & sc(x135, x131) & - (c(x132, x131)) & tsum(x132, x135, x134) & tsum(x135, x131, x133) & (x134=ch(x134)) & (x133=ch(x133)))) -> ((x135=ch(x135))) )) .
end_of_list.

0 comments on commit bb58c2c

Please sign in to comment.
You can’t perform that action at this time.