The mouse is big. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit is blue. The rabbit needs the mouse. The rabbit sees the mouse. The rabbit visits the mouse. If something visits the rabbit then the rabbit needs the mouse. If something visits the mouse and it sees the rabbit then the rabbit sees the mouse. All blue things are red.
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
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 visits the rabbit then the rabbit needs the mouse.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something visits the mouse and it sees the rabbit then the rabbit sees the mouse.
((("something" "visits" "mouse" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
The mouse is big.
True
1
proof
[(triple1)]
("mouse" "is" "big" "+")
triple1
The rabbit does not visit the mouse.
False
1
inv-proof
[(triple7)]
("rabbit" "visits" "mouse" "-")
triple7
The rabbit is red.
True
2
proof
[(((triple4) -> rule3))]
("rabbit" "is" "red" "+")
((triple4) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple4) -> rule3))]
("rabbit" "is" "red" "-")
((triple4) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "red" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The mouse is big.[(triple1)] The mouse needs the rabbit.[(triple2)] The mouse sees the rabbit.[(triple3)] The rabbit is blue.[(triple4)] The rabbit needs the mouse.[(triple5)] The rabbit sees the mouse.[(triple6)] The rabbit visits the mouse.[(triple7)] @1: The rabbit is red.[(((triple4) -> rule3))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
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 is red.
("rabbit" "is" "red" "+")
((triple4) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1