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