Although Charlie is seen as nice and round, his days of playing football have made him quite rough. Eric tends to be nice, but is young. Eric has rough blue skin. Fred is big and red, but he's young and will grow out of it. Harry grew up in a family with six other boys and that make him a rough guy.  Right now he's feeling blue because his dog is sick. If you meet a nice, young, red man, you will see that they are big too. Nice and blue people have to be big as well. A kind and cold person who is green is, surprisingly, also blue. Nice people who are big are always cold because they can't find space near the heater. Kind people who are blue with sadness and cold toward others are surprisingly red. Someone can be big and rough, but cold even though they are kind.
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Eric is young.
("Eric" "is" "young" "+")
Eric is rough.
("Eric" "is" "rough" "+")
Eric is nice.
("Eric" "is" "nice" "+")
Eric is blue.
("Eric" "is" "blue" "+")
Fred is young.
("Fred" "is" "young" "+")
Fred is red.
("Fred" "is" "red" "+")
Fred is big.
("Fred" "is" "big" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is young and nice and red then they are big.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and blue then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and cold and green then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is big and nice then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and kind and blue then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and rough and big then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Harry is rough.
True
1
proof
[(triple11)]
("Harry" "is" "rough" "+")
triple11
Harry is not rough.
False
1
inv-proof
[(triple11)]
("Harry" "is" "rough" "-")
triple11
Eric is big.
True
3
proof
[(((triple6 triple7) -> rule2))]
("Eric" "is" "big" "+")
((triple6 triple7) -> (rule2 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
Eric is not big.
False
3
inv-proof
[(((triple6 triple7) -> rule2))]
("Eric" "is" "big" "-")
((triple6 triple7) -> (rule2 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
Eric is cold.
True
5
proof
[(((((triple6 triple7) -> rule2) triple6) -> rule4))]
("Eric" "is" "cold" "+")
((((triple6 triple7) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is not cold.
False
5
inv-proof
[(((((triple6 triple7) -> rule2) triple6) -> rule4))]
("Eric" "is" "cold" "-")
((((triple6 triple7) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is kind.
True
10
proof
[(((((((triple6 triple7) -> rule2) triple6) -> rule4) triple5 ((triple6 triple7) -> rule2)) -> rule6))]
("Eric" "is" "kind" "+")
((((((triple6 triple7) -> (rule2 % int3)) triple6) -> (rule4 % int2)) triple5 ((triple6 triple7) -> (rule2 % int3))) -> (rule6 % int1))
Eric is kind.
("Eric" "is" "kind" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is not kind.
False
10
inv-proof
[(((((((triple6 triple7) -> rule2) triple6) -> rule4) triple5 ((triple6 triple7) -> rule2)) -> rule6))]
("Eric" "is" "kind" "-")
((((((triple6 triple7) -> (rule2 % int3)) triple6) -> (rule4 % int2)) triple5 ((triple6 triple7) -> (rule2 % int3))) -> (rule6 % int1))
Eric is kind.
("Eric" "is" "kind" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is red.
True
17
proof
[(((((((triple6 triple7) -> rule2) triple6) -> rule4) ((((((triple6 triple7) -> rule2) triple6) -> rule4) triple5 ((triple6 triple7) -> rule2)) -> rule6) triple7) -> rule5))]
("Eric" "is" "red" "+")
((((((triple6 triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) ((((((triple6 triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) triple5 ((triple6 triple7) -> (rule2 % int4))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is kind.
("Eric" "is" "kind" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
Eric is big.
("Eric" "is" "big" "+")
int4
Eric is not red.
False
17
inv-proof
[(((((((triple6 triple7) -> rule2) triple6) -> rule4) ((((((triple6 triple7) -> rule2) triple6) -> rule4) triple5 ((triple6 triple7) -> rule2)) -> rule6) triple7) -> rule5))]
("Eric" "is" "red" "-")
((((((triple6 triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) ((((((triple6 triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) triple5 ((triple6 triple7) -> (rule2 % int4))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is kind.
("Eric" "is" "kind" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
Eric is big.
("Eric" "is" "big" "+")
int4
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Fred is kind.
Unknown
rconc
[@1: Fred is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fred" "is" "kind" "+")
Harry is not red.
Unknown
inv-rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Harry" "is" "red" "-")
Fred is rough.
Unknown
random
[@0: Fred is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "rough" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Eric is green.
Unknown
random
[@0: Eric is green.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Fred is green.
Unknown
random
[@0: Fred is green.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "green" "+")
@0: Charlie is nice.[(triple3)] Charlie is rough.[(triple2)] Charlie is round.[(triple1)] Eric is blue.[(triple7)] Eric is nice.[(triple6)] Eric is rough.[(triple5)] Eric is young.[(triple4)] Fred is big.[(triple10)] Fred is red.[(triple9)] Fred is young.[(triple8)] Harry is blue.[(triple12)] Harry is rough.[(triple11)] @1: Eric is big.[(((triple6 triple7) -> rule2))] @2: Eric is cold.[(((((triple6 triple7) -> rule2) triple6) -> rule4))] @3: Eric is kind.[(((((((triple6 triple7) -> rule2) triple6) -> rule4) triple5 ((triple6 triple7) -> rule2)) -> rule6))] @4: Eric is red.[(((((((triple6 triple7) -> rule2) triple6) -> rule4) ((((((triple6 triple7) -> rule2) triple6) -> rule4) triple5 ((triple6 triple7) -> rule2)) -> rule6) triple7) -> rule5))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Eric is blue.
("Eric" "is" "blue" "+")
triple7
Eric is nice.
("Eric" "is" "nice" "+")
triple6
Eric is rough.
("Eric" "is" "rough" "+")
triple5
Eric is young.
("Eric" "is" "young" "+")
triple4
Fred is big.
("Fred" "is" "big" "+")
triple10
Fred is red.
("Fred" "is" "red" "+")
triple9
Fred is young.
("Fred" "is" "young" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Eric is big.
("Eric" "is" "big" "+")
((triple6 triple7) -> (rule2 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
((((triple6 triple7) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is kind.
("Eric" "is" "kind" "+")
((((((triple6 triple7) -> (rule2 % int3)) triple6) -> (rule4 % int2)) triple5 ((triple6 triple7) -> (rule2 % int3))) -> (rule6 % int1))
Eric is kind.
("Eric" "is" "kind" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is red.
("Eric" "is" "red" "+")
((((((triple6 triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) ((((((triple6 triple7) -> (rule2 % int4)) triple6) -> (rule4 % int3)) triple5 ((triple6 triple7) -> (rule2 % int4))) -> (rule6 % int2)) triple7) -> (rule5 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is kind.
("Eric" "is" "kind" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
int3
Eric is big.
("Eric" "is" "big" "+")
int4
Although Charlie is seen as nice and round, his days of playing football have made him quite rough.
Eric tends to be nice, but is young; Eric has rough blue skin.
Fred is big and red, but he's young and will grow out of it.
Harry grew up in a family with six other boys and that make him a rough guy; Right now he's feeling blue because his dog is sick.
If you meet a nice, young, red man, you will see that they are big too.
Nice and blue people have to be big as well.
A kind and cold person who is green is, surprisingly, also blue.
Nice people who are big are always cold because they can't find space near the heater.
Kind people who are blue with sadness and cold toward others are surprisingly red.
Someone can be big and rough, but cold even though they are kind.