Gary is green. All green, cold things are red. White, red things are smart. If Gary is young then Gary is rough. If Gary is red then Gary is white. All white things are green. If Gary is green then Gary is red.
Gary is green.
("Gary" "is" "green" "+")
All green, cold things are red.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
White, red things are smart.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Gary is young then Gary is rough.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is red then Gary is white.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "white" "+"))
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If Gary is green then Gary is red.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "red" "+"))
Gary is green.
True
1
proof
[(triple1)]
("Gary" "is" "green" "+")
triple1
Gary is not green.
False
1
inv-proof
[(triple1)]
("Gary" "is" "green" "-")
triple1
Gary is red.
True
2
proof
[(((triple1) -> rule6))]
("Gary" "is" "red" "+")
((triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple1) -> rule6))]
("Gary" "is" "red" "-")
((triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Gary" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("Gary" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
True
6
proof
[(((((((triple1) -> rule6)) -> rule4) ((triple1) -> rule6)) -> rule2))]
("Gary" "is" "smart" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) ((triple1) -> (rule6 % int3))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not smart.
False
6
inv-proof
[(((((((triple1) -> rule6)) -> rule4) ((triple1) -> rule6)) -> rule2))]
("Gary" "is" "smart" "-")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) ((triple1) -> (rule6 % int3))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Gary is green.[(triple1)] @1: Gary is red.[(((triple1) -> rule6))] @2: Gary is white.[(((((triple1) -> rule6)) -> rule4))] @3: Gary is smart.[(((((((triple1) -> rule6)) -> rule4) ((triple1) -> rule6)) -> rule2))]
Gary is green.
("Gary" "is" "green" "+")
triple1
Gary is red.
("Gary" "is" "red" "+")
((triple1) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) ((triple1) -> (rule6 % int3))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3