Bob is big. Bob is blue. Bob is furry. Bob is quiet. Bob is red. Bob is round. Bob is white. Gary is big. Gary is blue. Gary is furry. Gary is quiet. Gary is red. Gary is round. Gary is white. If Gary is furry and Gary is blue then Gary is white. If something is furry then it is quiet. All furry, red things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is furry and Gary is blue then Gary is white.
((("Gary" "is" "furry" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "white" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All furry, red things are big.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Gary is red.
True
1
proof
[(triple12)]
("Gary" "is" "red" "+")
triple12
Gary is not round.
False
1
inv-proof
[(triple13)]
("Gary" "is" "round" "-")
triple13
@0: Bob is big.[(triple1 OR ((triple3 triple5) -> rule3))] Bob is blue.[(triple2)] Bob is furry.[(triple3)] Bob is quiet.[(triple4 OR ((triple3) -> rule2))] Bob is red.[(triple5)] Bob is round.[(triple6)] Bob is white.[(triple7)] Gary is big.[(triple8 OR ((triple10 triple12) -> rule3))] Gary is blue.[(triple9)] Gary is furry.[(triple10)] Gary is quiet.[(triple11 OR ((triple10) -> rule2))] Gary is red.[(triple12)] Gary is round.[(triple13)] Gary is white.[(triple14 OR ((triple10 triple9) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple3 triple5) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
((triple10 triple12) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
((triple10) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple12
Gary is round.
("Gary" "is" "round" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple14
((triple10 triple9) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1