The cat eats the lion. The cat is red. The cat likes the lion. The cat visits the lion. The lion eats the cat. The lion is not big. The lion is blue. The lion is green. The lion is nice. The lion is red. The lion does not like the cat. The lion visits the cat. If someone likes the lion then they like the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion does not like the cat.
("lion" "likes" "cat" "-")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone likes the lion then they like the cat.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "cat" "+"))
The cat eats the lion.
True
1
proof
[(triple1)]
("cat" "eats" "lion" "+")
triple1
The lion likes the cat.
False
1
inv-proof
[(triple11)]
("lion" "likes" "cat" "+")
triple11
The cat likes the cat.
True
2
proof
[(((triple3) -> rule1))]
("cat" "likes" "cat" "+")
((triple3) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat does not like the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "likes" "cat" "-")
((triple3) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat eats the lion.[(triple1)] The cat is red.[(triple2)] The cat likes the lion.[(triple3)] The cat visits the lion.[(triple4)] The lion does not like the cat.[(triple11)] The lion eats the cat.[(triple5)] The lion is blue.[(triple7)] The lion is green.[(triple8)] The lion is nice.[(triple9)] The lion is not big.[(triple6)] The lion is red.[(triple10)] The lion visits the cat.[(triple12)] @1: The cat likes the cat.[(((triple3) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The cat visits the lion.
("cat" "visits" "lion" "+")
triple4
The lion does not like the cat.
("lion" "likes" "cat" "-")
triple11
The lion eats the cat.
("lion" "eats" "cat" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple7
The lion is green.
("lion" "is" "green" "+")
triple8
The lion is nice.
("lion" "is" "nice" "+")
triple9
The lion is not big.
("lion" "is" "big" "-")
triple6
The lion is red.
("lion" "is" "red" "+")
triple10
The lion visits the cat.
("lion" "visits" "cat" "+")
triple12
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple3) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1