Harry is rough. Smart, rough people are white. If someone is blue then they are kind. All blue, kind people are white. If Harry is rough then Harry is big. If Harry is big and Harry is smart then Harry is rough. If Harry is white then Harry is rough.
Harry is rough.
("Harry" "is" "rough" "+")
Smart, rough people are white.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All blue, kind people are white.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If Harry is rough then Harry is big.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "big" "+"))
If Harry is big and Harry is smart then Harry is rough.
((("Harry" "is" "big" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "rough" "+"))
If Harry is white then Harry is rough.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "rough" "+"))
Harry is rough.
True
1
proof
[(triple1)]
("Harry" "is" "rough" "+")
triple1
Harry is not rough.
False
1
inv-proof
[(triple1)]
("Harry" "is" "rough" "-")
triple1
Harry is big.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "big" "+")
((triple1) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "big" "-")
((triple1) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Harry is rough.[(triple1)] @1: Harry is big.[(((triple1) -> rule4))]
Harry is rough.
("Harry" "is" "rough" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
((triple1) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1