The diving trip left Charlie red and green all over, yet he remains the nice (though rather rough) guy he always has been. Eric is interestingly colored red and blue, and is also very kind. Harry wears all blue. A kind, round person will surely be red as well. Being a kind person even when you are blue is hard, but it means you are round with delight. A rough and kind person is big. Red people who are also kind often turn out to be cold from standing outdoors too long. I've been told that big, nice people are very rough. A cold and blue appearing person will be young as well. A young blue person that is kind is known for being extra nice to others, too.
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Eric is red.
("Eric" "is" "red" "+")
Eric is kind.
("Eric" "is" "kind" "+")
Eric is blue.
("Eric" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is kind and round then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and kind then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is kind and rough then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and red then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is big and nice then they are rough.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and blue then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is young and blue and kind then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Charlie is nice.
True
1
proof
[(triple3)]
("Charlie" "is" "nice" "+")
triple3
Charlie is not red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "-")
triple2
Eric is cold.
True
3
proof
[(((triple6 triple5) -> rule4) OR ((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4))]
("Eric" "is" "cold" "+")
((triple6 triple5) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is red.
("Eric" "is" "red" "+")
int2
Eric is round.
("Eric" "is" "round" "+")
int3
Eric is not cold.
False
3
inv-proof
[(((triple6 triple5) -> rule4) OR ((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4))]
("Eric" "is" "cold" "-")
((triple6 triple5) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is red.
("Eric" "is" "red" "+")
int2
Eric is round.
("Eric" "is" "round" "+")
int3
Eric is young.
True
5
proof
[(((((triple6 triple5) -> rule4) triple7) -> rule6) OR ((((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4) triple7) -> rule6))]
("Eric" "is" "young" "+")
((((triple6 triple5) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
((((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is red.
("Eric" "is" "red" "+")
int3
Eric is round.
("Eric" "is" "round" "+")
int4
Eric is not young.
False
5
inv-proof
[(((((triple6 triple5) -> rule4) triple7) -> rule6) OR ((((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4) triple7) -> rule6))]
("Eric" "is" "young" "-")
((((triple6 triple5) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
((((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is red.
("Eric" "is" "red" "+")
int3
Eric is round.
("Eric" "is" "round" "+")
int4
Eric is nice.
True
8
proof
[(((((((triple6 triple5) -> rule4) triple7) -> rule6) triple7 triple6) -> rule7) OR ((((((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4) triple7) -> rule6) triple7 triple6) -> rule7))]
("Eric" "is" "nice" "+")
((((((triple6 triple5) -> (rule4 % int3)) triple7) -> (rule6 % int2)) triple7 triple6) -> (rule7 % int1))
Eric is nice.
("Eric" "is" "nice" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
((((((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) triple7) -> (rule6 % int2)) triple7 triple6) -> (rule7 % int1))
Eric is nice.
("Eric" "is" "nice" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
Eric is red.
("Eric" "is" "red" "+")
int4
Eric is round.
("Eric" "is" "round" "+")
int5
Eric is not nice.
False
8
inv-proof
[(((((((triple6 triple5) -> rule4) triple7) -> rule6) triple7 triple6) -> rule7) OR ((((((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4) triple7) -> rule6) triple7 triple6) -> rule7))]
("Eric" "is" "nice" "-")
((((((triple6 triple5) -> (rule4 % int3)) triple7) -> (rule6 % int2)) triple7 triple6) -> (rule7 % int1))
Eric is nice.
("Eric" "is" "nice" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
((((((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) triple7) -> (rule6 % int2)) triple7 triple6) -> (rule7 % int1))
Eric is nice.
("Eric" "is" "nice" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
Eric is red.
("Eric" "is" "red" "+")
int4
Eric is round.
("Eric" "is" "round" "+")
int5
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "nice" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "cold" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Charlie is green.[(triple4)] Charlie is nice.[(triple3)] Charlie is red.[(triple2)] Charlie is rough.[(triple1)] Eric is blue.[(triple7)] Eric is kind.[(triple6)] Eric is red.[(triple5 OR ((triple6 ((triple7 triple6) -> rule2)) -> rule1))] Harry is blue.[(triple8)] @1: Eric is cold.[(((triple6 triple5) -> rule4) OR ((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4))] Eric is round.[(((triple7 triple6) -> rule2))] @2: Eric is young.[(((((triple6 triple5) -> rule4) triple7) -> rule6) OR ((((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4) triple7) -> rule6))] @3: Eric is nice.[(((((((triple6 triple5) -> rule4) triple7) -> rule6) triple7 triple6) -> rule7) OR ((((((triple6 ((triple6 ((triple7 triple6) -> rule2)) -> rule1)) -> rule4) triple7) -> rule6) triple7 triple6) -> rule7))]
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Eric is blue.
("Eric" "is" "blue" "+")
triple7
Eric is kind.
("Eric" "is" "kind" "+")
triple6
Eric is red.
("Eric" "is" "red" "+")
triple5
((triple6 ((triple7 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is round.
("Eric" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Eric is cold.
("Eric" "is" "cold" "+")
((triple6 triple5) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is red.
("Eric" "is" "red" "+")
int2
Eric is round.
("Eric" "is" "round" "+")
int3
Eric is round.
("Eric" "is" "round" "+")
((triple7 triple6) -> (rule2 % int1))
Eric is round.
("Eric" "is" "round" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
((((triple6 triple5) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
((((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple7) -> (rule6 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is red.
("Eric" "is" "red" "+")
int3
Eric is round.
("Eric" "is" "round" "+")
int4
Eric is nice.
("Eric" "is" "nice" "+")
((((((triple6 triple5) -> (rule4 % int3)) triple7) -> (rule6 % int2)) triple7 triple6) -> (rule7 % int1))
Eric is nice.
("Eric" "is" "nice" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
((((((triple6 ((triple6 ((triple7 triple6) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3)) triple7) -> (rule6 % int2)) triple7 triple6) -> (rule7 % int1))
Eric is nice.
("Eric" "is" "nice" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
Eric is red.
("Eric" "is" "red" "+")
int4
Eric is round.
("Eric" "is" "round" "+")
int5
The diving trip left Charlie red and green all over, yet he remains the nice (though rather rough) guy he always has been.
Eric is interestingly colored red and blue, and is also very kind.
Harry wears all blue.
A kind, round person will surely be red as well.
Being a kind person even when you are blue is hard, but it means you are round with delight.
A rough and kind person is big.
Red people who are also kind often turn out to be cold from standing outdoors too long.
I've been told that big, nice people are very rough.
A cold and blue appearing person will be young as well.
A young blue person that is kind is known for being extra nice to others, too.