Bob is not big. Bob is blue. Bob is not cold. Bob is furry. Bob is quiet. Bob is red. Bob is white. If someone is furry then they are quiet. If someone is white and not cold then they are furry. If someone is blue then they are white.
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and not cold then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Bob is furry.
True
1
proof
[(triple4 OR ((triple7 triple3) -> rule2) OR ((((triple2) -> rule3) triple3) -> rule2))]
("Bob" "is" "furry" "+")
triple4
((triple7 triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not red.
False
1
inv-proof
[(triple6)]
("Bob" "is" "red" "-")
triple6
@0: Bob is blue.[(triple2)] Bob is furry.[(triple4 OR ((triple7 triple3) -> rule2) OR ((((triple2) -> rule3) triple3) -> rule2))] Bob is not big.[(triple1)] Bob is not cold.[(triple3)] Bob is quiet.[(triple5 OR ((triple4) -> rule1) OR ((((triple7 triple3) -> rule2)) -> rule1) OR ((((((triple2) -> rule3) triple3) -> rule2)) -> rule1))] Bob is red.[(triple6)] Bob is white.[(triple7 OR ((triple2) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple4
((triple7 triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple2) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not cold.
("Bob" "is" "cold" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple4) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple7 triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple2) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
((triple2) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1