Skip to content
Permalink
Browse files

Prover9 translations of multidim_space_ped updated

  • Loading branch information...
thahmann committed Nov 9, 2018
1 parent 1ac96cf commit e9725646ebc50c9a70e3cbff1d450b3e7f6baa7f
@@ -7,9 +7,9 @@ formulas(sos).
( all x61 ( (pob(x61)) -> (- (f(x61))) )) .
( all x71 ( (m(x71)) -> (- (f(x71))) )) .
( all x81 ( (napo(x81)) -> (pob(x81)) )) .
( all x92 all x91 ( (hosts(x92, x91)) -> ((ped(x92) & f(x91))) )) .
( all x102 ( (f(x102)) <-> (( exists x101 hosts(x101, x102)) ) )) .
( all x112 all x111 ( (hosts(x112, x111)) -> (- (hosts(x111, x112))) )) .
( all x91 all x92 ( (hosts(x91, x92)) -> ((ped(x91) & f(x92))) )) .
( all x101 ( (f(x101)) <-> (( exists x102 hosts(x102, x101)) ) )) .
( all x111 all x112 ( (hosts(x111, x112)) -> (- (hosts(x112, x111))) )) .
( all x121 ( (f(x121)) <-> ((rpf(x121) | dpf(x121))) )) .
( all x131 (- (rpf(x131)) | - (dpf(x131)))) .
end_of_list.
@@ -1,7 +1,7 @@
formulas(sos).
% cl-imports multidim_space_ped/ped.clif
( all x12 all x11 ( (dk1(x12, x11)) -> (m(x12)) )) .
( all x22 all x21 ( (dk1(x22, x21)) -> ((pob(x21) | rpf(x21))) )) .
( all x32 all x31 all x33 ( ((dk1(x32, x31) & dk1(x33, x31))) -> ((x32=x33)) )) .
( all x41 ( ((pob(x41) | rpf(x41))) -> (( exists x42 dk1(x42, x41)) ) )) .
( all x11 all x12 ( (dk1(x11, x12)) -> (m(x11)) )) .
( all x21 all x22 ( (dk1(x21, x22)) -> ((pob(x22) | rpf(x22))) )) .
( all x32 all x33 all x31 ( ((dk1(x32, x33) & dk1(x31, x33))) -> ((x32=x31)) )) .
( all x42 ( ((pob(x42) | rpf(x42))) -> (( exists x41 dk1(x41, x42)) ) )) .
end_of_list.

0 comments on commit e972564

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