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