Bob is quiet. Bob is rough. Bob is round. White things are round. If something is round then it is not white. All white things are not quiet. If something is quiet and not white then it is blue. If something is white then it is furry. If something is blue and round then it is furry.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is round then it is not white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
All white things are not quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "-"))
If something is quiet and not white then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "white" "~")) -> ("something" "is" "blue" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is blue and round then it is furry.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Bob is rough.
True
1
proof
[(triple2)]
("Bob" "is" "rough" "+")
triple2
Bob is not quiet.
False
1
inv-proof
[(triple1)]
("Bob" "is" "quiet" "-")
triple1
Bob is not white.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "white" "-")
((triple3) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "white" "+")
((triple3) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is blue.
True
4
proof
[(((triple1 ((triple3) -> rule2)) -> rule4))]
("Bob" "is" "blue" "+")
((triple1 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Bob is not blue.
False
4
inv-proof
[(((triple1 ((triple3) -> rule2)) -> rule4))]
("Bob" "is" "blue" "-")
((triple1 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Bob is furry.
True
6
proof
[(((((triple1 ((triple3) -> rule2)) -> rule4) triple3) -> rule6))]
("Bob" "is" "furry" "+")
((((triple1 ((triple3) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
int3
Bob is not furry.
False
6
inv-proof
[(((((triple1 ((triple3) -> rule2)) -> rule4) triple3) -> rule6))]
("Bob" "is" "furry" "-")
((((triple1 ((triple3) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
int3
@0: Bob is quiet.[(triple1)] Bob is rough.[(triple2)] Bob is round.[(triple3)] @1: Bob is not white.[(((triple3) -> rule2))] @2: Bob is blue.[(((triple1 ((triple3) -> rule2)) -> rule4))] @3: Bob is furry.[(((((triple1 ((triple3) -> rule2)) -> rule4) triple3) -> rule6))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is not white.
("Bob" "is" "white" "-")
((triple3) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not white.
("Bob" "is" "white" "-")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1 ((triple3) -> (rule2 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
int3