Gary is red. All white things are green. If something is smart and blue then it is not red. If something is green and smart then it is white. If something is red then it is white. Green, white things are smart. All white, green things are kind.
Gary is red.
("Gary" "is" "red" "+")
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is smart and blue then it is not red.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "-"))
If something is green and smart then it is white.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Green, white things are smart.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
All white, green things are kind.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Gary is red.
True
1
proof
[(triple1)]
("Gary" "is" "red" "+")
triple1
Gary is not red.
False
1
inv-proof
[(triple1)]
("Gary" "is" "red" "-")
triple1
Gary is white.
True
2
proof
[(((triple1) -> rule4))]
("Gary" "is" "white" "+")
((triple1) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Gary" "is" "white" "-")
((triple1) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Gary" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Gary" "is" "green" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule1)) -> rule6))]
("Gary" "is" "kind" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not kind.
False
6
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule1)) -> rule6))]
("Gary" "is" "kind" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Gary is red.[(triple1)] @1: Gary is white.[(((triple1) -> rule4))] @2: Gary is green.[(((((triple1) -> rule4)) -> rule1))] @3: Gary is kind.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule1)) -> rule6))] Gary is smart.[(((((((triple1) -> rule4)) -> rule1) ((triple1) -> rule4)) -> rule5))]
Gary is red.
("Gary" "is" "red" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
((triple1) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2)) ((triple1) -> (rule4 % int3))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3