The lion sees the rabbit. The mouse eats the rabbit. The rabbit sees the mouse. If someone chases the rabbit then they eat the rabbit. If the mouse sees the lion and the lion chases the mouse then the lion chases the rabbit. If someone is big then they see the lion. If someone sees the lion then the lion sees the mouse. If someone sees the mouse then the mouse eats the rabbit. If someone sees the rabbit then the rabbit sees the lion. If the rabbit is rough then the rabbit chases the lion. If someone is nice and they see the mouse then the mouse sees the lion.
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone chases the rabbit then they eat the rabbit.
((("someone" "chases" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If the mouse sees the lion and the lion chases the mouse then the lion chases the rabbit.
((("mouse" "sees" "lion" "+") ("lion" "chases" "mouse" "+")) -> ("lion" "chases" "rabbit" "+"))
If someone is big then they see the lion.
((("someone" "is" "big" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion then the lion sees the mouse.
((("someone" "sees" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If someone sees the mouse then the mouse eats the rabbit.
((("someone" "sees" "mouse" "+")) -> ("mouse" "eats" "rabbit" "+"))
If someone sees the rabbit then the rabbit sees the lion.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
If the rabbit is rough then the rabbit chases the lion.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "chases" "lion" "+"))
If someone is nice and they see the mouse then the mouse sees the lion.
((("someone" "is" "nice" "+") ("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
The lion sees the rabbit.
True
1
proof
[(triple1)]
("lion" "sees" "rabbit" "+")
triple1
The rabbit does not see the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "mouse" "-")
triple3
The rabbit sees the lion.
True
2
proof
[(((triple1) -> rule6))]
("rabbit" "sees" "lion" "+")
((triple1) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit does not see the lion.
False
2
inv-proof
[(((triple1) -> rule6))]
("rabbit" "sees" "lion" "-")
((triple1) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The lion sees the mouse.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("lion" "sees" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The lion does not see the mouse.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("lion" "sees" "mouse" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2
The rabbit does not chase the lion.
Unknown
inv-rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "chases" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "lion" "+")
The mouse does not see the lion.
Unknown
inv-rconc
[@1: The mouse sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "lion" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion sees the rabbit.[(triple1)] The mouse eats the rabbit.[(triple2 OR ((triple3) -> rule5) OR ((((((triple1) -> rule6)) -> rule4)) -> rule5))] The rabbit sees the mouse.[(triple3)] @1: The rabbit sees the lion.[(((triple1) -> rule6))] @2: The lion sees the mouse.[(((((triple1) -> rule6)) -> rule4))]
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple2
((triple3) -> (rule5 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int3
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple3
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
((triple1) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int2