Dave is big. Dave is blue. Dave is furry. Dave is not kind. Dave is nice. Dave is red. Dave is smart. If Dave is big then Dave is blue. Red things are blue. If something is smart then it is red.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is big then Dave is blue.
((("Dave" "is" "big" "+")) -> ("Dave" "is" "blue" "+"))
Red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is smart then it is red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Dave is smart.
True
1
proof
[(triple7)]
("Dave" "is" "smart" "+")
triple7
Dave is not nice.
False
1
inv-proof
[(triple5)]
("Dave" "is" "nice" "-")
triple5
@0: Dave is big.[(triple1)] Dave is blue.[(triple2 OR ((triple1) -> rule1) OR ((triple6) -> rule2) OR ((((triple7) -> rule3)) -> rule2))] Dave is furry.[(triple3)] Dave is nice.[(triple5)] Dave is not kind.[(triple4)] Dave is red.[(triple6 OR ((triple7) -> rule3))] Dave is smart.[(triple7)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not kind.
("Dave" "is" "kind" "-")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple6
((triple7) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple7