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