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