Anne is blue. Anne is red. Anne is smart. Anne is white. Charlie is blue. Charlie is red. Charlie is smart. Charlie is white. Erin is kind. Erin is red. Erin is round. Erin is smart. Erin is white. Harry is blue. Harry is kind. Harry is white. If someone is nice then they are round. White people are round. If Anne is round and Anne is smart then Anne is white. If someone is red then they are white. All white, nice people are red. White, round people are nice.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Anne is round and Anne is smart then Anne is white.
((("Anne" "is" "round" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "white" "+"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All white, nice people are red.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
White, round people are nice.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Harry is white.
True
1
proof
[(triple16)]
("Harry" "is" "white" "+")
triple16
Charlie is not smart.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "smart" "-")
triple7
Anne is round.
True
2
proof
[(((triple4) -> rule2) OR ((((triple2) -> rule4)) -> rule2))]
("Anne" "is" "round" "+")
((triple4) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((triple13 triple11) -> rule6) OR ((triple13 ((triple13) -> rule2)) -> rule6) OR ((((triple10) -> rule4) triple11) -> rule6) OR ((((triple10) -> rule4) ((triple13) -> rule2)) -> rule6) OR ((triple13 ((((triple10) -> rule4)) -> rule2)) -> rule6) OR ((((triple10) -> rule4) ((((triple10) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "nice" "-")
((triple13 triple11) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple13 ((triple13) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple10) -> (rule4 % int2)) triple11) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple13) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((triple13 ((((triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((triple10) -> (rule4 % int3)) ((((triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Anne is nice.
True
4
proof
[(((triple4 ((triple4) -> rule2)) -> rule6) OR ((((triple2) -> rule4) ((triple4) -> rule2)) -> rule6) OR ((triple4 ((((triple2) -> rule4)) -> rule2)) -> rule6) OR ((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Anne" "is" "nice" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((triple4 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((triple16 ((triple16) -> rule2)) -> rule6))]
("Harry" "is" "nice" "-")
((triple16 ((triple16) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
True
6
proof
[(((triple16 ((triple16 ((triple16) -> rule2)) -> rule6)) -> rule5))]
("Harry" "is" "red" "+")
((triple16 ((triple16 ((triple16) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not red.
False
6
inv-proof
[(((triple16 ((triple16 ((triple16) -> rule2)) -> rule6)) -> rule5))]
("Harry" "is" "red" "-")
((triple16 ((triple16 ((triple16) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Anne is red.[(triple2 OR ((triple4 ((triple4 ((triple4) -> rule2)) -> rule6)) -> rule5))] Anne is smart.[(triple3)] Anne is white.[(triple4 OR ((triple2) -> rule4))] Charlie is blue.[(triple5)] Charlie is red.[(triple6 OR ((triple8 ((triple8 ((triple8) -> rule2)) -> rule6)) -> rule5))] Charlie is smart.[(triple7)] Charlie is white.[(triple8 OR ((triple6) -> rule4))] Erin is kind.[(triple9)] Erin is red.[(triple10 OR ((triple13 ((triple13 triple11) -> rule6)) -> rule5) OR ((triple13 ((triple13 ((triple13) -> rule2)) -> rule6)) -> rule5))] Erin is round.[(triple11 OR ((triple13) -> rule2) OR ((((triple10) -> rule4)) -> rule2))] Erin is smart.[(triple12)] Erin is white.[(triple13 OR ((triple10) -> rule4))] Harry is blue.[(triple14)] Harry is kind.[(triple15)] Harry is white.[(triple16)] @1: Anne is round.[(((triple4) -> rule2) OR ((((triple2) -> rule4)) -> rule2))] Charlie is round.[(((triple8) -> rule2) OR ((((triple6) -> rule4)) -> rule2))] Erin is nice.[(((triple13 triple11) -> rule6) OR ((triple13 ((triple13) -> rule2)) -> rule6) OR ((((triple10) -> rule4) triple11) -> rule6) OR ((((triple10) -> rule4) ((triple13) -> rule2)) -> rule6) OR ((triple13 ((((triple10) -> rule4)) -> rule2)) -> rule6) OR ((((triple10) -> rule4) ((((triple10) -> rule4)) -> rule2)) -> rule6))] Harry is round.[(((triple16) -> rule2))] @2: Anne is nice.[(((triple4 ((triple4) -> rule2)) -> rule6) OR ((((triple2) -> rule4) ((triple4) -> rule2)) -> rule6) OR ((triple4 ((((triple2) -> rule4)) -> rule2)) -> rule6) OR ((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule6))] Charlie is nice.[(((triple8 ((triple8) -> rule2)) -> rule6) OR ((((triple6) -> rule4) ((triple8) -> rule2)) -> rule6) OR ((triple8 ((((triple6) -> rule4)) -> rule2)) -> rule6) OR ((((triple6) -> rule4) ((((triple6) -> rule4)) -> rule2)) -> rule6))] Harry is nice.[(((triple16 ((triple16) -> rule2)) -> rule6))] @3: Harry is red.[(((triple16 ((triple16 ((triple16) -> rule2)) -> rule6)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple4 ((triple4 ((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((triple2) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
((triple8 ((triple8 ((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
((triple6) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is red.
("Erin" "is" "red" "+")
triple10
((triple13 ((triple13 triple11) -> (rule6 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple13 ((triple13 ((triple13) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple11
((triple13) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Erin is white.
("Erin" "is" "white" "+")
triple13
((triple10) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Anne is round.
("Anne" "is" "round" "+")
((triple4) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple8) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((triple13 triple11) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple13 ((triple13) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple10) -> (rule4 % int2)) triple11) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple13) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((triple13 ((((triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((triple10) -> (rule4 % int3)) ((((triple10) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((triple16) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((triple4 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple8 ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple6) -> (rule4 % int3)) ((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((triple8 ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple6) -> (rule4 % int3)) ((((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple16 ((triple16) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((triple16 ((triple16 ((triple16) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3