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