Charlie ate some rotten meat and now feels green. Dave vowed to always be rough, cold, blue, and big as possible. Fred ate some rotten meat and now feels green. Even though Gary is still young, he is already very round.  Gary is a nice guy and when he gets cold his skin turns blue. A cold, rough person is also round. A green, inexperienced person with a round shape who is kind to others gets very red when in the sun. If you have a big and round shape then you are going to be young, too. You will probably see that big, round, blue people are green, too. When you know someone who is young and green you can count on them being nice to everyone.
Charlie is green.
("Charlie" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is big.
("Dave" "is" "big" "+")
Fred is green.
("Fred" "is" "green" "+")
Gary is young.
("Gary" "is" "young" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If someone is rough and cold then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is green and round and kind then they are red.
((("someone" "is" "green" "+") ("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is round and big then they are young.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is round and big and blue then they are green.
((("someone" "is" "round" "+") ("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If someone is young and green then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Gary is round.
True
1
proof
[(triple8)]
("Gary" "is" "round" "+")
triple8
Dave is not cold.
False
1
inv-proof
[(triple3)]
("Dave" "is" "cold" "-")
triple3
Dave is round.
True
3
proof
[(((triple2 triple3) -> rule1))]
("Dave" "is" "round" "+")
((triple2 triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("Dave" "is" "round" "-")
((triple2 triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
True
5
proof
[(((((triple2 triple3) -> rule1) triple5) -> rule3))]
("Dave" "is" "young" "+")
((((triple2 triple3) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not green.
False
6
inv-proof
[(((((triple2 triple3) -> rule1) triple5 triple4) -> rule4))]
("Dave" "is" "green" "-")
((((triple2 triple3) -> (rule1 % int2)) triple5 triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
True
12
proof
[(((((((triple2 triple3) -> rule1) triple5) -> rule3) ((((triple2 triple3) -> rule1) triple5 triple4) -> rule4)) -> rule5))]
("Dave" "is" "nice" "+")
((((((triple2 triple3) -> (rule1 % int4)) triple5) -> (rule3 % int3)) ((((triple2 triple3) -> (rule1 % int4)) triple5 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not nice.
False
12
inv-proof
[(((((((triple2 triple3) -> rule1) triple5) -> rule3) ((((triple2 triple3) -> rule1) triple5 triple4) -> rule4)) -> rule5))]
("Dave" "is" "nice" "-")
((((((triple2 triple3) -> (rule1 % int4)) triple5) -> (rule3 % int3)) ((((triple2 triple3) -> (rule1 % int4)) triple5 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Fred is red.
Unknown
rconc
[@1: Fred is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fred" "is" "red" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "+")
Fred is not cold.
Unknown
inv-random
[@0: Fred is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "cold" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Charlie is green.[(triple1)] Dave is big.[(triple5)] Dave is blue.[(triple4)] Dave is cold.[(triple3)] Dave is rough.[(triple2)] Fred is green.[(triple6)] Gary is blue.[(triple11)] Gary is cold.[(triple10)] Gary is nice.[(triple9)] Gary is round.[(triple8)] Gary is young.[(triple7)] @1: Dave is round.[(((triple2 triple3) -> rule1))] @2: Dave is green.[(((((triple2 triple3) -> rule1) triple5 triple4) -> rule4))] Dave is young.[(((((triple2 triple3) -> rule1) triple5) -> rule3))] @3: Dave is nice.[(((((((triple2 triple3) -> rule1) triple5) -> rule3) ((((triple2 triple3) -> rule1) triple5 triple4) -> rule4)) -> rule5))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Fred is green.
("Fred" "is" "green" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is nice.
("Gary" "is" "nice" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple8
Gary is young.
("Gary" "is" "young" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
((triple2 triple3) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((((triple2 triple3) -> (rule1 % int2)) triple5 triple4) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple2 triple3) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple2 triple3) -> (rule1 % int4)) triple5) -> (rule3 % int3)) ((((triple2 triple3) -> (rule1 % int4)) triple5 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Charlie ate some rotten meat and now feels green.
Dave vowed to always be rough, cold, blue, and big as possible.
Fred ate some rotten meat and now feels green.
Even though Gary is still young, he is already very round; Gary is a nice guy and when he gets cold his skin turns blue.
A cold, rough person is also round.
A green, inexperienced person with a round shape who is kind to others gets very red when in the sun.
If you have a big and round shape then you are going to be young, too.
You will probably see that big, round, blue people are green, too.
When you know someone who is young and green you can count on them being nice to everyone.