Skip to content
Permalink
Browse files

updated Prover9 translations for codib

  • Loading branch information...
thahmann committed Nov 9, 2018
1 parent af91141 commit 271affe20dd0905e634d81f728a794db3067763c
@@ -1,16 +1,7 @@
formulas(sos).
% cl-imports multidim_space_codi/codi.clif
% cl-imports multidim_space_dim/definitions/covers.clif
% cl-imports multidim_space_codib/codi_bcont_minimal.clif
% cl-imports multidim_space_codi/definitions/min_max_in_dim.clif
% cl-imports multidim_space_codi/definitions/po.clif
% cl-imports multidim_space_codi/definitions/inc.clif
% cl-imports multidim_space_codi/definitions/sc.clif
% cl-imports multidim_space_codi/theorems/po_theorems.clif
% cl-imports multidim_space_codi/theorems/inc_theorems.clif
% cl-imports multidim_space_codi/theorems/sc_theorems.clif
( all x12 all x11 ( (bcont(x12, x11)) -> ((cont(x12, x11) & inc(x12, x11))) )) .
( all x22 all x21 all x24 all x23 ( ((sc(x22, x21) & min(x22) & p(x22, x24) & cont(x21, x24) & cont(x23, x22) & cont(x23, x21))) -> (bcont(x23, x22)) )) .
( all x32 all x31 all x33 all x34 ( ((sc(x32, x31) & p(x32, x34) & p(x31, x34) & cont(x33, x32) & cont(x33, x31) & covers(x34, x33))) -> (- (bcont(x33, x34))) )) .
( all x42 all x41 all x43 ( ((bcont(x42, x41) & p(x41, x43) & ( all x45 all x44 ( ((p(x45, x43) & - (po(x45, x41)) & p(x44, x42))) -> (- (cont(x44, x45))) )) )) -> (bcont(x42, x43)) )) .
( all x52 all x51 all x53 ( ((bcont(x52, x51) & cont(x53, x52))) -> (bcont(x53, x51)) )) .
end_of_list.
@@ -2,11 +2,11 @@ formulas(sos).
% cl-imports multidim_space_codi/codi.clif
% cl-imports multidim_space_dim/definitions/covers.clif
% cl-imports multidim_space_codi/definitions/po.clif
% cl-imports multidim_space_codi/definitions/inc.clif
% cl-imports multidim_space_codi/definitions/sc.clif
( all x12 all x11 ( (bcont(x12, x11)) -> ((cont(x12, x11) & inc(x12, x11))) )) .
( all x22 all x21 all x24 all x23 ( ((sc(x22, x21) & min(x22) & p(x22, x24) & cont(x21, x24) & cont(x23, x22) & cont(x23, x21))) -> (bcont(x23, x22)) )) .
( all x32 all x31 all x33 all x34 ( ((sc(x32, x31) & p(x32, x34) & p(x31, x34) & cont(x33, x32) & cont(x33, x31) & covers(x34, x33))) -> (- (bcont(x33, x34))) )) .
( all x42 all x41 all x43 ( ((bcont(x42, x41) & p(x41, x43) & ( all x45 all x44 ( ((p(x45, x43) & - (po(x45, x41)) & p(x44, x42))) -> (- (cont(x44, x45))) )) )) -> (bcont(x42, x43)) )) .
( all x52 all x51 all x53 ( ((bcont(x52, x51) & cont(x53, x52))) -> (bcont(x53, x51)) )) .
% cl-imports multidim_space_codi/definitions/min_max_in_dim.clif
( all x11 all x12 ( (bcont(x11, x12)) -> ((cont(x11, x12) & - (eqdim(x11, x12)))) )) .
( all x22 all x24 all x23 all x21 ( ((sc(x22, x24) & min(x22) & p(x22, x23) & cont(x24, x23) & cont(x21, x22) & cont(x21, x24))) -> (bcont(x21, x22)) )) .
( all x32 all x34 all x31 all x33 ( ((sc(x32, x34) & p(x32, x33) & p(x34, x33) & cont(x31, x32) & cont(x31, x34) & covers(x33, x31))) -> (- (bcont(x31, x33))) )) .
( all x42 all x45 all x41 ( ((bcont(x42, x45) & p(x45, x41) & ( all x44 all x43 ( ((p(x44, x41) & - (po(x44, x45)) & p(x43, x42))) -> (- (cont(x43, x44))) )) )) -> (bcont(x42, x41)) )) .
( all x52 all x53 all x51 ( ((bcont(x52, x53) & cont(x51, x52))) -> (bcont(x51, x53)) )) .
end_of_list.
@@ -3,11 +3,11 @@ formulas(sos).
% cl-imports multidim_space_codib/codib.clif
% cl-imports multidim_space_codib/definitions/icont.clif
% cl-imports multidim_space_codib/definitions/tcont.clif
( all x12 ( ((s(x12) & - (zex(x12)))) -> (( exists x11 (p(x11, x12) & min(x11))) ) )) .
( all x22 all x21 ( ((s(x22) & s(x21) & bcont(x22, x21))) -> ((cont(x22, x21) & inc(x22, x21))) )) .
( all x32 all x31 all x34 all x33 ( ((s(x32) & s(x31) & s(x34) & s(x33) & sc(x32, x31) & min(x32) & p(x32, x34) & cont(x31, x34) & cont(x33, x32) & cont(x33, x31))) -> (bcont(x33, x32)) )) .
( all x42 all x41 all x43 all x44 ( ((s(x42) & s(x41) & s(x44) & s(x43) & sc(x42, x41) & p(x42, x44) & p(x41, x44) & cont(x43, x42) & cont(x43, x41) & covers(x44, x43))) -> (- (bcont(x43, x44))) )) .
( all x52 all x51 all x53 ( ((s(x52) & s(x51) & s(x53) & bcont(x52, x51) & p(x51, x53) & ( all x55 all x54 ( ((s(x55) & s(x54) & p(x55, x53) & - (po(x55, x51)) & p(x54, x52))) -> (- (cont(x54, x55))) )) )) -> (bcont(x52, x53)) )) .
( all x62 all x61 all x63 ( ((s(x62) & s(x61) & s(x63) & bcont(x62, x61) & cont(x63, x62))) -> (bcont(x63, x61)) )) .
( all x72 all x71 ( ((s(x72) & s(x71) & bcont(x72, x71))) <-> ((s(x72) & s(x71) & - (zex(x72)) & ( all x73 ( ((p(x73, x72) & min(x73))) -> (bcont(x73, x71)) )) )) )) .
( all x11 ( ((s(x11) & - (zex(x11)))) -> (( exists x12 (p(x12, x11) & min(x12))) ) )) .
( all x21 all x22 ( ((s(x21) & s(x22) & bcont(x21, x22))) -> ((cont(x21, x22) & inc(x21, x22))) )) .
( all x32 all x34 all x33 all x31 ( ((s(x32) & s(x34) & s(x33) & s(x31) & sc(x32, x34) & min(x32) & p(x32, x33) & cont(x34, x33) & cont(x31, x32) & cont(x31, x34))) -> (bcont(x31, x32)) )) .
( all x42 all x44 all x41 all x43 ( ((s(x42) & s(x44) & s(x43) & s(x41) & sc(x42, x44) & p(x42, x43) & p(x44, x43) & cont(x41, x42) & cont(x41, x44) & covers(x43, x41))) -> (- (bcont(x41, x43))) )) .
( all x52 all x55 all x51 ( ((s(x52) & s(x55) & s(x51) & bcont(x52, x55) & p(x55, x51) & ( all x54 all x53 ( ((s(x54) & s(x53) & p(x54, x51) & - (po(x54, x55)) & p(x53, x52))) -> (- (cont(x53, x54))) )) )) -> (bcont(x52, x51)) )) .
( all x62 all x63 all x61 ( ((s(x62) & s(x63) & s(x61) & bcont(x62, x63) & cont(x61, x62))) -> (bcont(x61, x63)) )) .
( all x72 all x73 ( ((s(x72) & s(x73) & bcont(x72, x73))) <-> ((s(x72) & s(x73) & - (zex(x72)) & ( all x71 ( ((p(x71, x72) & min(x71))) -> (bcont(x71, x73)) )) )) )) .
end_of_list.
@@ -1,11 +1,11 @@
formulas(sos).
% cl-imports multidim_space_codib/codib_down.clif
( all x12 all x11 all x13 all x14 ( ((tsum(x12, x11, x13) & tsum(x12, x11, x14))) -> ((s(x12) & s(x11) & s(x13) & (x14=x13))) )) .
( all x22 all x21 all x23 ( (tsum(x22, x21, x23)) -> (tsum(x21, x22, x23)) )) .
( all x32 all x31 ( (lt(x32, x31)) -> (tsum(x32, x31, x31)) )) .
( all x42 all x41 all x43 all x44 ( ((tsum(x42, x41, x43) & leq(x42, x41) & cont(x44, x41))) -> (cont(x44, x43)) )) .
( all x52 all x51 all x53 all x54 ( ((tsum(x52, x51, x53) & cont(x54, x53) & - (cont(x54, x52)))) -> (cont(difference(x54, x52), x51)) )) .
( all x62 all x61 all x63 ( ((s(x63) & eqdim(x62, x61) & ( all x64 ( (po(x64, x63)) <-> ((po(x64, x62) | po(x64, x61))) )) )) -> (tsum(x62, x61, x63)) )) .
( all x72 all x71 ( ((eqdim(x72, x71) & ( all x73 ( ((cont(x73, x72) & cont(x73, x71) & min(x73))) -> (( exists x74 exists x75 (p(x74, x72) & p(x75, x71) & bcont(x73, x74) & bcont(x73, x75))) ) )) )) -> (( exists x73 tsum(x72, x71, x73)) ) )) .
( all x12 all x14 all x11 all x13 ( ((tsum(x12, x14, x11) & tsum(x12, x14, x13))) -> ((s(x12) & s(x14) & s(x11) & (x13=x11))) )) .
( all x22 all x23 all x21 ( (tsum(x22, x23, x21)) -> (tsum(x23, x22, x21)) )) .
( all x31 all x32 ( (lt(x31, x32)) -> (tsum(x31, x32, x32)) )) .
( all x42 all x44 all x41 all x43 ( ((tsum(x42, x44, x41) & leq(x42, x44) & cont(x43, x44))) -> (cont(x43, x41)) )) .
( all x52 all x54 all x51 all x53 ( ((tsum(x52, x54, x51) & cont(x53, x51) & - (cont(x53, x52)))) -> (cont(difference(x53, x52), x54)) )) .
( all x62 all x64 all x61 ( ((s(x61) & eqdim(x62, x64) & ( all x63 ( (po(x63, x61)) <-> ((po(x63, x62) | po(x63, x64))) )) )) -> (tsum(x62, x64, x61)) )) .
( all x72 all x75 ( ((eqdim(x72, x75) & ( all x71 ( ((cont(x71, x72) & cont(x71, x75) & min(x71))) -> (( exists x74 exists x73 (p(x74, x72) & p(x73, x75) & bcont(x71, x74) & bcont(x71, x73))) ) )) )) -> (( exists x71 tsum(x72, x75, x71)) ) )) .
( all x81 ( ((s(x81) & - (zex(x81)))) -> (cont(x81, cuni)) )) .
end_of_list.
@@ -1,4 +1,4 @@
formulas(sos).
% cl-imports multidim_space_codib/codi_bcont.clif
( all x12 ( (closed(x12)) <-> (( all x11 - (bcont(x11, x12))) ) )) .
( all x11 ( (closed(x11)) <-> (( all x12 - (bcont(x12, x11))) ) )) .
end_of_list.
@@ -1,4 +1,4 @@
formulas(sos).
% cl-imports multidim_space_codib/codi_bcont.clif
( all x12 all x11 ( (icont(x12, x11)) <-> ((cont(x12, x11) & ( all x13 ( (cont(x13, x12)) -> (- (bcont(x13, x11))) )) )) )) .
( all x12 all x13 ( (icont(x12, x13)) <-> ((cont(x12, x13) & ( all x11 ( (cont(x11, x12)) -> (- (bcont(x11, x13))) )) )) )) .
end_of_list.
@@ -1,4 +1,4 @@
formulas(sos).
% cl-imports multidim_space_codib/codi_bcont.clif
( all x12 all x11 ( (tcont(x12, x11)) <-> ((cont(x12, x11) & ( exists x13 (cont(x13, x12) & bcont(x13, x11))) )) )) .
( all x12 all x13 ( (tcont(x12, x13)) <-> ((cont(x12, x13) & ( exists x11 (cont(x11, x12) & bcont(x11, x13))) )) )) .
end_of_list.

0 comments on commit 271affe

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