Dave is big. Dave is not furry. Dave is nice. Dave is red. Dave is rough. Dave is smart. Dave is white. Erin is big. Erin is furry. Erin is nice. Erin is red. Erin is not rough. If Erin is not rough then Erin is white.
Dave is big.
("Dave" "is" "big" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
If Erin is not rough then Erin is white.
((("Erin" "is" "rough" "~")) -> ("Erin" "is" "white" "+"))
Erin is not rough.
True
1
proof
[(triple12)]
("Erin" "is" "rough" "-")
triple12
Erin is rough.
False
1
inv-proof
[(triple12)]
("Erin" "is" "rough" "+")
triple12
@0: Dave is big.[(triple1)] Dave is nice.[(triple3)] Dave is not furry.[(triple2)] Dave is red.[(triple4)] Dave is rough.[(triple5)] Dave is smart.[(triple6)] Dave is white.[(triple7)] Erin is big.[(triple8)] Erin is furry.[(triple9)] Erin is nice.[(triple10)] Erin is not rough.[(triple12)] Erin is red.[(triple11)] @1: Erin is white.[(((triple12) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is white.
("Dave" "is" "white" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
Erin is nice.
("Erin" "is" "nice" "+")
triple10
Erin is not rough.
("Erin" "is" "rough" "-")
triple12
Erin is red.
("Erin" "is" "red" "+")
triple11
Erin is white.
("Erin" "is" "white" "+")
((triple12) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1