Charlie is big. Charlie is red. Charlie is rough. All rough, red things are nice. If Charlie is big then Charlie is red. All big, nice things are young. If Charlie is furry then Charlie is kind. If something is red then it is furry. All rough, red things are big. If something is nice then it is rough. All young things are nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
All rough, red things are nice.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If Charlie is big then Charlie is red.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "+"))
All big, nice things are young.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Charlie is furry then Charlie is kind.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "kind" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All rough, red things are big.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Charlie is red.
True
1
proof
[(triple2 OR ((triple1) -> rule2))]
("Charlie" "is" "red" "+")
triple2
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple3 triple2) -> rule6))]
("Charlie" "is" "big" "-")
triple1
((triple3 triple2) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
@0: Charlie is big.[(triple1 OR ((triple3 triple2) -> rule6))] Charlie is red.[(triple2 OR ((triple1) -> rule2))] Charlie is rough.[(triple3)] @1: Charlie is furry.[(((triple2) -> rule5) OR ((((triple1) -> rule2)) -> rule5))] Charlie is nice.[(((triple3 triple2) -> rule1) OR ((triple3 ((triple1) -> rule2)) -> rule1))] @2: Charlie is kind.[(((((triple2) -> rule5)) -> rule4) OR ((((((triple1) -> rule2)) -> rule5)) -> rule4))] Charlie is young.[(((triple1 ((triple3 triple2) -> rule1)) -> rule3) OR ((((triple3 triple2) -> rule6) ((triple3 triple2) -> rule1)) -> rule3) OR ((triple1 ((triple3 ((triple1) -> rule2)) -> rule1)) -> rule3) OR ((((triple3 triple2) -> rule6) ((triple3 ((triple1) -> rule2)) -> rule1)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3 triple2) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
((triple1) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3 triple2) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 ((triple3 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple3 triple2) -> (rule6 % int3)) ((triple3 triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((triple1 ((triple3 ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((triple3 triple2) -> (rule6 % int4)) ((triple3 ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4