Bob is big and dresses in blue. Dave, that young round kid, is kind whenever he's blue. Eric is green, which is a possible explanation for why he is so nice. Harry is colored blue and red. He is also kind and cold to the touch. Nice blue people are often rough. I have found that blue, kind people are big. A kind red person is also a blue person. Big, kind people are nice. If a big person is cold and nice, then they are green. Young and kind folks are always big. Red people who are green and blue are always kind.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is big.
("Bob" "is" "big" "+")
Dave is young.
("Dave" "is" "young" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Eric is nice.
("Eric" "is" "nice" "+")
Eric is green.
("Eric" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is nice and blue then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is blue and kind then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and red then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind and big then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and big and nice then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is kind and young then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is red and blue and green then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Harry is red.
True
1
proof
[(triple9)]
("Harry" "is" "red" "+")
triple9
Bob is not big.
False
1
inv-proof
[(triple2)]
("Bob" "is" "big" "-")
triple2
Dave is big.
True
3
proof
[(((triple5 triple3) -> rule6) OR ((triple6 triple5) -> rule2))]
("Dave" "is" "big" "+")
((triple5 triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple6 triple5) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
3
inv-proof
[(((triple5 triple3) -> rule6) OR ((triple6 triple5) -> rule2))]
("Dave" "is" "big" "-")
((triple5 triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple6 triple5) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is nice.
True
5
proof
[(((triple10 ((triple12 triple10) -> rule2)) -> rule4) OR ((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4))]
("Harry" "is" "nice" "+")
((triple10 ((triple12 triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple10 ((((triple10 triple9) -> (rule3 % int3)) triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not nice.
False
5
inv-proof
[(((triple10 ((triple12 triple10) -> rule2)) -> rule4) OR ((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4))]
("Harry" "is" "nice" "-")
((triple10 ((triple12 triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple10 ((((triple10 triple9) -> (rule3 % int3)) triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Dave is rough.
True
7
proof
[(((((triple5 ((triple5 triple3) -> rule6)) -> rule4) triple6) -> rule1) OR ((((triple5 ((triple6 triple5) -> rule2)) -> rule4) triple6) -> rule1))]
("Dave" "is" "rough" "+")
((((triple5 ((triple5 triple3) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((triple5 ((triple6 triple5) -> (rule2 % int3))) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Harry is not rough.
False
7
inv-proof
[(((((triple10 ((triple12 triple10) -> rule2)) -> rule4) triple12) -> rule1) OR ((((triple10 ((triple12 triple10) -> rule2)) -> rule4) ((triple10 triple9) -> rule3)) -> rule1) OR ((((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4) triple12) -> rule1) OR ((((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4) ((triple10 triple9) -> rule3)) -> rule1))]
("Harry" "is" "rough" "-")
((((triple10 ((triple12 triple10) -> (rule2 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple10 ((triple12 triple10) -> (rule2 % int4))) -> (rule4 % int3)) ((triple10 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple10 ((((triple10 triple9) -> (rule3 % int4)) triple10) -> (rule2 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
((((triple10 ((((triple10 triple9) -> (rule3 % int4)) triple10) -> (rule2 % int3))) -> (rule4 % int2)) ((triple10 triple9) -> (rule3 % int4))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is rough.
Unknown
rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule7 <- FAIL)]]
("Bob" "is" "rough" "+")
Eric is not rough.
Unknown
inv-rconc
[@2: Eric is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Eric" "is" "rough" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is big.[(triple2)] Bob is blue.[(triple1)] Dave is blue.[(triple6)] Dave is kind.[(triple5)] Dave is round.[(triple4)] Dave is young.[(triple3)] Eric is green.[(triple8)] Eric is nice.[(triple7)] Harry is blue.[(triple12 OR ((triple10 triple9) -> rule3))] Harry is cold.[(triple11)] Harry is kind.[(triple10)] Harry is red.[(triple9)] @1: Dave is big.[(((triple5 triple3) -> rule6) OR ((triple6 triple5) -> rule2))] Harry is big.[(((triple12 triple10) -> rule2) OR ((((triple10 triple9) -> rule3) triple10) -> rule2))] @2: Dave is nice.[(((triple5 ((triple5 triple3) -> rule6)) -> rule4) OR ((triple5 ((triple6 triple5) -> rule2)) -> rule4))] Harry is nice.[(((triple10 ((triple12 triple10) -> rule2)) -> rule4) OR ((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4))] @3: Dave is rough.[(((((triple5 ((triple5 triple3) -> rule6)) -> rule4) triple6) -> rule1) OR ((((triple5 ((triple6 triple5) -> rule2)) -> rule4) triple6) -> rule1))] Harry is green.[(((triple11 ((triple12 triple10) -> rule2) ((triple10 ((triple12 triple10) -> rule2)) -> rule4)) -> rule5) OR ((triple11 ((((triple10 triple9) -> rule3) triple10) -> rule2) ((triple10 ((triple12 triple10) -> rule2)) -> rule4)) -> rule5) OR ((triple11 ((triple12 triple10) -> rule2) ((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4)) -> rule5) OR ((triple11 ((((triple10 triple9) -> rule3) triple10) -> rule2) ((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4)) -> rule5))] Harry is rough.[(((((triple10 ((triple12 triple10) -> rule2)) -> rule4) triple12) -> rule1) OR ((((triple10 ((triple12 triple10) -> rule2)) -> rule4) ((triple10 triple9) -> rule3)) -> rule1) OR ((((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4) triple12) -> rule1) OR ((((triple10 ((((triple10 triple9) -> rule3) triple10) -> rule2)) -> rule4) ((triple10 triple9) -> rule3)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple3
Eric is green.
("Eric" "is" "green" "+")
triple8
Eric is nice.
("Eric" "is" "nice" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple12
((triple10 triple9) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
((triple5 triple3) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple6 triple5) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple12 triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple10 triple9) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((triple5 ((triple5 triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple5 ((triple6 triple5) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple10 ((triple12 triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple10 ((((triple10 triple9) -> (rule3 % int3)) triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((triple5 ((triple5 triple3) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((triple5 ((triple6 triple5) -> (rule2 % int3))) -> (rule4 % int2)) triple6) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((triple11 ((triple12 triple10) -> (rule2 % int3)) ((triple10 ((triple12 triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((triple11 ((((triple10 triple9) -> (rule3 % int4)) triple10) -> (rule2 % int3)) ((triple10 ((triple12 triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
((triple11 ((triple12 triple10) -> (rule2 % int4)) ((triple10 ((((triple10 triple9) -> (rule3 % int3)) triple10) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((triple11 ((((triple10 triple9) -> (rule3 % int4)) triple10) -> (rule2 % int3)) ((triple10 ((((triple10 triple9) -> (rule3 % int4)) triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
((((triple10 ((triple12 triple10) -> (rule2 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((triple10 ((triple12 triple10) -> (rule2 % int4))) -> (rule4 % int3)) ((triple10 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
((((triple10 ((((triple10 triple9) -> (rule3 % int4)) triple10) -> (rule2 % int3))) -> (rule4 % int2)) triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
((((triple10 ((((triple10 triple9) -> (rule3 % int4)) triple10) -> (rule2 % int3))) -> (rule4 % int2)) ((triple10 triple9) -> (rule3 % int4))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Bob is big and dresses in blue.
Dave, that young round kid, is kind whenever he's blue.
Eric is green, which is a possible explanation for why he is so nice.
Harry is colored blue and red; He is also kind and cold to the touch.
Nice blue people are often rough.
I have found that blue, kind people are big.
A kind red person is also a blue person.
Big, kind people are nice.
If a big person is cold and nice, then they are green.
Young and kind folks are always big.
Red people who are green and blue are always kind.