Dave is big. Dave is not blue. Dave is furry. Dave is not green. Dave is nice. Dave is not round. Dave is not young. Erin is big. Erin is not blue. Erin is furry. Erin is green. Erin is nice. Erin is round. Erin is young. If Dave is not nice then Dave is blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is not young.
("Dave" "is" "young" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
If Dave is not nice then Dave is blue.
((("Dave" "is" "nice" "~")) -> ("Dave" "is" "blue" "+"))
Dave is not young.
True
1
proof
[(triple7)]
("Dave" "is" "young" "-")
triple7
Erin is not green.
False
1
inv-proof
[(triple11)]
("Erin" "is" "green" "-")
triple11
@0: Dave is big.[(triple1)] Dave is furry.[(triple3)] Dave is nice.[(triple5)] Dave is not blue.[(triple2)] Dave is not green.[(triple4)] Dave is not round.[(triple6)] Dave is not young.[(triple7)] Erin is big.[(triple8)] Erin is furry.[(triple10)] Erin is green.[(triple11)] Erin is nice.[(triple12)] Erin is not blue.[(triple9)] Erin is round.[(triple13)] Erin is young.[(triple14)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is not blue.
("Dave" "is" "blue" "-")
triple2
Dave is not green.
("Dave" "is" "green" "-")
triple4
Dave is not round.
("Dave" "is" "round" "-")
triple6
Dave is not young.
("Dave" "is" "young" "-")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
triple11
Erin is nice.
("Erin" "is" "nice" "+")
triple12
Erin is not blue.
("Erin" "is" "blue" "-")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14