Bob is cold. Bob is furry. Bob is kind. Bob is quiet. Bob is round. Bob is white. Bob is young. If Bob is quiet then Bob is white. If Bob is cold then Bob is furry.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
If Bob is quiet then Bob is white.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "white" "+"))
If Bob is cold then Bob is furry.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "furry" "+"))
Bob is white.
True
1
proof
[(triple6 OR ((triple4) -> rule1))]
("Bob" "is" "white" "+")
triple6
((triple4) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not round.
False
1
inv-proof
[(triple5)]
("Bob" "is" "round" "-")
triple5
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2 OR ((triple1) -> rule2))] Bob is kind.[(triple3)] Bob is quiet.[(triple4)] Bob is round.[(triple5)] Bob is white.[(triple6 OR ((triple4) -> rule1))] Bob is young.[(triple7)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple4) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7