The lion chases the rabbit. The lion eats the rabbit. The lion is young. The lion sees the rabbit. The rabbit chases the lion. The rabbit eats the lion. The rabbit is young. If someone eats the lion then they are green. If someone sees the lion then they see the rabbit. If someone chases the rabbit then the rabbit chases the lion. If someone chases the rabbit then the rabbit sees the lion. If someone sees the rabbit then they are nice. If someone sees the rabbit then the rabbit chases the lion.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If someone eats the lion then they are green.
((("someone" "eats" "lion" "+")) -> ("someone" "is" "green" "+"))
If someone sees the lion then they see the rabbit.
((("someone" "sees" "lion" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone chases the rabbit then the rabbit chases the lion.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
If someone chases the rabbit then the rabbit sees the lion.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If someone sees the rabbit then they are nice.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the rabbit then the rabbit chases the lion.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
The lion chases the rabbit.
True
1
proof
[(triple1)]
("lion" "chases" "rabbit" "+")
triple1
The lion does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("lion" "chases" "rabbit" "-")
triple1
The rabbit sees the lion.
True
2
proof
[(((triple1) -> rule4))]
("rabbit" "sees" "lion" "+")
((triple1) -> (rule4 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit does not see the lion.
False
2
inv-proof
[(((triple1) -> rule4))]
("rabbit" "sees" "lion" "-")
((triple1) -> (rule4 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit sees the rabbit.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("rabbit" "sees" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit does not see the rabbit.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("rabbit" "sees" "rabbit" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit is nice.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "is" "nice" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The rabbit is not nice.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "is" "nice" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "green" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
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 rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The lion chases the rabbit.[(triple1)] The lion eats the rabbit.[(triple2)] The lion is young.[(triple3)] The lion sees the rabbit.[(triple4)] The rabbit chases the lion.[(triple5 OR ((triple1) -> rule3) OR ((triple4) -> rule6) OR ((((((triple1) -> rule4)) -> rule2)) -> rule6))] The rabbit eats the lion.[(triple6)] The rabbit is young.[(triple7)] @1: The lion is nice.[(((triple4) -> rule5))] The rabbit is green.[(((triple6) -> rule1))] The rabbit sees the lion.[(((triple1) -> rule4))] @2: The rabbit sees the rabbit.[(((((triple1) -> rule4)) -> rule2))] @3: The rabbit is nice.[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple4
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple5
((triple1) -> (rule3 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
((triple4) -> (rule6 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
((triple4) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple6) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple1) -> (rule4 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3