Anne is kind. Erin is nice. Erin is not round. Harry is big. Harry is furry. Harry is green. Harry is smart. If Erin is nice and Erin is furry then Erin is round. If someone is kind then they are smart. If someone is smart and not furry then they are nice.
Anne is kind.
("Anne" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not round.
("Erin" "is" "round" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Erin is nice and Erin is furry then Erin is round.
((("Erin" "is" "nice" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "round" "+"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and not furry then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "nice" "+"))
Harry is smart.
True
1
proof
[(triple7)]
("Harry" "is" "smart" "+")
triple7
Erin is not nice.
False
1
inv-proof
[(triple2)]
("Erin" "is" "nice" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "smart" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "nice" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Erin is nice.[(triple2)] Erin is not round.[(triple3)] Harry is big.[(triple4)] Harry is furry.[(triple5)] Harry is green.[(triple6)] Harry is smart.[(triple7)] @1: Anne is smart.[(((triple1) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
Erin is not round.
("Erin" "is" "round" "-")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1