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