Bob is not big. Bob is blue. Bob is not furry. Bob is green. Bob is not nice. Bob is round. Bob is smart. If Bob is big and Bob is round then Bob is not nice. If someone is smart and blue then they are round.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is green.
("Bob" "is" "green" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
If Bob is big and Bob is round then Bob is not nice.
((("Bob" "is" "big" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "nice" "-"))
If someone is smart and blue then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
Bob is not furry.
True
1
proof
[(triple3)]
("Bob" "is" "furry" "-")
triple3
Bob is furry.
False
1
inv-proof
[(triple3)]
("Bob" "is" "furry" "+")
triple3
@0: Bob is blue.[(triple2)] Bob is green.[(triple4)] Bob is not big.[(triple1)] Bob is not furry.[(triple3)] Bob is not nice.[(triple5)] Bob is round.[(triple6 OR ((triple7 triple2) -> rule2))] Bob is smart.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not furry.
("Bob" "is" "furry" "-")
triple3
Bob is not nice.
("Bob" "is" "nice" "-")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple7 triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple7