Anne is big. Gary is blue. Harry is big. Kind things are big. All red things are kind. If something is young and red then it is blue. Kind, big things are young. If something is young then it is blue. Cold, big things are red. All kind things are blue. If something is red then it is blue.
Anne is big.
("Anne" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something is young and red then it is blue.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Kind, big things are young.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Cold, big things are red.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Harry is big.
True
1
proof
[(triple3)]
("Harry" "is" "big" "+")
triple3
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is not blue.
Unknown
inv-rconc
[@4: Anne is blue.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is big.[(triple1)] Gary is blue.[(triple2)] Harry is big.[(triple3)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3