Dave is big. Dave is blue. Dave is furry. Dave is quiet. Dave is rough. Dave is round. Dave is white. If Dave is blue then Dave is furry. If someone is blue then they are quiet. All furry people are blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If Dave is blue then Dave is furry.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "furry" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Dave is quiet.
True
1
proof
[(triple4 OR ((triple2) -> rule2) OR ((((triple3) -> rule3)) -> rule2))]
("Dave" "is" "quiet" "+")
triple4
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not round.
False
1
inv-proof
[(triple6)]
("Dave" "is" "round" "-")
triple6
@0: Dave is big.[(triple1)] Dave is blue.[(triple2 OR ((triple3) -> rule3))] Dave is furry.[(triple3 OR ((triple2) -> rule1))] Dave is quiet.[(triple4 OR ((triple2) -> rule2) OR ((((triple3) -> rule3)) -> rule2))] Dave is rough.[(triple5)] Dave is round.[(triple6)] Dave is white.[(triple7)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple3) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple2) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple2) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7