Gary is big. Harry is big. Harry is white. If Gary is smart then Gary is white. Cold people are big. If someone is cold and round then they are quiet. If someone is round then they are blue. All round, cold people are big. All smart, cold people are round.
Gary is big.
("Gary" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is white.
("Harry" "is" "white" "+")
If Gary is smart then Gary is white.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "white" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and round then they are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
All round, cold people are big.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All smart, cold people are round.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Gary is big.
True
1
proof
[(triple1)]
("Gary" "is" "big" "+")
triple1
Harry is not white.
False
1
inv-proof
[(triple3)]
("Harry" "is" "white" "-")
triple3
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Gary is big.[(triple1)] Harry is big.[(triple2)] Harry is white.[(triple3)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3