Harry is white. Green things are red. Kind, blue things are green. If something is kind then it is blue. If something is red and quiet then it is kind. If Harry is kind then Harry is blue. If Harry is white then Harry is red. If Harry is quiet then Harry is green. If Harry is red and Harry is quiet then Harry is green.
Harry is white.
("Harry" "is" "white" "+")
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Kind, blue things are green.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is red and quiet then it is kind.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Harry is kind then Harry is blue.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is white then Harry is red.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "red" "+"))
If Harry is quiet then Harry is green.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
If Harry is red and Harry is quiet then Harry is green.
((("Harry" "is" "red" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
Harry is white.
True
1
proof
[(triple1)]
("Harry" "is" "white" "+")
triple1
Harry is not white.
False
1
inv-proof
[(triple1)]
("Harry" "is" "white" "-")
triple1
Harry is red.
True
2
proof
[(((triple1) -> rule6))]
("Harry" "is" "red" "+")
((triple1) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple1) -> rule6))]
("Harry" "is" "red" "-")
((triple1) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is blue.
Unknown
rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Harry is white.[(triple1)] @1: Harry is red.[(((triple1) -> rule6))]
Harry is white.
("Harry" "is" "white" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
((triple1) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1