Bob is furry. All cold people are white. If Bob is white then Bob is big. If someone is white then they are cold. All white, quiet people are green. If someone is green then they are cold. If someone is furry then they are cold. Green, furry people are quiet. All green people are quiet.
Bob is furry.
("Bob" "is" "furry" "+")
All cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If Bob is white then Bob is big.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "big" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All white, quiet people are green.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Green, furry people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is cold.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "cold" "-")
((triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("Bob" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("Bob" "is" "big" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not big.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("Bob" "is" "big" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@3: Bob is quiet.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule8 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is green.
Unknown
rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is furry.[(triple1)] @1: Bob is cold.[(((triple1) -> rule6))] @2: Bob is white.[(((((triple1) -> rule6)) -> rule1))] @3: Bob is big.[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3