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