The mouse is nice. All green, kind things are nice. Young, kind things are nice. All nice things are rough. If the mouse is rough then the mouse is green. If something is rough then it is kind. If the mouse is young then the mouse is kind. If something is green and young then it is rough. If the mouse is green and the mouse is kind then the mouse is nice.
The mouse is nice.
("mouse" "is" "nice" "+")
All green, kind things are nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Young, kind things are nice.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If the mouse is rough then the mouse is green.
((("mouse" "is" "rough" "+")) -> ("mouse" "is" "green" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If the mouse is young then the mouse is kind.
((("mouse" "is" "young" "+")) -> ("mouse" "is" "kind" "+"))
If something is green and young then it is rough.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If the mouse is green and the mouse is kind then the mouse is nice.
((("mouse" "is" "green" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "is" "nice" "+"))
The mouse is nice.
True
1
proof
[(triple1)]
("mouse" "is" "nice" "+")
triple1
The mouse is not nice.
False
1
inv-proof
[(triple1)]
("mouse" "is" "nice" "-")
triple1
The mouse is rough.
True
2
proof
[(((triple1) -> rule3))]
("mouse" "is" "rough" "+")
((triple1) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("mouse" "is" "rough" "-")
((triple1) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("mouse" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("mouse" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
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 sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The mouse is nice.[(triple1)] @1: The mouse is rough.[(((triple1) -> rule3))] @2: The mouse is green.[(((((triple1) -> rule3)) -> rule4))] The mouse is kind.[(((((triple1) -> rule3)) -> rule5))]
The mouse is nice.
("mouse" "is" "nice" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple1) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2