Dave wears all blue. Red Eric is what folks call him, because he is quite red. Rough Gary can be nice and kind looking green. They always call him rough Harry. A round person who is cold is big. Someone who is colored green might feel blue, but if they are kind it means they will always be nice. A quite nice person will certainly be red. Being kind and young means that if they are also blue, they are always red. When you know someone who's red, rough and nice, you'll also see that they're cold. Nice people who are green and red will also have round shapes. Everyone knows that if you are cold, kind, and big, it goes without saying that you are round.
Dave is blue.
("Dave" "is" "blue" "+")
Eric is red.
("Eric" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is cold and round then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is blue and green and kind then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and kind and young then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is nice and red and rough then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and nice and red then they are round.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and kind and big then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Gary is green.
True
1
proof
[(triple6)]
("Gary" "is" "green" "+")
triple6
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Gary is red.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "red" "+")
((triple4) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "red" "-")
((triple4) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
True
5
proof
[(((triple6 triple4 ((triple4) -> rule3)) -> rule6))]
("Gary" "is" "round" "+")
((triple6 triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not cold.
False
5
inv-proof
[(((triple4 ((triple4) -> rule3) triple3) -> rule5))]
("Gary" "is" "cold" "-")
((triple4 ((triple4) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
True
11
proof
[(((((triple4 ((triple4) -> rule3) triple3) -> rule5) ((triple6 triple4 ((triple4) -> rule3)) -> rule6)) -> rule1))]
("Gary" "is" "big" "+")
((((triple4 ((triple4) -> (rule3 % int4)) triple3) -> (rule5 % int3)) ((triple6 triple4 ((triple4) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is not big.
False
11
inv-proof
[(((((triple4 ((triple4) -> rule3) triple3) -> rule5) ((triple6 triple4 ((triple4) -> rule3)) -> rule6)) -> rule1))]
("Gary" "is" "big" "-")
((((triple4 ((triple4) -> (rule3 % int4)) triple3) -> (rule5 % int3)) ((triple6 triple4 ((triple4) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Harry" "is" "big" "-")
Eric is round.
Unknown
rconc
[@1: Eric is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Eric" "is" "round" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Eric is cold.
Unknown
rconc
[@1: Eric is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Eric" "is" "cold" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Eric is young.
Unknown
random
[@0: Eric is young.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "young" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is blue.[(triple1)] Eric is red.[(triple2)] Gary is green.[(triple6)] Gary is kind.[(triple5)] Gary is nice.[(triple4)] Gary is rough.[(triple3)] Harry is rough.[(triple7)] @1: Gary is red.[(((triple4) -> rule3))] @2: Gary is cold.[(((triple4 ((triple4) -> rule3) triple3) -> rule5))] Gary is round.[(((triple6 triple4 ((triple4) -> rule3)) -> rule6))] @3: Gary is big.[(((((triple4 ((triple4) -> rule3) triple3) -> rule5) ((triple6 triple4 ((triple4) -> rule3)) -> rule6)) -> rule1))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Eric is red.
("Eric" "is" "red" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
((triple4) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple4 ((triple4) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple6 triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple4 ((triple4) -> (rule3 % int4)) triple3) -> (rule5 % int3)) ((triple6 triple4 ((triple4) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Dave wears all blue.
Red Eric is what folks call him, because he is quite red.
Rough Gary can be nice and kind looking green.
They always call him rough Harry.
A round person who is cold is big.
Someone who is colored green might feel blue, but if they are kind it means they will always be nice.
A quite nice person will certainly be red.
Being kind and young means that if they are also blue, they are always red.
When you know someone who's red, rough and nice, you'll also see that they're cold.
Nice people who are green and red will also have round shapes.
Everyone knows that if you are cold, kind, and big, it goes without saying that you are round.