The cow chases the lion. The cow is big. The cow is blue. The lion chases the cow. The lion is kind. The lion sees the cow. The lion visits the cow. If someone visits the cow and they chase the lion then the cow sees the lion. If someone visits the cow then they chase the cow. If someone is big and they see the lion then they see the cow.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone visits the cow and they chase the lion then the cow sees the lion.
((("someone" "visits" "cow" "+") ("someone" "chases" "lion" "+")) -> ("cow" "sees" "lion" "+"))
If someone visits the cow then they chase the cow.
((("someone" "visits" "cow" "+")) -> ("someone" "chases" "cow" "+"))
If someone is big and they see the lion then they see the cow.
((("someone" "is" "big" "+") ("someone" "sees" "lion" "+")) -> ("someone" "sees" "cow" "+"))
The cow is blue.
True
1
proof
[(triple3)]
("cow" "is" "blue" "+")
triple3
The lion does not chase the cow.
False
1
inv-proof
[(triple4 OR ((triple7) -> rule2))]
("lion" "chases" "cow" "-")
triple4
((triple7) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "cow" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The cow chases the lion.[(triple1)] The cow is big.[(triple2)] The cow is blue.[(triple3)] The lion chases the cow.[(triple4 OR ((triple7) -> rule2))] The lion is kind.[(triple5)] The lion sees the cow.[(triple6)] The lion visits the cow.[(triple7)]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The lion chases the cow.
("lion" "chases" "cow" "+")
triple4
((triple7) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion sees the cow.
("lion" "sees" "cow" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7