Gary is rough. If Gary is young and Gary is blue then Gary is smart. Smart, blue things are furry. All rough things are not red. If something is furry and not rough then it is red. If something is rough and red then it is smart. All rough things are smart. If Gary is smart then Gary is blue. All smart things are young.
Gary is rough.
("Gary" "is" "rough" "+")
If Gary is young and Gary is blue then Gary is smart.
((("Gary" "is" "young" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "smart" "+"))
Smart, blue things are furry.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All rough things are not red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "-"))
If something is furry and not rough then it is red.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "+"))
If something is rough and red then it is smart.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Gary is smart then Gary is blue.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "blue" "+"))
All smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
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 not red.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "red" "-")
((triple1) -> (rule3 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Gary" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
True
3
proof
[(((((triple1) -> rule6)) -> rule8))]
("Gary" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule7))]
("Gary" "is" "blue" "-")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
True
6
proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule2))]
("Gary" "is" "furry" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not furry.
False
6
inv-proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule2))]
("Gary" "is" "furry" "-")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
@0: Gary is rough.[(triple1)] @1: Gary is not red.[(((triple1) -> rule3))] Gary is smart.[(((triple1) -> rule6))] @2: Gary is blue.[(((((triple1) -> rule6)) -> rule7))] Gary is young.[(((((triple1) -> rule6)) -> rule8))] @3: Gary is furry.[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule2))]
Gary is rough.
("Gary" "is" "rough" "+")
triple1
Gary is not red.
("Gary" "is" "red" "-")
((triple1) -> (rule3 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3