Dave is furry. Dave is kind. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Dave is smart. Erin is furry. Erin is kind. Erin is not nice. Erin is quiet. Erin is red. Erin is rough. Erin is smart. If someone is kind and not furry then they are quiet. If someone is smart and nice then they are quiet. If someone is kind and not smart then they are nice.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If someone is kind and not furry then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "quiet" "+"))
If someone is smart and nice then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind and not smart then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "nice" "+"))
Erin is quiet.
True
1
proof
[(triple11)]
("Erin" "is" "quiet" "+")
triple11
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
@0: Dave is furry.[(triple1)] Dave is kind.[(triple2)] Dave is nice.[(triple3)] Dave is quiet.[(triple4 OR ((triple7 triple3) -> rule2))] Dave is red.[(triple5)] Dave is rough.[(triple6)] Dave is smart.[(triple7)] Erin is furry.[(triple8)] Erin is kind.[(triple9)] Erin is not nice.[(triple10)] Erin is quiet.[(triple11)] Erin is red.[(triple12)] Erin is rough.[(triple13)] Erin is smart.[(triple14)]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple7 triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
Erin is not nice.
("Erin" "is" "nice" "-")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13
Erin is smart.
("Erin" "is" "smart" "+")
triple14