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