Charlie is not big. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is white. If Charlie is quiet and Charlie is big then Charlie is white. If something is round then it is quiet. If something is white and not big then it is round. All round things are rough. If something is kind then it is rough. If something is big and not quiet then it is kind.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If Charlie is quiet and Charlie is big then Charlie is white.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "white" "+"))
If something is round then it is quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is white and not big then it is round.
((("something" "is" "white" "+") ("something" "is" "big" "~")) -> ("something" "is" "round" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is big and not quiet then it is kind.
((("something" "is" "big" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "kind" "+"))
Charlie is kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Charlie is not green.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "green" "-")
triple2
@0: Charlie is green.[(triple2)] Charlie is kind.[(triple3)] Charlie is not big.[(triple1)] Charlie is quiet.[(triple4 OR ((triple6) -> rule2) OR ((((triple7 triple1) -> rule3)) -> rule2))] Charlie is rough.[(triple5 OR ((triple3) -> rule5) OR ((triple6) -> rule4) OR ((((triple7 triple1) -> rule3)) -> rule4))] Charlie is round.[(triple6 OR ((triple7 triple1) -> rule3))] Charlie is white.[(triple7)]
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple6) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple7 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple3) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple6) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple7 triple1) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple7 triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple7