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