This file contains formulas in FORT syntax corresponding to the modeling
tasks solved by Carpa(+).

+ Zantema "Finding Small Counter Examples for Abstract Rewriting Properties"
- (long version) of IWC 2013 paper
- available from https://www.win.tue.nl/~hzantema/carpa.html

Example 2

"[0]SN & [1]SN & ~SN & (forall s, t, u ([0]s -> t & [1]t -> u =>
exists v ([0]s ->+ u | [1]s ->+ u)))"

"[0]SN & [1]SN & ~SN & (forall s, t ~([0]s -> t & [1]s -> t)) &
(forall s, t, u ([0]s -> t & [1]t -> u =>
exists v ([0]s ->+ u | [1]s ->+ u)))"

Example 4

"[0]CR & [1]CR & ~CR & (forall s, t, u ([0]s -> t & [1]s -> u =>
exists v ([1]t -> v & [0]v join u)))"

Example 5

"[0]CR & [1]CR & ~CR & (forall s, t, u ([0]s -> t & [1]s -> u =>
exists v (([1]t -> v | [0]t ->* v) & [0]u ->* v)))"

"[0]CR & [1]CR & ~CR & (forall s, t, u ([0]s -> t & [1]s -> u =>
exists v (([1]t -> v | [0]t -> v) & [0]u ->* v)))"

Example 6

"[0](CR & SN) & [1](CR & SN) & ~CR & (forall s, t, u ([0]s -> t & [1]s -> u
=> exists v ([1]t -> v & [0]v join u)))"

Example 7

"[0,1](CR & SN) & [0,2](CR & SN) & [1,2](CR & SN) & ~CR"

Example 8

"[0](CR & SN) & [1](CR & SN) & ~CR & (forall s, t, u ([0]s -> t &
[1]s -> u => exists v (([1]t -> v | [0]t ->* v) & [0]u ->* v)))"

"[0](CR & SN) & [1](CR & SN) & ~CR & (forall s, t, u ([0]s -> t &
[1]s -> u => exists v (([1]t -> v | [0]t -> v) & [0]u ->* v)))"


+ Zantema "Automatically Finding Particular Term Rewriting Systems"
- available from https://www.win.tue.nl/~hzantema/carpa.html

Example 10

"WCR & ~CR & forall t Fin(<-,t) & ~exists u (u +<- u)"

Example 11

"WCR & ~CR"

Example 12

"[0](WCR & ~CR & forall t Fin(<-,t) & ~exists u (u +<- u)) &
forall s, t ([0]s -> t => ([1]s -> t | [2]s -> t)) &"
forall s, t (([1]s -> t | [2]s -> t) => [0]s -> t) & [1]WCR & [2]WCR"

Example 13

"forall s, t, u (([0]s -> t & [1]t -> u) => exists v
([0]s -> v & [1]v ->* u)) &
~forall s, t, u (([0]s -> t & [1]t -> u) => exists v
([0]s -> v & [1]v -> u))"