Charlie is furry. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is smart. Charlie is white. Charlie is young. If Charlie is nice and Charlie is quiet then Charlie is young.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If Charlie is nice and Charlie is quiet then Charlie is young.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "young" "+"))
Charlie is smart.
True
1
proof
[(triple5)]
("Charlie" "is" "smart" "+")
triple5
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2)] Charlie is nice.[(triple3)] Charlie is quiet.[(triple4)] Charlie is smart.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple3 triple4) -> rule1))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple3 triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1