When you see Dave, you will notice he is cold, big and kind. Eric 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. Fred is a big, young boy who is very kind.  He stands out because his skin is blue and green. Harry is a man who is both round and rough. A young and cold person is red. A big, kind someone could also be cold in a green dress. A big person who looks blue is also going to look young. Kind big people are green and young. Cold people with rough, green skin are young. On a voyage across the sea it is always the round, kind people, green with seasickness that turn red with embarrassment.
If someone is cold and young then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is big and kind and cold then they are green.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is blue and big then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and green and big then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is cold and rough and green then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and green and round then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Dave is big.
True
1
proof
[(triple3)]
("Dave" "is" "big" "+")
triple3
Fred is not green.
False
1
inv-proof
[(triple8)]
("Fred" "is" "green" "-")
triple8
Dave is green.
True
4
proof
[(((triple3 triple1 triple2) -> rule2))]
("Dave" "is" "green" "+")
((triple3 triple1 triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
4
inv-proof
[(((triple3 triple1 triple2) -> rule2))]
("Dave" "is" "green" "-")
((triple3 triple1 triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
True
7
proof
[(((triple1 ((triple3 triple1 triple2) -> rule2) triple3) -> rule4))]
("Dave" "is" "young" "+")
((triple1 ((triple3 triple1 triple2) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not young.
False
7
inv-proof
[(((triple1 ((triple3 triple1 triple2) -> rule2) triple3) -> rule4))]
("Dave" "is" "young" "-")
((triple1 ((triple3 triple1 triple2) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
True
9
proof
[(((triple2 ((triple1 ((triple3 triple1 triple2) -> rule2) triple3) -> rule4)) -> rule1))]
("Dave" "is" "red" "+")
((triple2 ((triple1 ((triple3 triple1 triple2) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not red.
False
9
inv-proof
[(((triple2 ((triple1 ((triple3 triple1 triple2) -> rule2) triple3) -> rule4)) -> rule1))]
("Dave" "is" "red" "-")
((triple2 ((triple1 ((triple3 triple1 triple2) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Eric is not green.
Unknown
inv-rconc
[@1: Eric is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Eric" "is" "green" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Eric is not red.
Unknown
inv-rconc
[@1: Eric is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Eric" "is" "red" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Fred is not round.
Unknown
inv-random
[@0: Fred is round.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is big.[(triple3)] Dave is cold.[(triple2)] Dave is kind.[(triple1)] Eric is blue.[(triple5)] Eric is rough.[(triple4)] Fred is big.[(triple10)] Fred is blue.[(triple9)] Fred is green.[(triple8)] Fred is kind.[(triple7)] Fred is young.[(triple6 OR ((triple9 triple10) -> rule3) OR ((triple7 triple8 triple10) -> rule4))] Harry is rough.[(triple12)] Harry is round.[(triple11)] @1: Dave is green.[(((triple3 triple1 triple2) -> rule2))] @2: Dave is young.[(((triple1 ((triple3 triple1 triple2) -> rule2) triple3) -> rule4))] @3: Dave is red.[(((triple2 ((triple1 ((triple3 triple1 triple2) -> rule2) triple3) -> rule4)) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Eric is blue.
("Eric" "is" "blue" "+")
triple5
Eric is rough.
("Eric" "is" "rough" "+")
triple4
Fred is big.
("Fred" "is" "big" "+")
triple10
Fred is blue.
("Fred" "is" "blue" "+")
triple9
Fred is green.
("Fred" "is" "green" "+")
triple8
Fred is kind.
("Fred" "is" "kind" "+")
triple7
Fred is young.
("Fred" "is" "young" "+")
triple6
((triple9 triple10) -> (rule3 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
((triple7 triple8 triple10) -> (rule4 % int1))
Fred is young.
("Fred" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple11
Dave is green.
("Dave" "is" "green" "+")
((triple3 triple1 triple2) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1 ((triple3 triple1 triple2) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple2 ((triple1 ((triple3 triple1 triple2) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
When you see Dave, you will notice he is cold, big and kind.
Eric 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.
Fred is a big, young boy who is very kind; He stands out because his skin is blue and green.
Harry is a man who is both round and rough.
A young and cold person is red.
A big, kind someone could also be cold in a green dress.
A big person who looks blue is also going to look young.
Kind big people are green and young.
Cold people with rough, green skin are young.
On a voyage across the sea it is always the round, kind people, green with seasickness that turn red with embarrassment.