Erin is smart. Harry is blue. Harry is green. If something is big and nice then it is blue. If something is big and kind then it is blue. Kind things are nice. All big things are smart. Green things are blue. All green, smart things are red.
Erin is smart.
("Erin" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is big and nice then it is blue.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is big and kind then it is blue.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All green, smart things are red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Harry is blue.
True
1
proof
[(triple2 OR ((triple3) -> rule5))]
("Harry" "is" "blue" "+")
triple2
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Erin is not smart.
False
1
inv-proof
[(triple1)]
("Erin" "is" "smart" "-")
triple1
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Erin is smart.[(triple1)] Harry is blue.[(triple2 OR ((triple3) -> rule5))] Harry is green.[(triple3)]
Erin is smart.
("Erin" "is" "smart" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple3