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