Gary is rough. Nice people are kind. If someone is blue then they are kind. If someone is cold then they are not white. Cold, blue people are white. If someone is kind then they are white. If someone is rough then they are cold. If someone is cold and big then they are rough. If Gary is white and Gary is blue then Gary is big.
Gary is rough.
("Gary" "is" "rough" "+")
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold then they are not white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "-"))
Cold, blue people are white.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is kind then they are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and big then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Gary is white and Gary is blue then Gary is big.
((("Gary" "is" "white" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "big" "+"))
Gary is rough.
True
1
proof
[(triple1)]
("Gary" "is" "rough" "+")
triple1
Gary is not rough.
False
1
inv-proof
[(triple1)]
("Gary" "is" "rough" "-")
triple1
Gary is cold.
True
2
proof
[(((triple1) -> rule6))]
("Gary" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("Gary" "is" "cold" "-")
((triple1) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not white.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Gary" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("Gary" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Gary is rough.[(triple1)] @1: Gary is cold.[(((triple1) -> rule6))] @2: Gary is not white.[(((((triple1) -> rule6)) -> rule3))]
Gary is rough.
("Gary" "is" "rough" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2