The mouse is big. The mouse is blue. The mouse is green. The mouse is kind. The mouse is rough. The mouse needs the rabbit. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit is big. The rabbit is blue. The rabbit is kind. The rabbit is rough. The rabbit needs the mouse. The rabbit sees the mouse. The rabbit visits the mouse. If the mouse is green and the mouse needs the rabbit then the rabbit is green. If something is green then it visits the rabbit. If something is kind and green then it visits the mouse.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
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 the mouse is green and the mouse needs the rabbit then the rabbit is green.
((("mouse" "is" "green" "+") ("mouse" "needs" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If something is green then it visits the rabbit.
((("something" "is" "green" "+")) -> ("something" "visits" "rabbit" "+"))
If something is kind and green then it visits the mouse.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "visits" "mouse" "+"))
The mouse is rough.
True
1
proof
[(triple5)]
("mouse" "is" "rough" "+")
triple5
The rabbit is not rough.
False
1
inv-proof
[(triple12)]
("rabbit" "is" "rough" "-")
triple12
The mouse visits the mouse.
True
3
proof
[(((triple4 triple3) -> rule3))]
("mouse" "visits" "mouse" "+")
((triple4 triple3) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The rabbit is not green.
False
3
inv-proof
[(((triple3 triple6) -> rule1))]
("rabbit" "is" "green" "-")
((triple3 triple6) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
True
4
proof
[(((((triple3 triple6) -> rule1)) -> rule2))]
("rabbit" "visits" "rabbit" "+")
((((triple3 triple6) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit does not visit the rabbit.
False
4
inv-proof
[(((((triple3 triple6) -> rule1)) -> rule2))]
("rabbit" "visits" "rabbit" "-")
((((triple3 triple6) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
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 rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is big.[(triple1)] The mouse is blue.[(triple2)] The mouse is green.[(triple3)] The mouse is kind.[(triple4)] The mouse is rough.[(triple5)] The mouse needs the rabbit.[(triple6)] The mouse sees the rabbit.[(triple7)] The mouse visits the rabbit.[(triple8 OR ((triple3) -> rule2))] The rabbit is big.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is kind.[(triple11)] The rabbit is rough.[(triple12)] The rabbit needs the mouse.[(triple13)] The rabbit sees the mouse.[(triple14)] The rabbit visits the mouse.[(triple15 OR ((triple11 ((triple3 triple6) -> rule1)) -> rule3))] @1: The mouse visits the mouse.[(((triple4 triple3) -> rule3))] The rabbit is green.[(((triple3 triple6) -> rule1))] @2: The rabbit visits the rabbit.[(((((triple3 triple6) -> rule1)) -> rule2))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple6
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple7
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple8
((triple3) -> (rule2 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple13
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple14
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple15
((triple11 ((triple3 triple6) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple4 triple3) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple3 triple6) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple3 triple6) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2