Anne is cold. Charlie is kind. Erin is furry. Erin is kind. Erin is red. Harry is cold. Harry is furry. Nice, furry things are smart. If something is furry and cold then it is nice.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Nice, furry things are smart.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is furry and cold then it is nice.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Erin is furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "+")
triple3
Harry is not furry.
False
1
inv-proof
[(triple7)]
("Harry" "is" "furry" "-")
triple7
Harry is nice.
True
3
proof
[(((triple7 triple6) -> rule2))]
("Harry" "is" "nice" "+")
((triple7 triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
3
inv-proof
[(((triple7 triple6) -> rule2))]
("Harry" "is" "nice" "-")
((triple7 triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
True
5
proof
[(((((triple7 triple6) -> rule2) triple7) -> rule1))]
("Harry" "is" "smart" "+")
((((triple7 triple6) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not smart.
False
5
inv-proof
[(((((triple7 triple6) -> rule2) triple7) -> rule1))]
("Harry" "is" "smart" "-")
((((triple7 triple6) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is cold.[(triple1)] Charlie is kind.[(triple2)] Erin is furry.[(triple3)] Erin is kind.[(triple4)] Erin is red.[(triple5)] Harry is cold.[(triple6)] Harry is furry.[(triple7)] @1: Harry is nice.[(((triple7 triple6) -> rule2))] @2: Harry is smart.[(((((triple7 triple6) -> rule2) triple7) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 triple6) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7 triple6) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2