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