The bear eats the cat. The bear is kind. The bear likes the mouse. The bear visits the cat. The bear visits the mouse. The cat is big. The cat is kind. The cat likes the bear. The cat does not like the mouse. The cat visits the bear. The cat visits the mouse. The mouse does not eat the bear. The mouse is nice. The mouse is not red. The mouse visits the bear. If someone visits the mouse then the mouse eats the cat. If someone likes the bear then they eat the bear. If someone is rough and not red then they do not like the mouse.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat does not like the mouse.
("cat" "likes" "mouse" "-")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is not red.
("mouse" "is" "red" "-")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If someone visits the mouse then the mouse eats the cat.
((("someone" "visits" "mouse" "+")) -> ("mouse" "eats" "cat" "+"))
If someone likes the bear then they eat the bear.
((("someone" "likes" "bear" "+")) -> ("someone" "eats" "bear" "+"))
If someone is rough and not red then they do not like the mouse.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "likes" "mouse" "-"))
The mouse is nice.
True
1
proof
[(triple13)]
("mouse" "is" "nice" "+")
triple13
The cat likes the mouse.
False
1
inv-proof
[(triple9)]
("cat" "likes" "mouse" "+")
triple9
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "bear" "-")
The bear eats the mouse.
Unknown
random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "+")
@0: The bear eats the cat.[(triple1)] The bear is kind.[(triple2)] The bear likes the mouse.[(triple3)] The bear visits the cat.[(triple4)] The bear visits the mouse.[(triple5)] The cat does not like the mouse.[(triple9)] The cat is big.[(triple6)] The cat is kind.[(triple7)] The cat likes the bear.[(triple8)] The cat visits the bear.[(triple10)] The cat visits the mouse.[(triple11)] The mouse does not eat the bear.[(triple12)] The mouse is nice.[(triple13)] The mouse is not red.[(triple14)] The mouse visits the bear.[(triple15)] @1: The cat eats the bear.[(((triple8) -> rule2))] The mouse eats the cat.[(((triple11) -> rule1) OR ((triple5) -> rule1))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple3
The bear visits the cat.
("bear" "visits" "cat" "+")
triple4
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple5
The cat does not like the mouse.
("cat" "likes" "mouse" "-")
triple9
The cat is big.
("cat" "is" "big" "+")
triple6
The cat is kind.
("cat" "is" "kind" "+")
triple7
The cat likes the bear.
("cat" "likes" "bear" "+")
triple8
The cat visits the bear.
("cat" "visits" "bear" "+")
triple10
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple11
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
triple12
The mouse is nice.
("mouse" "is" "nice" "+")
triple13
The mouse is not red.
("mouse" "is" "red" "-")
triple14
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple15
The cat eats the bear.
("cat" "eats" "bear" "+")
((triple8) -> (rule2 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((triple11) -> (rule1 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
((triple5) -> (rule1 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1