Bob is big. Bob is nice. Bob is not rough. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is smart. All white people are nice. All big, kind people are smart. Nice people are kind. All nice, furry people are kind. If someone is smart and nice then they are white. If someone is rough then they are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
All big, kind people are smart.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All nice, furry people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart and nice then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Charlie is white.
True
3
proof
[(((triple7 triple6) -> rule5))]
("Charlie" "is" "white" "+")
((triple7 triple6) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
True
4
proof
[(((triple1 ((triple2) -> rule3)) -> rule2))]
("Bob" "is" "smart" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((triple1 ((triple2) -> rule3)) -> rule2))]
("Bob" "is" "smart" "-")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
True
6
proof
[(((((triple1 ((triple2) -> rule3)) -> rule2) triple2) -> rule5))]
("Bob" "is" "white" "+")
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not white.
False
6
inv-proof
[(((((triple1 ((triple2) -> rule3)) -> rule2) triple2) -> rule5))]
("Bob" "is" "white" "-")
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "furry" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is not rough.[(triple3)] Charlie is furry.[(triple4)] Charlie is kind.[(triple5 OR ((triple6) -> rule3) OR ((triple6 triple4) -> rule4))] Charlie is nice.[(triple6)] Charlie is smart.[(triple7)] @1: Bob is kind.[(((triple2) -> rule3))] Charlie is white.[(((triple7 triple6) -> rule5))] @2: Bob is smart.[(((triple1 ((triple2) -> rule3)) -> rule2))] @3: Bob is white.[(((((triple1 ((triple2) -> rule3)) -> rule2) triple2) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is not rough.
("Bob" "is" "rough" "-")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
((triple6) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple6 triple4) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple7 triple6) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1 ((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1 ((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3