Anne is furry. Anne is white. Erin is furry. Erin is not kind. Erin is round. Harry is not furry. Harry is not kind. Harry is nice. Harry is round. Harry is white. If someone is nice and not round then they are not young. If someone is white and nice then they are young. Furry people are white. All kind, young people are nice. White people are nice. If Harry is green then Harry is not furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is round.
("Erin" "is" "round" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is nice and not round then they are not young.
((("someone" "is" "nice" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "-"))
If someone is white and nice then they are young.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
All kind, young people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Harry is green then Harry is not furry.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "furry" "-"))
Anne is white.
True
1
proof
[(triple2 OR ((triple1) -> rule3))]
("Anne" "is" "white" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is not round.
False
1
inv-proof
[(triple5)]
("Erin" "is" "round" "-")
triple5
Erin is white.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "white" "+")
((triple3) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple2) -> rule5) OR ((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Erin is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("Erin" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("Erin" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
True
6
proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule2))]
("Erin" "is" "young" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is not young.
False
6
inv-proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule2))]
("Erin" "is" "young" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is furry.[(triple1)] Anne is white.[(triple2 OR ((triple1) -> rule3))] Erin is furry.[(triple3)] Erin is not kind.[(triple4)] Erin is round.[(triple5)] Harry is nice.[(triple8 OR ((triple10) -> rule5))] Harry is not furry.[(triple6)] Harry is not kind.[(triple7)] Harry is round.[(triple9)] Harry is white.[(triple10)] @1: Anne is nice.[(((triple2) -> rule5) OR ((((triple1) -> rule3)) -> rule5))] Erin is white.[(((triple3) -> rule3))] Harry is young.[(((triple10 triple8) -> rule2) OR ((triple10 ((triple10) -> rule5)) -> rule2))] @2: Anne is young.[(((triple2 ((triple2) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((triple2) -> rule5)) -> rule2) OR ((triple2 ((((triple1) -> rule3)) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule2))] Erin is nice.[(((((triple3) -> rule3)) -> rule5))] @3: Erin is young.[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is not kind.
("Erin" "is" "kind" "-")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple10) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not furry.
("Harry" "is" "furry" "-")
triple6
Harry is not kind.
("Harry" "is" "kind" "-")
triple7
Harry is round.
("Harry" "is" "round" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple10 triple8) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple10 ((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple1) -> (rule3 % int3)) ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3