Bob is white. Charlie is blue. Charlie is green. Gary is blue. Gary is nice. Gary is smart. Gary is white. If someone is smart and green then they are nice. If someone is blue then they are white. If Charlie is kind then Charlie is nice. If someone is kind then they are smart. All smart people are white. Kind people are nice. White, nice people are furry. Blue, white people are smart.
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is smart and green then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue then they are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Charlie is kind then Charlie is nice.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "nice" "+"))
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
White, nice people are furry.
((("someone" "is" "white" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Blue, white people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Charlie is blue.
True
1
proof
[(triple2)]
("Charlie" "is" "blue" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is white.[(triple1)] Charlie is blue.[(triple2)] Charlie is green.[(triple3)] Gary is blue.[(triple4)] Gary is nice.[(triple5)] Gary is smart.[(triple6 OR ((triple4 triple7) -> rule8) OR ((triple4 ((triple4) -> rule2)) -> rule8))] Gary is white.[(triple7 OR ((triple4) -> rule2) OR ((triple6) -> rule5))] @1: Charlie is white.[(((triple2) -> rule2))] Gary is furry.[(((triple7 triple5) -> rule7) OR ((((triple4) -> rule2) triple5) -> rule7) OR ((((triple6) -> rule5) triple5) -> rule7))] @2: Charlie is smart.[(((triple2 ((triple2) -> rule2)) -> rule8))] @3: Charlie is nice.[(((((triple2 ((triple2) -> rule2)) -> rule8) triple3) -> rule1))] @4: Charlie is furry.[(((((triple2) -> rule2) ((((triple2 ((triple2) -> rule2)) -> rule8) triple3) -> rule1)) -> rule7))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple4 triple7) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple4 ((triple4) -> (rule2 % int2))) -> (rule8 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple4) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple6) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple7 triple5) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple4) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple6) -> (rule5 % int2)) triple5) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule8 % int2)) triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule2 % int4)) ((((triple2 ((triple2) -> (rule2 % int4))) -> (rule8 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4