The mouse is cold. The mouse likes the rabbit. The rabbit is not blue. The rabbit is cold. The rabbit is not green. The rabbit is red. The rabbit is round. The rabbit likes the mouse. The rabbit sees the mouse. The rabbit visits the mouse. If someone visits the rabbit and the rabbit likes the mouse then they see the rabbit. If someone likes the mouse then the mouse sees the rabbit. If someone is red then they visit the rabbit.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone visits the rabbit and the rabbit likes the mouse then they see the rabbit.
((("someone" "visits" "rabbit" "+") ("rabbit" "likes" "mouse" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone likes the mouse then the mouse sees the rabbit.
((("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If someone is red then they visit the rabbit.
((("someone" "is" "red" "+")) -> ("someone" "visits" "rabbit" "+"))
The rabbit is cold.
True
1
proof
[(triple4)]
("rabbit" "is" "cold" "+")
triple4
The rabbit does not like the mouse.
False
1
inv-proof
[(triple8)]
("rabbit" "likes" "mouse" "-")
triple8
The mouse sees the rabbit.
True
2
proof
[(((triple8) -> rule2))]
("mouse" "sees" "rabbit" "+")
((triple8) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple6) -> rule3))]
("rabbit" "visits" "rabbit" "-")
((triple6) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit sees the rabbit.
True
4
proof
[(((((triple6) -> rule3) triple8) -> rule1))]
("rabbit" "sees" "rabbit" "+")
((((triple6) -> (rule3 % int2)) triple8) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit does not see the rabbit.
False
4
inv-proof
[(((((triple6) -> rule3) triple8) -> rule1))]
("rabbit" "sees" "rabbit" "-")
((((triple6) -> (rule3 % int2)) triple8) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The mouse does not visit the rabbit.
Unknown
inv-rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "rabbit" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
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 is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The mouse is cold.[(triple1)] The mouse likes the rabbit.[(triple2)] The rabbit is cold.[(triple4)] The rabbit is not blue.[(triple3)] The rabbit is not green.[(triple5)] The rabbit is red.[(triple6)] The rabbit is round.[(triple7)] The rabbit likes the mouse.[(triple8)] The rabbit sees the mouse.[(triple9)] The rabbit visits the mouse.[(triple10)] @1: The mouse sees the rabbit.[(((triple8) -> rule2))] The rabbit visits the rabbit.[(((triple6) -> rule3))] @2: The rabbit sees the rabbit.[(((((triple6) -> rule3) triple8) -> rule1))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple2
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple3
The rabbit is not green.
("rabbit" "is" "green" "-")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit is round.
("rabbit" "is" "round" "+")
triple7
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple8
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple9
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple10
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((triple8) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple6) -> (rule3 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple6) -> (rule3 % int2)) triple8) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2