The cat is blue. The cat is cold. The cat is kind. The cat is not rough. The cat is young. The cat likes the lion. The cat needs the lion. The cat does not visit the lion. The lion is cold. The lion is kind. The lion is rough. The lion is not young. The lion likes the cat. The lion needs the cat. The lion visits the cat. If the lion is kind and the lion does not need the cat then the cat is not cold. If someone needs the cat then the cat likes the lion. If someone likes the lion and they do not visit the lion then they visit the cat. If someone visits the cat then they are cold. If someone visits the cat and they visit the lion then the cat needs the lion. If the cat visits the lion then the lion is not cold.
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is not rough.
("cat" "is" "rough" "-")
The cat is young.
("cat" "is" "young" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat does not visit the lion.
("cat" "visits" "lion" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If the lion is kind and the lion does not need the cat then the cat is not cold.
((("lion" "is" "kind" "+") ("lion" "needs" "cat" "~")) -> ("cat" "is" "cold" "-"))
If someone needs the cat then the cat likes the lion.
((("someone" "needs" "cat" "+")) -> ("cat" "likes" "lion" "+"))
If someone likes the lion and they do not visit the lion then they visit the cat.
((("someone" "likes" "lion" "+") ("someone" "visits" "lion" "~")) -> ("someone" "visits" "cat" "+"))
If someone visits the cat then they are cold.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone visits the cat and they visit the lion then the cat needs the lion.
((("someone" "visits" "cat" "+") ("someone" "visits" "lion" "+")) -> ("cat" "needs" "lion" "+"))
If the cat visits the lion then the lion is not cold.
((("cat" "visits" "lion" "+")) -> ("lion" "is" "cold" "-"))
The lion likes the cat.
True
1
proof
[(triple13)]
("lion" "likes" "cat" "+")
triple13
The lion is not cold.
False
1
inv-proof
[(triple9 OR ((triple15) -> rule4))]
("lion" "is" "cold" "-")
triple9
((triple15) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The cat visits the cat.
True
3
proof
[(((triple6 triple8) -> rule3) OR ((((triple14) -> rule2) triple8) -> rule3))]
("cat" "visits" "cat" "+")
((triple6 triple8) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((((triple14) -> (rule2 % int2)) triple8) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((triple6 triple8) -> rule3) OR ((((triple14) -> rule2) triple8) -> rule3))]
("cat" "visits" "cat" "-")
((triple6 triple8) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((((triple14) -> (rule2 % int2)) triple8) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2
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 cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The cat does not visit the lion.[(triple8)] The cat is blue.[(triple1)] The cat is cold.[(triple2 OR ((((triple6 triple8) -> rule3)) -> rule4) OR ((((((triple14) -> rule2) triple8) -> rule3)) -> rule4))] The cat is kind.[(triple3)] The cat is not rough.[(triple4)] The cat is young.[(triple5)] The cat likes the lion.[(triple6 OR ((triple14) -> rule2))] The cat needs the lion.[(triple7)] The lion is cold.[(triple9 OR ((triple15) -> rule4))] The lion is kind.[(triple10)] The lion is not young.[(triple12)] The lion is rough.[(triple11)] The lion likes the cat.[(triple13)] The lion needs the cat.[(triple14)] The lion visits the cat.[(triple15)] @1: The cat visits the cat.[(((triple6 triple8) -> rule3) OR ((((triple14) -> rule2) triple8) -> rule3))]
The cat does not visit the lion.
("cat" "visits" "lion" "-")
triple8
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
((((triple6 triple8) -> (rule3 % int2))) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((((triple14) -> (rule2 % int3)) triple8) -> (rule3 % int2))) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat likes the lion.
("cat" "likes" "lion" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is not rough.
("cat" "is" "rough" "-")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the lion.
("cat" "likes" "lion" "+")
triple6
((triple14) -> (rule2 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple9
((triple15) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple10
The lion is not young.
("lion" "is" "young" "-")
triple12
The lion is rough.
("lion" "is" "rough" "+")
triple11
The lion likes the cat.
("lion" "likes" "cat" "+")
triple13
The lion needs the cat.
("lion" "needs" "cat" "+")
triple14
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple6 triple8) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((((triple14) -> (rule2 % int2)) triple8) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
int2