Bob is young. Erin is kind. Harry is rough. Smart, kind things are green. If something is rough then it is not green. If something is young and not cold then it is kind. If something is young and not rough then it is smart. All rough, kind things are young. If Harry is cold then Harry is kind.
Bob is young.
("Bob" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Smart, kind things are green.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is not green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "-"))
If something is young and not cold then it is kind.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "kind" "+"))
If something is young and not rough then it is smart.
((("something" "is" "young" "+") ("something" "is" "rough" "~")) -> ("something" "is" "smart" "+"))
All rough, kind things are young.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Harry is cold then Harry is kind.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "kind" "+"))
Harry is rough.
True
1
proof
[(triple3)]
("Harry" "is" "rough" "+")
triple3
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Erin" "is" "green" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is young.[(triple1)] Erin is kind.[(triple2)] Harry is rough.[(triple3)] @1: Harry is not green.[(((triple3) -> rule2))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is not green.
("Harry" "is" "green" "-")
((triple3) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1