Gary is smart. If someone is green and young then they are red. If someone is smart then they are red. Young people are kind. Red people are kind. If someone is red and not big then they are not green. Red people are green. If someone is green and not kind then they are quiet. All smart, kind people are not quiet.
Gary is smart.
("Gary" "is" "smart" "+")
If someone is green and young then they are red.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and not big then they are not green.
((("someone" "is" "red" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "green" "-"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is green and not kind then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "quiet" "+"))
All smart, kind people are not quiet.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "-"))
Gary is smart.
True
1
proof
[(triple1)]
("Gary" "is" "smart" "+")
triple1
Gary is not smart.
False
1
inv-proof
[(triple1)]
("Gary" "is" "smart" "-")
triple1
Gary is red.
True
2
proof
[(((triple1) -> rule2))]
("Gary" "is" "red" "+")
((triple1) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Gary" "is" "red" "-")
((triple1) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Gary" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Gary" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not quiet.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule8))]
("Gary" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule8))]
("Gary" "is" "quiet" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Gary is smart.[(triple1)] @1: Gary is red.[(((triple1) -> rule2))] @2: Gary is green.[(((((triple1) -> rule2)) -> rule6))] Gary is kind.[(((((triple1) -> rule2)) -> rule4))] @3: Gary is not quiet.[(((triple1 ((((triple1) -> rule2)) -> rule4)) -> rule8))]
Gary is smart.
("Gary" "is" "smart" "+")
triple1
Gary is red.
("Gary" "is" "red" "+")
((triple1) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3