Anne is green. Bob is not white. Charlie is red. Gary is cold. Cold, red people are not big. All cold, green people are not big. White people are cold. If someone is cold then they are green. All white people are green. All white people are not nice. All kind, green people are white. Big people are not kind.
Anne is green.
("Anne" "is" "green" "+")
Bob is not white.
("Bob" "is" "white" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Cold, red people are not big.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "-"))
All cold, green people are not big.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "-"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All white people are not nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "-"))
All kind, green people are white.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Big people are not kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
Bob is not white.
True
1
proof
[(triple2)]
("Bob" "is" "white" "-")
triple2
Charlie is not red.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "red" "-")
triple3
Gary is green.
True
2
proof
[(((triple4) -> rule4))]
("Gary" "is" "green" "+")
((triple4) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple4) -> rule4))]
("Gary" "is" "green" "-")
((triple4) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule7 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is green.[(triple1)] Bob is not white.[(triple2)] Charlie is red.[(triple3)] Gary is cold.[(triple4)] @1: Gary is green.[(((triple4) -> rule4))] @2: Gary is not big.[(((triple4 ((triple4) -> rule4)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is not white.
("Bob" "is" "white" "-")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
((triple4) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not big.
("Gary" "is" "big" "-")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2