The cat chases the lion. The cat is not round. The cat likes the lion. The lion does not chase the cat. The lion is green. The lion is red. The lion is round. The lion is young. The lion likes the cat. The lion does not need the cat. If someone needs the lion then they do not chase the lion. If the cat likes the lion then the cat is not young. If someone likes the lion and the lion likes the cat then they do not chase the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion does not chase the cat.
("lion" "chases" "cat" "-")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion does not need the cat.
("lion" "needs" "cat" "-")
If someone needs the lion then they do not chase the lion.
((("someone" "needs" "lion" "+")) -> ("someone" "chases" "lion" "-"))
If the cat likes the lion then the cat is not young.
((("cat" "likes" "lion" "+")) -> ("cat" "is" "young" "-"))
If someone likes the lion and the lion likes the cat then they do not chase the cat.
((("someone" "likes" "lion" "+") ("lion" "likes" "cat" "+")) -> ("someone" "chases" "cat" "-"))
The lion is round.
True
1
proof
[(triple7)]
("lion" "is" "round" "+")
triple7
The lion is not green.
False
1
inv-proof
[(triple5)]
("lion" "is" "green" "-")
triple5
The cat is not young.
True
2
proof
[(((triple3) -> rule2))]
("cat" "is" "young" "-")
((triple3) -> (rule2 % int1))
The cat is not young.
("cat" "is" "young" "-")
int1
The cat chases the cat.
False
3
inv-proof
[(((triple3 triple9) -> rule3))]
("cat" "chases" "cat" "+")
((triple3 triple9) -> (rule3 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The cat does not need the lion.
Unknown
inv-random
[@0: The cat needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "lion" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat chases the lion.[(triple1)] The cat is not round.[(triple2)] The cat likes the lion.[(triple3)] The lion does not chase the cat.[(triple4)] The lion does not need the cat.[(triple10)] The lion is green.[(triple5)] The lion is red.[(triple6)] The lion is round.[(triple7)] The lion is young.[(triple8)] The lion likes the cat.[(triple9)] @1: The cat does not chase the cat.[(((triple3 triple9) -> rule3))] The cat is not young.[(((triple3) -> rule2))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is not round.
("cat" "is" "round" "-")
triple2
The cat likes the lion.
("cat" "likes" "lion" "+")
triple3
The lion does not chase the cat.
("lion" "chases" "cat" "-")
triple4
The lion does not need the cat.
("lion" "needs" "cat" "-")
triple10
The lion is green.
("lion" "is" "green" "+")
triple5
The lion is red.
("lion" "is" "red" "+")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
triple8
The lion likes the cat.
("lion" "likes" "cat" "+")
triple9
The cat does not chase the cat.
("cat" "chases" "cat" "-")
((triple3 triple9) -> (rule3 % int1))
The cat does not chase the cat.
("cat" "chases" "cat" "-")
int1
The cat is not young.
("cat" "is" "young" "-")
((triple3) -> (rule2 % int1))
The cat is not young.
("cat" "is" "young" "-")
int1