The lion chases the rabbit. The lion is cold. The lion likes the rabbit. The lion needs the rabbit. The rabbit chases the lion. The rabbit is blue. The rabbit is not cold. The rabbit is nice. The rabbit is red. The rabbit is rough. The rabbit likes the lion. The rabbit needs the lion. If something is red and it likes the lion then the lion is blue. If something chases the rabbit then the rabbit needs the lion. If something needs the lion then the lion likes the rabbit. If something likes the rabbit and it is blue then it is rough. If something needs the rabbit and the rabbit is red then it does not need the lion. If the rabbit does not need the lion then the rabbit is cold.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If something is red and it likes the lion then the lion is blue.
((("something" "is" "red" "+") ("something" "likes" "lion" "+")) -> ("lion" "is" "blue" "+"))
If something chases the rabbit then the rabbit needs the lion.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "needs" "lion" "+"))
If something needs the lion then the lion likes the rabbit.
((("something" "needs" "lion" "+")) -> ("lion" "likes" "rabbit" "+"))
If something likes the rabbit and it is blue then it is rough.
((("something" "likes" "rabbit" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something needs the rabbit and the rabbit is red then it does not need the lion.
((("something" "needs" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("something" "needs" "lion" "-"))
If the rabbit does not need the lion then the rabbit is cold.
((("rabbit" "needs" "lion" "~")) -> ("rabbit" "is" "cold" "+"))
The rabbit is blue.
True
1
proof
[(triple6)]
("rabbit" "is" "blue" "+")
triple6
The lion does not like the rabbit.
False
1
inv-proof
[(triple3 OR ((triple12) -> rule3) OR ((((triple1) -> rule2)) -> rule3))]
("lion" "likes" "rabbit" "-")
triple3
((triple12) -> (rule3 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The lion is blue.
True
3
proof
[(((triple9 triple11) -> rule1))]
("lion" "is" "blue" "+")
((triple9 triple11) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is not blue.
False
3
inv-proof
[(((triple9 triple11) -> rule1))]
("lion" "is" "blue" "-")
((triple9 triple11) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is rough.
True
5
proof
[(((triple3 ((triple9 triple11) -> rule1)) -> rule4) OR ((((triple12) -> rule3) ((triple9 triple11) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule3) ((triple9 triple11) -> rule1)) -> rule4))]
("lion" "is" "rough" "+")
((triple3 ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple12) -> (rule3 % int3)) ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int4
The lion is not rough.
False
5
inv-proof
[(((triple3 ((triple9 triple11) -> rule1)) -> rule4) OR ((((triple12) -> rule3) ((triple9 triple11) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule3) ((triple9 triple11) -> rule1)) -> rule4))]
("lion" "is" "rough" "-")
((triple3 ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple12) -> (rule3 % int3)) ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int4
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 is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
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 chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is cold.[(triple2)] The lion likes the rabbit.[(triple3 OR ((triple12) -> rule3) OR ((((triple1) -> rule2)) -> rule3))] The lion needs the rabbit.[(triple4)] The rabbit chases the lion.[(triple5)] The rabbit is blue.[(triple6)] The rabbit is nice.[(triple8)] The rabbit is not cold.[(triple7)] The rabbit is red.[(triple9)] The rabbit is rough.[(triple10)] The rabbit likes the lion.[(triple11)] The rabbit needs the lion.[(triple12 OR ((triple1) -> rule2))] @1: The lion does not need the lion.[(((triple4 triple9) -> rule5))] The lion is blue.[(((triple9 triple11) -> rule1))] @2: The lion is rough.[(((triple3 ((triple9 triple11) -> rule1)) -> rule4) OR ((((triple12) -> rule3) ((triple9 triple11) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule3) ((triple9 triple11) -> rule1)) -> rule4))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple3
((triple12) -> (rule3 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple4
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple5
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple11
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple12
((triple1) -> (rule2 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The lion does not need the lion.
("lion" "needs" "lion" "-")
((triple4 triple9) -> (rule5 % int1))
The lion does not need the lion.
("lion" "needs" "lion" "-")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple9 triple11) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple3 ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple12) -> (rule3 % int3)) ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule3 % int3)) ((triple9 triple11) -> (rule1 % int2))) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int4