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