Big, red Dave is quite kind. Eric is a person both green and big. Fred always goes out of his way to show that he is kind to people. Harry is kind and has rough, round hands that are red. Harry is green with envy when he looks at people who don't have to work. A person who is nice and green with envy is round. A kind and green person who is rough around the edges is cold. Rough and green people are also nice. Cold and kind people tend to be blue. Anyone who is round and also cold will surely be big as well. People with rough red and blue skin are young.
Dave is red.
("Dave" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is big.
("Dave" "is" "big" "+")
Eric is green.
("Eric" "is" "green" "+")
Eric is big.
("Eric" "is" "big" "+")
Fred is kind.
("Fred" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is nice and green then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is green and rough and kind then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and green then they are nice.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and kind then they are blue.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and cold then they are big.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and red and blue then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple3)]
("Dave" "is" "big" "-")
triple3
Harry is nice.
True
3
proof
[(((triple8 triple11) -> rule3))]
("Harry" "is" "nice" "+")
((triple8 triple11) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not cold.
False
4
inv-proof
[(((triple11 triple8 triple10) -> rule2))]
("Harry" "is" "cold" "-")
((triple11 triple8 triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
True
6
proof
[(((triple7 ((triple11 triple8 triple10) -> rule2)) -> rule5) OR ((((((triple8 triple11) -> rule3) triple11) -> rule1) ((triple11 triple8 triple10) -> rule2)) -> rule5))]
("Harry" "is" "big" "+")
((triple7 ((triple11 triple8 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple8 triple11) -> (rule3 % int4)) triple11) -> (rule1 % int3)) ((triple11 triple8 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is not big.
False
6
inv-proof
[(((triple7 ((triple11 triple8 triple10) -> rule2)) -> rule5) OR ((((((triple8 triple11) -> rule3) triple11) -> rule1) ((triple11 triple8 triple10) -> rule2)) -> rule5))]
("Harry" "is" "big" "-")
((triple7 ((triple11 triple8 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple8 triple11) -> (rule3 % int4)) triple11) -> (rule1 % int3)) ((triple11 triple8 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is young.
True
9
proof
[(((triple8 triple9 ((((triple11 triple8 triple10) -> rule2) triple10) -> rule4)) -> rule6))]
("Harry" "is" "young" "+")
((triple8 triple9 ((((triple11 triple8 triple10) -> (rule2 % int3)) triple10) -> (rule4 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not young.
False
9
inv-proof
[(((triple8 triple9 ((((triple11 triple8 triple10) -> rule2) triple10) -> rule4)) -> rule6))]
("Harry" "is" "young" "-")
((triple8 triple9 ((((triple11 triple8 triple10) -> (rule2 % int3)) triple10) -> (rule4 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Eric is not blue.
Unknown
inv-rconc
[@1: Eric is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Eric" "is" "blue" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "nice" "+")
Fred is not rough.
Unknown
inv-random
[@0: Fred is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Fred is not green.
Unknown
inv-random
[@0: Fred is green.[CWA. Example of deepest failure = (FAIL)]]
("Fred" "is" "green" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Dave is big.[(triple3)] Dave is kind.[(triple2)] Dave is red.[(triple1)] Eric is big.[(triple5)] Eric is green.[(triple4)] Fred is kind.[(triple6)] Harry is green.[(triple11)] Harry is kind.[(triple10)] Harry is red.[(triple9)] Harry is rough.[(triple8)] Harry is round.[(triple7 OR ((((triple8 triple11) -> rule3) triple11) -> rule1))] @1: Harry is cold.[(((triple11 triple8 triple10) -> rule2))] Harry is nice.[(((triple8 triple11) -> rule3))] @2: Harry is big.[(((triple7 ((triple11 triple8 triple10) -> rule2)) -> rule5) OR ((((((triple8 triple11) -> rule3) triple11) -> rule1) ((triple11 triple8 triple10) -> rule2)) -> rule5))] Harry is blue.[(((((triple11 triple8 triple10) -> rule2) triple10) -> rule4))] @3: Harry is young.[(((triple8 triple9 ((((triple11 triple8 triple10) -> rule2) triple10) -> rule4)) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple1
Eric is big.
("Eric" "is" "big" "+")
triple5
Eric is green.
("Eric" "is" "green" "+")
triple4
Fred is kind.
("Fred" "is" "kind" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple7
((((triple8 triple11) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple11 triple8 triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple8 triple11) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7 ((triple11 triple8 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple8 triple11) -> (rule3 % int4)) triple11) -> (rule1 % int3)) ((triple11 triple8 triple10) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
((((triple11 triple8 triple10) -> (rule2 % int2)) triple10) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple8 triple9 ((((triple11 triple8 triple10) -> (rule2 % int3)) triple10) -> (rule4 % int2))) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Big, red Dave is quite kind.
Eric is a person both green and big.
Fred always goes out of his way to show that he is kind to people.
Harry is kind and has rough, round hands that are red; Harry is green with envy when he looks at people who don't have to work.
A person who is nice and green with envy is round.
A kind and green person who is rough around the edges is cold.
Rough and green people are also nice.
Cold and kind people tend to be blue.
Anyone who is round and also cold will surely be big as well.
People with rough red and blue skin are young.