The cat chases the lion. The cat is big. The cat is blue. The cat likes the lion. The cat needs the lion. The lion chases the cat. The lion is big. The lion is blue. The lion is kind. The lion is rough. The lion likes the cat. The lion needs the cat. If the cat likes the lion then the cat chases the lion. If something chases the lion and it likes the cat then the cat chases the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
If the cat likes the lion then the cat chases the lion.
((("cat" "likes" "lion" "+")) -> ("cat" "chases" "lion" "+"))
If something chases the lion and it likes the cat then the cat chases the lion.
((("something" "chases" "lion" "+") ("something" "likes" "cat" "+")) -> ("cat" "chases" "lion" "+"))
The lion is blue.
True
1
proof
[(triple8)]
("lion" "is" "blue" "+")
triple8
The cat is not blue.
False
1
inv-proof
[(triple3)]
("cat" "is" "blue" "-")
triple3
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "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 chases the lion.[(triple1 OR ((triple4) -> rule1))] The cat is big.[(triple2)] The cat is blue.[(triple3)] The cat likes the lion.[(triple4)] The cat needs the lion.[(triple5)] The lion chases the cat.[(triple6)] The lion is big.[(triple7)] The lion is blue.[(triple8)] The lion is kind.[(triple9)] The lion is rough.[(triple10)] The lion likes the cat.[(triple11)] The lion needs the cat.[(triple12)]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
((triple4) -> (rule1 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat likes the lion.
("cat" "likes" "lion" "+")
triple4
The cat needs the lion.
("cat" "needs" "lion" "+")
triple5
The lion chases the cat.
("lion" "chases" "cat" "+")
triple6
The lion is big.
("lion" "is" "big" "+")
triple7
The lion is blue.
("lion" "is" "blue" "+")
triple8
The lion is kind.
("lion" "is" "kind" "+")
triple9
The lion is rough.
("lion" "is" "rough" "+")
triple10
The lion likes the cat.
("lion" "likes" "cat" "+")
triple11
The lion needs the cat.
("lion" "needs" "cat" "+")
triple12