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