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