Anne is blue. Anne is kind. Fiona is rough. All blue, kind things are rough. If something is quiet and kind then it is nice. Kind things are quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All blue, kind things are rough.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and kind then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Fiona is rough.
True
1
proof
[(triple3)]
("Fiona" "is" "rough" "+")
triple3
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
Anne is rough.
True
3
proof
[(((triple1 triple2) -> rule1))]
("Anne" "is" "rough" "+")
((triple1 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("Anne" "is" "rough" "-")
((triple1 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("Anne" "is" "nice" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule2))]
("Anne" "is" "nice" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "nice" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2)] Fiona is rough.[(triple3)] @1: Anne is quiet.[(((triple2) -> rule3))] Anne is rough.[(((triple1 triple2) -> rule1))] @2: Anne is nice.[(((((triple2) -> rule3) triple2) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2