Dave is furry. Dave is green. Dave is nice. Dave is quiet. Dave is rough. Erin is furry. Erin is green. Erin is kind. Erin is nice. Erin is quiet. Erin is rough. Erin is smart. All furry things are nice. If Dave is furry and Dave is nice then Dave is kind.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Dave is furry and Dave is nice then Dave is kind.
((("Dave" "is" "furry" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "kind" "+"))
Erin is kind.
True
1
proof
[(triple8)]
("Erin" "is" "kind" "+")
triple8
Erin is not quiet.
False
1
inv-proof
[(triple10)]
("Erin" "is" "quiet" "-")
triple10
@0: Dave is furry.[(triple1)] Dave is green.[(triple2)] Dave is nice.[(triple3 OR ((triple1) -> rule1))] Dave is quiet.[(triple4)] Dave is rough.[(triple5)] Erin is furry.[(triple6)] Erin is green.[(triple7)] Erin is kind.[(triple8)] Erin is nice.[(triple9 OR ((triple6) -> rule1))] Erin is quiet.[(triple10)] Erin is rough.[(triple11)] Erin is smart.[(triple12)] @1: Dave is kind.[(((triple1 triple3) -> rule2) OR ((triple1 ((triple1) -> rule1)) -> rule2))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple1) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple6) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is rough.
("Erin" "is" "rough" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
((triple1 triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2