The cow chases the lion. The cow is big. The cow likes the lion. The cow visits the lion. The lion is green. The lion is red. The lion visits the cow. If something likes the lion then it visits the lion. If something visits the cow then it likes the lion.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is big.
("cow" "is" "big" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If something likes the lion then it visits the lion.
((("something" "likes" "lion" "+")) -> ("something" "visits" "lion" "+"))
If something visits the cow then it likes the lion.
((("something" "visits" "cow" "+")) -> ("something" "likes" "lion" "+"))
The lion is green.
True
1
proof
[(triple5)]
("lion" "is" "green" "+")
triple5
The lion does not visit the cow.
False
1
inv-proof
[(triple7)]
("lion" "visits" "cow" "-")
triple7
The lion likes the lion.
True
2
proof
[(((triple7) -> rule2))]
("lion" "likes" "lion" "+")
((triple7) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple7) -> rule2))]
("lion" "likes" "lion" "-")
((triple7) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the lion.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("lion" "visits" "lion" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion does not visit the lion.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("lion" "visits" "lion" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The lion likes the cow.
Unknown
random
[@0: The lion likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cow" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The cow chases the lion.[(triple1)] The cow is big.[(triple2)] The cow likes the lion.[(triple3)] The cow visits the lion.[(triple4 OR ((triple3) -> rule1))] The lion is green.[(triple5)] The lion is red.[(triple6)] The lion visits the cow.[(triple7)] @1: The lion likes the lion.[(((triple7) -> rule2))] @2: The lion visits the lion.[(((((triple7) -> rule2)) -> rule1))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
triple4
((triple3) -> (rule1 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple5
The lion is red.
("lion" "is" "red" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple7) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2