Anne is smart. Erin is cold. Harry is smart. If Erin is cold then Erin is smart. If someone is green then they are cold.
Anne is smart.
("Anne" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Erin is cold then Erin is smart.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "smart" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is smart.[(triple1)] Erin is cold.[(triple2)] Harry is smart.[(triple3)] @1: Erin is smart.[(((triple2) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1