The lion eats the rabbit. The lion is big. The lion is kind. The rabbit chases the lion. The rabbit eats the lion. The rabbit is green. The rabbit visits the lion. If someone eats the rabbit then they chase the lion. If someone visits the rabbit and the rabbit chases the lion then the lion eats the rabbit. If someone eats the lion and the lion eats the rabbit then they visit the rabbit. If someone is blue and they visit the rabbit then they visit the lion. If someone eats the rabbit then the rabbit eats the lion. If someone chases the rabbit and the rabbit is green then the rabbit is kind. If someone is green then they eat the lion. If someone chases the lion and they visit the rabbit then they chase the rabbit.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone eats the rabbit then they chase the lion.
((("someone" "eats" "rabbit" "+")) -> ("someone" "chases" "lion" "+"))
If someone visits the rabbit and the rabbit chases the lion then the lion eats the rabbit.
((("someone" "visits" "rabbit" "+") ("rabbit" "chases" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone eats the lion and the lion eats the rabbit then they visit the rabbit.
((("someone" "eats" "lion" "+") ("lion" "eats" "rabbit" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is blue and they visit the rabbit then they visit the lion.
((("someone" "is" "blue" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "lion" "+"))
If someone eats the rabbit then the rabbit eats the lion.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "eats" "lion" "+"))
If someone chases the rabbit and the rabbit is green then the rabbit is kind.
((("someone" "chases" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "is" "kind" "+"))
If someone is green then they eat the lion.
((("someone" "is" "green" "+")) -> ("someone" "eats" "lion" "+"))
If someone chases the lion and they visit the rabbit then they chase the rabbit.
((("someone" "chases" "lion" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
The lion is kind.
True
1
proof
[(triple3)]
("lion" "is" "kind" "+")
triple3
The rabbit does not visit the lion.
False
1
inv-proof
[(triple7)]
("rabbit" "visits" "lion" "-")
triple7
The rabbit visits the rabbit.
True
3
proof
[(((triple5 triple1) -> rule3) OR ((((triple1) -> rule5) triple1) -> rule3) OR ((((triple6) -> rule7) triple1) -> rule3))]
("rabbit" "visits" "rabbit" "+")
((triple5 triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int2
((((triple6) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int2
The rabbit does not visit the rabbit.
False
3
inv-proof
[(((triple5 triple1) -> rule3) OR ((((triple1) -> rule5) triple1) -> rule3) OR ((((triple6) -> rule7) triple1) -> rule3))]
("rabbit" "visits" "rabbit" "-")
((triple5 triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int2
((((triple6) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int2
The rabbit chases the rabbit.
True
5
proof
[(((triple4 ((triple5 triple1) -> rule3)) -> rule8) OR ((triple4 ((((triple1) -> rule5) triple1) -> rule3)) -> rule8) OR ((triple4 ((((triple6) -> rule7) triple1) -> rule3)) -> rule8))]
("rabbit" "chases" "rabbit" "+")
((triple4 ((triple5 triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
((triple4 ((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int3
((triple4 ((((triple6) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int3
The rabbit does not chase the rabbit.
False
5
inv-proof
[(((triple4 ((triple5 triple1) -> rule3)) -> rule8) OR ((triple4 ((((triple1) -> rule5) triple1) -> rule3)) -> rule8) OR ((triple4 ((((triple6) -> rule7) triple1) -> rule3)) -> rule8))]
("rabbit" "chases" "rabbit" "-")
((triple4 ((triple5 triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
((triple4 ((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int3
((triple4 ((((triple6) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int3
The rabbit is kind.
True
7
proof
[(((((triple4 ((triple5 triple1) -> rule3)) -> rule8) triple6) -> rule6) OR ((((triple4 ((((triple1) -> rule5) triple1) -> rule3)) -> rule8) triple6) -> rule6) OR ((((triple4 ((((triple6) -> rule7) triple1) -> rule3)) -> rule8) triple6) -> rule6))]
("rabbit" "is" "kind" "+")
((((triple4 ((triple5 triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
((((triple4 ((((triple1) -> (rule5 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int4
((((triple4 ((((triple6) -> (rule7 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int4
The rabbit is not kind.
False
7
inv-proof
[(((((triple4 ((triple5 triple1) -> rule3)) -> rule8) triple6) -> rule6) OR ((((triple4 ((((triple1) -> rule5) triple1) -> rule3)) -> rule8) triple6) -> rule6) OR ((((triple4 ((((triple6) -> rule7) triple1) -> rule3)) -> rule8) triple6) -> rule6))]
("rabbit" "is" "kind" "-")
((((triple4 ((triple5 triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
((((triple4 ((((triple1) -> (rule5 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int4
((((triple4 ((((triple6) -> (rule7 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int4
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion eats the lion.
Unknown
rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "eats" "lion" "+")
The lion does not chase the rabbit.
Unknown
inv-rconc
[@3: The lion chases the rabbit.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule7 <- FAIL)]]
("lion" "chases" "rabbit" "-")
The lion visits the rabbit.
Unknown
rconc
[@2: The lion visits the rabbit.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("lion" "visits" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The lion eats the rabbit.[(triple1)] The lion is big.[(triple2)] The lion is kind.[(triple3)] The rabbit chases the lion.[(triple4)] The rabbit eats the lion.[(triple5 OR ((triple1) -> rule5) OR ((triple6) -> rule7))] The rabbit is green.[(triple6)] The rabbit visits the lion.[(triple7)] @1: The lion chases the lion.[(((triple1) -> rule1))] The rabbit visits the rabbit.[(((triple5 triple1) -> rule3) OR ((((triple1) -> rule5) triple1) -> rule3) OR ((((triple6) -> rule7) triple1) -> rule3))] @2: The rabbit chases the rabbit.[(((triple4 ((triple5 triple1) -> rule3)) -> rule8) OR ((triple4 ((((triple1) -> rule5) triple1) -> rule3)) -> rule8) OR ((triple4 ((((triple6) -> rule7) triple1) -> rule3)) -> rule8))] @3: The rabbit is kind.[(((((triple4 ((triple5 triple1) -> rule3)) -> rule8) triple6) -> rule6) OR ((((triple4 ((((triple1) -> rule5) triple1) -> rule3)) -> rule8) triple6) -> rule6) OR ((((triple4 ((((triple6) -> rule7) triple1) -> rule3)) -> rule8) triple6) -> rule6))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple4
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple5
((triple1) -> (rule5 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
((triple6) -> (rule7 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple7
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple1) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple5 triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
((((triple1) -> (rule5 % int2)) triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int2
((((triple6) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple4 ((triple5 triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
((triple4 ((((triple1) -> (rule5 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int3
((triple4 ((((triple6) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int3
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple4 ((triple5 triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
((((triple4 ((((triple1) -> (rule5 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int4
((((triple4 ((((triple6) -> (rule7 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int4