The cat is nice. The cat is red. The cat likes the lion. The cat sees the tiger. The cat visits the lion. The cat visits the tiger. The lion is red. The lion sees the tiger. The tiger likes the cat. The tiger sees the cat. The tiger sees the lion. The tiger visits the cat. If something sees the lion and it sees the tiger then the tiger sees the cat. If something sees the cat then the cat likes the lion. If the tiger likes the cat then the cat is red.
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The lion is red.
("lion" "is" "red" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something sees the lion and it sees the tiger then the tiger sees the cat.
((("something" "sees" "lion" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
If something sees the cat then the cat likes the lion.
((("something" "sees" "cat" "+")) -> ("cat" "likes" "lion" "+"))
If the tiger likes the cat then the cat is red.
((("tiger" "likes" "cat" "+")) -> ("cat" "is" "red" "+"))
The lion is red.
True
1
proof
[(triple7)]
("lion" "is" "red" "+")
triple7
The tiger does not see the lion.
False
1
inv-proof
[(triple11)]
("tiger" "sees" "lion" "-")
triple11
The lion does not visit the cat.
Unknown
inv-random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "-")
The lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
@0: The cat is nice.[(triple1)] The cat is red.[(triple2 OR ((triple9) -> rule3))] The cat likes the lion.[(triple3 OR ((triple10) -> rule2))] The cat sees the tiger.[(triple4)] The cat visits the lion.[(triple5)] The cat visits the tiger.[(triple6)] The lion is red.[(triple7)] The lion sees the tiger.[(triple8)] The tiger likes the cat.[(triple9)] The tiger sees the cat.[(triple10)] The tiger sees the lion.[(triple11)] The tiger visits the cat.[(triple12)]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
((triple9) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
((triple10) -> (rule2 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The cat visits the lion.
("cat" "visits" "lion" "+")
triple5
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple6
The lion is red.
("lion" "is" "red" "+")
triple7
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple8
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple9
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple10
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple11
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple12