The mouse is blue. The mouse is green. The mouse is rough. If someone is green and blue then they are round. If someone is kind and round then they are green. If someone is rough and blue then they are green.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If someone is green and blue then they are round.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is kind and round then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and blue then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
The mouse is green.
True
1
proof
[(triple2 OR ((triple3 triple1) -> rule3))]
("mouse" "is" "green" "+")
triple2
((triple3 triple1) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not green.
False
1
inv-proof
[(triple2 OR ((triple3 triple1) -> rule3))]
("mouse" "is" "green" "-")
triple2
((triple3 triple1) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is round.
True
3
proof
[(((triple2 triple1) -> rule1) OR ((((triple3 triple1) -> rule3) triple1) -> rule1))]
("mouse" "is" "round" "+")
((triple2 triple1) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((((triple3 triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is not round.
False
3
inv-proof
[(((triple2 triple1) -> rule1) OR ((((triple3 triple1) -> rule3) triple1) -> rule1))]
("mouse" "is" "round" "-")
((triple2 triple1) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((((triple3 triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
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 blue.[(triple1)] The mouse is green.[(triple2 OR ((triple3 triple1) -> rule3))] The mouse is rough.[(triple3)] @1: The mouse is round.[(((triple2 triple1) -> rule1) OR ((((triple3 triple1) -> rule3) triple1) -> rule1))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
((triple3 triple1) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
((triple2 triple1) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((((triple3 triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2