Bob is big. Bob is furry. Bob is not green. Bob is quiet. Bob is red. Bob is not smart. Bob is white. Charlie is not big. Charlie is not furry. Charlie is green. Charlie is red. Charlie is not white. If Charlie is smart then Charlie is big. If Bob is not red and Bob is not green then Bob is quiet. If something is quiet and not red then it is furry. Smart things are furry. All green things are quiet. If something is smart and not furry then it is not white.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is white.
("Bob" "is" "white" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
If Charlie is smart then Charlie is big.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "big" "+"))
If Bob is not red and Bob is not green then Bob is quiet.
((("Bob" "is" "red" "~") ("Bob" "is" "green" "~")) -> ("Bob" "is" "quiet" "+"))
If something is quiet and not red then it is furry.
((("something" "is" "quiet" "+") ("something" "is" "red" "~")) -> ("something" "is" "furry" "+"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and not furry then it is not white.
((("something" "is" "smart" "+") ("something" "is" "furry" "~")) -> ("something" "is" "white" "-"))
Charlie is not big.
True
1
proof
[(triple8)]
("Charlie" "is" "big" "-")
triple8
Charlie is white.
False
1
inv-proof
[(triple12)]
("Charlie" "is" "white" "+")
triple12
Charlie is quiet.
True
2
proof
[(((triple10) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple10) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple10) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple10) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is not green.[(triple3)] Bob is not smart.[(triple6)] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is white.[(triple7)] Charlie is green.[(triple10)] Charlie is not big.[(triple8)] Charlie is not furry.[(triple9)] Charlie is not white.[(triple12)] Charlie is red.[(triple11)] @1: Charlie is quiet.[(((triple10) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is not green.
("Bob" "is" "green" "-")
triple3
Bob is not smart.
("Bob" "is" "smart" "-")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple10
Charlie is not big.
("Charlie" "is" "big" "-")
triple8
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple9
Charlie is not white.
("Charlie" "is" "white" "-")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
triple11
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple10) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1