Others enjoy Bob's company because he is so nice and kind. Charlie became so big that he is now very round. Fortunately the rather green man is still nice. In the snow sits Dave, crying from being cold. Fred ate some rotten meat and now feels green. A kind, round person will surely be red as well. Young people who rough around in the cold are known to be very red. A nice person who is always seen to be wearing green clothes will be rather big in size. It's said that any person with blue skin, round bones, and big feet is kind. Someone who's blue, nice and round will also be someone who's green. People who are rough and cold, but also nice, are considered green. When a round individual is nice to others, they are also feeling blue.
If someone is kind and round then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and young and cold then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is green and nice then they are big.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and round and big then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue and nice and round then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is rough and cold and nice then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is round and nice then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple5 OR ((((triple3 triple4) -> rule7) triple4 triple3) -> rule5))]
("Charlie" "is" "green" "-")
triple5
((((triple3 triple4) -> (rule7 % int2)) triple4 triple3) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is blue.
True
3
proof
[(((triple3 triple4) -> rule7))]
("Charlie" "is" "blue" "+")
((triple3 triple4) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is not blue.
False
3
inv-proof
[(((triple3 triple4) -> rule7))]
("Charlie" "is" "blue" "-")
((triple3 triple4) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
True
6
proof
[(((((triple3 triple4) -> rule7) triple3 triple6) -> rule4) OR ((((triple3 triple4) -> rule7) triple3 ((triple5 triple4) -> rule3)) -> rule4) OR ((((triple3 triple4) -> rule7) triple3 ((((((triple3 triple4) -> rule7) triple4 triple3) -> rule5) triple4) -> rule3)) -> rule4))]
("Charlie" "is" "kind" "+")
((((triple3 triple4) -> (rule7 % int2)) triple3 triple6) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3 triple4) -> (rule7 % int3)) triple3 ((triple5 triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple3 triple4) -> (rule7 % int4)) triple3 ((((((triple3 triple4) -> (rule7 % int4)) triple4 triple3) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is not kind.
False
6
inv-proof
[(((((triple3 triple4) -> rule7) triple3 triple6) -> rule4) OR ((((triple3 triple4) -> rule7) triple3 ((triple5 triple4) -> rule3)) -> rule4) OR ((((triple3 triple4) -> rule7) triple3 ((((((triple3 triple4) -> rule7) triple4 triple3) -> rule5) triple4) -> rule3)) -> rule4))]
("Charlie" "is" "kind" "-")
((((triple3 triple4) -> (rule7 % int2)) triple3 triple6) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3 triple4) -> (rule7 % int3)) triple3 ((triple5 triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple3 triple4) -> (rule7 % int4)) triple3 ((((((triple3 triple4) -> (rule7 % int4)) triple4 triple3) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is red.
True
8
proof
[(((((((triple3 triple4) -> rule7) triple3 triple6) -> rule4) triple3) -> rule1) OR ((((((triple3 triple4) -> rule7) triple3 ((triple5 triple4) -> rule3)) -> rule4) triple3) -> rule1) OR ((((((triple3 triple4) -> rule7) triple3 ((((((triple3 triple4) -> rule7) triple4 triple3) -> rule5) triple4) -> rule3)) -> rule4) triple3) -> rule1))]
("Charlie" "is" "red" "+")
((((((triple3 triple4) -> (rule7 % int3)) triple3 triple6) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple3 triple4) -> (rule7 % int4)) triple3 ((triple5 triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
((((((triple3 triple4) -> (rule7 % int5)) triple3 ((((((triple3 triple4) -> (rule7 % int5)) triple4 triple3) -> (rule5 % int4)) triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
int5
Charlie is not red.
False
8
inv-proof
[(((((((triple3 triple4) -> rule7) triple3 triple6) -> rule4) triple3) -> rule1) OR ((((((triple3 triple4) -> rule7) triple3 ((triple5 triple4) -> rule3)) -> rule4) triple3) -> rule1) OR ((((((triple3 triple4) -> rule7) triple3 ((((((triple3 triple4) -> rule7) triple4 triple3) -> rule5) triple4) -> rule3)) -> rule4) triple3) -> rule1))]
("Charlie" "is" "red" "-")
((((((triple3 triple4) -> (rule7 % int3)) triple3 triple6) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple3 triple4) -> (rule7 % int4)) triple3 ((triple5 triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
((((((triple3 triple4) -> (rule7 % int5)) triple3 ((((((triple3 triple4) -> (rule7 % int5)) triple4 triple3) -> (rule5 % int4)) triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
int5
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "blue" "+")
Fred is not red.
Unknown
inv-rconc
[@1: Fred is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fred" "is" "red" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "red" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Fred is rough.
Unknown
random
[@0: Fred is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "rough" "+")
@0: Bob is kind.[(triple2)] Bob is nice.[(triple1)] Charlie is big.[(triple6 OR ((triple5 triple4) -> rule3) OR ((((((triple3 triple4) -> rule7) triple4 triple3) -> rule5) triple4) -> rule3))] Charlie is green.[(triple5 OR ((((triple3 triple4) -> rule7) triple4 triple3) -> rule5))] Charlie is nice.[(triple4)] Charlie is round.[(triple3)] Dave is cold.[(triple7)] Fred is green.[(triple8)] @1: Charlie is blue.[(((triple3 triple4) -> rule7))] @2: Charlie is kind.[(((((triple3 triple4) -> rule7) triple3 triple6) -> rule4) OR ((((triple3 triple4) -> rule7) triple3 ((triple5 triple4) -> rule3)) -> rule4) OR ((((triple3 triple4) -> rule7) triple3 ((((((triple3 triple4) -> rule7) triple4 triple3) -> rule5) triple4) -> rule3)) -> rule4))] @3: Charlie is red.[(((((((triple3 triple4) -> rule7) triple3 triple6) -> rule4) triple3) -> rule1) OR ((((((triple3 triple4) -> rule7) triple3 ((triple5 triple4) -> rule3)) -> rule4) triple3) -> rule1) OR ((((((triple3 triple4) -> rule7) triple3 ((((((triple3 triple4) -> rule7) triple4 triple3) -> rule5) triple4) -> rule3)) -> rule4) triple3) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple6
((triple5 triple4) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((((triple3 triple4) -> (rule7 % int3)) triple4 triple3) -> (rule5 % int2)) triple4) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple5
((((triple3 triple4) -> (rule7 % int2)) triple4 triple3) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Fred is green.
("Fred" "is" "green" "+")
triple8
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3 triple4) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple3 triple4) -> (rule7 % int2)) triple3 triple6) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple3 triple4) -> (rule7 % int3)) triple3 ((triple5 triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple3 triple4) -> (rule7 % int4)) triple3 ((((((triple3 triple4) -> (rule7 % int4)) triple4 triple3) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple3 triple4) -> (rule7 % int3)) triple3 triple6) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple3 triple4) -> (rule7 % int4)) triple3 ((triple5 triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
((((((triple3 triple4) -> (rule7 % int5)) triple3 ((((((triple3 triple4) -> (rule7 % int5)) triple4 triple3) -> (rule5 % int4)) triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
int5
Others enjoy Bob's company because he is so nice and kind.
Charlie became so big that he is now very round; Fortunately the rather green man is still nice.
In the snow sits Dave, crying from being cold.
Fred ate some rotten meat and now feels green.
A kind, round person will surely be red as well.
Young people who rough around in the cold are known to be very red.
A nice person who is always seen to be wearing green clothes will be rather big in size.
It's said that any person with blue skin, round bones, and big feet is kind.
Someone who's blue, nice and round will also be someone who's green.
People who are rough and cold, but also nice, are considered green.
When a round individual is nice to others, they are also feeling blue.