Anne is smart. Dave is rough. Erin is red. Harry is round. If Erin is kind and Erin is smart then Erin is round. Smart things are red.
Anne is smart.
("Anne" "is" "smart" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If Erin is kind and Erin is smart then Erin is round.
((("Erin" "is" "kind" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "round" "+"))
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Harry is not round.
False
1
inv-proof
[(triple4)]
("Harry" "is" "round" "-")
triple4
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Anne is smart.[(triple1)] Dave is rough.[(triple2)] Erin is red.[(triple3)] Harry is round.[(triple4)] @1: Anne is red.[(((triple1) -> rule2))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1