If you met Charlie you will see that he is round and red, but he is cold. Big blue Dave is nice and young. Fred who is big in stature is almost always nice even when he is cold. Harry is a man who is both round and rough. People who are red and round are usually assumed to be green. You will find that a big, young, blue person is also quite round. If a kind person is also young and round shaped, they will be colored blue. A nice and colored blue person will be rather big. Someone nice and kind with a round belly that shakes when they laugh will also have rough hands from spending time outdoors with the reindeer. A person who is kind but also rough and is also colored blue, will be shaped round. Blue people round with fat are red from too much time in the sun.
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is big.
("Dave" "is" "big" "+")
Fred is nice.
("Fred" "is" "nice" "+")
Fred is cold.
("Fred" "is" "cold" "+")
Fred is big.
("Fred" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is red and round then they are green.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is young and big and blue then they are round.
((("someone" "is" "young" "+") ("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is kind and young and round then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and nice then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and round and nice then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind and rough and blue then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is blue and round then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Fred is cold.
True
1
proof
[(triple9)]
("Fred" "is" "cold" "+")
triple9
Fred is not big.
False
1
inv-proof
[(triple10)]
("Fred" "is" "big" "-")
triple10
Dave is round.
True
4
proof
[(((triple4 triple7 triple6) -> rule2) OR ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2))]
("Dave" "is" "round" "+")
((triple4 triple7 triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple4 ((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not round.
False
4
inv-proof
[(((triple4 triple7 triple6) -> rule2) OR ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2))]
("Dave" "is" "round" "-")
((triple4 triple7 triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple4 ((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
True
6
proof
[(((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) OR ((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7))]
("Dave" "is" "red" "+")
((triple6 ((triple4 triple7 triple6) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not red.
False
6
inv-proof
[(((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) OR ((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7))]
("Dave" "is" "red" "-")
((triple6 ((triple4 triple7 triple6) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is green.
True
11
proof
[(((((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) ((triple4 triple7 triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7) ((triple4 triple7 triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7) ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule1))]
("Dave" "is" "green" "+")
((((triple6 ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple6 ((triple4 triple7 triple6) -> (rule2 % int4))) -> (rule7 % int3)) ((triple4 ((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int4))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Dave is not green.
False
11
inv-proof
[(((((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) ((triple4 triple7 triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7) ((triple4 triple7 triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7) ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule1))]
("Dave" "is" "green" "-")
((((triple6 ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple6 ((triple4 triple7 triple6) -> (rule2 % int4))) -> (rule7 % int3)) ((triple4 ((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int4))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "big" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "big" "-")
Fred is round.
Unknown
rconc
[@1: Fred is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fred" "is" "round" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Fred is young.
Unknown
random
[@0: Fred is young.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "young" "+")
@0: Charlie is cold.[(triple3)] Charlie is red.[(triple2)] Charlie is round.[(triple1)] Dave is big.[(triple7 OR ((triple6 triple5) -> rule4))] Dave is blue.[(triple6)] Dave is nice.[(triple5)] Dave is young.[(triple4)] Fred is big.[(triple10)] Fred is cold.[(triple9)] Fred is nice.[(triple8)] Harry is rough.[(triple12)] Harry is round.[(triple11)] @1: Charlie is green.[(((triple2 triple1) -> rule1))] Dave is round.[(((triple4 triple7 triple6) -> rule2) OR ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2))] @2: Dave is red.[(((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) OR ((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7))] @3: Dave is green.[(((((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) ((triple4 triple7 triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 triple7 triple6) -> rule2)) -> rule7) ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7) ((triple4 triple7 triple6) -> rule2)) -> rule1) OR ((((triple6 ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule7) ((triple4 ((triple6 triple5) -> rule4) triple6) -> rule2)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple7
((triple6 triple5) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple4
Fred is big.
("Fred" "is" "big" "+")
triple10
Fred is cold.
("Fred" "is" "cold" "+")
triple9
Fred is nice.
("Fred" "is" "nice" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple11
Charlie is green.
("Charlie" "is" "green" "+")
((triple2 triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple4 triple7 triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple4 ((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple6 ((triple4 triple7 triple6) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((triple6 ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple6 ((triple4 triple7 triple6) -> (rule2 % int4))) -> (rule7 % int3)) ((triple4 ((triple6 triple5) -> (rule4 % int2)) triple6) -> (rule2 % int4))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 triple7 triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
((((triple6 ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule7 % int2)) ((triple4 ((triple6 triple5) -> (rule4 % int4)) triple6) -> (rule2 % int3))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
int4
If you met Charlie you will see that he is round and red, but he is cold.
Big blue Dave is nice and young.
Fred who is big in stature is almost always nice even when he is cold.
Harry is a man who is both round and rough.
People who are red and round are usually assumed to be green.
You will find that a big, young, blue person is also quite round.
If a kind person is also young and round shaped, they will be colored blue.
A nice and colored blue person will be rather big.
Someone nice and kind with a round belly that shakes when they laugh will also have rough hands from spending time outdoors with the reindeer.
A person who is kind but also rough and is also colored blue, will be shaped round.
Blue people round with fat are red from too much time in the sun.