Bob is big. Bob is furry. Bob is nice. Bob is not quiet. Bob is rough. Bob is smart. Bob is white. All smart, quiet things are rough. If something is furry and not quiet then it is white.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
All smart, quiet things are rough.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is furry and not quiet then it is white.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "+"))
Bob is rough.
True
1
proof
[(triple5)]
("Bob" "is" "rough" "+")
triple5
Bob is not rough.
False
1
inv-proof
[(triple5)]
("Bob" "is" "rough" "-")
triple5
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Bob is not quiet.[(triple4)] Bob is rough.[(triple5)] Bob is smart.[(triple6)] Bob is white.[(triple7 OR ((triple2 triple4) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple2 triple4) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1