Bob is big. Bob is furry. Bob is nice. Furry things are cold. If something is cold and big then it is rough. If something is round and furry then it is green.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is cold and big then it is rough.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is round and furry then it is green.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple3)]
("Bob" "is" "nice" "-")
triple3
Bob is cold.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
True
4
proof
[(((((triple2) -> rule1) triple1) -> rule2))]
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((((triple2) -> rule1) triple1) -> rule2))]
("Bob" "is" "rough" "-")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is nice.[(triple3)] @1: Bob is cold.[(((triple2) -> rule1))] @2: Bob is rough.[(((((triple2) -> rule1) triple1) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2