Bob is big. Bob is not blue. Bob is nice. Bob is not rough. Bob is round. Bob is not smart. Bob is white. White things are round. Blue things are smart. If Bob is smart and Bob is round then Bob is not blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If Bob is smart and Bob is round then Bob is not blue.
((("Bob" "is" "smart" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "blue" "-"))
Bob is white.
True
1
proof
[(triple7)]
("Bob" "is" "white" "+")
triple7
Bob is not white.
False
1
inv-proof
[(triple7)]
("Bob" "is" "white" "-")
triple7
@0: Bob is big.[(triple1)] Bob is nice.[(triple3)] Bob is not blue.[(triple2)] Bob is not rough.[(triple4)] Bob is not smart.[(triple6)] Bob is round.[(triple5 OR ((triple7) -> rule1))] Bob is white.[(triple7)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Bob is not rough.
("Bob" "is" "rough" "-")
triple4
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple7) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7