Harry is smart. If something is smart and furry then it is white. All furry things are rough. If Harry is white and Harry is furry then Harry is rough. Smart things are green. All green things are smart. Furry things are green.
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart and furry then it is white.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
All furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If Harry is white and Harry is furry then Harry is rough.
((("Harry" "is" "white" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "rough" "+"))
Smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Harry is smart.
True
1
proof
[(triple1)]
("Harry" "is" "smart" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple1)]
("Harry" "is" "smart" "-")
triple1
Harry is green.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "green" "+")
((triple1) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "green" "-")
((triple1) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Harry is smart.[(triple1)] @1: Harry is green.[(((triple1) -> rule4))]
Harry is smart.
("Harry" "is" "smart" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
((triple1) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1