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