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