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