The mouse is kind. The rabbit needs the mouse. If something sees the rabbit then the rabbit is cold. If something chases the rabbit and it sees the mouse then it chases the mouse. If something needs the mouse then the mouse sees the rabbit.
The mouse is kind.
("mouse" "is" "kind" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If something sees the rabbit then the rabbit is cold.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If something chases the rabbit and it sees the mouse then it chases the mouse.
((("something" "chases" "rabbit" "+") ("something" "sees" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something needs the mouse then the mouse sees the rabbit.
((("something" "needs" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
The rabbit needs the mouse.
True
1
proof
[(triple2)]
("rabbit" "needs" "mouse" "+")
triple2
The mouse is not kind.
False
1
inv-proof
[(triple1)]
("mouse" "is" "kind" "-")
triple1
The mouse sees the rabbit.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "sees" "rabbit" "+")
((triple2) -> (rule3 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse does not see the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "sees" "rabbit" "-")
((triple2) -> (rule3 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit is cold.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("rabbit" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("rabbit" "is" "cold" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@1: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse does not need the rabbit.
Unknown
inv-random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The mouse is kind.[(triple1)] The rabbit needs the mouse.[(triple2)] @1: The mouse sees the rabbit.[(((triple2) -> rule3))] @2: The rabbit is cold.[(((((triple2) -> rule3)) -> rule1))]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((triple2) -> (rule3 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2