Charlie always goes out of his way to show that he is kind to people. Dave always goes out of his way to show that he is kind to people. In the snow sits Eric, crying from being cold. Harry is cold and blue. He is round and has red rosy cheeks. He is green with envy of those who are happy. People that tend to be big and green also tend to be cold. This person is nice and young, also round, which makes them cold. Cold people who are young and green are actually nice. Anyone in the world who is nice, red, and young, is simultaneously rough. Being green, blue, and red all point to how young someone was.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Eric is cold.
("Eric" "is" "cold" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is big and green then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is young and nice and round then they are cold.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and green and young then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and red and young then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and blue and red then they are young.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Harry is blue.
True
1
proof
[(triple8)]
("Harry" "is" "blue" "+")
triple8
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Harry is young.
True
4
proof
[(((triple6 triple8 triple5) -> rule5))]
("Harry" "is" "young" "+")
((triple6 triple8 triple5) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
4
inv-proof
[(((triple6 triple8 triple5) -> rule5))]
("Harry" "is" "young" "-")
((triple6 triple8 triple5) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
True
7
proof
[(((triple7 triple6 ((triple6 triple8 triple5) -> rule5)) -> rule3))]
("Harry" "is" "nice" "+")
((triple7 triple6 ((triple6 triple8 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not nice.
False
7
inv-proof
[(((triple7 triple6 ((triple6 triple8 triple5) -> rule5)) -> rule3))]
("Harry" "is" "nice" "-")
((triple7 triple6 ((triple6 triple8 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
True
13
proof
[(((((triple7 triple6 ((triple6 triple8 triple5) -> rule5)) -> rule3) triple5 ((triple6 triple8 triple5) -> rule5)) -> rule4))]
("Harry" "is" "rough" "+")
((((triple7 triple6 ((triple6 triple8 triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple5 ((triple6 triple8 triple5) -> (rule5 % int3))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not rough.
False
13
inv-proof
[(((((triple7 triple6 ((triple6 triple8 triple5) -> rule5)) -> rule3) triple5 ((triple6 triple8 triple5) -> rule5)) -> rule4))]
("Harry" "is" "rough" "-")
((((triple7 triple6 ((triple6 triple8 triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple5 ((triple6 triple8 triple5) -> (rule5 % int3))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "nice" "+")
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Eric is rough.
Unknown
rconc
[@1: Eric is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Eric" "is" "rough" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Eric is blue.
Unknown
random
[@0: Eric is blue.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "blue" "+")
Eric is not round.
Unknown
inv-random
[@0: Eric is round.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "round" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Charlie is kind.[(triple1)] Dave is kind.[(triple2)] Eric is cold.[(triple3)] Harry is blue.[(triple8)] Harry is cold.[(triple7)] Harry is green.[(triple6)] Harry is red.[(triple5)] Harry is round.[(triple4)] @1: Harry is young.[(((triple6 triple8 triple5) -> rule5))] @2: Harry is nice.[(((triple7 triple6 ((triple6 triple8 triple5) -> rule5)) -> rule3))] @3: Harry is rough.[(((((triple7 triple6 ((triple6 triple8 triple5) -> rule5)) -> rule3) triple5 ((triple6 triple8 triple5) -> rule5)) -> rule4))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Eric is cold.
("Eric" "is" "cold" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple4
Harry is young.
("Harry" "is" "young" "+")
((triple6 triple8 triple5) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 triple6 ((triple6 triple8 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7 triple6 ((triple6 triple8 triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple5 ((triple6 triple8 triple5) -> (rule5 % int3))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie always goes out of his way to show that he is kind to people.
Dave always goes out of his way to show that he is kind to people.
In the snow sits Eric, crying from being cold.
Harry is cold and blue; He is round and has red rosy cheeks; He is green with envy of those who are happy.
People that tend to be big and green also tend to be cold.
This person is nice and young, also round, which makes them cold.
Cold people who are young and green are actually nice.
Anyone in the world who is nice, red, and young, is simultaneously rough.
Being green, blue, and red all point to how young someone was.