Charlie is not big. Charlie is green. Charlie is not nice. Charlie is not quiet. Charlie is not rough. Charlie is not round. Charlie is white. Dave is big. Dave is green. Dave is nice. Dave is quiet. Dave is rough. Dave is not round. Dave is white. If Charlie is quiet and Charlie is not round then Charlie is white. Quiet, white people are green. All quiet people are green.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is white.
("Dave" "is" "white" "+")
If Charlie is quiet and Charlie is not round then Charlie is white.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "round" "~")) -> ("Charlie" "is" "white" "+"))
Quiet, white people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Charlie is not big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Dave is not green.
False
1
inv-proof
[(triple9 OR ((triple11) -> rule3) OR ((triple11 triple14) -> rule2))]
("Dave" "is" "green" "-")
triple9
((triple11) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple11 triple14) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
@0: Charlie is green.[(triple2)] Charlie is not big.[(triple1)] Charlie is not nice.[(triple3)] Charlie is not quiet.[(triple4)] Charlie is not rough.[(triple5)] Charlie is not round.[(triple6)] Charlie is white.[(triple7)] Dave is big.[(triple8)] Dave is green.[(triple9 OR ((triple11) -> rule3) OR ((triple11 triple14) -> rule2))] Dave is nice.[(triple10)] Dave is not round.[(triple13)] Dave is quiet.[(triple11)] Dave is rough.[(triple12)] Dave is white.[(triple14)]
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple3
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple4
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Charlie is not round.
("Charlie" "is" "round" "-")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
((triple11) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple11 triple14) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is not round.
("Dave" "is" "round" "-")
triple13
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Dave is rough.
("Dave" "is" "rough" "+")
triple12
Dave is white.
("Dave" "is" "white" "+")
triple14