The mouse is rough. If something is green and kind then it is nice. Nice things are green. If the mouse is green and the mouse is nice then the mouse is kind. All rough, kind things are green. All blue things are green. If something is nice then it is green. If something is blue then it is rough. If something is rough then it is nice.
The mouse is rough.
("mouse" "is" "rough" "+")
If something is green and kind then it is nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If the mouse is green and the mouse is nice then the mouse is kind.
((("mouse" "is" "green" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "is" "kind" "+"))
All rough, kind things are green.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
The mouse is rough.
True
1
proof
[(triple1)]
("mouse" "is" "rough" "+")
triple1
The mouse is not rough.
False
1
inv-proof
[(triple1)]
("mouse" "is" "rough" "-")
triple1
The mouse is nice.
True
2
proof
[(((triple1) -> rule8))]
("mouse" "is" "nice" "+")
((triple1) -> (rule8 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple1) -> rule8))]
("mouse" "is" "nice" "-")
((triple1) -> (rule8 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The mouse is rough.[(triple1)] @1: The mouse is nice.[(((triple1) -> rule8))] @2: The mouse is green.[(((((triple1) -> rule8)) -> rule2) OR ((((triple1) -> rule8)) -> rule6))] @3: The mouse is kind.[(((((((triple1) -> rule8)) -> rule2) ((triple1) -> rule8)) -> rule3) OR ((((((triple1) -> rule8)) -> rule6) ((triple1) -> rule8)) -> rule3))]
The mouse is rough.
("mouse" "is" "rough" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
((triple1) -> (rule8 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
((((((triple1) -> (rule8 % int3))) -> (rule2 % int2)) ((triple1) -> (rule8 % int3))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2)) ((triple1) -> (rule8 % int3))) -> (rule3 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3