Charlie is green and young, but he is also kind. He has blue eyes and red hair. Red Eric is what folks call him, because he is quite red. Young Fred is big and round from his mother's good cooking.  Fred is the kind of kid who is nice and kind to everyone and who is red with a sunburn. If a kind person is also young and round shaped, they will be colored blue. A nice and blue person who's also red will be a rough person. Incredible as it may seem, young people who are red and have kind attitudes are always round. A cold person, who is kind in nature and young in years, is round. I bet you didn't know that nice, kind, cold people happen to be red. They found the ones that were round, blue, and green to be nice.
Charlie is young.
("Charlie" "is" "young" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Eric is red.
("Eric" "is" "red" "+")
Fred is young.
("Fred" "is" "young" "+")
Fred is round.
("Fred" "is" "round" "+")
Fred is red.
("Fred" "is" "red" "+")
Fred is nice.
("Fred" "is" "nice" "+")
Fred is kind.
("Fred" "is" "kind" "+")
Fred is big.
("Fred" "is" "big" "+")
If someone is kind and young and round then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and nice and red then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is young and red and kind then they are round.
((("someone" "is" "young" "+") ("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and kind and young then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and kind and cold then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is round and blue and green then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Fred is red.
True
1
proof
[(triple9)]
("Fred" "is" "red" "+")
triple9
Charlie is not red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "-")
triple2
Charlie is round.
True
4
proof
[(((triple1 triple2 triple3) -> rule3))]
("Charlie" "is" "round" "+")
((triple1 triple2 triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fred is not blue.
False
4
inv-proof
[(((triple11 triple7 triple8) -> rule1) OR ((triple11 triple7 ((triple7 triple9 triple11) -> rule3)) -> rule1))]
("Fred" "is" "blue" "-")
((triple11 triple7 triple8) -> (rule1 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
((triple11 triple7 ((triple7 triple9 triple11) -> (rule3 % int2))) -> (rule1 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Charlie is nice.
True
7
proof
[(((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) OR ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6))]
("Charlie" "is" "nice" "+")
((((triple1 triple2 triple3) -> (rule3 % int2)) triple5 triple4) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple1 triple2 triple3) -> (rule3 % int3)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Fred is not rough.
False
7
inv-proof
[(((((triple11 triple7 triple8) -> rule1) triple10 triple9) -> rule2) OR ((((triple11 triple7 ((triple7 triple9 triple11) -> rule3)) -> rule1) triple10 triple9) -> rule2))]
("Fred" "is" "rough" "-")
((((triple11 triple7 triple8) -> (rule1 % int2)) triple10 triple9) -> (rule2 % int1))
Fred is rough.
("Fred" "is" "rough" "+")
int1
Fred is blue.
("Fred" "is" "blue" "+")
int2
((((triple11 triple7 ((triple7 triple9 triple11) -> (rule3 % int3))) -> (rule1 % int2)) triple10 triple9) -> (rule2 % int1))
Fred is rough.
("Fred" "is" "rough" "+")
int1
Fred is blue.
("Fred" "is" "blue" "+")
int2
Fred is round.
("Fred" "is" "round" "+")
int3
Charlie is rough.
True
10
proof
[(((triple5 ((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) triple2) -> rule2) OR ((((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) ((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) triple2) -> rule2) OR ((triple5 ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6) triple2) -> rule2) OR ((((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6) triple2) -> rule2))]
("Charlie" "is" "rough" "+")
((triple5 ((((triple1 triple2 triple3) -> (rule3 % int3)) triple5 triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple1 triple2 triple3) -> (rule3 % int4)) triple5 triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((triple5 ((((triple1 triple2 triple3) -> (rule3 % int4)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple1 triple2 triple3) -> (rule3 % int4)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is not rough.
False
10
inv-proof
[(((triple5 ((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) triple2) -> rule2) OR ((((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) ((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) triple2) -> rule2) OR ((triple5 ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6) triple2) -> rule2) OR ((((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6) triple2) -> rule2))]
("Charlie" "is" "rough" "-")
((triple5 ((((triple1 triple2 triple3) -> (rule3 % int3)) triple5 triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple1 triple2 triple3) -> (rule3 % int4)) triple5 triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((triple5 ((((triple1 triple2 triple3) -> (rule3 % int4)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple1 triple2 triple3) -> (rule3 % int4)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Eric is blue.
Unknown
rconc
[@1: Eric is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Eric" "is" "blue" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is rough.
Unknown
rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "rough" "+")
Eric is not young.
Unknown
inv-random
[@0: Eric is young.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "young" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Eric is not big.
Unknown
inv-random
[@0: Eric is big.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "big" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is blue.[(triple5 OR ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1))] Charlie is green.[(triple4)] Charlie is kind.[(triple3)] Charlie is red.[(triple2)] Charlie is young.[(triple1)] Eric is red.[(triple6)] Fred is big.[(triple12)] Fred is kind.[(triple11)] Fred is nice.[(triple10)] Fred is red.[(triple9)] Fred is round.[(triple8 OR ((triple7 triple9 triple11) -> rule3))] Fred is young.[(triple7)] @1: Charlie is round.[(((triple1 triple2 triple3) -> rule3))] Fred is blue.[(((triple11 triple7 triple8) -> rule1) OR ((triple11 triple7 ((triple7 triple9 triple11) -> rule3)) -> rule1))] @2: Charlie is nice.[(((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) OR ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6))] Fred is rough.[(((((triple11 triple7 triple8) -> rule1) triple10 triple9) -> rule2) OR ((((triple11 triple7 ((triple7 triple9 triple11) -> rule3)) -> rule1) triple10 triple9) -> rule2))] @3: Charlie is rough.[(((triple5 ((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) triple2) -> rule2) OR ((((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) ((((triple1 triple2 triple3) -> rule3) triple5 triple4) -> rule6) triple2) -> rule2) OR ((triple5 ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6) triple2) -> rule2) OR ((((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) ((((triple1 triple2 triple3) -> rule3) ((triple3 triple1 ((triple1 triple2 triple3) -> rule3)) -> rule1) triple4) -> rule6) triple2) -> rule2))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Eric is red.
("Eric" "is" "red" "+")
triple6
Fred is big.
("Fred" "is" "big" "+")
triple12
Fred is kind.
("Fred" "is" "kind" "+")
triple11
Fred is nice.
("Fred" "is" "nice" "+")
triple10
Fred is red.
("Fred" "is" "red" "+")
triple9
Fred is round.
("Fred" "is" "round" "+")
triple8
((triple7 triple9 triple11) -> (rule3 % int1))
Fred is round.
("Fred" "is" "round" "+")
int1
Fred is young.
("Fred" "is" "young" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple1 triple2 triple3) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Fred is blue.
("Fred" "is" "blue" "+")
((triple11 triple7 triple8) -> (rule1 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
((triple11 triple7 ((triple7 triple9 triple11) -> (rule3 % int2))) -> (rule1 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1 triple2 triple3) -> (rule3 % int2)) triple5 triple4) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((triple1 triple2 triple3) -> (rule3 % int3)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Fred is rough.
("Fred" "is" "rough" "+")
((((triple11 triple7 triple8) -> (rule1 % int2)) triple10 triple9) -> (rule2 % int1))
Fred is rough.
("Fred" "is" "rough" "+")
int1
Fred is blue.
("Fred" "is" "blue" "+")
int2
((((triple11 triple7 ((triple7 triple9 triple11) -> (rule3 % int3))) -> (rule1 % int2)) triple10 triple9) -> (rule2 % int1))
Fred is rough.
("Fred" "is" "rough" "+")
int1
Fred is blue.
("Fred" "is" "blue" "+")
int2
Fred is round.
("Fred" "is" "round" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5 ((((triple1 triple2 triple3) -> (rule3 % int3)) triple5 triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple1 triple2 triple3) -> (rule3 % int4)) triple5 triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((triple5 ((((triple1 triple2 triple3) -> (rule3 % int4)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple1 triple2 triple3) -> (rule3 % int4)) ((triple3 triple1 ((triple1 triple2 triple3) -> (rule3 % int4))) -> (rule1 % int3)) triple4) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is green and young, but he is also kind; He has blue eyes and red hair.
Red Eric is what folks call him, because he is quite red.
Young Fred is big and round from his mother's good cooking; Fred is the kind of kid who is nice and kind to everyone and who is red with a sunburn.
If a kind person is also young and round shaped, they will be colored blue.
A nice and blue person who's also red will be a rough person.
Incredible as it may seem, young people who are red and have kind attitudes are always round.
A cold person, who is kind in nature and young in years, is round.
I bet you didn't know that nice, kind, cold people happen to be red.
They found the ones that were round, blue, and green to be nice.