Bob is cold. Bob is furry. Bob is green. Bob is quiet. Bob is red. Bob is white. Charlie is cold. Charlie is furry. Charlie is quiet. Charlie is red. Charlie is round. Charlie is white. If Bob is quiet and Bob is white then Bob is round.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If Bob is quiet and Bob is white then Bob is round.
((("Bob" "is" "quiet" "+") ("Bob" "is" "white" "+")) -> ("Bob" "is" "round" "+"))
Charlie is furry.
True
1
proof
[(triple8)]
("Charlie" "is" "furry" "+")
triple8
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
Bob is round.
True
3
proof
[(((triple4 triple6) -> rule1))]
("Bob" "is" "round" "+")
((triple4 triple6) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
3
inv-proof
[(((triple4 triple6) -> rule1))]
("Bob" "is" "round" "-")
((triple4 triple6) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3)] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is white.[(triple6)] Charlie is cold.[(triple7)] Charlie is furry.[(triple8)] Charlie is quiet.[(triple9)] Charlie is red.[(triple10)] Charlie is round.[(triple11)] Charlie is white.[(triple12)] @1: Bob is round.[(((triple4 triple6) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
Charlie is round.
("Charlie" "is" "round" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
Bob is round.
("Bob" "is" "round" "+")
((triple4 triple6) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1