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