Gary is furry. Gary is green. Gary is quiet. Gary is red. Gary is rough. Gary is round. Gary is white. If Gary is rough then Gary is green. White things are rough. All red things are round. If something is red and furry then it is green. If something is rough then it is white. All rough things are red. If Gary is round and Gary is furry then Gary is rough. If Gary is red and Gary is furry then Gary is round.
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is rough then Gary is green.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "green" "+"))
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is red and furry then it is green.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If Gary is round and Gary is furry then Gary is rough.
((("Gary" "is" "round" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is red and Gary is furry then Gary is round.
((("Gary" "is" "red" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "round" "+"))
Gary is red.
True
1
proof
[(triple4 OR ((triple5) -> rule6) OR ((((triple7) -> rule2)) -> rule6) OR ((((triple6 triple1) -> rule7)) -> rule6))]
("Gary" "is" "red" "+")
triple4
((triple5) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple6 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
@0: Gary is furry.[(triple1)] Gary is green.[(triple2 OR ((triple5) -> rule1) OR ((triple4 triple1) -> rule4) OR ((((triple7) -> rule2)) -> rule1) OR ((((triple6 triple1) -> rule7)) -> rule1) OR ((((triple5) -> rule6) triple1) -> rule4) OR ((((((triple4) -> rule3) triple1) -> rule7)) -> rule1) OR ((((((triple4 triple1) -> rule8) triple1) -> rule7)) -> rule1) OR ((((((triple7) -> rule2)) -> rule6) triple1) -> rule4) OR ((((((triple6 triple1) -> rule7)) -> rule6) triple1) -> rule4))] Gary is quiet.[(triple3)] Gary is red.[(triple4 OR ((triple5) -> rule6) OR ((((triple7) -> rule2)) -> rule6) OR ((((triple6 triple1) -> rule7)) -> rule6))] Gary is rough.[(triple5 OR ((triple7) -> rule2) OR ((triple6 triple1) -> rule7) OR ((((triple4) -> rule3) triple1) -> rule7) OR ((((triple4 triple1) -> rule8) triple1) -> rule7))] Gary is round.[(triple6 OR ((triple4) -> rule3) OR ((triple4 triple1) -> rule8) OR ((((triple5) -> rule6)) -> rule3) OR ((((triple5) -> rule6) triple1) -> rule8) OR ((((((triple7) -> rule2)) -> rule6)) -> rule3) OR ((((((triple7) -> rule2)) -> rule6) triple1) -> rule8))] Gary is white.[(triple7 OR ((triple5) -> rule5) OR ((((triple6 triple1) -> rule7)) -> rule5) OR ((((((triple4) -> rule3) triple1) -> rule7)) -> rule5) OR ((((((triple4 triple1) -> rule8) triple1) -> rule7)) -> rule5))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
((triple5) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple4 triple1) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple6 triple1) -> (rule7 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple5) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple4) -> (rule3 % int3)) triple1) -> (rule7 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple4 triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple7) -> (rule2 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple6 triple1) -> (rule7 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
((triple5) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((triple6 triple1) -> (rule7 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple5
((triple7) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple6 triple1) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((triple4) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple4 triple1) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple4) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple4 triple1) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple5) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
((((((triple7) -> (rule2 % int3))) -> (rule6 % int2)) triple1) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple5) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((((triple6 triple1) -> (rule7 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((((((triple4) -> (rule3 % int3)) triple1) -> (rule7 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple4 triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3