Charlie is big. Charlie is not furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is rough. Charlie is young. If someone is young and not furry then they are kind. All young people are kind. If someone is furry then they are nice. All big, green people are rough. Kind, green people are big. If someone is rough and not furry then they are big. If someone is green and kind then they are big. If someone is green and not kind then they are not big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not 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 young.
("Charlie" "is" "young" "+")
If someone is young and not furry then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All big, green people are rough.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Kind, green people are big.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is rough and not furry then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "big" "+"))
If someone is green and kind then they are big.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is green and not kind then they are not big.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "big" "-"))
Charlie is green.
True
1
proof
[(triple3)]
("Charlie" "is" "green" "+")
triple3
Charlie is not nice.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "nice" "-")
triple5
@0: Charlie is big.[(triple1 OR ((triple3 triple4) -> rule7) OR ((triple4 triple3) -> rule5) OR ((triple6 triple2) -> rule6) OR ((triple3 ((triple7) -> rule2)) -> rule7) OR ((triple3 ((triple7 triple2) -> rule1)) -> rule7) OR ((((triple7) -> rule2) triple3) -> rule5) OR ((((triple7 triple2) -> rule1) triple3) -> rule5))] Charlie is green.[(triple3)] Charlie is kind.[(triple4 OR ((triple7) -> rule2) OR ((triple7 triple2) -> rule1))] Charlie is nice.[(triple5)] Charlie is not furry.[(triple2)] Charlie is rough.[(triple6 OR ((triple1 triple3) -> rule4) OR ((((triple3 triple4) -> rule7) triple3) -> rule4) OR ((((triple4 triple3) -> rule5) triple3) -> rule4) OR ((((triple3 ((triple7) -> rule2)) -> rule7) triple3) -> rule4) OR ((((triple3 ((triple7 triple2) -> rule1)) -> rule7) triple3) -> rule4) OR ((((((triple7) -> rule2) triple3) -> rule5) triple3) -> rule4) OR ((((((triple7 triple2) -> rule1) triple3) -> rule5) triple3) -> rule4))] Charlie is young.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3 triple4) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple4 triple3) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple6 triple2) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple3 ((triple7) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple3 ((triple7 triple2) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple7 triple2) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple7) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple7 triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple1 triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple3 triple4) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple4 triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple3 ((triple7) -> (rule2 % int3))) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((triple3 ((triple7 triple2) -> (rule1 % int3))) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple7) -> (rule2 % int3)) triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple7 triple2) -> (rule1 % int3)) triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple7