Dave is round. Erin is cold. Harry is round. If Dave is rough and Dave is round then Dave is cold. If something is rough and not blue then it is round. If something is blue and cold then it is rough. If Dave is nice and Dave is big then Dave is not round. If something is kind and rough then it is not nice. If something is rough then it is not big.
Dave is round.
("Dave" "is" "round" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
If Dave is rough and Dave is round then Dave is cold.
((("Dave" "is" "rough" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "cold" "+"))
If something is rough and not blue then it is round.
((("something" "is" "rough" "+") ("something" "is" "blue" "~")) -> ("something" "is" "round" "+"))
If something is blue and cold then it is rough.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Dave is nice and Dave is big then Dave is not round.
((("Dave" "is" "nice" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "round" "-"))
If something is kind and rough then it is not nice.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "-"))
If something is rough then it is not big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "-"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "rough" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Dave is round.[(triple1)] Erin is cold.[(triple2)] Harry is round.[(triple3)]
Dave is round.
("Dave" "is" "round" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3