Gary is round. Gary is smart. Gary is white. Rough, round things are furry. If something is green then it is rough. Furry, smart things are white. Furry things are green. All white, round things are furry. Smart things are round.
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Rough, round things are furry.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Furry, smart things are white.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All white, round things are furry.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Gary is white.
True
1
proof
[(triple3)]
("Gary" "is" "white" "+")
triple3
Gary is not smart.
False
1
inv-proof
[(triple2)]
("Gary" "is" "smart" "-")
triple2
Gary is furry.
True
3
proof
[(((triple3 triple1) -> rule5) OR ((triple3 ((triple2) -> rule6)) -> rule5))]
("Gary" "is" "furry" "+")
((triple3 triple1) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((triple3 triple1) -> rule5) OR ((triple3 ((triple2) -> rule6)) -> rule5))]
("Gary" "is" "furry" "-")
((triple3 triple1) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
True
4
proof
[(((((triple3 triple1) -> rule5)) -> rule4) OR ((((triple3 ((triple2) -> rule6)) -> rule5)) -> rule4))]
("Gary" "is" "green" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not green.
False
4
inv-proof
[(((((triple3 triple1) -> rule5)) -> rule4) OR ((((triple3 ((triple2) -> rule6)) -> rule5)) -> rule4))]
("Gary" "is" "green" "-")
((((triple3 triple1) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
True
5
proof
[(((((((triple3 triple1) -> rule5)) -> rule4)) -> rule2) OR ((((((triple3 ((triple2) -> rule6)) -> rule5)) -> rule4)) -> rule2))]
("Gary" "is" "rough" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple3 ((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is not rough.
False
5
inv-proof
[(((((((triple3 triple1) -> rule5)) -> rule4)) -> rule2) OR ((((((triple3 ((triple2) -> rule6)) -> rule5)) -> rule4)) -> rule2))]
("Gary" "is" "rough" "-")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple3 ((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
@0: Gary is round.[(triple1 OR ((triple2) -> rule6))] Gary is smart.[(triple2)] Gary is white.[(triple3)] @1: Gary is furry.[(((triple3 triple1) -> rule5) OR ((triple3 ((triple2) -> rule6)) -> rule5))] @2: Gary is green.[(((((triple3 triple1) -> rule5)) -> rule4) OR ((((triple3 ((triple2) -> rule6)) -> rule5)) -> rule4))] @3: Gary is rough.[(((((((triple3 triple1) -> rule5)) -> rule4)) -> rule2) OR ((((((triple3 ((triple2) -> rule6)) -> rule5)) -> rule4)) -> rule2))]
Gary is round.
("Gary" "is" "round" "+")
triple1
((triple2) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
((triple3 triple1) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple3 triple1) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple3 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple3 triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((((triple3 ((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4