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