Dave looks red to most people, with blue features. Young Eric is wearing green pants. Even though he's a big dude, Fred is cold. Gary is a very kind, green but sometimes cold person. Whoever is rough and red must be kind. A nice person who is green is feeling cold. Could you imagine how weird it would be if someone was nice, blue, and kind, but not green also. It's easy to be round and blue when you are young. Young people tend to be blue all the time and rough. Someone blue and red is definitely round and dressed as a clown. A person that is the color red will definitely be round shaped.
Dave is red.
("Dave" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Eric is young.
("Eric" "is" "young" "+")
Eric is green.
("Eric" "is" "green" "+")
Fred is cold.
("Fred" "is" "cold" "+")
Fred is big.
("Fred" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If someone is rough and red then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and nice then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and blue and kind then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is round and blue then they are young.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is blue and young then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and red then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Fred is big.
True
1
proof
[(triple6)]
("Fred" "is" "big" "+")
triple6
Dave is not red.
False
1
inv-proof
[(triple1)]
("Dave" "is" "red" "-")
triple1
Dave is round.
True
2
proof
[(((triple1) -> rule7) OR ((triple2 triple1) -> rule6))]
("Dave" "is" "round" "+")
((triple1) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple2 triple1) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule7) OR ((triple2 triple1) -> rule6))]
("Dave" "is" "round" "-")
((triple1) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple2 triple1) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
True
4
proof
[(((((triple1) -> rule7) triple2) -> rule4) OR ((((triple2 triple1) -> rule6) triple2) -> rule4))]
("Dave" "is" "young" "+")
((((triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple2 triple1) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple1) -> rule7) triple2) -> rule4) OR ((((triple2 triple1) -> rule6) triple2) -> rule4))]
("Dave" "is" "young" "-")
((((triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple2 triple1) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
True
6
proof
[(((triple2 ((((triple1) -> rule7) triple2) -> rule4)) -> rule5) OR ((triple2 ((((triple2 triple1) -> rule6) triple2) -> rule4)) -> rule5))]
("Dave" "is" "rough" "+")
((triple2 ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple2 ((((triple2 triple1) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not rough.
False
6
inv-proof
[(((triple2 ((((triple1) -> rule7) triple2) -> rule4)) -> rule5) OR ((triple2 ((((triple2 triple1) -> rule6) triple2) -> rule4)) -> rule5))]
("Dave" "is" "rough" "-")
((triple2 ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple2 ((((triple2 triple1) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
True
8
proof
[(((((triple2 ((((triple1) -> rule7) triple2) -> rule4)) -> rule5) triple1) -> rule1) OR ((((triple2 ((((triple2 triple1) -> rule6) triple2) -> rule4)) -> rule5) triple1) -> rule1))]
("Dave" "is" "kind" "+")
((((triple2 ((((triple1) -> (rule7 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple2 ((((triple2 triple1) -> (rule6 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not kind.
False
8
inv-proof
[(((((triple2 ((((triple1) -> rule7) triple2) -> rule4)) -> rule5) triple1) -> rule1) OR ((((triple2 ((((triple2 triple1) -> rule6) triple2) -> rule4)) -> rule5) triple1) -> rule1))]
("Dave" "is" "kind" "-")
((((triple2 ((((triple1) -> (rule7 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple2 ((((triple2 triple1) -> (rule6 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Eric is not kind.
Unknown
inv-rconc
[@1: Eric is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Eric" "is" "kind" "-")
Fred is green.
Unknown
rconc
[@1: Fred is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fred" "is" "green" "+")
Eric is not round.
Unknown
inv-rconc
[@1: Eric is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Eric" "is" "round" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "cold" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "young" "-")
Eric is red.
Unknown
random
[@0: Eric is red.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "red" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Eric is not blue.
Unknown
inv-random
[@0: Eric is blue.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "blue" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Dave is blue.[(triple2)] Dave is red.[(triple1)] Eric is green.[(triple4)] Eric is young.[(triple3)] Fred is big.[(triple6)] Fred is cold.[(triple5)] Gary is cold.[(triple9)] Gary is green.[(triple8)] Gary is kind.[(triple7)] @1: Dave is round.[(((triple1) -> rule7) OR ((triple2 triple1) -> rule6))] @2: Dave is young.[(((((triple1) -> rule7) triple2) -> rule4) OR ((((triple2 triple1) -> rule6) triple2) -> rule4))] @3: Dave is rough.[(((triple2 ((((triple1) -> rule7) triple2) -> rule4)) -> rule5) OR ((triple2 ((((triple2 triple1) -> rule6) triple2) -> rule4)) -> rule5))] @4: Dave is kind.[(((((triple2 ((((triple1) -> rule7) triple2) -> rule4)) -> rule5) triple1) -> rule1) OR ((((triple2 ((((triple2 triple1) -> rule6) triple2) -> rule4)) -> rule5) triple1) -> rule1))]
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple1
Eric is green.
("Eric" "is" "green" "+")
triple4
Eric is young.
("Eric" "is" "young" "+")
triple3
Fred is big.
("Fred" "is" "big" "+")
triple6
Fred is cold.
("Fred" "is" "cold" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple2 triple1) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule7 % int2)) triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple2 triple1) -> (rule6 % int2)) triple2) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple2 ((((triple1) -> (rule7 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((triple2 ((((triple2 triple1) -> (rule6 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple2 ((((triple1) -> (rule7 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
((((triple2 ((((triple2 triple1) -> (rule6 % int4)) triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave looks red to most people, with blue features.
Young Eric is wearing green pants.
Even though he's a big dude, Fred is cold.
Gary is a very kind, green but sometimes cold person.
Whoever is rough and red must be kind.
A nice person who is green is feeling cold.
Could you imagine how weird it would be if someone was nice, blue, and kind, but not green also.
It's easy to be round and blue when you are young.
Young people tend to be blue all the time and rough.
Someone blue and red is definitely round and dressed as a clown.
A person that is the color red will definitely be round shaped.