Anne is blue. Bob is cold. Charlie is white. Gary is big. Blue people are not white. If someone is big then they are white. If someone is white then they are young. If Charlie is blue then Charlie is not cold. Blue, young people are not round. If Gary is round and Gary is blue then Gary is not cold. If someone is big and not white then they are kind. If someone is kind then they are cold.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Blue people are not white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "-"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If Charlie is blue then Charlie is not cold.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "cold" "-"))
Blue, young people are not round.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "-"))
If Gary is round and Gary is blue then Gary is not cold.
((("Gary" "is" "round" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "cold" "-"))
If someone is big and not white then they are kind.
((("someone" "is" "big" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is not white.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "white" "-")
((triple1) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Gary is not white.
False
2
inv-proof
[(((triple4) -> rule2))]
("Gary" "is" "white" "-")
((triple4) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "young" "-")
Charlie is cold.
Unknown
rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Bob is cold.[(triple2)] Charlie is white.[(triple3)] Gary is big.[(triple4)] @1: Anne is not white.[(((triple1) -> rule1))] Charlie is young.[(((triple3) -> rule3))] Gary is white.[(((triple4) -> rule2))] @2: Gary is young.[(((((triple4) -> rule2)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Anne is not white.
("Anne" "is" "white" "-")
((triple1) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple4) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2