Gary is round. If something is round then it is not furry. Blue, furry things are quiet. Red, blue things are round. All round things are red. All round, furry things are not green. If something is quiet then it is green. If Gary is not furry then Gary is quiet. If Gary is furry and Gary is rough then Gary is quiet.
Gary is round.
("Gary" "is" "round" "+")
If something is round then it is not furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "-"))
Blue, furry things are quiet.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Red, blue things are round.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
All round, furry things are not green.
((("something" "is" "round" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "-"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If Gary is not furry then Gary is quiet.
((("Gary" "is" "furry" "~")) -> ("Gary" "is" "quiet" "+"))
If Gary is furry and Gary is rough then Gary is quiet.
((("Gary" "is" "furry" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "quiet" "+"))
Gary is round.
True
1
proof
[(triple1)]
("Gary" "is" "round" "+")
triple1
Gary is not round.
False
1
inv-proof
[(triple1)]
("Gary" "is" "round" "-")
triple1
Gary is not furry.
True
2
proof
[(((triple1) -> rule1))]
("Gary" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Gary" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule7))]
("Gary" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7))]
("Gary" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
int2
Gary is green.
True
4
proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule6))]
("Gary" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
int3
Gary is not green.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule6))]
("Gary" "is" "green" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
int3
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Gary is round.[(triple1)] @1: Gary is not furry.[(((triple1) -> rule1))] Gary is red.[(((triple1) -> rule4))] @2: Gary is quiet.[(((((triple1) -> rule1)) -> rule7))] @3: Gary is green.[(((((((triple1) -> rule1)) -> rule7)) -> rule6))]
Gary is round.
("Gary" "is" "round" "+")
triple1
Gary is not furry.
("Gary" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple1) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
int2
Gary is green.
("Gary" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
int3