Bob is furry. Charlie is kind. All nice, big things are white. If something is furry then it is kind. If something is kind then it is big. If Charlie is nice then Charlie is not white. White things are furry. If something is furry then it is blue.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
All nice, big things are white.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If Charlie is nice then Charlie is not white.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "white" "-"))
White things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@3: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Charlie is kind.[(triple2)] @1: Bob is blue.[(((triple1) -> rule6))] Bob is kind.[(((triple1) -> rule2))] Charlie is big.[(((triple2) -> rule3))] @2: Bob is big.[(((((triple1) -> rule2)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2