The cat does not eat the lion. The cat is blue. The cat is not cold. The cat is red. The cat is rough. The cat is round. The cat needs the lion. The cat visits the lion. The lion eats the cat. The lion is blue. The lion is cold. The lion is rough. The lion is round. The lion needs the cat. The lion visits the cat. If someone eats the lion and the lion is round then they do not eat the cat. Rough people are red. If the cat is blue and the cat visits the lion then the lion is red.
The cat does not eat the lion.
("cat" "eats" "lion" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is not cold.
("cat" "is" "cold" "-")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone eats the lion and the lion is round then they do not eat the cat.
((("someone" "eats" "lion" "+") ("lion" "is" "round" "+")) -> ("someone" "eats" "cat" "-"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If the cat is blue and the cat visits the lion then the lion is red.
((("cat" "is" "blue" "+") ("cat" "visits" "lion" "+")) -> ("lion" "is" "red" "+"))
The lion is round.
True
1
proof
[(triple13)]
("lion" "is" "round" "+")
triple13
The cat eats the lion.
False
1
inv-proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The cat does not eat the lion.[(triple1)] The cat is blue.[(triple2)] The cat is not cold.[(triple3)] The cat is red.[(triple4 OR ((triple5) -> rule2))] The cat is rough.[(triple5)] The cat is round.[(triple6)] The cat needs the lion.[(triple7)] The cat visits the lion.[(triple8)] The lion eats the cat.[(triple9)] The lion is blue.[(triple10)] The lion is cold.[(triple11)] The lion is rough.[(triple12)] The lion is round.[(triple13)] The lion needs the cat.[(triple14)] The lion visits the cat.[(triple15)] @1: The lion is red.[(((triple12) -> rule2) OR ((triple2 triple8) -> rule3))]
The cat does not eat the lion.
("cat" "eats" "lion" "-")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is not cold.
("cat" "is" "cold" "-")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
((triple5) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat needs the lion.
("cat" "needs" "lion" "+")
triple7
The cat visits the lion.
("cat" "visits" "lion" "+")
triple8
The lion eats the cat.
("lion" "eats" "cat" "+")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion is cold.
("lion" "is" "cold" "+")
triple11
The lion is rough.
("lion" "is" "rough" "+")
triple12
The lion is round.
("lion" "is" "round" "+")
triple13
The lion needs the cat.
("lion" "needs" "cat" "+")
triple14
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
The lion is red.
("lion" "is" "red" "+")
((triple12) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple2 triple8) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1