Gary is white. Harry is big. Harry is round. If Gary is kind then Gary is cold. Round things are smart. All white, kind things are big.
Gary is white.
("Gary" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
If Gary is kind then Gary is cold.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "cold" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All white, kind things are big.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Harry is round.
True
1
proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Harry is not big.
False
1
inv-proof
[(triple2)]
("Harry" "is" "big" "-")
triple2
Harry is smart.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Gary is white.[(triple1)] Harry is big.[(triple2)] Harry is round.[(triple3)] @1: Harry is smart.[(((triple3) -> rule2))]
Gary is white.
("Gary" "is" "white" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1