Charlie is a big, young boy who is very kind.  He stands out because his skin is blue and green. Eric, like all young people, is nice. Fred is kind and round. Being round makes him a bit blue. To the touch Harry has rough, cold skin. A big person who is red and nice to others is also young. Santa Claus is red and kind. He is also very nice, especially to children. Young people tend to be blue all the time and rough. You will always find a cold, rough, red person to also be a round person. Rough people who are nice and have green thumbs are almost always young. When someone is big with rough skin they will look red.
Charlie is young.
("Charlie" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Eric is young.
("Eric" "is" "young" "+")
Eric is nice.
("Eric" "is" "nice" "+")
Fred is round.
("Fred" "is" "round" "+")
Fred is kind.
("Fred" "is" "kind" "+")
Fred is blue.
("Fred" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is red and nice and big then they are young.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is red and kind then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and young then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and rough and red then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is nice and green and rough then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is rough and big then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Harry is rough.
True
1
proof
[(triple11)]
("Harry" "is" "rough" "+")
triple11
Fred is not blue.
False
1
inv-proof
[(triple10)]
("Fred" "is" "blue" "-")
triple10
Charlie is rough.
True
3
proof
[(((triple4 triple1) -> rule3))]
("Charlie" "is" "rough" "+")
((triple4 triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
3
inv-proof
[(((triple4 triple1) -> rule3))]
("Charlie" "is" "rough" "-")
((triple4 triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
True
5
proof
[(((((triple4 triple1) -> rule3) triple5) -> rule6))]
("Charlie" "is" "red" "+")
((((triple4 triple1) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not red.
False
5
inv-proof
[(((((triple4 triple1) -> rule3) triple5) -> rule6))]
("Charlie" "is" "red" "-")
((((triple4 triple1) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
True
7
proof
[(((((((triple4 triple1) -> rule3) triple5) -> rule6) triple2) -> rule2))]
("Charlie" "is" "nice" "+")
((((((triple4 triple1) -> (rule3 % int3)) triple5) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not nice.
False
7
inv-proof
[(((((((triple4 triple1) -> rule3) triple5) -> rule6) triple2) -> rule2))]
("Charlie" "is" "nice" "-")
((((((triple4 triple1) -> (rule3 % int3)) triple5) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Fred is not red.
Unknown
inv-rconc
[@1: Fred is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fred" "is" "red" "-")
Harry is round.
Unknown
rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Eric is rough.
Unknown
rconc
[@1: Eric is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Eric" "is" "rough" "+")
Eric is not kind.
Unknown
inv-random
[@0: Eric is kind.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "kind" "-")
Eric is blue.
Unknown
random
[@0: Eric is blue.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "blue" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is big.[(triple5)] Charlie is blue.[(triple4)] Charlie is green.[(triple3)] Charlie is kind.[(triple2)] Charlie is young.[(triple1)] Eric is nice.[(triple7)] Eric is young.[(triple6)] Fred is blue.[(triple10)] Fred is kind.[(triple9)] Fred is round.[(triple8)] Harry is cold.[(triple12)] Harry is rough.[(triple11)] @1: Charlie is rough.[(((triple4 triple1) -> rule3))] @2: Charlie is red.[(((((triple4 triple1) -> rule3) triple5) -> rule6))] @3: Charlie is nice.[(((((((triple4 triple1) -> rule3) triple5) -> rule6) triple2) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Eric is nice.
("Eric" "is" "nice" "+")
triple7
Eric is young.
("Eric" "is" "young" "+")
triple6
Fred is blue.
("Fred" "is" "blue" "+")
triple10
Fred is kind.
("Fred" "is" "kind" "+")
triple9
Fred is round.
("Fred" "is" "round" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4 triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple4 triple1) -> (rule3 % int2)) triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple4 triple1) -> (rule3 % int3)) triple5) -> (rule6 % int2)) triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is a big, young boy who is very kind; He stands out because his skin is blue and green.
Eric, like all young people, is nice.
Fred is kind and round; Being round makes him a bit blue.
To the touch Harry has rough, cold skin.
A big person who is red and nice to others is also young.
Santa Claus is red and kind; He is also very nice, especially to children.
Young people tend to be blue all the time and rough.
You will always find a cold, rough, red person to also be a round person.
Rough people who are nice and have green thumbs are almost always young.
When someone is big with rough skin they will look red.