Anne is furry. Anne is kind. Anne is rough. Anne is not young. Erin is blue. Erin is furry. Erin is kind. Erin is not quiet. Harry is blue. Harry is rough. If something is round and young then it is quiet. All rough things are quiet. If something is kind then it is furry. If Harry is blue then Harry is kind. If Harry is furry then Harry is round. If something is quiet then it is kind. If Anne is not rough then Anne is kind. If Anne is furry and Anne is not young then Anne is round.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not young.
("Anne" "is" "young" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is round and young then it is quiet.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If Harry is blue then Harry is kind.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "kind" "+"))
If Harry is furry then Harry is round.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "round" "+"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Anne is not rough then Anne is kind.
((("Anne" "is" "rough" "~")) -> ("Anne" "is" "kind" "+"))
If Anne is furry and Anne is not young then Anne is round.
((("Anne" "is" "furry" "+") ("Anne" "is" "young" "~")) -> ("Anne" "is" "round" "+"))
Erin is blue.
True
1
proof
[(triple5)]
("Erin" "is" "blue" "+")
triple5
Harry is not rough.
False
1
inv-proof
[(triple10)]
("Harry" "is" "rough" "-")
triple10
Anne is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple9) -> rule4) OR ((((triple10) -> rule2)) -> rule6))]
("Harry" "is" "kind" "-")
((triple9) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
True
3
proof
[(((((triple9) -> rule4)) -> rule3) OR ((((((triple10) -> rule2)) -> rule6)) -> rule3))]
("Harry" "is" "furry" "+")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not furry.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule3) OR ((((((triple10) -> rule2)) -> rule6)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is round.
True
4
proof
[(((((((triple9) -> rule4)) -> rule3)) -> rule5) OR ((((((((triple10) -> rule2)) -> rule6)) -> rule3)) -> rule5))]
("Harry" "is" "round" "+")
((((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((((triple10) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not round.
False
4
inv-proof
[(((((((triple9) -> rule4)) -> rule3)) -> rule5) OR ((((((((triple10) -> rule2)) -> rule6)) -> rule3)) -> rule5))]
("Harry" "is" "round" "-")
((((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((((triple10) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is furry.[(triple1 OR ((triple2) -> rule3) OR ((((((triple3) -> rule2)) -> rule6)) -> rule3))] Anne is kind.[(triple2 OR ((((triple3) -> rule2)) -> rule6))] Anne is not young.[(triple4)] Anne is rough.[(triple3)] Erin is blue.[(triple5)] Erin is furry.[(triple6 OR ((triple7) -> rule3))] Erin is kind.[(triple7)] Erin is not quiet.[(triple8)] Harry is blue.[(triple9)] Harry is rough.[(triple10)] @1: Anne is quiet.[(((triple3) -> rule2))] Anne is round.[(((triple1 triple4) -> rule8) OR ((((triple2) -> rule3) triple4) -> rule8) OR ((((((((triple3) -> rule2)) -> rule6)) -> rule3) triple4) -> rule8))] Harry is kind.[(((triple9) -> rule4) OR ((((triple10) -> rule2)) -> rule6))] Harry is quiet.[(((triple10) -> rule2))] @2: Harry is furry.[(((((triple9) -> rule4)) -> rule3) OR ((((((triple10) -> rule2)) -> rule6)) -> rule3))] @3: Harry is round.[(((((((triple9) -> rule4)) -> rule3)) -> rule5) OR ((((((((triple10) -> rule2)) -> rule6)) -> rule3)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((((triple3) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not young.
("Anne" "is" "young" "-")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
((triple7) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple7
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1 triple4) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule3 % int2)) triple4) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((((triple3) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple4) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((triple9) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple10) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((((((triple9) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((((triple10) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4