Gary is quiet. Quiet things are furry. All big things are not furry. Furry things are green. If something is big and not blue then it is quiet. All quiet, green things are young. If Gary is blue then Gary is not quiet. If Gary is blue then Gary is not green. If something is big and not young then it is not red.
Gary is quiet.
("Gary" "is" "quiet" "+")
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All big things are not furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "-"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is big and not blue then it is quiet.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
All quiet, green things are young.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Gary is blue then Gary is not quiet.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "quiet" "-"))
If Gary is blue then Gary is not green.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "green" "-"))
If something is big and not young then it is not red.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "red" "-"))
Gary is quiet.
True
1
proof
[(triple1)]
("Gary" "is" "quiet" "+")
triple1
Gary is not quiet.
False
1
inv-proof
[(triple1)]
("Gary" "is" "quiet" "-")
triple1
Gary is furry.
True
2
proof
[(((triple1) -> rule1))]
("Gary" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Gary" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Gary" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Gary" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule5))]
("Gary" "is" "young" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not young.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule5))]
("Gary" "is" "young" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Gary is quiet.[(triple1)] @1: Gary is furry.[(((triple1) -> rule1))] @2: Gary is green.[(((((triple1) -> rule1)) -> rule3))] @3: Gary is young.[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule5))]
Gary is quiet.
("Gary" "is" "quiet" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3