Eric was born only a few years ago so he is young. Fred is big and rough, but he is also green, and is nice and kind when you want him to be. Harry has rough skin that is tinged with both red and green.  He has a round shape and is nice to everyone he meets. People who are rough and green with envy are young. A big and young, round someone looks red. Everyone who manages to be both rough and round are also kind. Red haired people who are nice and kind are looked up to because they are always big. Someone who happens to be cold and green and big all at once must also be round in shape. When someone is rough like sandpaper and young like a tadpole they are always round. Kind people, for example, like the ones at the bank are always blue.
Eric is young.
("Eric" "is" "young" "+")
Fred is rough.
("Fred" "is" "rough" "+")
Fred is nice.
("Fred" "is" "nice" "+")
Fred is kind.
("Fred" "is" "kind" "+")
Fred is green.
("Fred" "is" "green" "+")
Fred is big.
("Fred" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is rough and green then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is big and young and round then they are red.
((("someone" "is" "big" "+") ("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and round then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and nice and red then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and green and big then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and young then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Fred is nice.
True
1
proof
[(triple3)]
("Fred" "is" "nice" "+")
triple3
Fred is not big.
False
1
inv-proof
[(triple6)]
("Fred" "is" "big" "-")
triple6
Harry is young.
True
3
proof
[(((triple8 triple11) -> rule1))]
("Harry" "is" "young" "+")
((triple8 triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Fred is not blue.
False
2
inv-proof
[(((triple4) -> rule7) OR ((((triple2 ((triple2 ((triple2 triple5) -> rule1)) -> rule6)) -> rule3)) -> rule7))]
("Fred" "is" "blue" "-")
((triple4) -> (rule7 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
((((triple2 ((triple2 ((triple2 triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
Fred is kind.
("Fred" "is" "kind" "+")
int2
Fred is round.
("Fred" "is" "round" "+")
int3
Fred is young.
("Fred" "is" "young" "+")
int4
Harry is blue.
True
4
proof
[(((((triple8 triple7) -> rule3)) -> rule7) OR ((((triple8 ((triple8 ((triple8 triple11) -> rule1)) -> rule6)) -> rule3)) -> rule7))]
("Harry" "is" "blue" "+")
((((triple8 triple7) -> (rule3 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple8 ((triple8 ((triple8 triple11) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is not big.
False
6
inv-proof
[(((((triple8 triple7) -> rule3) triple10 triple9) -> rule4) OR ((((triple8 ((triple8 ((triple8 triple11) -> rule1)) -> rule6)) -> rule3) triple10 triple9) -> rule4))]
("Harry" "is" "big" "-")
((((triple8 triple7) -> (rule3 % int2)) triple10 triple9) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple8 ((triple8 ((triple8 triple11) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple10 triple9) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Fred is red.
True
10
proof
[(((triple6 ((triple2 triple5) -> rule1) ((triple2 ((triple2 triple5) -> rule1)) -> rule6)) -> rule2))]
("Fred" "is" "red" "+")
((triple6 ((triple2 triple5) -> (rule1 % int3)) ((triple2 ((triple2 triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fred is red.
("Fred" "is" "red" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is young.
("Fred" "is" "young" "+")
int3
Fred is not red.
False
10
inv-proof
[(((triple6 ((triple2 triple5) -> rule1) ((triple2 ((triple2 triple5) -> rule1)) -> rule6)) -> rule2))]
("Fred" "is" "red" "-")
((triple6 ((triple2 triple5) -> (rule1 % int3)) ((triple2 ((triple2 triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fred is red.
("Fred" "is" "red" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is young.
("Fred" "is" "young" "+")
int3
Eric is not big.
Unknown
inv-rconc
[@1: Eric is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Eric" "is" "big" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not red.
Unknown
inv-rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is blue.
Unknown
rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Charlie" "is" "blue" "+")
Eric is not nice.
Unknown
inv-random
[@0: Eric is nice.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "nice" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Eric is cold.
Unknown
random
[@0: Eric is cold.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "cold" "+")
@0: Eric is young.[(triple1)] Fred is big.[(triple6)] Fred is green.[(triple5)] Fred is kind.[(triple4 OR ((triple2 ((triple2 ((triple2 triple5) -> rule1)) -> rule6)) -> rule3))] Fred is nice.[(triple3)] Fred is rough.[(triple2)] Harry is green.[(triple11)] Harry is nice.[(triple10)] Harry is red.[(triple9)] Harry is rough.[(triple8)] Harry is round.[(triple7 OR ((triple8 ((triple8 triple11) -> rule1)) -> rule6))] @1: Fred is blue.[(((triple4) -> rule7) OR ((((triple2 ((triple2 ((triple2 triple5) -> rule1)) -> rule6)) -> rule3)) -> rule7))] Fred is young.[(((triple2 triple5) -> rule1))] Harry is kind.[(((triple8 triple7) -> rule3) OR ((triple8 ((triple8 ((triple8 triple11) -> rule1)) -> rule6)) -> rule3))] Harry is young.[(((triple8 triple11) -> rule1))] @2: Fred is round.[(((triple2 ((triple2 triple5) -> rule1)) -> rule6))] Harry is big.[(((((triple8 triple7) -> rule3) triple10 triple9) -> rule4) OR ((((triple8 ((triple8 ((triple8 triple11) -> rule1)) -> rule6)) -> rule3) triple10 triple9) -> rule4))] Harry is blue.[(((((triple8 triple7) -> rule3)) -> rule7) OR ((((triple8 ((triple8 ((triple8 triple11) -> rule1)) -> rule6)) -> rule3)) -> rule7))] @3: Fred is red.[(((triple6 ((triple2 triple5) -> rule1) ((triple2 ((triple2 triple5) -> rule1)) -> rule6)) -> rule2))]
Eric is young.
("Eric" "is" "young" "+")
triple1
Fred is big.
("Fred" "is" "big" "+")
triple6
Fred is green.
("Fred" "is" "green" "+")
triple5
Fred is kind.
("Fred" "is" "kind" "+")
triple4
((triple2 ((triple2 ((triple2 triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Fred is kind.
("Fred" "is" "kind" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is young.
("Fred" "is" "young" "+")
int3
Fred is nice.
("Fred" "is" "nice" "+")
triple3
Fred is rough.
("Fred" "is" "rough" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple7
((triple8 ((triple8 triple11) -> (rule1 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Fred is blue.
("Fred" "is" "blue" "+")
((triple4) -> (rule7 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
((((triple2 ((triple2 ((triple2 triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fred is blue.
("Fred" "is" "blue" "+")
int1
Fred is kind.
("Fred" "is" "kind" "+")
int2
Fred is round.
("Fred" "is" "round" "+")
int3
Fred is young.
("Fred" "is" "young" "+")
int4
Fred is young.
("Fred" "is" "young" "+")
((triple2 triple5) -> (rule1 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple8 triple7) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple8 ((triple8 ((triple8 triple11) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((triple8 triple11) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
((triple2 ((triple2 triple5) -> (rule1 % int2))) -> (rule6 % int1))
Fred is round.
("Fred" "is" "round" "+")
int1
Fred is young.
("Fred" "is" "young" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple8 triple7) -> (rule3 % int2)) triple10 triple9) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple8 ((triple8 ((triple8 triple11) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple10 triple9) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
((((triple8 triple7) -> (rule3 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple8 ((triple8 ((triple8 triple11) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Fred is red.
("Fred" "is" "red" "+")
((triple6 ((triple2 triple5) -> (rule1 % int3)) ((triple2 ((triple2 triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fred is red.
("Fred" "is" "red" "+")
int1
Fred is round.
("Fred" "is" "round" "+")
int2
Fred is young.
("Fred" "is" "young" "+")
int3
Eric was born only a few years ago so he is young.
Fred is big and rough, but he is also green, and is nice and kind when you want him to be.
Harry has rough skin that is tinged with both red and green; He has a round shape and is nice to everyone he meets.
People who are rough and green with envy are young.
A big and young, round someone looks red.
Everyone who manages to be both rough and round are also kind.
Red haired people who are nice and kind are looked up to because they are always big.
Someone who happens to be cold and green and big all at once must also be round in shape.
When someone is rough like sandpaper and young like a tadpole they are always round.
Kind people, for example, like the ones at the bank are always blue.