The cow chases the mouse. The cow is cold. The cow is rough. The cow is round. The cow is young. The cow sees the mouse. The cow visits the mouse. The mouse is nice. The mouse is rough. The mouse is young. The mouse sees the cow. The mouse visits the cow. If someone chases the cow then the cow sees the mouse. If someone visits the mouse then the mouse sees the cow.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If someone chases the cow then the cow sees the mouse.
((("someone" "chases" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If someone visits the mouse then the mouse sees the cow.
((("someone" "visits" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The cow does not visit the mouse.
False
1
inv-proof
[(triple7)]
("cow" "visits" "mouse" "-")
triple7
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The cow chases the mouse.[(triple1)] The cow is cold.[(triple2)] The cow is rough.[(triple3)] The cow is round.[(triple4)] The cow is young.[(triple5)] The cow sees the mouse.[(triple6)] The cow visits the mouse.[(triple7)] The mouse is nice.[(triple8)] The mouse is rough.[(triple9)] The mouse is young.[(triple10)] The mouse sees the cow.[(triple11 OR ((triple7) -> rule2))] The mouse visits the cow.[(triple12)]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple6
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse is young.
("mouse" "is" "young" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple11
((triple7) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple12