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