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