Charlie is smart. Dave is green. Harry is big. Rough, white people are cold. All rough people are cold. Kind people are white. All big, rough people are not white. All smart people are not green. Rough people are kind. If someone is rough then they are kind. If someone is white and green then they are rough.
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is green.
("Dave" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Rough, white people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
All big, rough people are not white.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "-"))
All smart people are not green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "-"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is white and green then they are rough.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Charlie" "is" "cold" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Charlie is smart.[(triple1)] Dave is green.[(triple2)] Harry is big.[(triple3)] @1: Charlie is not green.[(((triple1) -> rule5))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Charlie is not green.
("Charlie" "is" "green" "-")
((triple1) -> (rule5 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1