Bob is cold. Bob is furry. Bob is nice. Bob is quiet. Bob is red. Bob is not smart. Bob is young. If Bob is red and Bob is not nice then Bob is not quiet. If something is red then it is cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is young.
("Bob" "is" "young" "+")
If Bob is red and Bob is not nice then Bob is not quiet.
((("Bob" "is" "red" "+") ("Bob" "is" "nice" "~")) -> ("Bob" "is" "quiet" "-"))
If something is red then it is cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Bob is young.
True
1
proof
[(triple7)]
("Bob" "is" "young" "+")
triple7
Bob is smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "+")
triple6
@0: Bob is cold.[(triple1 OR ((triple5) -> rule2))] Bob is furry.[(triple2)] Bob is nice.[(triple3)] Bob is not smart.[(triple6)] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is young.[(triple7)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple5) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
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 young.
("Bob" "is" "young" "+")
triple7