The cow chases the mouse. The lion is rough. The mouse needs the lion. The rabbit sees the cow. If the cow chases the mouse then the cow chases the rabbit.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If the cow chases the mouse then the cow chases the rabbit.
((("cow" "chases" "mouse" "+")) -> ("cow" "chases" "rabbit" "+"))
The lion is rough.
True
1
proof
[(triple2)]
("lion" "is" "rough" "+")
triple2
The mouse does not need the lion.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "lion" "-")
triple3
The cow chases the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("cow" "chases" "rabbit" "+")
((triple1) -> (rule1 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow does not chase the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "chases" "rabbit" "-")
((triple1) -> (rule1 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The rabbit needs the mouse.
Unknown
random
[@0: The rabbit needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "mouse" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cow chases the mouse.[(triple1)] The lion is rough.[(triple2)] The mouse needs the lion.[(triple3)] The rabbit sees the cow.[(triple4)] @1: The cow chases the rabbit.[(((triple1) -> rule1))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple3
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple4
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((triple1) -> (rule1 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1