Gary is green. If something is quiet then it is green. If something is nice then it is cold. If something is green then it is white. If something is white and green then it is nice. All smart, rough things are white. All quiet, nice things are green.
Gary is green.
("Gary" "is" "green" "+")
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is white and green then it is nice.
((("something" "is" "white" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All smart, rough things are white.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All quiet, nice things are green.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
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 white.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "white" "+")
((triple1) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "white" "-")
((triple1) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule4))]
("Gary" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule4))]
("Gary" "is" "nice" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
True
5
proof
[(((((((triple1) -> rule3) triple1) -> rule4)) -> rule2))]
("Gary" "is" "cold" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((((((triple1) -> rule3) triple1) -> rule4)) -> rule2))]
("Gary" "is" "cold" "-")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
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 smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Gary is green.[(triple1)] @1: Gary is white.[(((triple1) -> rule3))] @2: Gary is nice.[(((((triple1) -> rule3) triple1) -> rule4))] @3: Gary is cold.[(((((((triple1) -> rule3) triple1) -> rule4)) -> rule2))]
Gary is green.
("Gary" "is" "green" "+")
triple1
Gary is white.
("Gary" "is" "white" "+")
((triple1) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3