Anne is furry. Anne is not nice. Anne is red. Bob is rough. Gary is not blue. Gary is nice. Gary is not rough. Gary is white. Harry is not rough. Harry is white. All blue, nice things are rough. All quiet, red things are white. If Harry is blue and Harry is red then Harry is nice. If something is red and rough then it is not quiet. Furry things are quiet. If Bob is furry then Bob is nice.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is white.
("Gary" "is" "white" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is white.
("Harry" "is" "white" "+")
All blue, nice things are rough.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All quiet, red things are white.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If Harry is blue and Harry is red then Harry is nice.
((("Harry" "is" "blue" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "nice" "+"))
If something is red and rough then it is not quiet.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If Bob is furry then Bob is nice.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "nice" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not red.
False
1
inv-proof
[(triple3)]
("Anne" "is" "red" "-")
triple3
Anne is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
True
4
proof
[(((((triple1) -> rule5) triple3) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not white.
False
4
inv-proof
[(((((triple1) -> rule5) triple3) -> rule2))]
("Anne" "is" "white" "-")
((((triple1) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "nice" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "quiet" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is furry.[(triple1)] Anne is not nice.[(triple2)] Anne is red.[(triple3)] Bob is rough.[(triple4)] Gary is nice.[(triple6)] Gary is not blue.[(triple5)] Gary is not rough.[(triple7)] Gary is white.[(triple8)] Harry is not rough.[(triple9)] Harry is white.[(triple10)] @1: Anne is quiet.[(((triple1) -> rule5))] @2: Anne is white.[(((((triple1) -> rule5) triple3) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is not nice.
("Anne" "is" "nice" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is not blue.
("Gary" "is" "blue" "-")
triple5
Gary is not rough.
("Gary" "is" "rough" "-")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is not rough.
("Harry" "is" "rough" "-")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2