Gary is blue. If something is nice and smart then it is not white. If something is green and nice then it is not big. If something is green then it is not big. If something is blue then it is nice. All white things are nice. If something is smart then it is young. If Gary is nice then Gary is young. If Gary is smart and Gary is green then Gary is young.
Gary is blue.
("Gary" "is" "blue" "+")
If something is nice and smart then it is not white.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "-"))
If something is green and nice then it is not big.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "-"))
If something is green then it is not big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Gary is nice then Gary is young.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "young" "+"))
If Gary is smart and Gary is green then Gary is young.
((("Gary" "is" "smart" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "young" "+"))
Gary is blue.
True
1
proof
[(triple1)]
("Gary" "is" "blue" "+")
triple1
Gary is not blue.
False
1
inv-proof
[(triple1)]
("Gary" "is" "blue" "-")
triple1
Gary is nice.
True
2
proof
[(((triple1) -> rule4))]
("Gary" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("Gary" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
True
3
proof
[(((((triple1) -> rule4)) -> rule7))]
("Gary" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7))]
("Gary" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Gary is blue.[(triple1)] @1: Gary is nice.[(((triple1) -> rule4))] @2: Gary is young.[(((((triple1) -> rule4)) -> rule7))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2