Bob is blue. Bob is green. Bob is quiet. If something is big then it is furry. If something is rough then it is furry. If Bob is blue then Bob is rough. If something is furry and blue then it is green. All blue things are young. If something is young and green then it is quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If Bob is blue then Bob is rough.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "rough" "+"))
If something is furry and blue then it is green.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is young and green then it is quiet.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Bob is green.
True
1
proof
[(triple2 OR ((((((triple1) -> rule3)) -> rule2) triple1) -> rule4))]
("Bob" "is" "green" "+")
triple2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not green.
False
1
inv-proof
[(triple2 OR ((((((triple1) -> rule3)) -> rule2) triple1) -> rule4))]
("Bob" "is" "green" "-")
triple2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is rough.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
@0: Bob is blue.[(triple1)] Bob is green.[(triple2 OR ((((((triple1) -> rule3)) -> rule2) triple1) -> rule4))] Bob is quiet.[(triple3 OR ((((triple1) -> rule5) triple2) -> rule6) OR ((((triple1) -> rule5) ((((((triple1) -> rule3)) -> rule2) triple1) -> rule4)) -> rule6))] @1: Bob is rough.[(((triple1) -> rule3))] Bob is young.[(((triple1) -> rule5))] @2: Bob is furry.[(((((triple1) -> rule3)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((((triple1) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple1) -> (rule5 % int5)) ((((((triple1) -> (rule3 % int4))) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Bob is young.
("Bob" "is" "young" "+")
int5
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2