The cow chases the tiger. The mouse chases the cow. The rabbit is cold. The tiger is cold. If something needs the cow and the cow eats the rabbit then it is rough. If something eats the rabbit then the rabbit eats the mouse.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something needs the cow and the cow eats the rabbit then it is rough.
((("something" "needs" "cow" "+") ("cow" "eats" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If something eats the rabbit then the rabbit eats the mouse.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
The rabbit is cold.
True
1
proof
[(triple3)]
("rabbit" "is" "cold" "+")
triple3
The rabbit is not cold.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "cold" "-")
triple3
The rabbit does not eat the mouse.
Unknown
inv-rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "mouse" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow chases the tiger.[(triple1)] The mouse chases the cow.[(triple2)] The rabbit is cold.[(triple3)] The tiger is cold.[(triple4)]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple2
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple4