The cat is blue. The cat is young. The cat needs the rabbit. The lion chases the rabbit. The lion is blue. The lion is green. The lion likes the cat. The lion likes the rabbit. The lion needs the cat. The rabbit chases the lion. The rabbit is blue. The rabbit is green. The rabbit is kind. The rabbit is young. The rabbit needs the cat. If something likes the rabbit and the rabbit likes the cat then the rabbit needs the cat. If the rabbit needs the lion and the lion is blue then the lion needs the rabbit. If something likes the cat and it is blue then the cat chases the lion. If something is young then it needs the lion. If something chases the lion and the lion is green then it is green. If something is green then it chases the rabbit.
The cat is blue.
("cat" "is" "blue" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If something likes the rabbit and the rabbit likes the cat then the rabbit needs the cat.
((("something" "likes" "rabbit" "+") ("rabbit" "likes" "cat" "+")) -> ("rabbit" "needs" "cat" "+"))
If the rabbit needs the lion and the lion is blue then the lion needs the rabbit.
((("rabbit" "needs" "lion" "+") ("lion" "is" "blue" "+")) -> ("lion" "needs" "rabbit" "+"))
If something likes the cat and it is blue then the cat chases the lion.
((("something" "likes" "cat" "+") ("something" "is" "blue" "+")) -> ("cat" "chases" "lion" "+"))
If something is young then it needs the lion.
((("something" "is" "young" "+")) -> ("something" "needs" "lion" "+"))
If something chases the lion and the lion is green then it is green.
((("something" "chases" "lion" "+") ("lion" "is" "green" "+")) -> ("something" "is" "green" "+"))
If something is green then it chases the rabbit.
((("something" "is" "green" "+")) -> ("something" "chases" "rabbit" "+"))
The cat is young.
True
1
proof
[(triple2)]
("cat" "is" "young" "+")
triple2
The lion does not like the cat.
False
1
inv-proof
[(triple7)]
("lion" "likes" "cat" "-")
triple7
The rabbit chases the rabbit.
True
2
proof
[(((triple12) -> rule6) OR ((((triple10 triple6) -> rule5)) -> rule6))]
("rabbit" "chases" "rabbit" "+")
((triple12) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((((triple10 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple12) -> rule6) OR ((((triple10 triple6) -> rule5)) -> rule6))]
("rabbit" "chases" "rabbit" "-")
((triple12) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((((triple10 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The lion needs the rabbit.
True
4
proof
[(((((triple14) -> rule4) triple5) -> rule2))]
("lion" "needs" "rabbit" "+")
((((triple14) -> (rule4 % int2)) triple5) -> (rule2 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The lion does not need the rabbit.
False
4
inv-proof
[(((((triple14) -> rule4) triple5) -> rule2))]
("lion" "needs" "rabbit" "-")
((((triple14) -> (rule4 % int2)) triple5) -> (rule2 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The cat chases the rabbit.
True
6
proof
[(((((((triple7 triple5) -> rule3) triple6) -> rule5)) -> rule6))]
("cat" "chases" "rabbit" "+")
((((((triple7 triple5) -> (rule3 % int3)) triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The cat does not chase the rabbit.
False
6
inv-proof
[(((((((triple7 triple5) -> rule3) triple6) -> rule5)) -> rule6))]
("cat" "chases" "rabbit" "-")
((((((triple7 triple5) -> (rule3 % int3)) triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "needs" "lion" "-")
The cat likes the lion.
Unknown
random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cat likes the rabbit.
Unknown
random
[@0: The cat likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "rabbit" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The lion chases the cat.
Unknown
random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "+")
@0: The cat is blue.[(triple1)] The cat is young.[(triple2)] The cat needs the rabbit.[(triple3)] The lion chases the rabbit.[(triple4 OR ((triple6) -> rule6))] The lion is blue.[(triple5)] The lion is green.[(triple6)] The lion likes the cat.[(triple7)] The lion likes the rabbit.[(triple8)] The lion needs the cat.[(triple9)] The rabbit chases the lion.[(triple10)] The rabbit is blue.[(triple11)] The rabbit is green.[(triple12 OR ((triple10 triple6) -> rule5))] The rabbit is kind.[(triple13)] The rabbit is young.[(triple14)] The rabbit needs the cat.[(triple15)] @1: The cat chases the lion.[(((triple7 triple5) -> rule3))] The cat needs the lion.[(((triple2) -> rule4))] The rabbit chases the rabbit.[(((triple12) -> rule6) OR ((((triple10 triple6) -> rule5)) -> rule6))] The rabbit needs the lion.[(((triple14) -> rule4))] @2: The cat is green.[(((((triple7 triple5) -> rule3) triple6) -> rule5))] The lion needs the rabbit.[(((((triple14) -> rule4) triple5) -> rule2))] @3: The cat chases the rabbit.[(((((((triple7 triple5) -> rule3) triple6) -> rule5)) -> rule6))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple4
((triple6) -> (rule6 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is green.
("lion" "is" "green" "+")
triple6
The lion likes the cat.
("lion" "likes" "cat" "+")
triple7
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple8
The lion needs the cat.
("lion" "needs" "cat" "+")
triple9
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple10
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple11
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
((triple10 triple6) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple15
The cat chases the lion.
("cat" "chases" "lion" "+")
((triple7 triple5) -> (rule3 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple2) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple12) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((((triple10 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((triple14) -> (rule4 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((((triple7 triple5) -> (rule3 % int2)) triple6) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((((triple14) -> (rule4 % int2)) triple5) -> (rule2 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((((((triple7 triple5) -> (rule3 % int3)) triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3