Bob is furry. Bob is green. Bob is kind. If someone is nice and white then they are blue. All green, white people are kind. If Bob is nice then Bob is big. If someone is furry then they are nice. If Bob is green then Bob is nice. If someone is green and blue then they are nice.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
If someone is nice and white then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
All green, white people are kind.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Bob is nice then Bob is big.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "big" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If Bob is green then Bob is nice.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "nice" "+"))
If someone is green and blue then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Bob is nice.
True
2
proof
[(((triple1) -> rule4) OR ((triple2) -> rule5))]
("Bob" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple2) -> rule5))]
("Bob" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
("Bob" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
("Bob" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is furry.[(triple1)] Bob is green.[(triple2)] Bob is kind.[(triple3)] @1: Bob is nice.[(((triple1) -> rule4) OR ((triple2) -> rule5))] @2: Bob is big.[(((((triple1) -> rule4)) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2