Bob has a round face and is very nice. Charlie is a nice and red, but very kind person as soon as you meet him. This Dave guy is red. He is also kind and yet cold. People think Eric is nice and kind for someone so young.  Eric wears his favorite color green all the time. Big, young people feel cold all the time. It's inevitable that young, green people are big. Show me someone who is cold and kind, and I'll show you how green they are. A green person that is cold is often considered to be red. Being blue, cold, and rough must be very trying. At least they are also big. Invariably, any young person whose skin appears rough and green is bound to be quite big. People who are nice and kind are somewhat young.
Bob is round.
("Bob" "is" "round" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Eric is young.
("Eric" "is" "young" "+")
Eric is nice.
("Eric" "is" "nice" "+")
Eric is kind.
("Eric" "is" "kind" "+")
Eric is green.
("Eric" "is" "green" "+")
If someone is young and big then they are cold.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is young and green then they are big.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and kind then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is green and cold then they are red.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and cold and rough then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is young and green and rough then they are big.
((("someone" "is" "young" "+") ("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and nice then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Eric is green.
True
1
proof
[(triple12)]
("Eric" "is" "green" "+")
triple12
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Dave is green.
True
3
proof
[(((triple8 triple7) -> rule3))]
("Dave" "is" "green" "+")
((triple8 triple7) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Eric is not big.
False
3
inv-proof
[(((triple9 triple12) -> rule2) OR ((((triple11 triple10) -> rule7) triple12) -> rule2))]
("Eric" "is" "big" "-")
((triple9 triple12) -> (rule2 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
((((triple11 triple10) -> (rule7 % int2)) triple12) -> (rule2 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
True
5
proof
[(((triple9 ((triple9 triple12) -> rule2)) -> rule1) OR ((((triple11 triple10) -> rule7) ((triple9 triple12) -> rule2)) -> rule1) OR ((triple9 ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1) OR ((((triple11 triple10) -> rule7) ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1))]
("Eric" "is" "cold" "+")
((triple9 ((triple9 triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
((((triple11 triple10) -> (rule7 % int3)) ((triple9 triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
((triple9 ((((triple11 triple10) -> (rule7 % int3)) triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
((((triple11 triple10) -> (rule7 % int3)) ((((triple11 triple10) -> (rule7 % int3)) triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
Eric is not cold.
False
5
inv-proof
[(((triple9 ((triple9 triple12) -> rule2)) -> rule1) OR ((((triple11 triple10) -> rule7) ((triple9 triple12) -> rule2)) -> rule1) OR ((triple9 ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1) OR ((((triple11 triple10) -> rule7) ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1))]
("Eric" "is" "cold" "-")
((triple9 ((triple9 triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
((((triple11 triple10) -> (rule7 % int3)) ((triple9 triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
((triple9 ((((triple11 triple10) -> (rule7 % int3)) triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
((((triple11 triple10) -> (rule7 % int3)) ((((triple11 triple10) -> (rule7 % int3)) triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
Eric is red.
True
7
proof
[(((triple12 ((triple9 ((triple9 triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((((triple11 triple10) -> rule7) ((triple9 triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((triple9 ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((((triple11 triple10) -> rule7) ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1)) -> rule4))]
("Eric" "is" "red" "+")
((triple12 ((triple9 ((triple9 triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
((triple12 ((((triple11 triple10) -> (rule7 % int4)) ((triple9 triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
((triple12 ((triple9 ((((triple11 triple10) -> (rule7 % int4)) triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
((triple12 ((((triple11 triple10) -> (rule7 % int4)) ((((triple11 triple10) -> (rule7 % int4)) triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
Eric is not red.
False
7
inv-proof
[(((triple12 ((triple9 ((triple9 triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((((triple11 triple10) -> rule7) ((triple9 triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((triple9 ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((((triple11 triple10) -> rule7) ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1)) -> rule4))]
("Eric" "is" "red" "-")
((triple12 ((triple9 ((triple9 triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
((triple12 ((((triple11 triple10) -> (rule7 % int4)) ((triple9 triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
((triple12 ((triple9 ((((triple11 triple10) -> (rule7 % int4)) triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
((triple12 ((((triple11 triple10) -> (rule7 % int4)) ((((triple11 triple10) -> (rule7 % int4)) triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Bob" "is" "big" "+")
Charlie is not green.
Unknown
inv-rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "young" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Eric is blue.
Unknown
random
[@0: Eric is blue.[CWA. Example of deepest failure = (FAIL)]]
("Eric" "is" "blue" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is nice.[(triple2)] Bob is round.[(triple1)] Charlie is kind.[(triple5)] Charlie is nice.[(triple4)] Charlie is red.[(triple3)] Dave is cold.[(triple8)] Dave is kind.[(triple7)] Dave is red.[(triple6 OR ((((triple8 triple7) -> rule3) triple8) -> rule4))] Eric is green.[(triple12)] Eric is kind.[(triple11)] Eric is nice.[(triple10)] Eric is young.[(triple9 OR ((triple11 triple10) -> rule7))] @1: Charlie is young.[(((triple5 triple4) -> rule7))] Dave is green.[(((triple8 triple7) -> rule3))] Eric is big.[(((triple9 triple12) -> rule2) OR ((((triple11 triple10) -> rule7) triple12) -> rule2))] @2: Eric is cold.[(((triple9 ((triple9 triple12) -> rule2)) -> rule1) OR ((((triple11 triple10) -> rule7) ((triple9 triple12) -> rule2)) -> rule1) OR ((triple9 ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1) OR ((((triple11 triple10) -> rule7) ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1))] @3: Eric is red.[(((triple12 ((triple9 ((triple9 triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((((triple11 triple10) -> rule7) ((triple9 triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((triple9 ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1)) -> rule4) OR ((triple12 ((((triple11 triple10) -> rule7) ((((triple11 triple10) -> rule7) triple12) -> rule2)) -> rule1)) -> rule4))]
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple6
((((triple8 triple7) -> (rule3 % int2)) triple8) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Eric is green.
("Eric" "is" "green" "+")
triple12
Eric is kind.
("Eric" "is" "kind" "+")
triple11
Eric is nice.
("Eric" "is" "nice" "+")
triple10
Eric is young.
("Eric" "is" "young" "+")
triple9
((triple11 triple10) -> (rule7 % int1))
Eric is young.
("Eric" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple5 triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple8 triple7) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
((triple9 triple12) -> (rule2 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
((((triple11 triple10) -> (rule7 % int2)) triple12) -> (rule2 % int1))
Eric is big.
("Eric" "is" "big" "+")
int1
Eric is young.
("Eric" "is" "young" "+")
int2
Eric is cold.
("Eric" "is" "cold" "+")
((triple9 ((triple9 triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
((((triple11 triple10) -> (rule7 % int3)) ((triple9 triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
((triple9 ((((triple11 triple10) -> (rule7 % int3)) triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
((((triple11 triple10) -> (rule7 % int3)) ((((triple11 triple10) -> (rule7 % int3)) triple12) -> (rule2 % int2))) -> (rule1 % int1))
Eric is cold.
("Eric" "is" "cold" "+")
int1
Eric is big.
("Eric" "is" "big" "+")
int2
Eric is young.
("Eric" "is" "young" "+")
int3
Eric is red.
("Eric" "is" "red" "+")
((triple12 ((triple9 ((triple9 triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
((triple12 ((((triple11 triple10) -> (rule7 % int4)) ((triple9 triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
((triple12 ((triple9 ((((triple11 triple10) -> (rule7 % int4)) triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
((triple12 ((((triple11 triple10) -> (rule7 % int4)) ((((triple11 triple10) -> (rule7 % int4)) triple12) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Eric is red.
("Eric" "is" "red" "+")
int1
Eric is cold.
("Eric" "is" "cold" "+")
int2
Eric is big.
("Eric" "is" "big" "+")
int3
Eric is young.
("Eric" "is" "young" "+")
int4
Bob has a round face and is very nice.
Charlie is a nice and red, but very kind person as soon as you meet him.
This Dave guy is red; He is also kind and yet cold.
People think Eric is nice and kind for someone so young; Eric wears his favorite color green all the time.
Big, young people feel cold all the time.
It's inevitable that young, green people are big.
Show me someone who is cold and kind, and I'll show you how green they are.
A green person that is cold is often considered to be red.
Being blue, cold, and rough must be very trying; At least they are also big.
Invariably, any young person whose skin appears rough and green is bound to be quite big.
People who are nice and kind are somewhat young.