Dave is furry. Dave is green. Dave is quiet. Dave is red. Dave is not rough. Dave is smart. Dave is not young. If something is smart then it is quiet. If something is quiet and not green then it is furry. If something is green and not rough then it is not young.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not young.
("Dave" "is" "young" "-")
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and not green then it is furry.
((("something" "is" "quiet" "+") ("something" "is" "green" "~")) -> ("something" "is" "furry" "+"))
If something is green and not rough then it is not young.
((("something" "is" "green" "+") ("something" "is" "rough" "~")) -> ("something" "is" "young" "-"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
@0: Dave is furry.[(triple1)] Dave is green.[(triple2)] Dave is not rough.[(triple5)] Dave is not young.[(triple7 OR ((triple2 triple5) -> rule3))] Dave is quiet.[(triple3 OR ((triple6) -> rule1))] Dave is red.[(triple4)] Dave is smart.[(triple6)]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is not rough.
("Dave" "is" "rough" "-")
triple5
Dave is not young.
("Dave" "is" "young" "-")
triple7
((triple2 triple5) -> (rule3 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
((triple6) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple6