Bob is cold. Bob is kind. Bob is round. If something is green and kind then it is big. If Bob is big then Bob is furry. Round things are green.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
If something is green and kind then it is big.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If Bob is big then Bob is furry.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "furry" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Bob is kind.
True
1
proof
[(triple2)]
("Bob" "is" "kind" "+")
triple2
Bob is not round.
False
1
inv-proof
[(triple3)]
("Bob" "is" "round" "-")
triple3
Bob is green.
True
2
proof
[(((triple3) -> rule3))]
("Bob" "is" "green" "+")
((triple3) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Bob" "is" "green" "-")
((triple3) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
True
4
proof
[(((((triple3) -> rule3) triple2) -> rule1))]
("Bob" "is" "big" "+")
((((triple3) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not big.
False
4
inv-proof
[(((((triple3) -> rule3) triple2) -> rule1))]
("Bob" "is" "big" "-")
((((triple3) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
True
5
proof
[(((((((triple3) -> rule3) triple2) -> rule1)) -> rule2))]
("Bob" "is" "furry" "+")
((((((triple3) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not furry.
False
5
inv-proof
[(((((((triple3) -> rule3) triple2) -> rule1)) -> rule2))]
("Bob" "is" "furry" "-")
((((((triple3) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2)] Bob is round.[(triple3)] @1: Bob is green.[(((triple3) -> rule3))] @2: Bob is big.[(((((triple3) -> rule3) triple2) -> rule1))] @3: Bob is furry.[(((((((triple3) -> rule3) triple2) -> rule1)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple3) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple3) -> (rule3 % int2)) triple2) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple3) -> (rule3 % int3)) triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3