Dave is big. Dave is nice. Dave is not quiet. Dave is red. Dave is not rough. Dave is white. Dave is not young. All big people are white. All quiet people are not white. If someone is white and rough then they are quiet. If Dave is quiet then Dave is big. If Dave is young then Dave is big. All rough, white people are not nice. If someone is big and not rough then they are nice. If Dave is quiet and Dave is young then Dave is not red.
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is white.
("Dave" "is" "white" "+")
Dave is not young.
("Dave" "is" "young" "-")
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All quiet people are not white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "-"))
If someone is white and rough then they are quiet.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is quiet then Dave is big.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "big" "+"))
If Dave is young then Dave is big.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "big" "+"))
All rough, white people are not nice.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "-"))
If someone is big and not rough then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "nice" "+"))
If Dave is quiet and Dave is young then Dave is not red.
((("Dave" "is" "quiet" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "red" "-"))
Dave is not quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
@0: Dave is big.[(triple1)] Dave is nice.[(triple2 OR ((triple1 triple5) -> rule7))] Dave is not quiet.[(triple3)] Dave is not rough.[(triple5)] Dave is not young.[(triple7)] Dave is red.[(triple4)] Dave is white.[(triple6 OR ((triple1) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
((triple1 triple5) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple3
Dave is not rough.
("Dave" "is" "rough" "-")
triple5
Dave is not young.
("Dave" "is" "young" "-")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1