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