Dave is blue. Dave is furry. Dave is kind. Dave is red. Dave is rough. Dave is round. Dave is smart. Rough, kind things are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Rough, kind things are blue.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Dave is blue.
True
1
proof
[(triple1 OR ((triple5 triple3) -> rule1))]
("Dave" "is" "blue" "+")
triple1
((triple5 triple3) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
@0: Dave is blue.[(triple1 OR ((triple5 triple3) -> rule1))] Dave is furry.[(triple2)] Dave is kind.[(triple3)] Dave is red.[(triple4)] Dave is rough.[(triple5)] Dave is round.[(triple6)] Dave is smart.[(triple7)]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple5 triple3) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7