The cow likes the lion. The lion likes the cow. The lion sees the cow. If something needs the cow then it is kind. If the cow likes the lion then the lion sees the cow. If something needs the cow then it sees the cow. If something sees the lion then it needs the lion. If the lion likes the cow then the cow is round. If something likes the cow then it needs the cow. If something sees the lion and it sees the cow then the cow sees the lion. If the cow sees the lion and the cow needs the lion then the lion sees the cow.
The cow likes the lion.
("cow" "likes" "lion" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If something needs the cow then it is kind.
((("something" "needs" "cow" "+")) -> ("something" "is" "kind" "+"))
If the cow likes the lion then the lion sees the cow.
((("cow" "likes" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If something needs the cow then it sees the cow.
((("something" "needs" "cow" "+")) -> ("something" "sees" "cow" "+"))
If something sees the lion then it needs the lion.
((("something" "sees" "lion" "+")) -> ("something" "needs" "lion" "+"))
If the lion likes the cow then the cow is round.
((("lion" "likes" "cow" "+")) -> ("cow" "is" "round" "+"))
If something likes the cow then it needs the cow.
((("something" "likes" "cow" "+")) -> ("something" "needs" "cow" "+"))
If something sees the lion and it sees the cow then the cow sees the lion.
((("something" "sees" "lion" "+") ("something" "sees" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If the cow sees the lion and the cow needs the lion then the lion sees the cow.
((("cow" "sees" "lion" "+") ("cow" "needs" "lion" "+")) -> ("lion" "sees" "cow" "+"))
The cow likes the lion.
True
1
proof
[(triple1)]
("cow" "likes" "lion" "+")
triple1
The lion does not like the cow.
False
1
inv-proof
[(triple2)]
("lion" "likes" "cow" "-")
triple2
The cow does not see the cow.
Unknown
inv-rconc
[@2: The cow sees the cow.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("cow" "sees" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cow likes the lion.[(triple1)] The lion likes the cow.[(triple2)] The lion sees the cow.[(triple3 OR ((triple1) -> rule2) OR ((((triple2) -> rule6)) -> rule3))] @1: The cow is round.[(((triple2) -> rule5))] The lion needs the cow.[(((triple2) -> rule6))] @2: The lion is kind.[(((((triple2) -> rule6)) -> rule1))]
The cow likes the lion.
("cow" "likes" "lion" "+")
triple1
The lion likes the cow.
("lion" "likes" "cow" "+")
triple2
The lion sees the cow.
("lion" "sees" "cow" "+")
triple3
((triple1) -> (rule2 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((triple2) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
((triple2) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2