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