Anne is not big. Anne is furry. Anne is green. Anne is kind. Anne is quiet. Anne is not rough. Anne is white. Charlie is big. Charlie is green. Charlie is kind. Charlie is rough. Charlie is white. Harry is not green. Harry is kind. Harry is quiet. Harry is rough. If someone is kind and not rough then they are furry. If someone is big then they are furry. All white people are furry. Kind people are white. If Harry is rough and Harry is not green then Harry is white. If Harry is not kind then Harry is not furry. If Anne is not rough then Anne is quiet. If Harry is kind and Harry is not white then Harry is not quiet.
Anne is not big.
("Anne" "is" "big" "-")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is kind and not rough then they are furry.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "furry" "+"))
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All white people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If Harry is rough and Harry is not green then Harry is white.
((("Harry" "is" "rough" "+") ("Harry" "is" "green" "~")) -> ("Harry" "is" "white" "+"))
If Harry is not kind then Harry is not furry.
((("Harry" "is" "kind" "~")) -> ("Harry" "is" "furry" "-"))
If Anne is not rough then Anne is quiet.
((("Anne" "is" "rough" "~")) -> ("Anne" "is" "quiet" "+"))
If Harry is kind and Harry is not white then Harry is not quiet.
((("Harry" "is" "kind" "+") ("Harry" "is" "white" "~")) -> ("Harry" "is" "quiet" "-"))
Charlie is white.
True
1
proof
[(triple12 OR ((triple10) -> rule4))]
("Charlie" "is" "white" "+")
triple12
((triple10) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not kind.
False
1
inv-proof
[(triple10)]
("Charlie" "is" "kind" "-")
triple10
Harry is white.
True
2
proof
[(((triple14) -> rule4) OR ((triple16 triple13) -> rule5))]
("Harry" "is" "white" "+")
((triple14) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple16 triple13) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple12) -> rule3) OR ((triple8) -> rule2) OR ((((triple10) -> rule4)) -> rule3))]
("Charlie" "is" "furry" "-")
((triple12) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Harry is furry.
True
3
proof
[(((((triple14) -> rule4)) -> rule3) OR ((((triple16 triple13) -> rule5)) -> rule3))]
("Harry" "is" "furry" "+")
((((triple14) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple16 triple13) -> (rule5 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple14) -> rule4)) -> rule3) OR ((((triple16 triple13) -> rule5)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple14) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple16 triple13) -> (rule5 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is furry.[(triple2 OR ((triple7) -> rule3) OR ((triple4 triple6) -> rule1) OR ((((triple4) -> rule4)) -> rule3))] Anne is green.[(triple3)] Anne is kind.[(triple4)] Anne is not big.[(triple1)] Anne is not rough.[(triple6)] Anne is quiet.[(triple5 OR ((triple6) -> rule7))] Anne is white.[(triple7 OR ((triple4) -> rule4))] Charlie is big.[(triple8)] Charlie is green.[(triple9)] Charlie is kind.[(triple10)] Charlie is rough.[(triple11)] Charlie is white.[(triple12 OR ((triple10) -> rule4))] Harry is kind.[(triple14)] Harry is not green.[(triple13)] Harry is quiet.[(triple15)] Harry is rough.[(triple16)] @1: Charlie is furry.[(((triple12) -> rule3) OR ((triple8) -> rule2) OR ((((triple10) -> rule4)) -> rule3))] Harry is white.[(((triple14) -> rule4) OR ((triple16 triple13) -> rule5))] @2: Harry is furry.[(((((triple14) -> rule4)) -> rule3) OR ((((triple16 triple13) -> rule5)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple7) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 triple6) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple6
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((triple6) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple4) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is rough.
("Charlie" "is" "rough" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
((triple10) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is not green.
("Harry" "is" "green" "-")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple16
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple12) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple8) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple14) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple16 triple13) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple14) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple16 triple13) -> (rule5 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2