The cow is kind. The cow likes the lion. The cow likes the tiger. The cow sees the lion. The cow visits the lion. The lion is not young. The tiger is green. The tiger is red. The tiger sees the cow. The tiger sees the lion. If someone likes the tiger then they see the cow. If someone is kind and not round then they visit the cow. If the lion is not kind then the lion does not visit the tiger.
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is not young.
("lion" "is" "young" "-")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone likes the tiger then they see the cow.
((("someone" "likes" "tiger" "+")) -> ("someone" "sees" "cow" "+"))
If someone is kind and not round then they visit the cow.
((("someone" "is" "kind" "+") ("someone" "is" "round" "~")) -> ("someone" "visits" "cow" "+"))
If the lion is not kind then the lion does not visit the tiger.
((("lion" "is" "kind" "~")) -> ("lion" "visits" "tiger" "-"))
The tiger sees the lion.
True
1
proof
[(triple10)]
("tiger" "sees" "lion" "+")
triple10
The tiger is not red.
False
1
inv-proof
[(triple8)]
("tiger" "is" "red" "-")
triple8
The cow sees the cow.
True
2
proof
[(((triple3) -> rule1))]
("cow" "sees" "cow" "+")
((triple3) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("cow" "sees" "cow" "-")
((triple3) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The lion does not visit the cow.
Unknown
inv-rconc
[@1: The lion visits the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "cow" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "cow" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The cow is kind.[(triple1)] The cow likes the lion.[(triple2)] The cow likes the tiger.[(triple3)] The cow sees the lion.[(triple4)] The cow visits the lion.[(triple5)] The lion is not young.[(triple6)] The tiger is green.[(triple7)] The tiger is red.[(triple8)] The tiger sees the cow.[(triple9)] The tiger sees the lion.[(triple10)] @1: The cow sees the cow.[(((triple3) -> rule1))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow likes the lion.
("cow" "likes" "lion" "+")
triple2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The cow visits the lion.
("cow" "visits" "lion" "+")
triple5
The lion is not young.
("lion" "is" "young" "-")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple9
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple10
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple3) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1