Anne is smart. Harry is furry. Harry is not kind. Harry is quiet. Harry is red. Harry is smart. Harry is white. If someone is smart then they are red. All white people are quiet. All smart people are quiet. Quiet, red people are not nice. All kind people are nice. If someone is red and not white then they are smart.
Anne is smart.
("Anne" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Quiet, red people are not nice.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and not white then they are smart.
((("someone" "is" "red" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "smart" "+"))
Harry is red.
True
1
proof
[(triple5 OR ((triple6) -> rule1))]
("Harry" "is" "red" "+")
triple5
((triple6) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not furry.
False
1
inv-proof
[(triple2)]
("Harry" "is" "furry" "-")
triple2
Harry is not nice.
True
3
proof
[(((triple4 triple5) -> rule4) OR ((triple4 ((triple6) -> rule1)) -> rule4) OR ((((triple6) -> rule3) triple5) -> rule4) OR ((((triple7) -> rule2) triple5) -> rule4) OR ((((triple6) -> rule3) ((triple6) -> rule1)) -> rule4) OR ((((triple7) -> rule2) ((triple6) -> rule1)) -> rule4))]
("Harry" "is" "nice" "-")
((triple4 triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
((triple4 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple6) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple6) -> (rule3 % int3)) ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple7) -> (rule2 % int3)) ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
False
3
inv-proof
[(((triple4 triple5) -> rule4) OR ((triple4 ((triple6) -> rule1)) -> rule4) OR ((((triple6) -> rule3) triple5) -> rule4) OR ((((triple7) -> rule2) triple5) -> rule4) OR ((((triple6) -> rule3) ((triple6) -> rule1)) -> rule4) OR ((((triple7) -> rule2) ((triple6) -> rule1)) -> rule4))]
("Harry" "is" "nice" "+")
((triple4 triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
((triple4 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple6) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple6) -> (rule3 % int3)) ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple7) -> (rule2 % int3)) ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is smart.[(triple1)] Harry is furry.[(triple2)] Harry is not kind.[(triple3)] Harry is quiet.[(triple4 OR ((triple6) -> rule3) OR ((triple7) -> rule2))] Harry is red.[(triple5 OR ((triple6) -> rule1))] Harry is smart.[(triple6)] Harry is white.[(triple7)] @1: Anne is quiet.[(((triple1) -> rule3))] Anne is red.[(((triple1) -> rule1))] Harry is not nice.[(((triple4 triple5) -> rule4) OR ((triple4 ((triple6) -> rule1)) -> rule4) OR ((((triple6) -> rule3) triple5) -> rule4) OR ((((triple7) -> rule2) triple5) -> rule4) OR ((((triple6) -> rule3) ((triple6) -> rule1)) -> rule4) OR ((((triple7) -> rule2) ((triple6) -> rule1)) -> rule4))] @2: Anne is not nice.[(((((triple1) -> rule3) ((triple1) -> rule1)) -> rule4))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
Harry is not kind.
("Harry" "is" "kind" "-")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
((triple6) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple7) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple5
((triple6) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
((triple4 triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
((triple4 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple6) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple6) -> (rule3 % int3)) ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((triple7) -> (rule2 % int3)) ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Anne is not nice.
("Anne" "is" "nice" "-")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3