The mouse is blue. The mouse is not green. The mouse likes the rabbit. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit is blue. The rabbit is green. The rabbit is rough. The rabbit needs the mouse. The rabbit sees the mouse. If something sees the rabbit then it does not like the mouse. If the mouse sees the rabbit then the rabbit likes the mouse. If something likes the mouse and the mouse does not like the rabbit then the rabbit likes the mouse. If the mouse needs the rabbit then the rabbit needs the mouse. If the rabbit likes the mouse then the rabbit is young. If something sees the mouse and the mouse is green then it is rough.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
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 is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something sees the rabbit then it does not like the mouse.
((("something" "sees" "rabbit" "+")) -> ("something" "likes" "mouse" "-"))
If the mouse sees the rabbit then the rabbit likes the mouse.
((("mouse" "sees" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something likes the mouse and the mouse does not like the rabbit then the rabbit likes the mouse.
((("something" "likes" "mouse" "+") ("mouse" "likes" "rabbit" "~")) -> ("rabbit" "likes" "mouse" "+"))
If the mouse needs the rabbit then the rabbit needs the mouse.
((("mouse" "needs" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If the rabbit likes the mouse then the rabbit is young.
((("rabbit" "likes" "mouse" "+")) -> ("rabbit" "is" "young" "+"))
If something sees the mouse and the mouse is green then it is rough.
((("something" "sees" "mouse" "+") ("mouse" "is" "green" "+")) -> ("something" "is" "rough" "+"))
The mouse likes the rabbit.
True
1
proof
[(triple3)]
("mouse" "likes" "rabbit" "+")
triple3
The mouse is not blue.
False
1
inv-proof
[(triple1)]
("mouse" "is" "blue" "-")
triple1
The mouse does not like the mouse.
True
2
proof
[(((triple5) -> rule1))]
("mouse" "likes" "mouse" "-")
((triple5) -> (rule1 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The rabbit does not like the mouse.
False
2
inv-proof
[(((triple5) -> rule2))]
("rabbit" "likes" "mouse" "-")
((triple5) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple5) -> rule2)) -> rule5))]
("rabbit" "is" "young" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule5))]
("rabbit" "is" "young" "-")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "rough" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The mouse is blue.[(triple1)] The mouse is not green.[(triple2)] The mouse likes the rabbit.[(triple3)] The mouse needs the rabbit.[(triple4)] The mouse sees the rabbit.[(triple5)] The rabbit is blue.[(triple6)] The rabbit is green.[(triple7)] The rabbit is rough.[(triple8)] The rabbit needs the mouse.[(triple9 OR ((triple4) -> rule4))] The rabbit sees the mouse.[(triple10)] @1: The mouse does not like the mouse.[(((triple5) -> rule1))] The rabbit likes the mouse.[(((triple5) -> rule2))] @2: The rabbit is young.[(((((triple5) -> rule2)) -> rule5))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is not green.
("mouse" "is" "green" "-")
triple2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple4
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple5
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple9
((triple4) -> (rule4 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple10
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
((triple5) -> (rule1 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((triple5) -> (rule2 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2