Charlie is green. Charlie is quiet. Charlie is young. All nice, green people are young. If Charlie is big then Charlie is furry. If Charlie is green then Charlie is young. Green people are rough. If someone is furry then they are nice. If Charlie is rough then Charlie is young. If Charlie is rough then Charlie is furry. All young people are nice.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is young.
("Charlie" "is" "young" "+")
All nice, green people are young.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Charlie is big then Charlie is furry.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "furry" "+"))
If Charlie is green then Charlie is young.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "young" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is rough then Charlie is young.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "young" "+"))
If Charlie is rough then Charlie is furry.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "furry" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Charlie is young.
True
1
proof
[(triple3 OR ((triple1) -> rule3) OR ((((triple1) -> rule4)) -> rule6) OR ((((((((triple1) -> rule4)) -> rule7)) -> rule5) triple1) -> rule1))]
("Charlie" "is" "young" "+")
triple3
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
@0: Charlie is green.[(triple1)] Charlie is quiet.[(triple2)] Charlie is young.[(triple3 OR ((triple1) -> rule3) OR ((((triple1) -> rule4)) -> rule6) OR ((((((((triple1) -> rule4)) -> rule7)) -> rule5) triple1) -> rule1))] @1: Charlie is nice.[(((triple3) -> rule8) OR ((((triple1) -> rule3)) -> rule8) OR ((((((triple1) -> rule4)) -> rule6)) -> rule8) OR ((((((triple1) -> rule4)) -> rule7)) -> rule5))] Charlie is rough.[(((triple1) -> rule4))] @2: Charlie is furry.[(((((triple1) -> rule4)) -> rule7))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((((triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2)) triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2