The cow chases the lion. The lion chases the cow. The lion visits the cow. If someone chases the cow and they visit the cow then the cow visits the lion. If someone likes the cow then they visit the lion. If someone visits the lion then they chase the lion.
The cow chases the lion.
("cow" "chases" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone chases the cow and they visit the cow then the cow visits the lion.
((("someone" "chases" "cow" "+") ("someone" "visits" "cow" "+")) -> ("cow" "visits" "lion" "+"))
If someone likes the cow then they visit the lion.
((("someone" "likes" "cow" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the lion then they chase the lion.
((("someone" "visits" "lion" "+")) -> ("someone" "chases" "lion" "+"))
The lion chases the cow.
True
1
proof
[(triple2)]
("lion" "chases" "cow" "+")
triple2
The cow does not chase the lion.
False
1
inv-proof
[(triple1 OR ((((triple2 triple3) -> rule1)) -> rule3))]
("cow" "chases" "lion" "-")
triple1
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The cow chases the lion.[(triple1 OR ((((triple2 triple3) -> rule1)) -> rule3))] The lion chases the cow.[(triple2)] The lion visits the cow.[(triple3)] @1: The cow visits the lion.[(((triple2 triple3) -> rule1))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple2
The lion visits the cow.
("lion" "visits" "cow" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
((triple2 triple3) -> (rule1 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1