The cat is big. The cat is not kind. The cat is red. The cat is round. The cat likes the lion. The cat needs the lion. The cat does not visit the lion. The lion is big. The lion is not kind. The lion is red. The lion is round. The lion is young. The lion does not like the cat. The lion needs the cat. The lion visits the cat. If something visits the lion then it does not like the lion. If something is red and it likes the lion then it does not visit the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
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 big.
("lion" "is" "big" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion does not like the cat.
("lion" "likes" "cat" "-")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If something visits the lion then it does not like the lion.
((("something" "visits" "lion" "+")) -> ("something" "likes" "lion" "-"))
If something is red and it likes the lion then it does not visit the cat.
((("something" "is" "red" "+") ("something" "likes" "lion" "+")) -> ("something" "visits" "cat" "-"))
The cat is round.
True
1
proof
[(triple4)]
("cat" "is" "round" "+")
triple4
The lion does not visit the cat.
False
1
inv-proof
[(triple15)]
("lion" "visits" "cat" "-")
triple15
The cat does not visit the cat.
True
3
proof
[(((triple3 triple5) -> rule2))]
("cat" "visits" "cat" "-")
((triple3 triple5) -> (rule2 % int1))
The cat does not visit the cat.
("cat" "visits" "cat" "-")
int1
The cat visits the cat.
False
3
inv-proof
[(((triple3 triple5) -> rule2))]
("cat" "visits" "cat" "+")
((triple3 triple5) -> (rule2 % int1))
The cat does not visit the cat.
("cat" "visits" "cat" "-")
int1
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 likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
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 visit the lion.[(triple7)] The cat is big.[(triple1)] The cat is not kind.[(triple2)] The cat is red.[(triple3)] The cat is round.[(triple4)] The cat likes the lion.[(triple5)] The cat needs the lion.[(triple6)] The lion does not like the cat.[(triple13)] The lion is big.[(triple8)] The lion is not kind.[(triple9)] The lion is red.[(triple10)] The lion is round.[(triple11)] The lion is young.[(triple12)] The lion needs the cat.[(triple14)] The lion visits the cat.[(triple15)] @1: The cat does not visit the cat.[(((triple3 triple5) -> rule2))]
The cat does not visit the lion.
("cat" "visits" "lion" "-")
triple7
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is not kind.
("cat" "is" "kind" "-")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat likes the lion.
("cat" "likes" "lion" "+")
triple5
The cat needs the lion.
("cat" "needs" "lion" "+")
triple6
The lion does not like the cat.
("lion" "likes" "cat" "-")
triple13
The lion is big.
("lion" "is" "big" "+")
triple8
The lion is not kind.
("lion" "is" "kind" "-")
triple9
The lion is red.
("lion" "is" "red" "+")
triple10
The lion is round.
("lion" "is" "round" "+")
triple11
The lion is young.
("lion" "is" "young" "+")
triple12
The lion needs the cat.
("lion" "needs" "cat" "+")
triple14
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
The cat does not visit the cat.
("cat" "visits" "cat" "-")
((triple3 triple5) -> (rule2 % int1))
The cat does not visit the cat.
("cat" "visits" "cat" "-")
int1