Charlie is big. Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is rough. Charlie is white. If someone is rough and furry then they are white. Furry people are kind. If Charlie is furry then Charlie is big. If someone is white and furry then they are big. All nice people are rough. If Charlie is kind and Charlie is big then Charlie is white. If someone is kind and green then they are rough. All white, green people are kind.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If someone is rough and furry then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is furry then Charlie is big.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "big" "+"))
If someone is white and furry then they are big.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is kind and Charlie is big then Charlie is white.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "white" "+"))
If someone is kind and green then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All white, green people are kind.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Charlie is kind.
True
1
proof
[(triple4 OR ((triple2) -> rule2) OR ((triple7 triple3) -> rule8) OR ((((triple6 triple2) -> rule1) triple3) -> rule8) OR ((((((triple5) -> rule5) triple2) -> rule1) triple3) -> rule8))]
("Charlie" "is" "kind" "+")
triple4
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple7 triple3) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple6 triple2) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple5) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
@0: Charlie is big.[(triple1 OR ((triple2) -> rule3) OR ((triple7 triple2) -> rule4) OR ((((triple6 triple2) -> rule1) triple2) -> rule4) OR ((((((triple5) -> rule5) triple2) -> rule1) triple2) -> rule4) OR ((((((triple4 triple3) -> rule7) triple2) -> rule1) triple2) -> rule4) OR ((((((((triple2) -> rule2) triple3) -> rule7) triple2) -> rule1) triple2) -> rule4))] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4 OR ((triple2) -> rule2) OR ((triple7 triple3) -> rule8) OR ((((triple6 triple2) -> rule1) triple3) -> rule8) OR ((((((triple5) -> rule5) triple2) -> rule1) triple3) -> rule8))] Charlie is nice.[(triple5)] Charlie is rough.[(triple6 OR ((triple5) -> rule5) OR ((triple4 triple3) -> rule7) OR ((((triple2) -> rule2) triple3) -> rule7) OR ((((triple7 triple3) -> rule8) triple3) -> rule7))] Charlie is white.[(triple7 OR ((triple4 triple1) -> rule6) OR ((triple6 triple2) -> rule1) OR ((triple4 ((triple2) -> rule3)) -> rule6) OR ((((triple2) -> rule2) triple1) -> rule6) OR ((((triple5) -> rule5) triple2) -> rule1) OR ((((triple4 triple3) -> rule7) triple2) -> rule1) OR ((((triple2) -> rule2) ((triple2) -> rule3)) -> rule6) OR ((((((triple2) -> rule2) triple3) -> rule7) triple2) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple7 triple2) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6 triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple5) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple4 triple3) -> (rule7 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((((triple2) -> (rule2 % int4)) triple3) -> (rule7 % int3)) triple2) -> (rule1 % int2)) triple2) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple7 triple3) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple6 triple2) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple5) -> (rule5 % int3)) triple2) -> (rule1 % int2)) triple3) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple5) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 triple3) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2)) triple3) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7 triple3) -> (rule8 % int2)) triple3) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple4 triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple6 triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple4 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple2) -> (rule2 % int2)) triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple5) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple4 triple3) -> (rule7 % int2)) triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple2) -> (rule2 % int3)) triple3) -> (rule7 % int2)) triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3