The mouse is red. The mouse needs the rabbit. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit is cold. The rabbit needs the mouse. The rabbit sees the mouse. If something sees the mouse and it visits the mouse then it is big. If something visits the rabbit and the rabbit is kind then it is round. If something visits the rabbit then the rabbit is kind.
The mouse is red.
("mouse" "is" "red" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something sees the mouse and it visits the mouse then it is big.
((("something" "sees" "mouse" "+") ("something" "visits" "mouse" "+")) -> ("something" "is" "big" "+"))
If something visits the rabbit and the rabbit is kind then it is round.
((("something" "visits" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something visits the rabbit then the rabbit is kind.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
The mouse sees the rabbit.
True
1
proof
[(triple3)]
("mouse" "sees" "rabbit" "+")
triple3
The rabbit is not cold.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "cold" "-")
triple5
The rabbit is kind.
True
2
proof
[(((triple4) -> rule3))]
("rabbit" "is" "kind" "+")
((triple4) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple4) -> rule3))]
("rabbit" "is" "kind" "-")
((triple4) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The mouse is round.
True
4
proof
[(((triple4 ((triple4) -> rule3)) -> rule2))]
("mouse" "is" "round" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The mouse is not round.
False
4
inv-proof
[(((triple4 ((triple4) -> rule3)) -> rule2))]
("mouse" "is" "round" "-")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "big" "+")
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "round" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is red.[(triple1)] The mouse needs the rabbit.[(triple2)] The mouse sees the rabbit.[(triple3)] The mouse visits the rabbit.[(triple4)] The rabbit is cold.[(triple5)] The rabbit needs the mouse.[(triple6)] The rabbit sees the mouse.[(triple7)] @1: The rabbit is kind.[(((triple4) -> rule3))] @2: The mouse is round.[(((triple4 ((triple4) -> rule3)) -> rule2))]
The mouse is red.
("mouse" "is" "red" "+")
triple1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple3
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple6
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple4) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple4 ((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2