Alan is kind and round. Being round makes him a bit blue. Dave was born only a few years ago so he is young. Fred was born only a few years ago so he is young. Young Harry is red from staying in the sun too long.  Even though he is uncomfortable from feeling cold, he is still kind to others. Santa Claus is red and kind. He is also very nice, especially to children. A quite nice person who is red and green is also big. Rough and kind people are big. If someone is a bit rough, but also nice, then they qualify as round. Julie is really nice to gardeners since she has a green thumb. An individual who is big and nice is also green.
Alan is round.
("Alan" "is" "round" "+")
Alan is kind.
("Alan" "is" "kind" "+")
Alan is blue.
("Alan" "is" "blue" "+")
Dave is young.
("Dave" "is" "young" "+")
Fred is young.
("Fred" "is" "young" "+")
Harry is young.
("Harry" "is" "young" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If someone is red and kind then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and green and nice then they are big.
((("someone" "is" "red" "+") ("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and kind then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and rough then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is big and nice then they are green.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Harry is young.
True
1
proof
[(triple6)]
("Harry" "is" "young" "+")
triple6
Harry is not young.
False
1
inv-proof
[(triple6)]
("Harry" "is" "young" "-")
triple6
Harry is nice.
True
3
proof
[(((triple7 triple8) -> rule1))]
("Harry" "is" "nice" "+")
((triple7 triple8) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
3
inv-proof
[(((triple7 triple8) -> rule1))]
("Harry" "is" "nice" "-")
((triple7 triple8) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
True
4
proof
[(((((triple7 triple8) -> rule1)) -> rule5))]
("Harry" "is" "green" "+")
((((triple7 triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple7 triple8) -> rule1)) -> rule5))]
("Harry" "is" "green" "-")
((((triple7 triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
True
9
proof
[(((triple7 ((((triple7 triple8) -> rule1)) -> rule5) ((triple7 triple8) -> rule1)) -> rule2))]
("Harry" "is" "big" "+")
((triple7 ((((triple7 triple8) -> (rule1 % int3))) -> (rule5 % int2)) ((triple7 triple8) -> (rule1 % int3))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not big.
False
9
inv-proof
[(((triple7 ((((triple7 triple8) -> rule1)) -> rule5) ((triple7 triple8) -> rule1)) -> rule2))]
("Harry" "is" "big" "-")
((triple7 ((((triple7 triple8) -> (rule1 % int3))) -> (rule5 % int2)) ((triple7 triple8) -> (rule1 % int3))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Fred is not green.
Unknown
inv-rconc
[@2: Fred is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fred" "is" "green" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "+")
Alan is not nice.
Unknown
inv-rconc
[@1: Alan is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Alan" "is" "nice" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Fred is not kind.
Unknown
inv-random
[@0: Fred is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "kind" "-")
Alan is red.
Unknown
random
[@0: Alan is red.[CWA. Example of deepest failure = (FAIL)]]
("Alan" "is" "red" "+")
@0: Alan is blue.[(triple3)] Alan is kind.[(triple2)] Alan is round.[(triple1)] Dave is young.[(triple4)] Fred is young.[(triple5)] Harry is cold.[(triple9)] Harry is kind.[(triple8)] Harry is red.[(triple7)] Harry is young.[(triple6)] @1: Harry is nice.[(((triple7 triple8) -> rule1))] @2: Harry is green.[(((((triple7 triple8) -> rule1)) -> rule5))] @3: Harry is big.[(((triple7 ((((triple7 triple8) -> rule1)) -> rule5) ((triple7 triple8) -> rule1)) -> rule2))]
Alan is blue.
("Alan" "is" "blue" "+")
triple3
Alan is kind.
("Alan" "is" "kind" "+")
triple2
Alan is round.
("Alan" "is" "round" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple4
Fred is young.
("Fred" "is" "young" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple7
Harry is young.
("Harry" "is" "young" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 triple8) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple7 triple8) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple7 ((((triple7 triple8) -> (rule1 % int3))) -> (rule5 % int2)) ((triple7 triple8) -> (rule1 % int3))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Alan is kind and round; Being round makes him a bit blue.
Dave was born only a few years ago so he is young.
Fred was born only a few years ago so he is young.
Young Harry is red from staying in the sun too long; Even though he is uncomfortable from feeling cold, he is still kind to others.
Santa Claus is red and kind; He is also very nice, especially to children.
A quite nice person who is red and green is also big.
Rough and kind people are big.
If someone is a bit rough, but also nice, then they qualify as round.
Julie is really nice to gardeners since she has a green thumb.
An individual who is big and nice is also green.