Anne is blue. Charlie is blue. Harry is furry. Quiet, blue things are rough. If something is green then it is rough. All quiet things are furry. Rough things are kind. Furry things are rough. All quiet, rough things are furry.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Quiet, blue things are rough.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All quiet, rough things are furry.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Harry is rough.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "rough" "-")
((triple3) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is kind.
Unknown
rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is blue.[(triple1)] Charlie is blue.[(triple2)] Harry is furry.[(triple3)] @1: Harry is rough.[(((triple3) -> rule5))] @2: Harry is kind.[(((((triple3) -> rule5)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2