Bob is blue. Bob is furry. Bob is quiet. Bob is round. Bob is not smart. Bob is white. Bob is young. If Bob is furry and Bob is smart then Bob is round. If Bob is not white then Bob is not round. If Bob is smart and Bob is white then Bob is quiet. All white, round people are blue. If someone is furry then they are quiet. If Bob is quiet and Bob is not furry then Bob is young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
If Bob is furry and Bob is smart then Bob is round.
((("Bob" "is" "furry" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "round" "+"))
If Bob is not white then Bob is not round.
((("Bob" "is" "white" "~")) -> ("Bob" "is" "round" "-"))
If Bob is smart and Bob is white then Bob is quiet.
((("Bob" "is" "smart" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "quiet" "+"))
All white, round people are blue.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is quiet and Bob is not furry then Bob is young.
((("Bob" "is" "quiet" "+") ("Bob" "is" "furry" "~")) -> ("Bob" "is" "young" "+"))
Bob is round.
True
1
proof
[(triple4)]
("Bob" "is" "round" "+")
triple4
Bob is not white.
False
1
inv-proof
[(triple6)]
("Bob" "is" "white" "-")
triple6
@0: Bob is blue.[(triple1 OR ((triple6 triple4) -> rule4))] Bob is furry.[(triple2)] Bob is not smart.[(triple5)] Bob is quiet.[(triple3 OR ((triple2) -> rule5))] Bob is round.[(triple4)] Bob is white.[(triple6)] Bob is young.[(triple7)]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple6 triple4) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is not smart.
("Bob" "is" "smart" "-")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple2) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7