Erin is kind. Erin is smart. Harry is furry. Harry is green. Harry is kind. Harry is quiet. Harry is white. If Erin is quiet and Erin is kind then Erin is furry. White, quiet things are furry. If something is smart and not cold then it is not green.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If Erin is quiet and Erin is kind then Erin is furry.
((("Erin" "is" "quiet" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "furry" "+"))
White, quiet things are furry.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is smart and not cold then it is not green.
((("something" "is" "smart" "+") ("something" "is" "cold" "~")) -> ("something" "is" "green" "-"))
Harry is quiet.
True
1
proof
[(triple6)]
("Harry" "is" "quiet" "+")
triple6
Harry is not quiet.
False
1
inv-proof
[(triple6)]
("Harry" "is" "quiet" "-")
triple6
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Erin is kind.[(triple1)] Erin is smart.[(triple2)] Harry is furry.[(triple3 OR ((triple7 triple6) -> rule2))] Harry is green.[(triple4)] Harry is kind.[(triple5)] Harry is quiet.[(triple6)] Harry is white.[(triple7)]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
((triple7 triple6) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7