Alan was green with envy. Though everyone thought he was a nice, young guy he was always blue. He would only focus on how round he was compared to others. To the touch Bob has rough, cold skin. Charlie has become rough with permanent red skin from working outdoors for so many years.  He always feels cold.  He is kind to both people and animals. They always call him rough Harry. When anyone can be described as nice, young and big, they can also be described as red. If you big person approaches and is cold, fear not because they are nice. Cold, red people are generally kind and big. If you meet a person who is green, big and blue, you will find them to be nice. Nice people are kind and rough when they are young. Somebody having round, cold and kind traits is also sure to be young.
If someone is nice and big and young then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is big and cold then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind and red and cold then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and green and big then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and kind and rough then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is round and kind and cold then they are young.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Alan is young.
True
1
proof
[(triple1)]
("Alan" "is" "young" "+")
triple1
Charlie is not kind.
False
1
inv-proof
[(triple10)]
("Charlie" "is" "kind" "-")
triple10
Charlie is big.
True
4
proof
[(((triple10 triple9 triple11) -> rule3))]
("Charlie" "is" "big" "+")
((triple10 triple9 triple11) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
4
inv-proof
[(((triple10 triple9 triple11) -> rule3))]
("Charlie" "is" "big" "-")
((triple10 triple9 triple11) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
True
6
proof
[(((((triple10 triple9 triple11) -> rule3) triple11) -> rule2))]
("Charlie" "is" "nice" "+")
((((triple10 triple9 triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not nice.
False
6
inv-proof
[(((((triple10 triple9 triple11) -> rule3) triple11) -> rule2))]
("Charlie" "is" "nice" "-")
((((triple10 triple9 triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
True
9
proof
[(((((((triple10 triple9 triple11) -> rule3) triple11) -> rule2) triple10 triple8) -> rule5))]
("Charlie" "is" "young" "+")
((((((triple10 triple9 triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2)) triple10 triple8) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not young.
False
9
inv-proof
[(((((((triple10 triple9 triple11) -> rule3) triple11) -> rule2) triple10 triple8) -> rule5))]
("Charlie" "is" "young" "-")
((((((triple10 triple9 triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2)) triple10 triple8) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Alan is big.
Unknown
rconc
[@1: Alan is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Alan" "is" "big" "+")
Harry is not red.
Unknown
inv-rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "red" "-")
Alan is red.
Unknown
rconc
[@2: Alan is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Alan" "is" "red" "+")
Alan is not kind.
Unknown
inv-random
[@0: Alan is kind.[CWA. Example of deepest failure = (FAIL)]]
("Alan" "is" "kind" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Alan is blue.[(triple5)] Alan is green.[(triple4)] Alan is nice.[(triple3)] Alan is round.[(triple2)] Alan is young.[(triple1)] Bob is cold.[(triple7)] Bob is rough.[(triple6)] Charlie is cold.[(triple11)] Charlie is kind.[(triple10)] Charlie is red.[(triple9)] Charlie is rough.[(triple8)] Harry is rough.[(triple12)] @1: Charlie is big.[(((triple10 triple9 triple11) -> rule3))] @2: Charlie is nice.[(((((triple10 triple9 triple11) -> rule3) triple11) -> rule2))] @3: Charlie is young.[(((((((triple10 triple9 triple11) -> rule3) triple11) -> rule2) triple10 triple8) -> rule5))]
Alan is blue.
("Alan" "is" "blue" "+")
triple5
Alan is green.
("Alan" "is" "green" "+")
triple4
Alan is nice.
("Alan" "is" "nice" "+")
triple3
Alan is round.
("Alan" "is" "round" "+")
triple2
Alan is young.
("Alan" "is" "young" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple7
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple11
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple10 triple9 triple11) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple10 triple9 triple11) -> (rule3 % int2)) triple11) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple10 triple9 triple11) -> (rule3 % int3)) triple11) -> (rule2 % int2)) triple10 triple8) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Alan was green with envy; Though everyone thought he was a nice, young guy he was always blue; He would only focus on how round he was compared to others.
To the touch Bob has rough, cold skin.
Charlie has become rough with permanent red skin from working outdoors for so many years; He always feels cold; He is kind to both people and animals.
They always call him rough Harry.
When anyone can be described as nice, young and big, they can also be described as red.
If you big person approaches and is cold, fear not because they are nice.
Cold, red people are generally kind and big.
If you meet a person who is green, big and blue, you will find them to be nice.
Nice people are kind and rough when they are young.
Somebody having round, cold and kind traits is also sure to be young.