Gary is furry. Gary is kind. Gary is quiet. Cold, green people are round. Quiet people are round. If Gary is smart then Gary is green. All furry, green people are kind. If Gary is furry and Gary is quiet then Gary is round. If Gary is quiet then Gary is smart. If someone is green then they are cold. All quiet, cold people are green.
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Cold, green people are round.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Gary is smart then Gary is green.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "green" "+"))
All furry, green people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Gary is furry and Gary is quiet then Gary is round.
((("Gary" "is" "furry" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "round" "+"))
If Gary is quiet then Gary is smart.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "smart" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All quiet, cold people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Gary is kind.
True
1
proof
[(triple2 OR ((triple1 ((((triple3) -> rule6)) -> rule3)) -> rule4))]
("Gary" "is" "kind" "+")
triple2
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Gary is round.
True
2
proof
[(((triple3) -> rule2) OR ((triple1 triple3) -> rule5) OR ((((((((triple3) -> rule6)) -> rule3)) -> rule7) ((((triple3) -> rule6)) -> rule3)) -> rule1))]
("Gary" "is" "round" "+")
((triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "smart" "-")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
@0: Gary is furry.[(triple1)] Gary is kind.[(triple2 OR ((triple1 ((((triple3) -> rule6)) -> rule3)) -> rule4))] Gary is quiet.[(triple3)] @1: Gary is round.[(((triple3) -> rule2) OR ((triple1 triple3) -> rule5) OR ((((((((triple3) -> rule6)) -> rule3)) -> rule7) ((((triple3) -> rule6)) -> rule3)) -> rule1))] Gary is smart.[(((triple3) -> rule6))] @2: Gary is green.[(((((triple3) -> rule6)) -> rule3))] @3: Gary is cold.[(((((((triple3) -> rule6)) -> rule3)) -> rule7))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple1 triple3) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple3) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3